---

Step * of Lemma rroot-abs_wf

∀i:{2...}. ∀x:ℝ.  (rroot-abs(i;x) ∈ ℝ)
BY
{ TACTIC:(Auto
          THEN Unfold `rroot-abs` 0
          THEN (RW (AddrC [2;1] (RevLemmaC `exp-fastexp`)) 0 THENA Auto)
          THEN (GenConcl ⌜2^(i - 1) = b ∈ ℕ⌝⋅ THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto)
          THEN MemTypeCD) }

1
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
⊢ λn.eval k = n^i in
     eval z = |x| k in
       iroot(i;b * z) ∈ ℕ+ ⟶ ℤ

2
.....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))

3
.....wf..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. f : ℕ+ ⟶ ℤ
⊢ istype(regular-seq(f))

---

Latex:

---

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\mBbbR{}.    (rroot-abs(i;x)  \mmember{}  \mBbbR{})


By

---

Latex:
TACTIC:(Auto
                THEN  Unfold  `rroot-abs`  0
                THEN  (RW  (AddrC  [2;1]  (RevLemmaC  `exp-fastexp`))  0  THENA  Auto)
                THEN  (GenConcl  \mkleeneopen{}2\^{}(i  -  1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  MemTypeCD)

---

Home Index