### Nuprl Lemma : cbv_sqle

`∀[a,X,Y:Base].  eval x = a in X[x] ≤ eval x = a in Y[x] supposing (a)↓ `` (X[a] ≤ Y[a])`

Proof

Definitions occuring in Statement :  has-value: `(a)↓` callbyvalue: callbyvalue uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` implies: `P `` Q` base: `Base` sqle: `s ≤ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` has-value: `(a)↓` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  base_wf sqle_wf_base is-exception_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut divergentSqle callbyvalueCallbyvalue sqequalHypSubstitution hypothesis sqequalRule callbyvalueReduce independent_functionElimination thin callbyvalueExceptionCases axiomSqleEquality exceptionSqequal sqleReflexivity baseApply closedConclusion baseClosed hypothesisEquality lemma_by_obid isectElimination functionEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[a,X,Y:Base].    eval  x  =  a  in  X[x]  \mleq{}  eval  x  =  a  in  Y[x]  supposing  (a)\mdownarrow{}  {}\mRightarrow{}  (X[a]  \mleq{}  Y[a])

Date html generated: 2016_05_13-PM-03_45_45
Last ObjectModification: 2016_01_14-PM-07_06_40

Theory : computation

Home Index