Step
*
of Lemma
search_succ
∀[k:ℕ]. ∀[P:ℕk + 1 ⟶ 𝔹].
(search(k + 1;P) = if P 0 then 1 if 0 <z search(k;λi.(P (i + 1))) then search(k;λi.(P (i + 1))) + 1 else 0 fi ∈ ℤ)
BY
{ (Auto THEN (((InstLemma `search_property` [k + 1; P] THEN Auto) THEN SplitOnConclITE) THENA Auto)) }
1
.....truecase.....
1. k : ℕ
2. P : ℕk + 1 ⟶ 𝔹
3. (∃i:ℕk + 1. (↑(P i)))
⇒ 0 < search(k + 1;P)
4. (∃i:ℕk + 1. (↑(P i)))
⇐ 0 < search(k + 1;P)
5. (↑(P (search(k + 1;P) - 1))) ∧ (∀j:ℕk + 1. ¬↑(P j) supposing j < search(k + 1;P) - 1) supposing 0 < search(k + 1;P)
6. ↑(P 0)
⊢ search(k + 1;P) = 1 ∈ ℤ
2
.....falsecase.....
1. k : ℕ
2. P : ℕk + 1 ⟶ 𝔹
3. (∃i:ℕk + 1. (↑(P i)))
⇒ 0 < search(k + 1;P)
4. (∃i:ℕk + 1. (↑(P i)))
⇐ 0 < search(k + 1;P)
5. (↑(P (search(k + 1;P) - 1))) ∧ (∀j:ℕk + 1. ¬↑(P j) supposing j < search(k + 1;P) - 1) supposing 0 < search(k + 1;P)
6. ¬↑(P 0)
⊢ search(k + 1;P) = if 0 <z search(k;λi.(P (i + 1))) then search(k;λi.(P (i + 1))) + 1 else 0 fi ∈ ℤ
Latex:
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[P:\mBbbN{}k + 1 {}\mrightarrow{} \mBbbB{}].
(search(k + 1;P)
= if P 0 then 1
if 0 <z search(k;\mlambda{}i.(P (i + 1))) then search(k;\mlambda{}i.(P (i + 1))) + 1
else 0
fi )
By
Latex:
(Auto THEN (((InstLemma `search\_property` [k + 1; P] THEN Auto) THEN SplitOnConclITE) THENA Auto))
Home
Index