---

Step * of Lemma combine-list-cons

∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
  ∀[L:A List]. ∀[a:A]. (combine-list(x,y.f[x;y];[a / L]) = f[a;combine-list(x,y.f[x;y];L)] ∈ A) supposing 0 < ||L|| 
  supposing Assoc(A;λx,y. f[x;y])
BY
{ (Auto THEN DVar `L' THEN All Reduce THEN Auto THEN RepUR ``combine-list`` 0 THEN Thin (-2)) }

1
1. A : Type
2. f : A ⟶ A ⟶ A
3. Assoc(A;λx,y. f[x;y])
4. u : A
5. v : A List
6. a : A
⊢ accumulate (with value x and list item y):
   f[x;y]
  over list:
    v
  with starting value:
   f[a;u])
= f[a;accumulate (with value x and list item y):
       f[x;y]
      over list:
        v
      with starting value:
       u)]
∈ A

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    \mforall{}[L:A  List]
        \mforall{}[a:A].  (combine-list(x,y.f[x;y];[a  /  L])  =  f[a;combine-list(x,y.f[x;y];L)]) 
        supposing  0  <  ||L|| 
    supposing  Assoc(A;\mlambda{}x,y.  f[x;y])


By

---

Latex:
(Auto  THEN  DVar  `L'  THEN  All  Reduce  THEN  Auto  THEN  RepUR  ``combine-list``  0  THEN  Thin  (-2))

---

Home Index