---

Step * of Lemma list_accum-remove-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
  (∀[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)) 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
{ (InductionOnList⋅ 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. u : T
10. v : T List
11. ∀[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:
          remove-repeats(eq;v)
        with starting value:
         n)
      ∈ A)
12. n : A
⊢ accumulate (with value a and list item z):
   f[a;g[z]]
  over list:
    [u / v]
  with starting value:
   n)
= accumulate (with value a and list item z):
   f[a;g[z]]
  over list:
    remove-repeats(eq;[u / v])
  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: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:
                  remove-repeats(eq;as)
              with  starting  value:
                n)))  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:
(InductionOnList\mcdot{}  THEN  Auto)

---

Home Index