---

Step * of Lemma State-class-es-sv1

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[init:Id ─→ bag(B)].
  (es-sv-class(es;State-class(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))
BY
{ ((UnivCD THENA Auto) THEN Unfold `State-class` 0) }

1
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. f : A ─→ B ─→ B
6. X : EClass(A)
7. init : Id ─→ bag(B)
8. es-sv-class(es;X)
9. ∀l:Id. (#(init l) ≤ 1)
⊢ es-sv-class(es;λx,s. if bag-null(x) then s else lifting-2(f) x s fi |X, Memory-class(f;init;X)|)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    (es-sv-class(es;State-class(init;f;X)))  supposing  ((\mforall{}l:Id.  (\#(init  l)  \mleq{}  1))  and  es-sv-class(es;X))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `State-class`  0)

---

Home Index