Nuprl Lemma : test5-cform-normalize

∀[a,B:Top].
  (if a is an atom then <B[if a is an atom then 1 otherwise 2]
                        , B[if a = Ax then 3 otherwise if a is a pair then 3 otherwise if a is lambda then 3
                                                                                       otherwise if a is an integer
                                                                                                 3
                                                                                                 else 4]
                        > otherwise B[if a is an atom then 1 otherwise 2] ~ if a is an atom then <B[1], B[4]> otherwise \000CB[2])


Proof



Definitions occuring in Statement :  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s],  isatom: if z is an atom then a otherwise b,  ispair: if z is a pair then a otherwise b,  isaxiom: if z = Ax then a otherwise b,  islambda: if z is lambda then a otherwise b,  isint: isint def,  pair: <a, b>,  natural_number: $n,  sqequal: s ~ t
Definitions unfolded in proof :  has-value: (a)↓,  all: ∀x:A. B[x],  member: t ∈ T,  implies: P ⇒ Q,  or: P ∨ Q,  not: ¬A,  false: False,  top: Top,  uall: ∀[x:A]. B[x]
Lemmas referenced :  not-atom-member-int,  has-value-implies-dec-isint-2,  has-value-implies-dec-islambda-2,  atom-implies-ispair-right,  has-value-implies-dec-ispair-2,  is-exception_wf,  has-value_wf_base,  top_wf,  not-btrue-sqeq-bfalse,  has-value-implies-dec-isaxiom-2,  has-value-implies-dec-isatom-2
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalReflexivity,  cut,  sqequalSqle,  divergentSqle,  callbyvalueIsatom,  sqequalHypSubstitution,  sqequalTransitivity,  computationStep,  hypothesis,  lemma_by_obid,  dependent_functionElimination,  thin,  hypothesisEquality,  independent_functionElimination,  unionElimination,  isatomReduceTrue,  equalityTransitivity,  equalitySymmetry,  sqleRule,  sqleReflexivity,  because_Cache,  voidElimination,  lambdaFormation,  isect_memberEquality,  voidEquality,  isectElimination,  baseApply,  closedConclusion,  baseClosed,  introduction,  isatomExceptionCases,  axiomSqleEquality,  exceptionSqequal,  isintReduceTrue,  isect_memberFormation,  sqequalAxiom
Latex:
\mforall{}[a,B:Top].
    (if  a  is  an  atom  then  <B[if  a  is  an  atom  then  1  otherwise  2]
                                                ,  B[if  a  =  Ax  then  3  otherwise  if  a  is  a  pair  then  3
                                                                                                              otherwise  if  a  is  lambda  then  3
                                                                                                                                  otherwise  if  a  is  an  integer  then  3
                                                                                                                                                      else  4]
                                                >  otherwise  B[if  a  is  an  atom  then  1  otherwise  2]  \msim{}  if  a  is  an  atom  then  <B[\000C1],  B[4]>  otherwise  B[2])


Date html generated: 2016_05_13-PM-04_08_15
Last ObjectModification: 2016_01_14-PM-07_46_37

Theory : fun_1


Home Index