### Nuprl Lemma : strictness-atom_eq-right

`∀[a,b,c:Top].  (if a=⊥ then b else c fi  ~ eval x = a in ⊥)`

Proof

Definitions occuring in Statement :  bottom: `⊥` callbyvalue: callbyvalue uall: `∀[x:A]. B[x]` top: `Top` atom_eq: `if a=b then c else d fi ` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` has-value: `(a)↓` and: `P ∧ Q` not: `¬A` implies: `P `` Q` uimplies: `b 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 callbyvalueAtomEq sqequalHypSubstitution hypothesis sqequalRule baseApply closedConclusion baseClosed hypothesisEquality productElimination lemma_by_obid independent_functionElimination isectElimination because_Cache independent_isectElimination equalityTransitivity equalitySymmetry voidElimination atom_eqExceptionCases axiomSqleEquality exceptionSqequal sqleReflexivity callbyvalueCallbyvalue callbyvalueReduce callbyvalueExceptionCases sqequalAxiom isect_memberEquality

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

Date html generated: 2016_05_13-PM-03_44_13
Last ObjectModification: 2016_01_14-PM-07_07_42

Theory : computation

Home Index