Nuprl Lemma : decide-bottom

[x:Top]. (case of inl(a) => ⊥ inr(b) => ⊥ eval in ⊥)


Definitions occuring in Statement :  bottom: callbyvalue: callbyvalue uall: [x:A]. B[x] top: Top decide: case of inl(x) => s[x] inr(y) => t[y] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T has-value: (a)↓ all: x:A. B[x] or: P ∨ Q uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  btrue: tt top: Top bfalse: ff not: ¬A false: False
Lemmas referenced :  exception-not-bottom bottom_diverge is-exception_wf has-value_wf_base assert_of_bnot eqff_to_assert bottom-sqle eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases top_wf isl_wf injection-eta
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle sqleRule thin divergentSqle callbyvalueDecide sqequalHypSubstitution hypothesis lemma_by_obid dependent_functionElimination equalityTransitivity equalitySymmetry isectElimination because_Cache unionElimination instantiate cumulativity independent_isectElimination independent_functionElimination productElimination sqequalRule isect_memberEquality voidElimination voidEquality decideExceptionCases axiomSqleEquality exceptionSqequal sqleReflexivity baseApply closedConclusion baseClosed hypothesisEquality callbyvalueCallbyvalue callbyvalueReduce callbyvalueExceptionCases sqequalAxiom

\mforall{}[x:Top].  (case  x  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mbot{}  \msim{}  eval  u  =  x  in  \mbot{})

Date html generated: 2016_05_13-PM-03_45_09
Last ObjectModification: 2016_01_14-PM-07_06_27

Theory : computation

Home Index