### Nuprl Lemma : strictness-atom1_eq-right

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

Proof

Definitions occuring in Statement :  bottom: `⊥` callbyvalue: callbyvalue atom_eq: atomeqn def uall: `∀[x:A]. B[x]` top: `Top` 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 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