---

Step * of Lemma co-regext-loopset

No Annotations
seteq(co-regext(loopset());loopset())
BY
{ Assert ⌜∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})⌝⋅ }

1
.....assertion..... 
∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})

2
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
⊢ seteq(co-regext(loopset());loopset())

---

Latex:

---

Latex:
No  Annotations
seteq(co-regext(loopset());loopset())


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})\mkleeneclose{}\mcdot{}

---

Home Index