---

Step * 1 of Lemma rroot-abs_wf


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) ∈ ℕ+ ⟶ ℤ
BY
{ TACTIC:((MemCD THENA Auto)
          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 RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
          THEN Auto) }

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \mBbbR{}
3.  b  :  \mBbbN{}
4.  2\^{}(i  -  1)  =  b
\mvdash{}  \mlambda{}n.eval  k  =  n\^{}i  in
          eval  z  =  |x|  k  in
              iroot(i;b  *  z)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}


By

---

Latex:
TACTIC:((MemCD  THENA  Auto)
                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  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
                THEN  Auto)

---

Home Index