---

Step * of Lemma closures-meet-sq'-ext

∀[P,Q:ℝ ⟶ ℙ].
  ((∃a:{a:ℝ| P a} . (∃b:ℝ [((Q b) ∧ (a < b))]))
  ⇒ (∃c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} 
       ∀a:{a:ℝ| P a} . ∀b:{b:ℝ| (Q b) ∧ (a < b)} .
         ∃a':{a':ℝ| P a'} . (∃b':{b':ℝ| (Q b') ∧ (a' < b')}  [((a ≤ a') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))]))
  ⇒ (∃y:ℝ. (y ∈ closure(λz.(↓P z)) ∧ y ∈ closure(λz.(↓Q z)))))
BY
{ Extract of Obid: closures-meet-sq'
  not unfolding  divide radd rsub rminus  primrec int-to-real absval rlessw rdiv rmul exp-ratio canonical-bound
  finishing with ((Subst' canonical-bound(λn.|r0 n|) ~ 2 0 THENA Computation)
                  THEN Unfold `let` 0
                  THEN Reduce 0
                  THEN Auto)
  normalizes to:
  
  λinit,hyp. let c,step = hyp 
             in let a,b = init 
                in let s = λn.primrec(n;<a, b>;λi,r. let a,a1 = r in let a',b' = step a a1 in <a', b'>) in
                    let d = canonical-bound(λn.|((λn.|(b - a) n|) + (r1/r1)) n|) in
                    <λn.eval m = 4 * n in
                        let x,y = primrec(eval x = rlessw(λn.|c n|;λk.(2 * k * 1)) in
                                          eval a = exp-ratio(|c x| + (2 * x * 1);4 * x;0;eval b = d in
                                                                                         if (b) < (2)
                                                                                            then 2 * 2 * m
                                                                                            else if (b) < (1)
                                                                                                    then 2 * 1 * m
                                                                                                    else (2 * b * m);1) \000Cin
                                            if (0) < (a)  then a  else 0;<a, b>;λi,r. let a,a1 = r in let a',b' = step a\000C a1 in <a', b'>) 
                        in (x m) ÷ 4
                    , <λn.(fst((s n)))
                      , λk.eval x = rlessw(λn.|c n|;λk.(2 * k * 1)) in
                           eval a = exp-ratio(|c x| + (2 * x * 1);4 * x;0;eval b = d in
                                                                          if (b) < (2)
                                                                             then 2 * 2 * 4 * k
                                                                             else if (b) < (1)
                                                                                     then 2 * 1 * 4 * k
                                                                                     else (2 * b * 4 * k);1) in
                             if (0) < (a)  then a + 1  else 1
                      , λn.let a,v1 = s n 
                           in Ax>
                    , λn.(snd((s n)))
                    , λk.eval x = rlessw(λn.|c n|;λk.(2 * k * 1)) in
                         eval x = exp-ratio(|c x| + (2 * x * 1);4 * x;0;eval b = d in
                                                                        if (b) < (2)
                                                                           then 2 * 2 * 2 * k
                                                                           else if (b) < (1)
                                                                                   then 2 * 1 * 2 * k
                                                                                   else (2 * b * 2 * k);1) in
                           if (0) < (x)
                              then eval x1 = rlessw(λn.|c n|;λk.(2 * k * 1)) in
                                   eval x1 = exp-ratio(|c x1| + (2 * x1 * 1);4 * x1;0;eval b = d in
                                                                                      if (b) < (2)
                                                                                         then 2 * 2 * 4 * 2 * k
                                                                                         else if (b) < (1)
                                                                                                 then 2 * 1 * 4 * 2 * k
                                                                                                 else (2
                                                                                                      * b
                                                                                                      * 4
                                                                                                      * 2
                                                                                                      * k);1) in
                                     if (0) < (x1)
                                        then eval b = x1 + 1 in
                                             if (b) < (x)  then x  else b
                                        else if (1) < (x)  then x  else 1
                              else eval x = rlessw(λn.|c n|;λk.(2 * k * 1)) in
                                   eval a = exp-ratio(|c x| + (2 * x * 1);4 * x;0;eval b = d in
                                                                                  if (b) < (2)
                                                                                     then 2 * 2 * 4 * 2 * k
                                                                                     else if (b) < (1)
                                                                                             then 2 * 1 * 4 * 2 * k
                                                                                             else (2 * b * 4 * 2 * k);1)\000C in
                                     if (0) < (a)  then eval b = a + 1 in if (b) < (0)  then 0  else b  else 1
                    , λn.let a,v1 = s n 
                         in Ax> }

---

Latex:

---

Latex:
\mforall{}[P,Q:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}a:\{a:\mBbbR{}|  P  a\}  .  (\mexists{}b:\mBbbR{}  [((Q  b)  \mwedge{}  (a  <  b))]))
    {}\mRightarrow{}  (\mexists{}c:\{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\} 
              \mforall{}a:\{a:\mBbbR{}|  P  a\}  .  \mforall{}b:\{b:\mBbbR{}|  (Q  b)  \mwedge{}  (a  <  b)\}  .
                  \mexists{}a':\{a':\mBbbR{}|  P  a'\}  .  (\mexists{}b':\{b':\mBbbR{}|  (Q  b')  \mwedge{}  (a'  <  b')\}    [((a  \mleq{}  a')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  ((b'  -  a')  \mleq{}  ((\000Cb  -  a)  *  c)))]))
    {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  (y  \mmember{}  closure(\mlambda{}z.(\mdownarrow{}P  z))  \mwedge{}  y  \mmember{}  closure(\mlambda{}z.(\mdownarrow{}Q  z)))))


By

---

Latex:
...

---

Home Index