---

Step * of Lemma Memory-class-single-val

∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f: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-class(f;init;X);S))
BY
{ ((UnivCD THENA Auto) THEN skip{[tactic]}) }

1
1. Info : Type
2. A : Type
3. S : Type
4. init : Id ⟶ bag(S)
5. f : A ⟶ S ⟶ S
6. X : EClass(A)
7. es : EO+(Info)@i'
8. single-valued-classrel(es;X;A)@i
9. ∀l:Id. single-valued-bag(init l;S)@i
⊢ single-valued-classrel(es;Memory-class(f;init;X);S)

---

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)
        (single-valued-classrel(es;X;A)
        {}\mRightarrow{}  (\mforall{}l:Id.  single-valued-bag(init  l;S))
        {}\mRightarrow{}  single-valued-classrel(es;Memory-class(f;init;X);S))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  skip\{[tactic]\})

---

Home Index