---

Step * of Lemma list_accum_append

∀[A:Top List]. ∀[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:
          accumulate (with value x and list item a):
           f[x;a]
          over list:
            A
          with starting value:
           y)))
BY
{ ((((InductionOnList THEN Reduce 0 THEN UnivCD) THENA Auto) THEN Try (Trivial) THEN BackThruSomeHyp) THENA Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Top  List].  \mforall{}[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:
                    accumulate  (with  value  x  and  list  item  a):
                      f[x;a]
                    over  list:
                        A
                    with  starting  value:
                      y)))


By

---

Latex:
((((InductionOnList  THEN  Reduce  0  THEN  UnivCD)  THENA  Auto)  THEN  Try  (Trivial)  THEN  BackThruSomeHyp)
  THENA  Auto
  )

---

Home Index