---

Step * of Lemma member-loop-class-memory

∀[Info,B:Type]. ∀[X:EClass(B ⟶ B)]. ∀[init:Id ⟶ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  (e ∈b loop-class-memory(X;init) ~ 0 <z #(init loc(e)))
BY
{ ((UnivCD THENA Auto)
   THEN VrBoolCase ⌜e ∈b loop-class-memory(X;init)⌝⋅
   THEN VrBoolCase ⌜0 <z #(init loc(e))⌝⋅
   THEN (RWO "loop-class-memory-member<" (-2) THEN Auto)
   THEN RW assert_pushdownC (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (e  \mmember{}\msubb{}  loop-class-memory(X;init)  \msim{}  0  <z  \#(init  loc(e)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  VrBoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  loop-class-memory(X;init)\mkleeneclose{}\mcdot{}
  THEN  VrBoolCase  \mkleeneopen{}0  <z  \#(init  loc(e))\mkleeneclose{}\mcdot{}
  THEN  (RWO  "loop-class-memory-member<"  (-2)  THEN  Auto)
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto)

---

Home Index