---

Step * 1 of Lemma State-class-es-sv


1. Info : Type
2. A : Type
3. es : EO+(Info)
4. f : Top
5. X : EClass(A)
6. init : Id ─→ bag(Top)
7. es-sv-class(es;X)
8. ∀l:Id. (#(init l) ≤ 1)
⊢ es-sv-class(es;State-class(init;f;X))
BY
{ (RepUR ``State-class es-sv-class simple-comb-2 simple-comb`` 0 THEN Auto THEN (SplitOnConclITE THENA MaAuto)) }

1
.....truecase..... 
1. Info : Type
2. A : Type
3. es : EO+(Info)
4. f : Top
5. X : EClass(A)
6. init : Id ─→ bag(Top)
7. es-sv-class(es;X)
8. ∀l:Id. (#(init l) ≤ 1)
9. e : E@i
10. (X es e) = {} ∈ bag(A)
⊢ #(Memory-class(f;init;X) es e) ≤ 1

2
.....falsecase..... 
1. Info : Type
2. A : Type
3. es : EO+(Info)
4. f : Top
5. X : EClass(A)
6. init : Id ─→ bag(Top)
7. es-sv-class(es;X)
8. ∀l:Id. (#(init l) ≤ 1)
9. e : E@i
10. ¬((X es e) = {} ∈ bag(A))
⊢ #(lifting-2(f) (X es e) (Memory-class(f;init;X) es e)) ≤ 1

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  es  :  EO+(Info)
4.  f  :  Top
5.  X  :  EClass(A)
6.  init  :  Id  {}\mrightarrow{}  bag(Top)
7.  es-sv-class(es;X)
8.  \mforall{}l:Id.  (\#(init  l)  \mleq{}  1)
\mvdash{}  es-sv-class(es;State-class(init;f;X))


By

---

Latex:
(RepUR  ``State-class  es-sv-class  simple-comb-2  simple-comb``  0
  THEN  Auto
  THEN  (SplitOnConclITE  THENA  MaAuto))

---

Home Index