Nuprl Lemma : strictness-atom2_eq-left

[a,b,c:Top].  (if ⊥=2 then else ~ ⊥)


Proof




Definitions occuring in Statement :  bottom: atom_eq: atomeqn def uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T has-value: (a)↓ and: P ∧ Q not: ¬A implies:  Q uimplies: supposing a false: False top: Top
Lemmas referenced :  top_wf bottom-sqle is-exception_wf has-value_wf_base exception-not-bottom atom2-value-type value-type-has-value bottom_diverge
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle sqleRule thin divergentSqle callbyvalueAtomnEq sqequalHypSubstitution hypothesis baseClosed sqequalRule baseApply closedConclusion hypothesisEquality productElimination lemma_by_obid independent_functionElimination isectElimination atomnEquality independent_isectElimination equalityTransitivity equalitySymmetry voidElimination atom2_eqExceptionCases axiomSqleEquality sqleReflexivity isect_memberEquality voidEquality sqequalAxiom because_Cache

Latex:
\mforall{}[a,b,c:Top].    (if  \mbot{}=2  a  then  b  else  c  \msim{}  \mbot{})



Date html generated: 2016_05_13-PM-03_44_21
Last ObjectModification: 2016_01_14-PM-07_07_05

Theory : computation


Home Index