Step
*
of Lemma
test2-cform-normalize
∀[a,B:Top].
(if a is lambda then <B[if a is lambda then 1 otherwise 2]
, B[if a = Ax then 3 otherwise if a is a pair then 3
otherwise if a is an integer then 3
else if a is an atom then 3
otherwise isatom1(a;3;isatom2(a;3;4))]
> otherwise B[if a is lambda then 1 otherwise 2] ~ if a is lambda then <B[1], B[4]> otherwise B[2\000C])
BY
{ (Repeat (RW (HigherC NormalizeCFormTestC) 0⋅) THEN Auto) }
Latex:
Latex:
\mforall{}[a,B:Top].
(if a is lambda then <B[if a is lambda then 1 otherwise 2]
, B[if a = Ax then 3
otherwise if a is a pair then 3
otherwise if a is an integer then 3
else if a is an atom then 3
otherwise isatom1(a;3;isatom2(a;3;4))]
> otherwise B[if a is lambda then 1 otherwise 2] \msim{} if a is lambda then <B[1],\000C B[4]> otherwise B[2])
By
Latex:
(Repeat (RW (HigherC NormalizeCFormTestC) 0\mcdot{}) THEN Auto)
Home
Index