### Nuprl Lemma : exception-not-value_1

`∀[nm,val,t:Base].  (exception(nm; val) ≤ t) `` False supposing (t)↓`

Proof

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

Latex:
\mforall{}[nm,val,t:Base].    (exception(nm;  val)  \mleq{}  t)  {}\mRightarrow{}  False  supposing  (t)\mdownarrow{}

Date html generated: 2016_05_13-PM-03_23_16
Last ObjectModification: 2016_01_14-PM-06_46_12

Theory : call!by!value_1

Home Index