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