---

Step * of Lemma Kripke2a

∀a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(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. increasing-sequence(a)
4. m : ℕ
5. ¬(∃n:ℕ. ((a n) ≥ m ))
⊢ False

---

Latex:

---

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


By

---

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

---

Home Index