---

Step * of Lemma fix-diverges

∀f:partial(Void) ⟶ partial(Void). (fix(f) ~ ⊥)
BY
{ (Auto
   THEN BLemma `partial-void`
   THEN InstLemma `fixpoint-induction-bottom` [⌜Void⌝;⌜partial(Void)⌝;⌜λ2x.x⌝;⌜f⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f:partial(Void)  {}\mrightarrow{}  partial(Void).  (fix(f)  \msim{}  \mbot{})


By

---

Latex:
(Auto
  THEN  BLemma  `partial-void`
  THEN  InstLemma  `fixpoint-induction-bottom`  [\mkleeneopen{}Void\mkleeneclose{};\mkleeneopen{}partial(Void)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index