---

Step * 2 2 1 of Lemma list_accum_set-equal


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
15. cs : T List
16. ds : T List
17. bs = (cs @ [u / ds]) ∈ (T List)
18. set-equal(T;v;cs @ ds)
⊢ 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:
    cs @ [u / ds]
  with starting value:
   n)
∈ A
BY
{ (InstLemma `list_accum_permute` [⌜T⌝;⌜A⌝;⌜g⌝;⌜f⌝]⋅ THENA 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. 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
15. cs : T List
16. ds : T List
17. bs = (cs @ [u / ds]) ∈ (T List)
18. set-equal(T;v;cs @ ds)
19. ∀[as,bs:T List]. ∀[n:A].
      (accumulate (with value a and list item z):
        f[a;g[z]]
       over list:
         as @ bs
       with starting value:
        n)
      = accumulate (with value a and list item z):
         f[a;g[z]]
        over list:
          bs @ as
        with starting value:
         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:
    cs @ [u / ds]
  with starting value:
   n)
∈ A

---

Latex:

---

Latex:

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{}[bs:T  List]
          (\mforall{}[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)))  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
15.  cs  :  T  List
16.  ds  :  T  List
17.  bs  =  (cs  @  [u  /  ds])
18.  set-equal(T;v;cs  @  ds)
\mvdash{}  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:
        cs  @  [u  /  ds]
    with  starting  value:
      n)


By

---

Latex:
(InstLemma  `list\_accum\_permute`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index