---

Step * 2 2 1 1 2 1 1 of Lemma binary-search_wf


1. d : ℤ
2. 0 < d
3. ∀a:ℤ. ∀b:{a + 1...}.
     (((b - a) ≤ (d - 1))
     ⇒ (∀f:{a..b + 1-} ⟶ 𝔹
           binary-search(f;a;b) ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))}  
           supposing ↓∃x:{a..b-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))))
4. a : ℤ
5. b : {a + 1...}
6. (b - a) ≤ d
7. f : {a..b + 1-} ⟶ 𝔹
8. x : {a..b-}
9. ∀y:{a..x + 1-}. (¬↑(f y))
10. ∀z:{x + 1..b + 1-}. (↑(f z))
11. ¬(b = (a + 1) ∈ ℤ)
12. v : ℤ
13. ¬↑(f (a + v))
14. ((b - a) ÷ 2) = v ∈ ℤ
15. 0 < v
16. v < b - a
⊢ ∃x:{a + v..b-}. ((∀y:{a + v..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))
BY
{ D 0 With ⌜x⌝  }

1
.....wf..... 
1. d : ℤ
2. 0 < d
3. ∀a:ℤ. ∀b:{a + 1...}.
     (((b - a) ≤ (d - 1))
     ⇒ (∀f:{a..b + 1-} ⟶ 𝔹
           binary-search(f;a;b) ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))}  
           supposing ↓∃x:{a..b-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))))
4. a : ℤ
5. b : {a + 1...}
6. (b - a) ≤ d
7. f : {a..b + 1-} ⟶ 𝔹
8. x : {a..b-}
9. ∀y:{a..x + 1-}. (¬↑(f y))
10. ∀z:{x + 1..b + 1-}. (↑(f z))
11. ¬(b = (a + 1) ∈ ℤ)
12. v : ℤ
13. ¬↑(f (a + v))
14. ((b - a) ÷ 2) = v ∈ ℤ
15. 0 < v
16. v < b - a
⊢ x ∈ {a + v..b-}

2
1. d : ℤ
2. 0 < d
3. ∀a:ℤ. ∀b:{a + 1...}.
     (((b - a) ≤ (d - 1))
     ⇒ (∀f:{a..b + 1-} ⟶ 𝔹
           binary-search(f;a;b) ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))}  
           supposing ↓∃x:{a..b-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))))
4. a : ℤ
5. b : {a + 1...}
6. (b - a) ≤ d
7. f : {a..b + 1-} ⟶ 𝔹
8. x : {a..b-}
9. ∀y:{a..x + 1-}. (¬↑(f y))
10. ∀z:{x + 1..b + 1-}. (↑(f z))
11. ¬(b = (a + 1) ∈ ℤ)
12. v : ℤ
13. ¬↑(f (a + v))
14. ((b - a) ÷ 2) = v ∈ ℤ
15. 0 < v
16. v < b - a
⊢ (∀y:{a + v..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z)))

3
.....wf..... 
1. d : ℤ
2. 0 < d
3. ∀a:ℤ. ∀b:{a + 1...}.
     (((b - a) ≤ (d - 1))
     ⇒ (∀f:{a..b + 1-} ⟶ 𝔹
           binary-search(f;a;b) ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))}  
           supposing ↓∃x:{a..b-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))))
4. a : ℤ
5. b : {a + 1...}
6. (b - a) ≤ d
7. f : {a..b + 1-} ⟶ 𝔹
8. x : {a..b-}
9. ∀y:{a..x + 1-}. (¬↑(f y))
10. ∀z:{x + 1..b + 1-}. (↑(f z))
11. ¬(b = (a + 1) ∈ ℤ)
12. v : ℤ
13. ¬↑(f (a + v))
14. ((b - a) ÷ 2) = v ∈ ℤ
15. 0 < v
16. v < b - a
17. x1 : {a + v..b-}
⊢ istype((∀y:{a + v..x1 + 1-}. (¬↑(f y))) ∧ (∀z:{x1 + 1..b + 1-}. (↑(f z))))

---

Latex:

---

Latex:

1.  d  :  \mBbbZ{}
2.  0  <  d
3.  \mforall{}a:\mBbbZ{}.  \mforall{}b:\{a  +  1...\}.
          (((b  -  a)  \mleq{}  (d  -  1))
          {}\mRightarrow{}  (\mforall{}f:\{a..b  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}
                      binary-search(f;a;b)  \mmember{}  \{x:\{a..b\msupminus{}\}|  (\mneg{}\muparrow{}(f  x))  \mwedge{}  (\muparrow{}(f  (x  +  1)))\}   
                      supposing  \mdownarrow{}\mexists{}x:\{a..b\msupminus{}\}.  ((\mforall{}y:\{a..x  +  1\msupminus{}\}.  (\mneg{}\muparrow{}(f  y)))  \mwedge{}  (\mforall{}z:\{x  +  1..b  +  1\msupminus{}\}.  (\muparrow{}(f  z))))))
4.  a  :  \mBbbZ{}
5.  b  :  \{a  +  1...\}
6.  (b  -  a)  \mleq{}  d
7.  f  :  \{a..b  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}
8.  x  :  \{a..b\msupminus{}\}
9.  \mforall{}y:\{a..x  +  1\msupminus{}\}.  (\mneg{}\muparrow{}(f  y))
10.  \mforall{}z:\{x  +  1..b  +  1\msupminus{}\}.  (\muparrow{}(f  z))
11.  \mneg{}(b  =  (a  +  1))
12.  v  :  \mBbbZ{}
13.  \mneg{}\muparrow{}(f  (a  +  v))
14.  ((b  -  a)  \mdiv{}  2)  =  v
15.  0  <  v
16.  v  <  b  -  a
\mvdash{}  \mexists{}x:\{a  +  v..b\msupminus{}\}.  ((\mforall{}y:\{a  +  v..x  +  1\msupminus{}\}.  (\mneg{}\muparrow{}(f  y)))  \mwedge{}  (\mforall{}z:\{x  +  1..b  +  1\msupminus{}\}.  (\muparrow{}(f  z))))


By

---

Latex:
D  0  With  \mkleeneopen{}x\mkleeneclose{} 

---

Home Index