---

Step * of Lemma fix-not-exception

∀[G,g:Base].  ¬is-exception(G fix(g)) supposing ∀j:ℕ. (¬is-exception(G (g^j ⊥)))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN Unfold `is-exception` -1
   THEN ExceptionCompactness (-1)
   THEN Unhide
   THEN Fold  `is-exception` (-1)
   THEN InstHyp [⌜j⌝] 3⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G,g:Base].    \mneg{}is-exception(G  fix(g))  supposing  \mforall{}j:\mBbbN{}.  (\mneg{}is-exception(G  (g\^{}j  \mbot{})))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `is-exception`  -1
  THEN  ExceptionCompactness  (-1)
  THEN  Unhide
  THEN  Fold    `is-exception`  (-1)
  THEN  InstHyp  [\mkleeneopen{}j\mkleeneclose{}]  3\mcdot{}
  THEN  Auto)

---

Home Index