---

Step * of Lemma cover-seq-property-ext

∀[A,B:ℝ ⟶ ℙ].
  ∀d:r:ℝ ⟶ (A[r] + B[r]). ∀a,b:ℝ.
    (A[a]
    ⇒ B[b]
    ⇒ (∀n:ℕ
          (A[fst(cover-seq(d;a;b;n))]
          ∧ B[snd(cover-seq(d;a;b;n))]
          ∧ ((cover-seq(d;a;b;n + 1) = let a,b = cover-seq(d;a;b;n) in <a, (a + b/r(2))> ∈ (ℝ × ℝ))
            ∨ (cover-seq(d;a;b;n + 1) = let a,b = cover-seq(d;a;b;n) in <(a + b/r(2)), b> ∈ (ℝ × ℝ))))))
BY
{ Extract of Obid: cover-seq-property
  normalizes to:
  
  λd,a,b,Aa,Bb,n. primrec(n;if d (a + b/r(2)) then <Aa, Bb, inr Ax > else <Aa, Bb, inl Ax> fi ;
                          λi,x. let A,B,_ = x in 
                               <let v1,v2 = cover-seq(d;a;b;(i + 1) - 1) 
                                in case d (v1 + v2/r(2)) of inl(x) => x | inr(y) => A
                               , let v1,v2 = cover-seq(d;a;b;(i + 1) - 1) 
                                 in case d (v1 + v2/r(2)) of inl(x) => B | inr(y) => y
                               , let v1,v2 = cover-seq(d;a;b;i + 1) 
                                 in if d (v1 + v2/r(2)) then inr Ax  else inl Ax fi >)
  
  not unfolding  cover-seq primrec radd rdiv int-to-real
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}d:r:\mBbbR{}  {}\mrightarrow{}  (A[r]  +  B[r]).  \mforall{}a,b:\mBbbR{}.
        (A[a]
        {}\mRightarrow{}  B[b]
        {}\mRightarrow{}  (\mforall{}n:\mBbbN{}
                    (A[fst(cover-seq(d;a;b;n))]
                    \mwedge{}  B[snd(cover-seq(d;a;b;n))]
                    \mwedge{}  ((cover-seq(d;a;b;n  +  1)  =  let  a,b  =  cover-seq(d;a;b;n)  in  <a,  (a  +  b/r(2))>)
                        \mvee{}  (cover-seq(d;a;b;n  +  1)  =  let  a,b  =  cover-seq(d;a;b;n)  in  <(a  +  b/r(2)),  b>)))))


By

---

Latex:
Extract  of  Obid:  cover-seq-property
normalizes  to:

\mlambda{}d,a,b,Aa,Bb,n.  primrec(n;if  d  (a  +  b/r(2))  then  <Aa,  Bb,  inr  Ax  >  else  <Aa,  Bb,  inl  Ax>  fi  ;
                                                \mlambda{}i,x.  let  A,B,$_{}$  =  x  in 
                                                          <let  v1,v2  =  cover-seq(d;a;b;(i  +  1)  -  1) 
                                                            in  case  d  (v1  +  v2/r(2))  of  inl(x)  =>  x  |  inr(y)  =>  A
                                                          ,  let  v1,v2  =  cover-seq(d;a;b;(i  +  1)  -  1) 
                                                              in  case  d  (v1  +  v2/r(2))  of  inl(x)  =>  B  |  inr(y)  =>  y
                                                          ,  let  v1,v2  =  cover-seq(d;a;b;i  +  1) 
                                                              in  if  d  (v1  +  v2/r(2))  then  inr  Ax    else  inl  Ax  fi  >)

not  unfolding    cover-seq  primrec  radd  rdiv  int-to-real
finishing  with  Auto

---

Home Index