---

Step * of Lemma length-as-accum

∀[L:Top List]. (||L|| ~ accumulate (with value n and list item x): n + 1over list:  Lwith starting value: 0))
BY
{ xxx((Assert ∀L:Top List. ∀n:ℤ.
                (||L|| + n ~ accumulate (with value n and list item x):
                              n + 1
                             over list:
                               L
                             with starting value:
                              n)) BY
             (InductionOnList THEN Reduce 0 THEN Auto THEN RWO "-2<" 0 THEN Auto))
      THEN ParallelLast
      THEN RWO  "-1<" 0
      THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[L:Top  List]
    (||L||  \msim{}  accumulate  (with  value  n  and  list  item  x):
                        n  +  1
                      over  list:
                          L
                      with  starting  value:
                        0))


By

---

Latex:
xxx((Assert  \mforall{}L:Top  List.  \mforall{}n:\mBbbZ{}.
                            (||L||  +  n  \msim{}  accumulate  (with  value  n  and  list  item  x):
                                                        n  +  1
                                                      over  list:
                                                          L
                                                      with  starting  value:
                                                        n))  BY
                      (InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  RWO  "-2<"  0  THEN  Auto))
        THEN  ParallelLast
        THEN  RWO    "-1<"  0
        THEN  Auto')xxx

---

Home Index