---

Step * of Lemma State-class-es-sv

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ─→ bag(Top)].
  (es-sv-class(es;State-class(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))
BY
{ (UnivCD
   THEN Try (Complete (Auto))
   THEN Try (Complete (((GenConcl ⌈State-class(init;f;X) = Z ∈ EClass(Top)⌉⋅
                         THENA Try ((Using [`es',⌈es⌉] (BLemma `State-class-top`)⋅ THEN Auto))
                         )
                        THEN Auto
                        )))) }

1
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))

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Top].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(Top)].
    (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
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Complete  (((GenConcl  \mkleeneopen{}State-class(init;f;X)  =  Z\mkleeneclose{}\mcdot{}
                                              THENA  Try  ((Using  [`es',\mkleeneopen{}es\mkleeneclose{}]  (BLemma  `State-class-top`)\mcdot{}  THEN  Auto))
                                              )
                                            THEN  Auto
                                            ))))

---

Home Index