---

Step * of Lemma rec-combined-class-opt-1-es-sv

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

1
1. Info : Type
2. A : Type
3. es : EO+(Info)
4. F : Top
5. X : EClass(A)
6. init : Id ─→ bag(Top)
7. ∀l:Id. (#(init l) ≤ 1)
8. es-sv-class(es;X)
⊢ es-sv-class(es;rec-comb(λn.[X][n];λi,w,s. (lifting-2(F) (w 0) s);init))

---

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;lifting-2(F)|X,Prior(self)?init|))  supposing 
          (es-sv-class(es;X)  and 
          (\mforall{}l:Id.  (\#(init  l)  \mleq{}  1)))


By

---

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

---

Home Index