---

Step * 1 of Lemma list_accum_permute1

.....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
BY
{ All (RepUR ``comm assoc infix_ap so_apply``) }

1
1. T : Type
2. A : Type
3. g : T ⟶ A
4. f : A ⟶ A ⟶ A
5. ∀[x,y:A].  ((f x y) = (f y x) ∈ A)
6. ∀[x,y,z:A].  ((f x (f y z)) = (f (f x y) z) ∈ A)
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:
        v
      with starting value:
       f n (g x))
     = 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:
.....subterm.....  T:t
2:n
1.  T  :  Type
2.  A  :  Type
3.  g  :  T  {}\mrightarrow{}  A
4.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
5.  Comm(A;\mlambda{}x,y.  f[x;y])
6.  Assoc(A;\mlambda{}x,y.  f[x;y])
7.  u  :  T
8.  v  :  T  List
9.  \mforall{}[x:T].  \mforall{}[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))
10.  x  :  T
11.  n  :  A
\mvdash{}  f[f[n;g[x]];g[u]]  =  f[f[n;g[u]];g[x]]


By

---

Latex:
All  (RepUR  ``comm  assoc  infix\_ap  so\_apply``)

---

Home Index