---

Step * of Lemma State-comb-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-comb(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))
BY
{ ((UnivCD THENA MaAuto)
   THEN RepUR ``State-comb rec-combined-class-opt-1`` 0
   THEN Using [`A',⌈λn.A⌉;`n',⌈1⌉] (BLemma `rec-comb-es-sv`)⋅
   THEN RepeatFor 2 ((Reduce 0 THEN Auto))
   THEN Try (Complete ((IntSegCases (-1) THEN Reduce 0 THEN Auto)))
   THEN (SplitOnConclITE THENA MaAuto)
   THEN Auto
   THEN RepUR ``lifting-2 lifting2 lifting-gen-rev`` 0
   THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 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)
10. bs : k:ℕ1 ─→ bag(A)@i
11. l : Id@i
12. b : bag(B)@i
13. ∀k:ℕ1. (#(bs k) ≤ 1)@i
14. #(b) ≤ 1@i
15. ¬((bs 0) = {} ∈ bag(A))
⊢ #(∪x∈bs 0.∪x@0∈b.{f x x@0}) ≤ 1

---

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-comb(init;f;X)))  supposing  ((\mforall{}l:Id.  (\#(init  l)  \mleq{}  1))  and  es-sv-class(es;X))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  RepUR  ``State-comb  rec-combined-class-opt-1``  0
  THEN  Using  [`A',\mkleeneopen{}\mlambda{}n.A\mkleeneclose{};`n',\mkleeneopen{}1\mkleeneclose{}]  (BLemma  `rec-comb-es-sv`)\mcdot{}
  THEN  RepeatFor  2  ((Reduce  0  THEN  Auto))
  THEN  Try  (Complete  ((IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto)))
  THEN  (SplitOnConclITE  THENA  MaAuto)
  THEN  Auto
  THEN  RepUR  ``lifting-2  lifting2  lifting-gen-rev``  0
  THEN  RepeatFor  3  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0)))

---

Home Index