---

Step * of Lemma test_stuck_apply

∀[x,y,z:Top].  (<x, y> z ~ ⊥)
BY
{ RW (SweepUpC StuckApplyC) 0 }

1
∀[x,y,z:Top].  (⊥ ~ ⊥)

---

Latex:

---

Latex:
\mforall{}[x,y,z:Top].    (<x,  y>  z  \msim{}  \mbot{})


By

---

Latex:
RW  (SweepUpC  StuckApplyC)  0

---

Home Index