---

Step * of Lemma Memory-loc-class-single-val

∀[Info,A,S:Type]. ∀[init:Id ─→ bag(S)]. ∀[f:Id ─→ A ─→ S ─→ S]. ∀[X:EClass(A)].
  ∀es:EO+(Info)
    (single-valued-classrel(es;X;A)
    ⇒ (∀l:Id. single-valued-bag(init l;S))
    ⇒ single-valued-classrel(es;Memory-loc-class(f;init;X);S))
BY
{ ((UnivCD THENA Auto)
   THEN (Unfold `single-valued-classrel` 0 THEN Auto)
   THEN (RWO "Memory-classrel-loc" (-1) THENA Auto)
   THEN (RWO "Memory-classrel-loc" (-2) THENA Auto)
   THEN (InstLemma `Memory-class-single-val` [⌈Info⌉;⌈A⌉;⌈S⌉;⌈init⌉;⌈f loc(e)⌉;⌈X⌉;⌈es⌉]⋅ THENA Auto)
   THEN Unfold `single-valued-classrel` (-1)
   THEN InstHyp [⌈e⌉;⌈v1⌉;⌈v2⌉] (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,S:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X:EClass(A)].
    \mforall{}es:EO+(Info)
        (single-valued-classrel(es;X;A)
        {}\mRightarrow{}  (\mforall{}l:Id.  single-valued-bag(init  l;S))
        {}\mRightarrow{}  single-valued-classrel(es;Memory-loc-class(f;init;X);S))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Unfold  `single-valued-classrel`  0  THEN  Auto)
  THEN  (RWO  "Memory-classrel-loc"  (-1)  THENA  Auto)
  THEN  (RWO  "Memory-classrel-loc"  (-2)  THENA  Auto)
  THEN  (InstLemma  `Memory-class-single-val`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}f  loc(e)\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `single-valued-classrel`  (-1)
  THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index