---

Step * of Lemma bag-accum-single

∀[init,f,x:Top].  (bag-accum(v,x.f[v;x];init;{x}) ~ f[init;x])
BY
{ (Auto THEN RepUR ``bag-accum single-bag`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[init,f,x:Top].    (bag-accum(v,x.f[v;x];init;\{x\})  \msim{}  f[init;x])


By

---

Latex:
(Auto  THEN  RepUR  ``bag-accum  single-bag``  0  THEN  Auto)

---

Home Index