---

Step * of Lemma Accum-loc-classrel-Memory

∀[Info,B,A:Type]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  (v ∈ Accum-loc-class(f;init;X)(e)
  ⇐⇒ ↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Memory-loc-class(f;init;X)(e) ∧ (v = (f loc(e) a b) ∈ B)))
BY
{ ((UnivCD THENA (Auto THEN Try ((Fold `eclass` 0 THEN Auto))))
   THEN Try ((Unfold `label` 0 THEN Auto))
   THEN (RWO "Accum-loc-classrel-Memory-sq" 0 THENA Auto)
   THEN (RWO "bag-member-lifting-loc-2" 0 THENA (Auto THEN Fold `eclass` 0 THEN Auto))
   THEN Fold `classrel` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].
\mforall{}[e:E].  \mforall{}[v:B].
    (v  \mmember{}  Accum-loc-class(f;init;X)(e)
    \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}a:A.  \mexists{}b:B.  (a  \mmember{}  X(e)  \mwedge{}  b  \mmember{}  Memory-loc-class(f;init;X)(e)  \mwedge{}  (v  =  (f  loc(e)  a  b))))


By

---

Latex:
((UnivCD  THENA  (Auto  THEN  Try  ((Fold  `eclass`  0  THEN  Auto))))
  THEN  Try  ((Unfold  `label`  0  THEN  Auto))
  THEN  (RWO  "Accum-loc-classrel-Memory-sq"  0  THENA  Auto)
  THEN  (RWO  "bag-member-lifting-loc-2"  0  THENA  (Auto  THEN  Fold  `eclass`  0  THEN  Auto))
  THEN  Fold  `classrel`  0
  THEN  Auto)

---

Home Index