---

Step * 1 of Lemma search_property

.....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))
BY
{ ((((Unfold `search` 0 THEN Reduce 0) THEN Auto) THEN ExRepD) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((((Unfold  `search`  0  THEN  Reduce  0)  THEN  Auto)  THEN  ExRepD)  THEN  Auto)

---

Home Index