---

Step * of Lemma Kripke2b

∀a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ⇒ init0(a) ⇒ increasing-sequence(a) ⇒ (¬(∀m:ℕ. ∃n:ℕ. ((a n) ≥ m ))))
BY
{ ((UnivCD THENA Auto) THEN (D 0 THENA Auto)) }

1
1. a : ℕ ⟶ ℕ
2. is-absolutely-free{i:l}(a)
3. init0(a)
4. increasing-sequence(a)
5. ∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )
⊢ False

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
    (is-absolutely-free\{i:l\}(a)
    {}\mRightarrow{}  init0(a)
    {}\mRightarrow{}  increasing-sequence(a)
    {}\mRightarrow{}  (\mneg{}(\mforall{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  ))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index