---

Step * of Lemma rroot-odd-2-regular

No Annotations
∀i:{2...}. ∀x:ℝ.  2-regular-seq(rroot-odd(i;x))
BY
{ (Auto
   THEN (Assert regular-seq(λn.(rroot-abs(i;x) n)) BY
               (GenConclAtAddr [2;1;1] THEN D -2 THEN Unhide THEN Auto))
   THEN RepeatFor 3 (ParallelLast')
   THEN RepUR ``rroot-abs`` -1
   THEN RepUR ``rroot-odd`` 0
   THEN (Assert 2^i - 1 ~ 2^(i - 1) BY
               Auto)
   THEN HypSubst' (-1) 0
   THEN HypSubst' (-1) (-2)
   THEN Thin (-1)
   THEN (GenConcl ⌜2^(i - 1) = b ∈ ℕ⌝⋅ THENA Auto)
   THEN PromoteHyp (-2) 1
   THEN HypSubst' (-1) (-2)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (CallByValueReduce (-2) THENA Auto)
   THEN All Reduce
   THEN (All (RWO "exp-fastexp<") THENA Auto)) }

1
1. b : ℕ
2. i : {2...}
3. x : ℝ
4. n : ℕ+
5. m : ℕ+
6. |(m * eval k = n^i in eval z = |x| k in   iroot(i;b * z)) - n * eval k = m^i in eval z = |x| k in   iroot(i;b * z)| 
   ≤ (2 * (n + m))
7. 2^(i - 1) = b ∈ ℕ
⊢ |(m * eval k = n^i in eval z = x k in   if z <z 0 then -iroot(i;b * (-z)) else iroot(i;b * z) fi ) - n
  * eval k = m^i in
    eval z = x k in
      if z <z 0 then -iroot(i;b * (-z)) else iroot(i;b * z) fi | ≤ (4 * (n + m))

---

Latex:

---

Latex:
No  Annotations
\mforall{}i:\{2...\}.  \mforall{}x:\mBbbR{}.    2-regular-seq(rroot-odd(i;x))


By

---

Latex:
(Auto
  THEN  (Assert  regular-seq(\mlambda{}n.(rroot-abs(i;x)  n))  BY
                          (GenConclAtAddr  [2;1;1]  THEN  D  -2  THEN  Unhide  THEN  Auto))
  THEN  RepeatFor  3  (ParallelLast')
  THEN  RepUR  ``rroot-abs``  -1
  THEN  RepUR  ``rroot-odd``  0
  THEN  (Assert  2\^{}i  -  1  \msim{}  2\^{}(i  -  1)  BY
                          Auto)
  THEN  HypSubst'  (-1)  0
  THEN  HypSubst'  (-1)  (-2)
  THEN  Thin  (-1)
  THEN  (GenConcl  \mkleeneopen{}2\^{}(i  -  1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  PromoteHyp  (-2)  1
  THEN  HypSubst'  (-1)  (-2)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (CallByValueReduce  (-2)  THENA  Auto)
  THEN  All  Reduce
  THEN  (All  (RWO  "exp-fastexp<")  THENA  Auto))

---

Home Index