---

Step * 1 1 1 of Lemma reals-uncountable


1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. f : ℕ ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))}  ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))} 
6. ∀n:ℕ. ∀p:{p:ℝ × ℝ| (fst(p)) < (snd(p))} .
     let x,y = p 
     in let x',y' = f n p 
        in (x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ (((z n) < x') ∨ (y' < (z n))) ∧ ((y' - x') < (r1/r(n + 1)))
7. ∀n:ℕ. (primrec(n;<x, y>;f) ∈ {p:ℝ × ℝ| (fst(p)) < (snd(p))} )
⊢ ∀n:ℕ
    (((fst(primrec(n;<x, y>;f))) ≤ (fst(primrec(n + 1;<x, y>;f))))
    ∧ ((fst(primrec(n + 1;<x, y>;f))) < (snd(primrec(n + 1;<x, y>;f))))
    ∧ ((snd(primrec(n + 1;<x, y>;f))) ≤ (snd(primrec(n;<x, y>;f))))
    ∧ (((z n) < (fst(primrec(n + 1;<x, y>;f)))) ∨ ((snd(primrec(n + 1;<x, y>;f))) < (z n)))
    ∧ (((snd(primrec(n + 1;<x, y>;f))) - fst(primrec(n + 1;<x, y>;f))) < (r1/r(n + 1))))
BY
{ ((D 0 THENA Auto)
   THEN (Subst' primrec(n + 1;<x, y>;f) ~ f n primrec(n;<x, y>;f) 0
         THENA (((RW (AddrC [1] (LemmaC `primrec-unroll`)) 0) THENA Auto)
                THEN ((SplitOnConclITE THENA Auto) THENL [Auto'; Subst' (n + 1) - 1 ~ n 0])
                THEN Auto)⋅
         )
   ) }

1
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. f : ℕ ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))}  ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))} 
6. ∀n:ℕ. ∀p:{p:ℝ × ℝ| (fst(p)) < (snd(p))} .
     let x,y = p 
     in let x',y' = f n p 
        in (x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ (((z n) < x') ∨ (y' < (z n))) ∧ ((y' - x') < (r1/r(n + 1)))
7. ∀n:ℕ. (primrec(n;<x, y>;f) ∈ {p:ℝ × ℝ| (fst(p)) < (snd(p))} )
8. n : ℕ
⊢ ((fst(primrec(n;<x, y>;f))) ≤ (fst((f n primrec(n;<x, y>;f)))))
∧ ((fst((f n primrec(n;<x, y>;f)))) < (snd((f n primrec(n;<x, y>;f)))))
∧ ((snd((f n primrec(n;<x, y>;f)))) ≤ (snd(primrec(n;<x, y>;f))))
∧ (((z n) < (fst((f n primrec(n;<x, y>;f))))) ∨ ((snd((f n primrec(n;<x, y>;f)))) < (z n)))
∧ (((snd((f n primrec(n;<x, y>;f)))) - fst((f n primrec(n;<x, y>;f)))) < (r1/r(n + 1)))

---

Latex:

---

Latex:

1.  z  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x  :  \mBbbR{}
3.  y  :  \mBbbR{}
4.  x  <  y
5.  f  :  \mBbbN{}  {}\mrightarrow{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}    {}\mrightarrow{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\} 
6.  \mforall{}n:\mBbbN{}.  \mforall{}p:\{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}  .
          let  x,y  =  p 
          in  let  x',y'  =  f  n  p 
                in  (x  \mleq{}  x')
                      \mwedge{}  (x'  <  y')
                      \mwedge{}  (y'  \mleq{}  y)
                      \mwedge{}  (((z  n)  <  x')  \mvee{}  (y'  <  (z  n)))
                      \mwedge{}  ((y'  -  x')  <  (r1/r(n  +  1)))
7.  \mforall{}n:\mBbbN{}.  (primrec(n;<x,  y>f)  \mmember{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}  )
\mvdash{}  \mforall{}n:\mBbbN{}
        (((fst(primrec(n;<x,  y>f)))  \mleq{}  (fst(primrec(n  +  1;<x,  y>f))))
        \mwedge{}  ((fst(primrec(n  +  1;<x,  y>f)))  <  (snd(primrec(n  +  1;<x,  y>f))))
        \mwedge{}  ((snd(primrec(n  +  1;<x,  y>f)))  \mleq{}  (snd(primrec(n;<x,  y>f))))
        \mwedge{}  (((z  n)  <  (fst(primrec(n  +  1;<x,  y>f))))  \mvee{}  ((snd(primrec(n  +  1;<x,  y>f)))  <  (z  n)))
        \mwedge{}  (((snd(primrec(n  +  1;<x,  y>f)))  -  fst(primrec(n  +  1;<x,  y>f)))  <  (r1/r(n  +  1))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Subst'  primrec(n  +  1;<x,  y>f)  \msim{}  f  n  primrec(n;<x,  y>f)  0
              THENA  (((RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0)  THENA  Auto)
                            THEN  ((SplitOnConclITE  THENA  Auto)  THENL  [Auto';  Subst'  (n  +  1)  -  1  \msim{}  n  0])
                            THEN  Auto)\mcdot{}
              )
  )

---

Home Index