---

Step * of Lemma rec-combined-loc-class-opt-1-es-sv0

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:Id ─→ A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[init:Id ─→ bag(B)].
  (es-sv-class(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|)) supposing 
     (es-sv-class(es;X) and 
     (∀l:Id. (#(init l) ≤ 1)))
BY
{ ((UnivCD THENA MaAuto) THEN Unfold `rec-combined-loc-class-opt-1` 0) }

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

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[F:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    (es-sv-class(es;lifting-loc-2(F)|Loc,  X,  Prior(self)?init|))  supposing 
          (es-sv-class(es;X)  and 
          (\mforall{}l:Id.  (\#(init  l)  \mleq{}  1)))


By

---

Latex:
((UnivCD  THENA  MaAuto)  THEN  Unfold  `rec-combined-loc-class-opt-1`  0)

---

Home Index