Nuprl Lemma : strictness-atom1_eq-right

[a,b,c:Top].  (if a=1 ⊥ then else eval in ⊥)


Proof




Definitions occuring in Statement :  bottom: callbyvalue: callbyvalue 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
Lemmas referenced :  top_wf is-exception_wf has-value_wf_base exception-not-bottom 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 sqequalRule baseApply closedConclusion baseClosed hypothesisEquality productElimination lemma_by_obid independent_functionElimination isectElimination because_Cache independent_isectElimination equalityTransitivity equalitySymmetry voidElimination atom1_eqExceptionCases axiomSqleEquality exceptionSqequal sqleReflexivity callbyvalueCallbyvalue callbyvalueReduce callbyvalueExceptionCases sqequalAxiom isect_memberEquality

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



Date html generated: 2016_05_13-PM-03_44_18
Last ObjectModification: 2016_01_14-PM-07_07_16

Theory : computation


Home Index