---

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