---

Step * 2 1 1 1 of Lemma search_property


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))
4. P : ℕk ⟶ 𝔹
5. (∃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)
6. ∃i:ℕk - 1. (↑(P i))
7. ∃i:ℕk. (↑(P i))
⊢ (∃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
{ (((SimpHyp (-3) THEN ExRepD) THEN SimpHyp (-5)) THEN Subst' search(k;P) = search(k - 1;P) ∈ ℤ 0) }

1
.....equality..... 
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. 0 < search(k - 1;P)
6. (↑(P (search(k - 1;P) - 1))) ∧ (∀j:ℕk - 1. ¬↑(P j) supposing j < search(k - 1;P) - 1)
7. i1 : ℕk - 1
8. ↑(P i1)
9. i : ℕk
10. ↑(P i)
⊢ search(k;P) = search(k - 1;P) ∈ ℤ

2
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))
4. P : ℕk ⟶ 𝔹
5. 0 < search(k - 1;P)
6. (↑(P (search(k - 1;P) - 1))) ∧ (∀j:ℕk - 1. ¬↑(P j) supposing j < search(k - 1;P) - 1)
7. i1 : ℕk - 1
8. ↑(P i1)
9. i : ℕk
10. ↑(P i)
⊢ (∃i:ℕk. (↑(P i)) ⇐⇒ 0 < search(k - 1;P))
∧ (↑(P (search(k - 1;P) - 1))) ∧ (∀j:ℕk. ¬↑(P j) supposing j < search(k - 1;P) - 1) supposing 0 < search(k - 1;P)

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  [\%1]  :  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))  \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)
6.  \mexists{}i:\mBbbN{}k  -  1.  (\muparrow{}(P  i))
7.  \mexists{}i:\mBbbN{}k.  (\muparrow{}(P  i))
\mvdash{}  (\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:
(((SimpHyp  (-3)  THEN  ExRepD)  THEN  SimpHyp  (-5))  THEN  Subst'  search(k;P)  =  search(k  -  1;P)  0)

---

Home Index