---

Step * 1 of Lemma combine-list-cons


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
BY
{ (MoveToConcl 4 THEN ListInd 4 THEN Reduce 0 THEN Auto)⋅ }

1
1. A : Type
2. f : A ⟶ A ⟶ A
3. Assoc(A;λx,y. f[x;y])
4. a : A
5. u : A
6. v : A List
7. ∀u: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)
8. u@0 : A
⊢ accumulate (with value x and list item y):
   f[x;y]
  over list:
    v
  with starting value:
   f[f[a;u@0];u])
= f[a;accumulate (with value x and list item y):
       f[x;y]
      over list:
        v
      with starting value:
       f[u@0;u])]
∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
3.  Assoc(A;\mlambda{}x,y.  f[x;y])
4.  u  :  A
5.  v  :  A  List
6.  a  :  A
\mvdash{}  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)]


By

---

Latex:
(MoveToConcl  4  THEN  ListInd  4  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index