---

Step * of Lemma Accum-class-es-sv

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)]. ∀[f:Top].
  (es-sv-class(es;Accum-class(f;init;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))
BY
{ ((UnivCD
    THENA (Auto
           THEN RepUR ``Accum-class rec-combined-class-opt-1 lifting-2`` 0
           THEN RepUR ``lifting2 lifting-loc-gen-rev lifting-gen-rev`` 0
           THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` 0 THEN Reduce 0))
           THEN Try (Fold `eclass` 0)
           THEN Using [`n',⌜1⌝;`A',⌜λx.Top⌝] (BLemma `rec-comb_wf`)⋅
           THEN MaAuto)
    )
   THEN Unfold `Accum-class` 0
   THEN ProveEsSvClass) }

---

Latex:

---

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


By

---

Latex:
((UnivCD
    THENA  (Auto
                  THEN  RepUR  ``Accum-class  rec-combined-class-opt-1  lifting-2``  0
                  THEN  RepUR  ``lifting2  lifting-loc-gen-rev  lifting-gen-rev``  0
                  THEN  RepeatFor  3  ((RecUnfold  `lifting-gen-list-rev`  0  THEN  Reduce  0))
                  THEN  Try  (Fold  `eclass`  0)
                  THEN  Using  [`n',\mkleeneopen{}1\mkleeneclose{};`A',\mkleeneopen{}\mlambda{}x.Top\mkleeneclose{}]  (BLemma  `rec-comb\_wf`)\mcdot{}
                  THEN  MaAuto)
    )
  THEN  Unfold  `Accum-class`  0
  THEN  ProveEsSvClass)

---

Home Index