---

Step * 1 of Lemma list_accum_as_reduce


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
BY
{ (Thin (-2) THEN ListInd (-2) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
4.  \mforall{}a:A.  \mforall{}x1,x2:T.    (f[f[a;x1];x2]  =  f[f[a;x2];x1])
5.  u  :  T
6.  v  :  T  List
7.  \mforall{}[a0:A]
          (accumulate  (with  value  a  and  list  item  x):
              f[a;x]
            over  list:
                v
            with  starting  value:
              a0)
          =  reduce(\mlambda{}x,a.  f[a;x];a0;v))
8.  a0  :  A
\mvdash{}  reduce(\mlambda{}x,a.  f[a;x];f[a0;u];v)  =  f[reduce(\mlambda{}x,a.  f[a;x];a0;v);u]


By

---

Latex:
(Thin  (-2)  THEN  ListInd  (-2)  THEN  Reduce  0  THEN  Auto)

---

Home Index