---

Step * of Lemma divide-and-conquer-ext

∀[Q:a:ℤ ⟶ {a...} ⟶ ℙ]
  ∀s:{2...}
    ((∀a:ℤ. ∀b:{a..a + s-}.  Q[a;b])
    ⇒ (∀a,b,c:ℤ.  (Q[a;c] ⇒ Q[a;b]) ∨ (Q[c;b] ⇒ Q[a;b]) supposing a < c ∧ c < b)
    ⇒ (∀a:ℤ. ∀b:{a...}.  Q[a;b]))
BY
{ Extract of Obid: divide-and-conquer
  not unfolding  divide
  finishing with Auto
  normalizes to:
  
  λs,base,div,a,b. (letrec f(a)=λb.if (b - a) < (s)
                                      then base a b
                                      else eval c = a + ((b - a) ÷ s) in
                                           case div a b c
                                            of inl(lower) =>
                                            lower (f a c)
                                            | inr(upper) =>
                                            upper (f c b) in
                     f(a) 
                    b) }

---

Latex:

---

Latex:
\mforall{}[Q:a:\mBbbZ{}  {}\mrightarrow{}  \{a...\}  {}\mrightarrow{}  \mBbbP{}]
    \mforall{}s:\{2...\}
        ((\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a..a  +  s\msupminus{}\}.    Q[a;b])
        {}\mRightarrow{}  (\mforall{}a,b,c:\mBbbZ{}.    (Q[a;c]  {}\mRightarrow{}  Q[a;b])  \mvee{}  (Q[c;b]  {}\mRightarrow{}  Q[a;b])  supposing  a  <  c  \mwedge{}  c  <  b)
        {}\mRightarrow{}  (\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a...\}.    Q[a;b]))


By

---

Latex:
Extract  of  Obid:  divide-and-conquer
not  unfolding    divide
finishing  with  Auto
normalizes  to:

\mlambda{}s,base,div,a,b.  (letrec  f(a)=\mlambda{}b.if  (b  -  a)  <  (s)
                                                                        then  base  a  b
                                                                        else  eval  c  =  a  +  ((b  -  a)  \mdiv{}  s)  in
                                                                                  case  div  a  b  c
                                                                                    of  inl(lower)  =>
                                                                                    lower  (f  a  c)
                                                                                    |  inr(upper)  =>
                                                                                    upper  (f  c  b)  in
                                      f(a) 
                                    b)

---

Home Index