---

Step * of Lemma list_accum_is_reduce

∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
  (∀[as:A List]. ∀[n:A].
     (accumulate (with value a and list item b):
       f[a;b]
      over list:
        as
      with starting value:
       n)
     = reduce(f;n;as)
     ∈ A)) supposing 
     (Assoc(A;λx,y. f[x;y]) and 
     Comm(A;λx,y. f[x;y]))
BY
{ (Auto THEN RWO "list_accum_as_reduce" 0 THEN Auto) }

1
1. A : Type
2. f : A ⟶ A ⟶ A
3. Comm(A;λx,y. f[x;y])
4. Assoc(A;λx,y. f[x;y])
5. as : A List
6. n : A
7. a : A
8. x1 : A
9. x2 : A
⊢ f[f[a;x1];x2] = f[f[a;x2];x1] ∈ A

2
1. A : Type
2. f : A ⟶ A ⟶ A
3. Comm(A;λx,y. f[x;y])
4. Assoc(A;λx,y. f[x;y])
5. as : A List
6. n : A
⊢ reduce(λb,a. f[a;b];n;as) = reduce(f;n;as) ∈ A

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as:A  List].  \mforall{}[n:A].
          (accumulate  (with  value  a  and  list  item  b):
              f[a;b]
            over  list:
                as
            with  starting  value:
              n)
          =  reduce(f;n;as)))  supposing 
          (Assoc(A;\mlambda{}x,y.  f[x;y])  and 
          Comm(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
(Auto  THEN  RWO  "list\_accum\_as\_reduce"  0  THEN  Auto)

---

Home Index