### Nuprl Lemma : has-value-monotonic

`∀[a,b:Base].  ((b)↓) supposing ((a ≤ b) and (a)↓)`

Proof

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

Latex:
\mforall{}[a,b:Base].    ((b)\mdownarrow{})  supposing  ((a  \mleq{}  b)  and  (a)\mdownarrow{})

Date html generated: 2016_05_13-PM-03_46_24
Last ObjectModification: 2016_01_14-PM-07_11_10

Theory : call!by!value_2

Home Index