---

Step * 1 of Lemma int_upper_uwell_founded


1. n : ℤ
2. ∀[P:ℕ ⟶ ℙ]. ((∀[n:ℕ]. ((∀[m:ℕn]. P[m]) ⇒ P[n])) ⇒ (∀[n:ℕ]. P[n]))
3. [P] : {n...} ⟶ ℙ
4. ∀[j:{n...}]. ((∀[k:{k:{n...}| k < j} ]. P[k]) ⇒ P[j])
5. [n1] : {n...}
6. [n@0] : ℕ
7. ∀[m:ℕn@0]. P[n + m]
⊢ P[n + n@0]
BY
{ (BHyp 4 THEN Auto') }

1
1. n : ℤ
2. ∀[P:ℕ ⟶ ℙ]. ((∀[n:ℕ]. ((∀[m:ℕn]. P[m]) ⇒ P[n])) ⇒ (∀[n:ℕ]. P[n]))
3. [P] : {n...} ⟶ ℙ
4. ∀[j:{n...}]. ((∀[k:{k:{n...}| k < j} ]. P[k]) ⇒ P[j])
5. [n1] : {n...}
6. [n@0] : ℕ
7. ∀[m:ℕn@0]. P[n + m]
8. [k] : {k:{n...}| k < n + n@0} 
⊢ P[k]

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  \mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}[n:\mBbbN{}].  ((\mforall{}[m:\mBbbN{}n].  P[m])  {}\mRightarrow{}  P[n]))  {}\mRightarrow{}  (\mforall{}[n:\mBbbN{}].  P[n]))
3.  [P]  :  \{n...\}  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}[j:\{n...\}].  ((\mforall{}[k:\{k:\{n...\}|  k  <  j\}  ].  P[k])  {}\mRightarrow{}  P[j])
5.  [n1]  :  \{n...\}
6.  [n@0]  :  \mBbbN{}
7.  \mforall{}[m:\mBbbN{}n@0].  P[n  +  m]
\mvdash{}  P[n  +  n@0]


By

---

Latex:
(BHyp  4  THEN  Auto')

---

Home Index