---

Step * of Lemma list_accum_cons_lemma

∀y,x,z,f:Top.
  (accumulate (with value a and list item b):
    f[a;b]
   over list:
     [x / y]
   with starting value:
    z) ~ accumulate (with value a and list item b):
          f[a;b]
         over list:
           y
         with starting value:
          f[z;x]))
BY
{ ((UnivCD THENA Auto) THEN Try (RW (AddrC [1] (RecUnfoldC `list_accum` ANDTHENC ReduceC)) 0)⋅) }

1
1. y : Top
2. x : Top
3. z : Top
4. f : Top
⊢ accumulate (with value a and list item b):
   f[a;b]
  over list:
    y
  with starting value:
   f[z;x]) ~ accumulate (with value a and list item b):
              f[a;b]
             over list:
               y
             with starting value:
              f[z;x])

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Try  (RW  (AddrC  [1]  (RecUnfoldC  `list\_accum`  ANDTHENC  ReduceC))  0)\mcdot{})

---

Home Index