---

Step * 1 1 of Lemma partial-void


1. z : partial(Void)@i
2. (z)↓@i
⊢ Void
BY
{ (UseWitness ⌜z⌝⋅ THEN BLemma `termination` THEN Auto) }

---

Latex:

---

Latex:

1.  z  :  partial(Void)@i
2.  (z)\mdownarrow{}@i
\mvdash{}  Void


By

---

Latex:
(UseWitness  \mkleeneopen{}z\mkleeneclose{}\mcdot{}  THEN  BLemma  `termination`  THEN  Auto)

---

Home Index