---

Step * of Lemma reduce-as-combine-list

No Annotations
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
  (∀[L:A List]. ∀[z:A].  (reduce(f;z;L) = combine-list(x,y.f[x;y];[z / L]) ∈ A)) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))
BY
{ (RepUR ``combine-list comm assoc so_apply`` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN (RWO "-2<" 0 THEN Auto)
   THEN All (RepUR ``comm assoc so_apply``)) }

1
1. A : Type
2. f : A ⟶ A ⟶ A
3. ∀[x,y,z:A].  ((f x (f y z)) = (f (f x y) z) ∈ A)
4. ∀[x,y:A].  ((f x y) = (f y x) ∈ A)
5. u : A
6. v : A List
7. ∀[z:A]. (reduce(f;z;v) = accumulate (with value x and list item y): f x yover list:  vwith starting value: z) ∈ A)
8. z : A
⊢ (f u reduce(f;z;v)) = reduce(f;f z u;v) ∈ A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[L:A  List].  \mforall{}[z:A].    (reduce(f;z;L)  =  combine-list(x,y.f[x;y];[z  /  L])))  supposing 
          (Comm(A;\mlambda{}x,y.  f[x;y])  and 
          Assoc(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
(RepUR  ``combine-list  comm  assoc  so\_apply``  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "-2<"  0  THEN  Auto)
  THEN  All  (RepUR  ``comm  assoc  so\_apply``))

---

Home Index