---

Step * of Lemma binary-search_wf

∀a:ℤ. ∀b:{a + 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))))
BY
{ ((Assert ⌜∀d:ℕ. ∀a:ℤ. ∀b:{a + 1...}.
              (((b - a) ≤ d)
              ⇒ (∀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))))))⌝⋅
   THENM ((UnivCD THENA Auto) THEN InstHyp [⌜b - a⌝;⌜a⌝;⌜b⌝;⌜f⌝] 1⋅ THEN Auto)
   )
   THEN InductionOnNat
   THEN (UnivCD THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN CompleteAuto))
   THEN RecUnfold `binary-search` 0
   THEN ( Decide ⌜b = (a + 1) ∈ ℤ⌝⋅ THENA Auto)
   THEN Reduce 0) }

1
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-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))
9. b = (a + 1) ∈ ℤ
⊢ a ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))} 

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-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))
9. ¬(b = (a + 1) ∈ ℤ)
⊢ eval c = a + ((b - a) ÷ 2) in
  if f c then binary-search(f;a;c) else binary-search(f;c;b) fi  ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))} 

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a  +  1...\}.  \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))))


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}a:\mBbbZ{}.  \mforall{}b:\{a  +  1...\}.
                        (((b  -  a)  \mleq{}  d)
                        {}\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))))))\mkleeneclose{}\mcdot{}
  THENM  ((UnivCD  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}b  -  a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  CompleteAuto))
  THEN  RecUnfold  `binary-search`  0
  THEN  (  Decide  \mkleeneopen{}b  =  (a  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Reduce  0)

---

Home Index