---

Step * of Lemma Memory1-functional

∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  ∀es:EO+(Info). (single-valued-classrel(es;X;A) ⇒ Memory1(init;tr;X) is functional)
BY
{ (Auto
   THEN Try ((Fold `eclass` 0 THEN Auto))
   THEN Unfold `Memory1` 0
   THEN (BLemma `Memory-loc-class-functional`  THEN Reduce 0)
   THEN Auto
   THEN ProveSingleVal) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[tr:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].
    \mforall{}es:EO+(Info).  (single-valued-classrel(es;X;A)  {}\mRightarrow{}  Memory1(init;tr;X)  is  functional)


By

---

Latex:
(Auto
  THEN  Try  ((Fold  `eclass`  0  THEN  Auto))
  THEN  Unfold  `Memory1`  0
  THEN  (BLemma  `Memory-loc-class-functional`    THEN  Reduce  0)
  THEN  Auto
  THEN  ProveSingleVal)

---

Home Index