---

Step * 1 1 1 1 1 of Lemma old-Kripke2a


1. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ.  ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))
2. a : ℕ ⟶ ℕ
3. increasing-sequence(a)
4. m : ℕ
5. ¬(∃n:ℕ. ((a n) ≥ m ))
6. k : ℕ
7. ∀g:ℕ ⟶ ℕ. ((a = g ∈ (ℕk ⟶ ℕ)) ⇒ (¬(∃n:ℕ. ((g n) ≥ m ))))
8. a k < m
9. ∀y:ℕk. a y < m
⊢ False
BY
{ ((InstHyp [⌜λx.if x ≤z k then a x else (a k) + (x - k) fi ⌝] (-3)⋅ THENA Auto) THEN AllReduce) }

1
1. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ.  ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))
2. a : ℕ ⟶ ℕ
3. increasing-sequence(a)
4. m : ℕ
5. ¬(∃n:ℕ. ((a n) ≥ m ))
6. k : ℕ
7. ∀g:ℕ ⟶ ℕ. ((a = g ∈ (ℕk ⟶ ℕ)) ⇒ (¬(∃n:ℕ. ((g n) ≥ m ))))
8. a k < m
9. ∀y:ℕk. a y < m
10. ¬(∃n:ℕ. (if n ≤z k then a n else (a k) + (n - k) fi  ≥ m ))
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}P:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((P  f)  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  =  g)  {}\mRightarrow{}  (P  g))))
2.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
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{}  (\mneg{}(\mexists{}n:\mBbbN{}.  ((g  n)  \mgeq{}  m  ))))
8.  a  k  <  m
9.  \mforall{}y:\mBbbN{}k.  a  y  <  m
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}x.if  x  \mleq{}z  k  then  a  x  else  (a  k)  +  (x  -  k)  fi  \mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  AllReduce)

---

Home Index