Step
*
of Lemma
length-normal-form
∀[A:Top]. (rec-case(A) of [] => 0 | _::as' => _.||as'|| + 1 ~ ||A||)
BY
{ ((UnivCD THENA Auto) THEN SymbComp 0 THEN RW (AddrC [2] UnrollLoopsOnceC) 0 THEN Auto) }
Latex:
\mforall{}[A:Top]. (rec-case(A) of [] => 0 | $_{}$::as' => $_{}$.||as\000C'|| + 1 \msim{} ||A||)
By
((UnivCD THENA Auto) THEN SymbComp 0 THEN RW (AddrC [2] UnrollLoopsOnceC) 0 THEN Auto)
Home
Index