---

Step * of Lemma list_accum-set-equal-idemp

∀[T:Type]. ∀[eq:EqDecider(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 set-equal(T;as;bs)) supposing 
     ((∀x:A. (f[x;x] = x ∈ A)) and 
     Assoc(A;λx,y. f[x;y]) and 
     Comm(A;λx,y. f[x;y]))
BY
{ (InstLemma `list_accum-remove-repeats` [] THEN RepeatFor 8 ((ParallelLast' THENA Auto)) THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. A : Type
4. g : T ⟶ A
5. f : A ⟶ A ⟶ A
6. Comm(A;λx,y. f[x;y])
7. Assoc(A;λx,y. f[x;y])
8. ∀x:A. (f[x;x] = x ∈ A)
9. ∀[as: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:
         remove-repeats(eq;as)
       with starting value:
        n)
     ∈ A)
10. as : T List
11. bs : T List
12. set-equal(T;as;bs)
13. 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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[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  set-equal(T;as;bs))  supposing 
          ((\mforall{}x:A.  (f[x;x]  =  x))  and 
          Assoc(A;\mlambda{}x,y.  f[x;y])  and 
          Comm(A;\mlambda{}x,y.  f[x;y]))


By

---

Latex:
(InstLemma  `list\_accum-remove-repeats`  []  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))  THEN  Auto)

---

Home Index