---

Step * 1 1 of Lemma co-regext-loopset


1. t : coW(Unit;x.Unit)@i
2. ∀[w:coW(Unit;x.set-dom((λp.loopset()) x))]. (regextfun(λp.loopset();w) ∈ coSet{i:l})
⊢ regextfun(λp.loopset();t) ∈ coSet{i:l}
BY
{ (BHyp -1
   THEN Reduce 0
   THEN Unfold `loopset` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN RepUR ``set-dom`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  t  :  coW(Unit;x.Unit)@i
2.  \mforall{}[w:coW(Unit;x.set-dom((\mlambda{}p.loopset())  x))].  (regextfun(\mlambda{}p.loopset();w)  \mmember{}  coSet\{i:l\})
\mvdash{}  regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\}


By

---

Latex:
(BHyp  -1
  THEN  Reduce  0
  THEN  Unfold  `loopset`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  RepUR  ``set-dom``  0
  THEN  Auto)

---

Home Index