---

Step * of Lemma Memory-loc-class-mem

∀[Info,B,A:Type].
  ∀R:A ⟶ B ⟶ B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B. ∀a:A.
    ((∀a:A. ∀s:B. ∀e:E.
        (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-loc-class(f;init;X)(e) ⇒ R[a;s;f loc(e) a s]))
    ⇒ (∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
          (e1 ≤loc e 
          ⇒ (e <loc e')
          ⇒ (e' <loc e2)
          ⇒ a1 ∈ X(e)
          ⇒ s1 ∈ Memory-loc-class(f;init;X)(e)
          ⇒ a2 ∈ X(e')
          ⇒ s2 ∈ Memory-loc-class(f;init;X)(e')
          ⇒ R[a1;s1;s2]
          ⇒ R[a1;s1;f loc(e2) a2 s2]))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ (e1 <loc e2)
    ⇒ a ∈ X(e1)
    ⇒ v1 ∈ Memory-loc-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-loc-class(f;init;X)(e2)
    ⇒ R[a;v1;v2])
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "Memory-classrel-loc" (-1) THENA Auto)
   THEN (RWO "Memory-classrel-loc" (-2) THENA Auto)
   THEN (RWO "Memory-classrel-loc" (-7) THENA Auto)
   THEN (RWO "Memory-classrel-loc" (-8) THENA Auto)
   THEN InstLemma `Memory-class-mem` [⌜Info⌝;⌜B⌝;⌜A⌝;⌜R⌝;⌜f loc(e2)⌝;⌜init⌝;⌜X⌝;⌜es⌝;⌜e1⌝;⌜e2⌝;⌜v1⌝;⌜v2⌝;⌜a⌝]⋅
   THEN Auto
   THEN ExRepD
   THEN MaAuto
   THEN InstHyp [⌜a1⌝;⌜s⌝;⌜e⌝] (-15)⋅
   THEN MaAuto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].
    \mforall{}R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B.  \mforall{}init:Id  {}\mrightarrow{}  bag(B).  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).
    \mforall{}e1,e2:E.  \mforall{}v1,v2:B.  \mforall{}a:A.
        ((\mforall{}a:A.  \mforall{}s:B.  \mforall{}e:E.
                (e1  \mleq{}loc  e 
                {}\mRightarrow{}  (e  <loc  e2)
                {}\mRightarrow{}  a  \mmember{}  X(e)
                {}\mRightarrow{}  s  \mmember{}  Memory-loc-class(f;init;X)(e)
                {}\mRightarrow{}  R[a;s;f  loc(e)  a  s]))
        {}\mRightarrow{}  (\mforall{}a1,a2:A.  \mforall{}s1,s2:B.  \mforall{}e,e':E.
                    (e1  \mleq{}loc  e 
                    {}\mRightarrow{}  (e  <loc  e')
                    {}\mRightarrow{}  (e'  <loc  e2)
                    {}\mRightarrow{}  a1  \mmember{}  X(e)
                    {}\mRightarrow{}  s1  \mmember{}  Memory-loc-class(f;init;X)(e)
                    {}\mRightarrow{}  a2  \mmember{}  X(e')
                    {}\mRightarrow{}  s2  \mmember{}  Memory-loc-class(f;init;X)(e')
                    {}\mRightarrow{}  R[a1;s1;s2]
                    {}\mRightarrow{}  R[a1;s1;f  loc(e2)  a2  s2]))
        {}\mRightarrow{}  single-valued-classrel(es;X;A)
        {}\mRightarrow{}  single-valued-bag(init  loc(e1);B)
        {}\mRightarrow{}  (e1  <loc  e2)
        {}\mRightarrow{}  a  \mmember{}  X(e1)
        {}\mRightarrow{}  v1  \mmember{}  Memory-loc-class(f;init;X)(e1)
        {}\mRightarrow{}  v2  \mmember{}  Memory-loc-class(f;init;X)(e2)
        {}\mRightarrow{}  R[a;v1;v2])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "Memory-classrel-loc"  (-1)  THENA  Auto)
  THEN  (RWO  "Memory-classrel-loc"  (-2)  THENA  Auto)
  THEN  (RWO  "Memory-classrel-loc"  (-7)  THENA  Auto)
  THEN  (RWO  "Memory-classrel-loc"  (-8)  THENA  Auto)
  THEN  InstLemma  `Memory-class-mem`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}f  loc(e2)\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};
  \mkleeneopen{}v2\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ExRepD
  THEN  MaAuto
  THEN  InstHyp  [\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-15)\mcdot{}
  THEN  MaAuto)

---

Home Index