---

Step * 1 1 of Lemma combine-list-cons


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
BY
{ (Subst ⌜f[f[a;u@0];u] = f[a;f[u@0;u]] ∈ A⌝ 0⋅ THEN Auto) }

1
.....equality..... 
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
⊢ f[f[a;u@0];u] = f[a;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.  a  :  A
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}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)])
8.  u@0  :  A
\mvdash{}  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])]


By

---

Latex:
(Subst  \mkleeneopen{}f[f[a;u@0];u]  =  f[a;f[u@0;u]]\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index