Nuprl Lemma : exception-not-value-or-bottom

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

Proof

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

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

Date html generated: 2016_05_13-PM-03_23_19
Last ObjectModification: 2016_01_14-PM-06_46_15

Theory : call!by!value_1

Home Index