---

Step * of Lemma list_accum_permute1

∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
  (∀[L:T List]. ∀[x:T]. ∀[n:A].
     (accumulate (with value a and list item z):
       f[a;g[z]]
      over list:
        [x / L]
      with starting value:
       n)
     = accumulate (with value a and list item z):
        f[a;g[z]]
       over list:
         L @ [x]
       with starting value:
        n)
     ∈ A)) supposing 
     (Assoc(A;λx,y. f[x;y]) and 
     Comm(A;λx,y. f[x;y]))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN (RWO "9<" 0 THENA Auto) THEN Reduce 0 THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
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. ∀[x:T]. ∀[n:A].
     (accumulate (with value a and list item z):
       f[a;g[z]]
      over list:
        [x / v]
      with starting value:
       n)
     = accumulate (with value a and list item z):
        f[a;g[z]]
       over list:
         v @ [x]
       with starting value:
        n)
     ∈ A)
10. x : T
11. n : A
⊢ f[f[n;g[x]];g[u]] = f[f[n;g[u]];g[x]] ∈ A

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[g:T  {}\mrightarrow{}  A].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[L:T  List].  \mforall{}[x:T].  \mforall{}[n:A].
          (accumulate  (with  value  a  and  list  item  z):
              f[a;g[z]]
            over  list:
                [x  /  L]
            with  starting  value:
              n)
          =  accumulate  (with  value  a  and  list  item  z):
                f[a;g[z]]
              over  list:
                  L  @  [x]
              with  starting  value:
                n)))  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
  THEN  (RWO  "9<"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto)

---

Home Index