Step
*
1
of Lemma
int_upper_ind
1. i : ℤ
2. [E] : {i...} ⟶ ℙ{u}
3. E[i]
4. ∀k:{i + 1...}. (E[k - 1]
⇒ E[k])
⊢ ∀k:{i...}. E[k]
BY
{ (BackThruLemmaWithUnfolds `int_upper_well_founded` ``wellfounded`` THENA Auto) }
1
1. i : ℤ
2. [E] : {i...} ⟶ ℙ{u}
3. E[i]
4. ∀k:{i + 1...}. (E[k - 1]
⇒ E[k])
⊢ ∀j:{i...}. ((∀k:{i...}. (k < j
⇒ E[k]))
⇒ E[j])
Latex:
Latex:
1. i : \mBbbZ{}
2. [E] : \{i...\} {}\mrightarrow{} \mBbbP{}\{u\}
3. E[i]
4. \mforall{}k:\{i + 1...\}. (E[k - 1] {}\mRightarrow{} E[k])
\mvdash{} \mforall{}k:\{i...\}. E[k]
By
Latex:
(BackThruLemmaWithUnfolds `int\_upper\_well\_founded` ``wellfounded`` THENA Auto)
Home
Index