---

Step * of Lemma search_property

∀k:ℕ. ∀P:ℕk ⟶ 𝔹.
  ((∃i:ℕk. (↑(P i)) ⇐⇒ 0 < search(k;P))
  ∧ (↑(P (search(k;P) - 1))) ∧ (∀j:ℕk. ¬↑(P j) supposing j < search(k;P) - 1) supposing 0 < search(k;P))
BY
{ ((D 0 THENA Auto) THEN NatInd 1) }

1
.....basecase..... 
∀P:ℕ0 ⟶ 𝔹
  ((∃i:ℕ0. (↑(P i)) ⇐⇒ 0 < search(0;P))
  ∧ (↑(P (search(0;P) - 1))) ∧ (∀j:ℕ0. ¬↑(P j) supposing j < search(0;P) - 1) supposing 0 < search(0;P))

2
.....upcase..... 
1. k : ℤ
2. [%1] : 0 < k
3. ∀P:ℕk - 1 ⟶ 𝔹
     ((∃i:ℕk - 1. (↑(P i)) ⇐⇒ 0 < search(k - 1;P))
     ∧ (↑(P (search(k - 1;P) - 1))) ∧ (∀j:ℕk - 1. ¬↑(P j) supposing j < search(k - 1;P) - 1) 
       supposing 0 < search(k - 1;P))
⊢ ∀P:ℕk ⟶ 𝔹
    ((∃i:ℕk. (↑(P i)) ⇐⇒ 0 < search(k;P))
    ∧ (↑(P (search(k;P) - 1))) ∧ (∀j:ℕk. ¬↑(P j) supposing j < search(k;P) - 1) supposing 0 < search(k;P))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}P:\mBbbN{}k  {}\mrightarrow{}  \mBbbB{}.
    ((\mexists{}i:\mBbbN{}k.  (\muparrow{}(P  i))  \mLeftarrow{}{}\mRightarrow{}  0  <  search(k;P))
    \mwedge{}  (\muparrow{}(P  (search(k;P)  -  1)))  \mwedge{}  (\mforall{}j:\mBbbN{}k.  \mneg{}\muparrow{}(P  j)  supposing  j  <  search(k;P)  -  1) 
        supposing  0  <  search(k;P))


By

---

Latex:
((D  0  THENA  Auto)  THEN  NatInd  1)

---

Home Index