Step * 2 2 of Lemma binary-search_wf


1. : ℤ
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. : ℤ
5. {a 1...}
6. (b a) ≤ d
7. {a..b 1-} ⟶ 𝔹
8. ↓∃x:{a..b-}. ((∀y:{a..x 1-}. (¬↑(f y))) ∧ (∀z:{x 1..b 1-}. (↑(f z))))
9. ¬(b (a 1) ∈ ℤ)
10. 0 < (b a) ÷ 2 ∧ (b a) ÷ 2 < a
⊢ eval ((b a) ÷ 2) in
  if then binary-search(f;a;c) else binary-search(f;c;b) fi  ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x 1)))} 
BY
TACTIC:(MoveToConcl (-1) THEN (GenConclTerm ⌜(b a) ÷ 2⌝⋅ THENA Auto) THEN (D THENA Auto)) }

1
1. : ℤ
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. : ℤ
5. {a 1...}
6. (b a) ≤ d
7. {a..b 1-} ⟶ 𝔹
8. ↓∃x:{a..b-}. ((∀y:{a..x 1-}. (¬↑(f y))) ∧ (∀z:{x 1..b 1-}. (↑(f z))))
9. ¬(b (a 1) ∈ ℤ)
10. : ℤ
11. ((b a) ÷ 2) v ∈ ℤ
12. 0 < v ∧ v < a
⊢ eval in
  if then binary-search(f;a;c) else binary-search(f;c;b) fi  ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x 1)))} 


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.  \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))))
9.  \mneg{}(b  =  (a  +  1))
10.  0  <  (b  -  a)  \mdiv{}  2  \mwedge{}  (b  -  a)  \mdiv{}  2  <  b  -  a
\mvdash{}  eval  c  =  a  +  ((b  -  a)  \mdiv{}  2)  in
    if  f  c  then  binary-search(f;a;c)  else  binary-search(f;c;b)  fi    \mmember{}  \{x:\{a..b\msupminus{}\}| 
                                                                                                                                        (\mneg{}\muparrow{}(f  x))  \mwedge{}  (\muparrow{}(f  (x  +  1)))\} 


By


Latex:
TACTIC:(MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}(b  -  a)  \mdiv{}  2\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (D  0  THENA  Auto))




Home Index