---

Step * of Lemma Memory-loc-class-is-prior-State-loc-comb

∀[Info,B,A:Type]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)].
  ∀X:EClass(A). (Memory-loc-class(f;init;X) = Prior(State-loc-comb(init;f;X))?init ∈ EClass(B))
BY
{ ProveMemoryClassesEqual⋅ }

---

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).  (Memory-loc-class(f;init;X)  =  Prior(State-loc-comb(init;f;X))?init)


By

---

Latex:
ProveMemoryClassesEqual\mcdot{}

---

Home Index