---

Step * of Lemma Memory-class-single-val2

∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:A ⟶ S ⟶ S]. ∀[X:EClass(A)].
  ∀es:EO+(Info). ∀e:E. ∀s1,s2:S.
    (single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e);S)
    ⇒ s1 ∈ Memory-class(f;init;X)(e)
    ⇒ s2 ∈ Memory-class(f;init;X)(e)
    ⇒ (s1 = s2 ∈ S))
BY
{ ((UnivCD THENA Auto)
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN Try (Complete ((UseSingleVal (-3) (-1) THEN Auto)))
   THEN Try (Complete ((Assert ⌜False⌝⋅ THEN Auto)))
   THEN Try (Complete ((FLemma `iterated_classrel-single-val` [-3;-1] THEN Auto)))) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  Try  (Complete  ((UseSingleVal  (-3)  (-1)  THEN  Auto)))
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  Try  (Complete  ((FLemma  `iterated\_classrel-single-val`  [-3;-1]  THEN  Auto))))

---

Home Index