---

Step * 2 1 2 2 1 of Lemma search_property


1. k : ℤ
2. 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))
4. P : ℕk ⟶ 𝔹
5. (∃i:ℕk - 1. (↑(P i))) ⇒ 0 < search(k - 1;P)
6. (∃i:ℕk - 1. (↑(P i))) ⇐ 0 < search(k - 1;P)
7. (↑(P (search(k - 1;P) - 1))) ∧ (∀j:ℕk - 1. ¬↑(P j) supposing j < search(k - 1;P) - 1) supposing 0 < search(k - 1;P)
8. ¬(∃i:ℕk - 1. (↑(P i)))
9. ¬0 < search(k - 1;P)
10. ¬↑(P (k - 1))
⊢ search(k;P) = 0 ∈ ℤ
BY
{ ((((Unfold `search` 0 THEN RWO "primrec-unroll" 0 THENA Auto) THEN Reduce 0) THEN Fold `search` 0)
   THEN Repeat (SplitOnConclITE THEN Auto')
   ) }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}P:\mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbB{}
          ((\mexists{}i:\mBbbN{}k  -  1.  (\muparrow{}(P  i))  \mLeftarrow{}{}\mRightarrow{}  0  <  search(k  -  1;P))
          \mwedge{}  (\muparrow{}(P  (search(k  -  1;P)  -  1)))  \mwedge{}  (\mforall{}j:\mBbbN{}k  -  1.  \mneg{}\muparrow{}(P  j)  supposing  j  <  search(k  -  1;P)  -  1) 
              supposing  0  <  search(k  -  1;P))
4.  P  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbB{}
5.  (\mexists{}i:\mBbbN{}k  -  1.  (\muparrow{}(P  i)))  {}\mRightarrow{}  0  <  search(k  -  1;P)
6.  (\mexists{}i:\mBbbN{}k  -  1.  (\muparrow{}(P  i)))  \mLeftarrow{}{}  0  <  search(k  -  1;P)
7.  (\muparrow{}(P  (search(k  -  1;P)  -  1)))  \mwedge{}  (\mforall{}j:\mBbbN{}k  -  1.  \mneg{}\muparrow{}(P  j)  supposing  j  <  search(k  -  1;P)  -  1) 
      supposing  0  <  search(k  -  1;P)
8.  \mneg{}(\mexists{}i:\mBbbN{}k  -  1.  (\muparrow{}(P  i)))
9.  \mneg{}0  <  search(k  -  1;P)
10.  \mneg{}\muparrow{}(P  (k  -  1))
\mvdash{}  search(k;P)  =  0


By

---

Latex:
((((Unfold  `search`  0  THEN  RWO  "primrec-unroll"  0  THENA  Auto)  THEN  Reduce  0)  THEN  Fold  `search`  0)
  THEN  Repeat  (SplitOnConclITE  THEN  Auto')
  )

---

Home Index