---

Step * 1 of Lemma Memory-class-single-val


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)
BY
{ (D 0 THEN Auto) }

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
10. e : E@i
11. v1 : S@i
12. v2 : S@i
13. v1 ∈ Memory-class(f;init;X)(e)@i
14. v2 ∈ Memory-class(f;init;X)(e)@i
⊢ v1 = v2 ∈ S

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index