---

Step * 1 2 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. a1@0 : T
8. a2 : T
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    [a2; [a1@0 / a1]]
  with starting value:
   init)
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    [a1@0; [a2 / a1]]
  with starting value:
   init)
∈ S
BY
{ (Reduce 0 THEN EqCD THEN Auto)⋅ }

---

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.  a1@0  :  T
8.  a2  :  T
\mvdash{}  accumulate  (with  value  v  and  list  item  x):
      f[v;x]
    over  list:
        [a2;  [a1@0  /  a1]]
    with  starting  value:
      init)
=  accumulate  (with  value  v  and  list  item  x):
      f[v;x]
    over  list:
        [a1@0;  [a2  /  a1]]
    with  starting  value:
      init)


By

---

Latex:
(Reduce  0  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index