### Nuprl Lemma : normalization-isaxiom

`∀[a,b,c:Top].  (if a = Ax then b a otherwise c ~ if a = Ax then b Ax otherwise c)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` top: `Top` isaxiom: `if z = Ax then a otherwise b` apply: `f a` sqequal: `s ~ t` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` has-value: `(a)↓` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` top: `Top`
Lemmas referenced :  is-exception_wf has-value_wf_base top_wf has-value-implies-dec-isaxiom-2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle sqleRule thin divergentSqle callbyvalueIsaxiom sqequalHypSubstitution hypothesis lemma_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination unionElimination sqequalRule sqleReflexivity lambdaFormation isect_memberEquality voidElimination voidEquality because_Cache isaxiomExceptionCases axiomSqleEquality exceptionSqequal baseApply closedConclusion baseClosed isectElimination sqequalAxiom

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

Date html generated: 2016_05_13-PM-03_43_30
Last ObjectModification: 2016_01_14-PM-07_08_05

Theory : computation

Home Index