---

Step * 1 1 1 of Lemma Kripke2a


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))
8. a k < m
⊢ False
BY
{ (Assert  ⌜∀y:ℕk. a y < m⌝⋅
   THENA ((UnivCD THENA Auto)
          THEN (InstLemma `increasing-sequence-prop1` [⌜a⌝]⋅ THENA Auto)
          THEN InstHyp [⌜y⌝;⌜k⌝] (-1)⋅
          THEN Auto)
   ) }

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))
8. a k < m
9. ∀y:ℕk. a y < m
⊢ False

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  \mforall{}P:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  ((P  a)  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((a  =  g)  {}\mRightarrow{}  (P  g))))
3.  increasing-sequence(a)
4.  m  :  \mBbbN{}
5.  \mneg{}(\mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  ))
6.  k  :  \mBbbN{}
7.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((a  =  g)  {}\mRightarrow{}  ((\mlambda{}a.(\mneg{}(\mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  ))))  g))
8.  a  k  <  m
\mvdash{}  False


By

---

Latex:
(Assert    \mkleeneopen{}\mforall{}y:\mBbbN{}k.  a  y  <  m\mkleeneclose{}\mcdot{}
  THENA  ((UnivCD  THENA  Auto)
                THEN  (InstLemma  `increasing-sequence-prop1`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]  (-1)\mcdot{}
                THEN  Auto)
  )

---

Home Index