---

Step * of Lemma State-comb-es-sv

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (es-sv-class(es;State-comb(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))
BY
{ (UnivCD THENA (Auto THEN Try (Fold `eclass` 0) THEN Using [`es',⌜es⌝] (BLemma `State-comb-top`)⋅ 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-comb(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-comb(init;f;X)))  supposing  ((\mforall{}l:Id.  (\#(init  l)  \mleq{}  1))  and  es-sv-class(es;X))


By

---

Latex:
(UnivCD
  THENA  (Auto  THEN  Try  (Fold  `eclass`  0)  THEN  Using  [`es',\mkleeneopen{}es\mkleeneclose{}]  (BLemma  `State-comb-top`)\mcdot{}  THEN  Auto)
  )

---

Home Index