---

Step * of Lemma list_accum_set-equal

∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
  (∀[as,bs:T List].
     (∀[n:A]
        (accumulate (with value a and list item z):
          f[a;g[z]]
         over list:
           as
         with starting value:
          n)
        = accumulate (with value a and list item z):
           f[a;g[z]]
          over list:
            bs
          with starting value:
           n)
        ∈ A)) supposing 
        (no_repeats(T;bs) and 
        no_repeats(T;as) and 
        set-equal(T;as;bs))) supposing 
     (Assoc(A;λx,y. f[x;y]) and 
     Comm(A;λx,y. f[x;y]))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. A : Type
3. g : T ⟶ A
4. f : A ⟶ A ⟶ A
5. Comm(A;λx,y. f[x;y])
6. Assoc(A;λx,y. f[x;y])
7. bs : T List
8. set-equal(T;[];bs)
9. no_repeats(T;[])
10. no_repeats(T;bs)
11. n : A
⊢ n = accumulate (with value a and list item z): f[a;g[z]]over list:  bswith starting value: n) ∈ A

2
1. T : Type
2. A : Type
3. g : T ⟶ A
4. f : A ⟶ A ⟶ A
5. Comm(A;λx,y. f[x;y])
6. Assoc(A;λx,y. f[x;y])
7. u : T
8. v : T List
9. ∀[bs:T List]
     (∀[n:A]
        (accumulate (with value a and list item z):
          f[a;g[z]]
         over list:
           v
         with starting value:
          n)
        = accumulate (with value a and list item z):
           f[a;g[z]]
          over list:
            bs
          with starting value:
           n)
        ∈ A)) supposing 
        (no_repeats(T;bs) and 
        no_repeats(T;v) and 
        set-equal(T;v;bs))
10. bs : T List
11. set-equal(T;[u / v];bs)
12. no_repeats(T;[u / v])
13. no_repeats(T;bs)
14. n : A
⊢ accumulate (with value a and list item z):
   f[a;g[z]]
  over list:
    v
  with starting value:
   f[n;g[u]])
= accumulate (with value a and list item z):
   f[a;g[z]]
  over list:
    bs
  with starting value:
   n)
∈ A

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[g:T  {}\mrightarrow{}  A].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as,bs:T  List].
          (\mforall{}[n:A]
                (accumulate  (with  value  a  and  list  item  z):
                    f[a;g[z]]
                  over  list:
                      as
                  with  starting  value:
                    n)
                =  accumulate  (with  value  a  and  list  item  z):
                      f[a;g[z]]
                    over  list:
                        bs
                    with  starting  value:
                      n)))  supposing 
                (no\_repeats(T;bs)  and 
                no\_repeats(T;as)  and 
                set-equal(T;as;bs)))  supposing 
          (Assoc(A;\mlambda{}x,y.  f[x;y])  and 
          Comm(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index