---

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