---

Step * 2 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:ℕ]. P[n + n@0]
⊢ P[n1]
BY
{ (InstHyp [⌜n1 - n⌝] (-1)⋅ THEN Auto') }

---

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.  \mforall{}[n@0:\mBbbN{}].  P[n  +  n@0]
\mvdash{}  P[n1]


By

---

Latex:
(InstHyp  [\mkleeneopen{}n1  -  n\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto')

---

Home Index