Step
*
2
1
1
1
of Lemma
def-cont-induction-lemma
1. P : ℕ ⟶ ℙ
2. ∀n:ℕ. (P[n]
⇒ P[n + 1])
3. l : ℤ
4. q : ℤ List
5. ∀[n,m:ℕ]. P[n]
⇒ P[m] supposing (q = [n, m) ∈ (ℤ List)) ∧ (n ≤ m)
6. n : ℕ
7. m : ℕ
8. [l / q] = [n, m) ∈ (ℤ List)
9. n ≤ m
10. P[n]
⊢ (q = [n + 1, m) ∈ (ℤ List)) ∧ (l = n ∈ ℤ)
BY
{ (RecUnfold `from-upto` (-3)⋅
THEN (SplitOnHypITE -3 THEN Auto')
THEN OnMaybeHyp 9 (\h. ((CallByValueReduce h THENA Auto) THEN RWO "cons_one_one" h THEN Auto)))⋅ }
Latex:
Latex:
1. P : \mBbbN{} {}\mrightarrow{} \mBbbP{}
2. \mforall{}n:\mBbbN{}. (P[n] {}\mRightarrow{} P[n + 1])
3. l : \mBbbZ{}
4. q : \mBbbZ{} List
5. \mforall{}[n,m:\mBbbN{}]. P[n] {}\mRightarrow{} P[m] supposing (q = [n, m)) \mwedge{} (n \mleq{} m)
6. n : \mBbbN{}
7. m : \mBbbN{}
8. [l / q] = [n, m)
9. n \mleq{} m
10. P[n]
\mvdash{} (q = [n + 1, m)) \mwedge{} (l = n)
By
Latex:
(RecUnfold `from-upto` (-3)\mcdot{}
THEN (SplitOnHypITE -3 THEN Auto')
THEN OnMaybeHyp 9 (\mbackslash{}h. ((CallByValueReduce h THENA Auto) THEN RWO "cons\_one\_one" h THEN Auto)))\mcdot{}
Home
Index