---

Step * 2 2 1 1 of Lemma co-regext-loopset

.....assertion..... 
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) = loopset() ∈ coSet{i:l})
3. co-regext(loopset()) ~ mk-coset(coW(Unit;x.Unit);λw.regextfun(λp.loopset();w))
4. z : coSet{i:l}@i'
5. seteq(z;loopset())
⊢ coW(Unit;x.Unit)
BY
{ UseWitness ⌜fix((λx.<⋅, λu.x>))⌝ THEN (InstLemma `fix_wf_corec` [⌜parm{i'}⌝;⌜λ2W.T:Unit × (Unit ⟶ W)⌝;⌜λx.<⋅, λu.x>⌝]
                                         ⋅
                                         THEN Auto
                                         )⋅ }

---

Latex:

---

Latex:
.....assertion..... 
1.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})
2.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  =  loopset())
3.  co-regext(loopset())  \msim{}  mk-coset(coW(Unit;x.Unit);\mlambda{}w.regextfun(\mlambda{}p.loopset();w))
4.  z  :  coSet\{i:l\}@i'
5.  seteq(z;loopset())
\mvdash{}  coW(Unit;x.Unit)


By

---

Latex:
UseWitness  \mkleeneopen{}fix((\mlambda{}x.<\mcdot{},  \mlambda{}u.x>))\mkleeneclose{}  THEN 
(InstLemma  `fix\_wf\_corec`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}W.T:Unit  \mtimes{}  (Unit  {}\mrightarrow{}  W)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.<\mcdot{},  \mlambda{}u.x>\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index