Nuprl Lemma : test4-cform-normalize

∀[a,B:Top].
  (if a is an integer then <B[if a is an integer then 1
                              else 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 atom
                                                                                                    then 3 otherwise 4]
                           >
   else B[if a is an integer then 1
          else 2] ~ if a is an integer then <B[1], B[4]>
                    else B[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-isatom-2,  has-value-implies-dec-islambda-2,  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-isint-2
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalReflexivity,  cut,  sqequalSqle,  divergentSqle,  callbyvalueIsint,  sqequalHypSubstitution,  sqequalTransitivity,  computationStep,  hypothesis,  lemma_by_obid,  dependent_functionElimination,  thin,  hypothesisEquality,  independent_functionElimination,  unionElimination,  isintReduceTrue,  equalityTransitivity,  equalitySymmetry,  sqleRule,  sqleReflexivity,  because_Cache,  voidElimination,  lambdaFormation,  isect_memberEquality,  voidEquality,  isectElimination,  baseApply,  closedConclusion,  baseClosed,  introduction,  isintExceptionCases,  axiomSqleEquality,  exceptionSqequal,  isect_memberFormation,  sqequalAxiom
Latex:
\mforall{}[a,B:Top].
    (if  a  is  an  integer  then  <B[if  a  is  an  integer  then  1
                                                            else  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  atom  then  3
                                                                                                                                                            otherwise  4]
                                                      >
      else  B[if  a  is  an  integer  then  1
                    else  2]  \msim{}  if  a  is  an  integer  then  <B[1],  B[4]>
                                        else  B[2])


Date html generated: 2016_05_13-PM-04_08_13
Last ObjectModification: 2016_01_14-PM-07_46_32

Theory : fun_1


Home Index