---

Step * of Lemma list_accum_cons

∀[A,B,y,f:Top].
  (accumulate (with value x and list item a):
    f[x;a]
   over list:
     [A / B]
   with starting value:
    y) ~ accumulate (with value x and list item a):
          f[x;a]
         over list:
           B
         with starting value:
          f[y;A]))
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,y,f:Top].
    (accumulate  (with  value  x  and  list  item  a):
        f[x;a]
      over  list:
          [A  /  B]
      with  starting  value:
        y)  \msim{}  accumulate  (with  value  x  and  list  item  a):
                    f[x;a]
                  over  list:
                      B
                  with  starting  value:
                    f[y;A]))


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index