---

Step * 1 of Lemma Kripke2a


1. a : ℕ ⟶ ℕ
2. is-absolutely-free{i:l}(a)
3. increasing-sequence(a)
4. m : ℕ
5. ¬(∃n:ℕ. ((a n) ≥ m ))
⊢ False
BY
{ (Unfold `is-absolutely-free` 2
   THEN (InstHyp [⌜λa.(¬(∃n:ℕ. ((a n) ≥ m )))⌝] 2⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN Fold `not` 0
   THEN (RWO "not-quotient-true" 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN ExRepD) }

1
1. a : ℕ ⟶ ℕ
2. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ((P a) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((a = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))
3. increasing-sequence(a)
4. m : ℕ
5. ¬(∃n:ℕ. ((a n) ≥ m ))
6. k : ℕ
7. ∀g:ℕ ⟶ ℕ. ((a = g ∈ (ℕk ⟶ ℕ)) ⇒ ((λa.(¬(∃n:ℕ. ((a n) ≥ m )))) g))
⊢ False

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  is-absolutely-free\{i:l\}(a)
3.  increasing-sequence(a)
4.  m  :  \mBbbN{}
5.  \mneg{}(\mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  ))
\mvdash{}  False


By

---

Latex:
(Unfold  `is-absolutely-free`  2
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}a.(\mneg{}(\mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  )))\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  Fold  `not`  0
  THEN  (RWO  "not-quotient-true"  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD)

---

Home Index