---

Step * of 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])
BY
{ (NormalizeCFormTest 0 THEN Auto) }

---

Latex:

---

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])


By

---

Latex:
(NormalizeCFormTest  0  THEN  Auto)

---

Home Index