---

Step * of Lemma regext-loopset-empty

seteq(regext(loopset());{})
BY
{ (Assert regext(loopset()) ~ mk-coset(W(Unit;x.Unit);λw.regextfun(λp.loopset();w)) BY
         (RW (SubC (TagC (mk_tag_term 0))) 0 THEN Auto THEN Computation)) }

1
1. regext(loopset()) ~ mk-coset(W(Unit;x.Unit);λw.regextfun(λp.loopset();w))
⊢ seteq(regext(loopset());{})

---

Latex:

---

Latex:
seteq(regext(loopset());\{\})


By

---

Latex:
(Assert  regext(loopset())  \msim{}  mk-coset(W(Unit;x.Unit);\mlambda{}w.regextfun(\mlambda{}p.loopset();w))  BY
              (RW  (SubC  (TagC  (mk\_tag\_term  0)))  0  THEN  Auto  THEN  Computation))

---

Home Index