Step
*
2
1
1
1
2
2
of Lemma
search_succ
1. k : ℕ
2. P : ℕk + 1 ⟶ 𝔹
3. ¬↑(P 0)
4. 0 < search(k;λi.(P (i + 1)))
5. ↑(P search(k;λi.(P (i + 1))))
6. ∀j:ℕk. ¬↑(P (j + 1)) supposing j < search(k;λi.(P (i + 1))) - 1
7. 0 < search(k + 1;P)
8. ↑(P (search(k + 1;P) - 1))
9. ∀j:ℕk + 1. ¬↑(P j) supposing j < search(k + 1;P) - 1
10. 0 < search(k;λi.(P (i + 1)))
⊢ search(k + 1;P) = (search(k;λi.(P (i + 1))) + 1) ∈ ℤ
BY
{ ((((RepeatFor 7 (MoveToConcl (-1)) THEN GenConcl search(k;λi.(P (i + 1))) = x ∈ ℕk + 1) THENA Auto)
THEN GenConcl search(k + 1;P) = y ∈ ℕk + 2
)
THEN Auto'
) }
1
1. k : ℕ
2. P : ℕk + 1 ⟶ 𝔹
3. ¬↑(P 0)
4. x : ℕk + 1
5. search(k;λi.(P (i + 1))) = x ∈ ℕk + 1
6. y : ℕk + 2
7. search(k + 1;P) = y ∈ ℕk + 2
8. 0 < x
9. ↑(P x)
10. ∀j:ℕk. ¬↑(P (j + 1)) supposing j < x - 1
11. 0 < y
12. ↑(P (y - 1))
13. ∀j:ℕk + 1. ¬↑(P j) supposing j < y - 1
14. 0 < x
⊢ y = (x + 1) ∈ ℤ
Latex:
Latex:
1. k : \mBbbN{}
2. P : \mBbbN{}k + 1 {}\mrightarrow{} \mBbbB{}
3. \mneg{}\muparrow{}(P 0)
4. 0 < search(k;\mlambda{}i.(P (i + 1)))
5. \muparrow{}(P search(k;\mlambda{}i.(P (i + 1))))
6. \mforall{}j:\mBbbN{}k. \mneg{}\muparrow{}(P (j + 1)) supposing j < search(k;\mlambda{}i.(P (i + 1))) - 1
7. 0 < search(k + 1;P)
8. \muparrow{}(P (search(k + 1;P) - 1))
9. \mforall{}j:\mBbbN{}k + 1. \mneg{}\muparrow{}(P j) supposing j < search(k + 1;P) - 1
10. 0 < search(k;\mlambda{}i.(P (i + 1)))
\mvdash{} search(k + 1;P) = (search(k;\mlambda{}i.(P (i + 1))) + 1)
By
Latex:
((((RepeatFor 7 (MoveToConcl (-1)) THEN GenConcl search(k;\mlambda{}i.(P (i + 1))) = x) THENA Auto)
THEN GenConcl search(k + 1;P) = y
)
THEN Auto'
)
Home
Index