---

Step * of Lemma list_accum_as_reduce

∀[T,A:Type]. ∀[f:A ⟶ T ⟶ A].
  ∀[L:T List]. ∀[a0:A].
    (accumulate (with value a and list item x):
      f[a;x]
     over list:
       L
     with starting value:
      a0)
    = reduce(λx,a. f[a;x];a0;L)
    ∈ A) 
  supposing ∀a:A. ∀x1,x2:T.  (f[f[a;x1];x2] = f[f[a;x2];x1] ∈ A)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN (RWO "-2" 0 THENA Auto)) }

1
1. T : Type
2. A : Type
3. f : A ⟶ T ⟶ A
4. ∀a:A. ∀x1,x2:T.  (f[f[a;x1];x2] = f[f[a;x2];x1] ∈ A)
5. u : T
6. v : T List
7. ∀[a0:A]
     (accumulate (with value a and list item x):
       f[a;x]
      over list:
        v
      with starting value:
       a0)
     = reduce(λx,a. f[a;x];a0;v)
     ∈ A)
8. a0 : A
⊢ reduce(λx,a. f[a;x];f[a0;u];v) = f[reduce(λx,a. f[a;x];a0;v);u] ∈ A

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A].
    \mforall{}[L:T  List].  \mforall{}[a0:A].
        (accumulate  (with  value  a  and  list  item  x):
            f[a;x]
          over  list:
              L
          with  starting  value:
            a0)
        =  reduce(\mlambda{}x,a.  f[a;x];a0;L)) 
    supposing  \mforall{}a:A.  \mforall{}x1,x2:T.    (f[f[a;x1];x2]  =  f[f[a;x2];x1])


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  (RWO  "-2"  0  THENA  Auto))

---

Home Index