---

Step * 1 1 of Lemma bag-accum_wf


1. T : Type
2. S : Type
3. init : S
4. f : S ⟶ T ⟶ S
5. ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)
6. a1 : T List
7. a : T
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    a1 @ [a]
  with starting value:
   init)
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    [a / a1]
  with starting value:
   init)
∈ S
BY
{ (MoveToConcl 3 THEN ListInd (-2) THEN Reduce 0 THEN Auto)⋅ }

1
1. T : Type
2. S : Type
3. f : S ⟶ T ⟶ S
4. ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)
5. a : T
6. u : T
7. v : T List
8. ∀init:S
     (accumulate (with value v and list item x):
       f[v;x]
      over list:
        v @ [a]
      with starting value:
       init)
     = accumulate (with value v and list item x):
        f[v;x]
       over list:
         [a / v]
       with starting value:
        init)
     ∈ S)
9. init : S
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    v @ [a]
  with starting value:
   f[init;u])
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    v
  with starting value:
   f[f[init;a];u])
∈ S

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  init  :  S
4.  f  :  S  {}\mrightarrow{}  T  {}\mrightarrow{}  S
5.  \mforall{}v:S.  \mforall{}x,y:T.    (f[f[v;y];x]  =  f[f[v;x];y])
6.  a1  :  T  List
7.  a  :  T
\mvdash{}  accumulate  (with  value  v  and  list  item  x):
      f[v;x]
    over  list:
        a1  @  [a]
    with  starting  value:
      init)
=  accumulate  (with  value  v  and  list  item  x):
      f[v;x]
    over  list:
        [a  /  a1]
    with  starting  value:
      init)


By

---

Latex:
(MoveToConcl  3  THEN  ListInd  (-2)  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index