Step * 1 1 of Lemma int_upper_uwell_founded


1. : ℤ
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@0} 
⊢ P[k]
BY
(InstHyp [⌜n⌝(-2)⋅ 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.  [n@0]  :  \mBbbN{}
7.  \mforall{}[m:\mBbbN{}n@0].  P[n  +  m]
8.  [k]  :  \{k:\{n...\}|  k  <  n  +  n@0\} 
\mvdash{}  P[k]


By


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




Home Index