Nuprl Lemma : has-value-monotonic

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


Definitions occuring in Statement :  has-value: (a)↓ uimplies: 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: supposing a has-value: (a)↓ prop: all: x:A. B[x] implies:  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

\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