---

Step * 1 of Lemma list_accum_permute

.....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. ∀[bs:T List]. ∀[n:A].
     (accumulate (with value a and list item z):
       f[a;g[z]]
      over list:
        v @ bs
      with starting value:
       n)
     = accumulate (with value a and list item z):
        f[a;g[z]]
       over list:
         bs @ v
       with starting value:
        n)
     ∈ A)
10. bs : T List
11. n : A
⊢ accumulate (with value a and list item z):
   f[a;g[z]]
  over list:
    bs
  with starting value:
   f[n;g[u]])
= f[accumulate (with value a and list item z):
     f[a;g[z]]
    over list:
      bs
    with starting value:
     n);g[u]]
∈ A
BY
{ ((InstLemma `list_accum_permute1` [⌜T⌝;⌜A⌝;⌜g⌝;⌜f⌝;⌜bs⌝;⌜u⌝;⌜n⌝]⋅ THENA Auto)
   THEN (RWO "list_accum_append" (-1) THENA Auto)
   THEN Reduce (-1)) }

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 @ bs
      with starting value:
       n)
     = accumulate (with value a and list item z):
        f[a;g[z]]
       over list:
         bs @ v
       with starting value:
        n)
     ∈ A)
10. bs : T List
11. n : A
12. accumulate (with value a and list item z):
     f[a;g[z]]
    over list:
      bs
    with starting value:
     f[n;g[u]])
= f[accumulate (with value a and list item z):
     f[a;g[z]]
    over list:
      bs
    with starting value:
     n);g[u]]
∈ A
⊢ accumulate (with value a and list item z):
   f[a;g[z]]
  over list:
    bs
  with starting value:
   f[n;g[u]])
= f[accumulate (with value a and list item z):
     f[a;g[z]]
    over list:
      bs
    with starting value:
     n);g[u]]
∈ 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{}[bs:T  List].  \mforall{}[n:A].
          (accumulate  (with  value  a  and  list  item  z):
              f[a;g[z]]
            over  list:
                v  @  bs
            with  starting  value:
              n)
          =  accumulate  (with  value  a  and  list  item  z):
                f[a;g[z]]
              over  list:
                  bs  @  v
              with  starting  value:
                n))
10.  bs  :  T  List
11.  n  :  A
\mvdash{}  accumulate  (with  value  a  and  list  item  z):
      f[a;g[z]]
    over  list:
        bs
    with  starting  value:
      f[n;g[u]])
=  f[accumulate  (with  value  a  and  list  item  z):
          f[a;g[z]]
        over  list:
            bs
        with  starting  value:
          n);g[u]]


By

---

Latex:
((InstLemma  `list\_accum\_permute1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "list\_accum\_append"  (-1)  THENA  Auto)
  THEN  Reduce  (-1))

---

Home Index