---

Step * 2 of Lemma rroot-abs_wf

.....set predicate..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
⊢ regular-seq(λn.eval k = n^i in
                 eval z = |x| k in
                   iroot(i;b * z))
BY
{ TACTIC:(RepeatFor 2 (((D 0 THENA Auto) THEN Reduce 0))
          THEN (GenConcl ⌜n^i = k ∈ ℕ+⌝⋅
                THENA (Auto
                       THEN (InstLemma `exp_preserves_lt` [⌜i⌝;⌜0⌝;⌜n⌝]⋅ THENA Auto)
                       THEN RWO "exp-zero" (-1)
                       THEN Auto)
                )
          THEN (GenConcl ⌜m^i = j ∈ ℕ+⌝⋅
                THENA (Auto
                       THEN (InstLemma `exp_preserves_lt` [⌜i⌝;⌜0⌝;⌜m⌝]⋅ THENA Auto)
                       THEN RWO "exp-zero" (-1)
                       THEN Auto)
                )
          THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
⊢ |(m * iroot(i;b * (|x| k))) - n * iroot(i;b * (|x| j))| ≤ (2 * (n + m))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  i  :  \{2...\}
2.  x  :  \mBbbR{}
3.  b  :  \mBbbN{}
4.  2\^{}(i  -  1)  =  b
\mvdash{}  regular-seq(\mlambda{}n.eval  k  =  n\^{}i  in
                                  eval  z  =  |x|  k  in
                                      iroot(i;b  *  z))


By

---

Latex:
TACTIC:(RepeatFor  2  (((D  0  THENA  Auto)  THEN  Reduce  0))
                THEN  (GenConcl  \mkleeneopen{}n\^{}i  =  k\mkleeneclose{}\mcdot{}
                            THENA  (Auto
                                          THEN  (InstLemma  `exp\_preserves\_lt`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                          THEN  RWO  "exp-zero"  (-1)
                                          THEN  Auto)
                            )
                THEN  (GenConcl  \mkleeneopen{}m\^{}i  =  j\mkleeneclose{}\mcdot{}
                            THENA  (Auto
                                          THEN  (InstLemma  `exp\_preserves\_lt`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                          THEN  RWO  "exp-zero"  (-1)
                                          THEN  Auto)
                            )
                THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index