---

Step * of Lemma div-search-lemma-ext

∀a:ℤ. ∀b:{a + 1...}. ∀f:ℤ ⟶ 𝔹.
  ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))] 
  supposing ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))]
BY
{ Extract of Obid: div-search-lemma
  not unfolding  divide
  finishing with Auto
  normalizes to:
  
  λa,b,f. (letrec g(a)=λb.if (b - a) < (2)
                             then a
                             else eval c = a + ((b - a) ÷ 2) in
                                  if f c then g a c else g c b fi  in
            g(a) 
           b) }

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a  +  1...\}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.
    \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))))] 
    supposing  \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:
Extract  of  Obid:  div-search-lemma
not  unfolding    divide
finishing  with  Auto
normalizes  to:

\mlambda{}a,b,f.  (letrec  g(a)=\mlambda{}b.if  (b  -  a)  <  (2)
                                                      then  a
                                                      else  eval  c  =  a  +  ((b  -  a)  \mdiv{}  2)  in
                                                                if  f  c  then  g  a  c  else  g  c  b  fi    in
                    g(a) 
                  b)

---

Home Index