---

Step * of Lemma bag-accum_wf

∀[T,S:Type]. ∀[init:S]. ∀[f:S ⟶ T ⟶ S]. ∀[bs:bag(T)].
  bag-accum(v,x.f[v;x];init;bs) ∈ S supposing ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)
BY
{ (Auto THEN BagD (-2) THEN Auto THEN Unfold `bag-accum` 0⋅) }

1
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. as : T List
7. bs : T List
8. permutation(T;as;bs)
⊢ accumulate (with value v and list item x):
   f[v;x]
  over list:
    as
  with starting value:
   init)
= accumulate (with value v and list item x):
   f[v;x]
  over list:
    bs
  with starting value:
   init)
∈ S

---

Latex:

---

Latex:
\mforall{}[T,S:Type].  \mforall{}[init:S].  \mforall{}[f:S  {}\mrightarrow{}  T  {}\mrightarrow{}  S].  \mforall{}[bs:bag(T)].
    bag-accum(v,x.f[v;x];init;bs)  \mmember{}  S  supposing  \mforall{}v:S.  \mforall{}x,y:T.    (f[f[v;y];x]  =  f[f[v;x];y])


By

---

Latex:
(Auto  THEN  BagD  (-2)  THEN  Auto  THEN  Unfold  `bag-accum`  0\mcdot{})

---

Home Index