---

Step * 1 1 of Lemma rinv_functionality


1. x : ℝ
2. y : ℝ
3. x = y
4. a : ℕ+
5. ↑eval k = x a in
    4 <z |k|
6. ∀[i:ℕ+a]. (¬↑eval k = x i in 4 <z |k|)
7. b : ℕ+
8. ↑eval k = y b in
    4 <z |k|
9. ∀[i:ℕ+b]. (¬↑eval k = y i in 4 <z |k|)
⊢ bdd-diff(eval n = a in
           if (n =z 1)
           then accelerate(5;reg-seq-inv(x))
           else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;x)))
           fi ;eval n = b in
               if (n =z 1)
               then accelerate(5;reg-seq-inv(y))
               else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;y)))
               fi )
BY
{ ((CallByValueReduce (-5)⋅ THENA Auto)
   THEN (RW assert_pushdownC (-5) THENA Auto)
   THEN InstLemma `rnonzero-lemma1` [⌜x⌝;⌜a⌝]⋅
   THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. x = y
4. a : ℕ+
5. 4 < |x a|
6. ∀[i:ℕ+a]. (¬↑eval k = x i in 4 <z |k|)
7. b : ℕ+
8. ↑eval k = y b in
    4 <z |k|
9. ∀[i:ℕ+b]. (¬↑eval k = y i in 4 <z |k|)
10. ∀m:ℕ+. ((a ≤ m) ⇒ (m ≤ (a * |x m|)))
⊢ bdd-diff(eval n = a in
           if (n =z 1)
           then accelerate(5;reg-seq-inv(x))
           else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;x)))
           fi ;eval n = b in
               if (n =z 1)
               then accelerate(5;reg-seq-inv(y))
               else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;y)))
               fi )

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  x  =  y
4.  a  :  \mBbbN{}\msupplus{}
5.  \muparrow{}eval  k  =  x  a  in
        4  <z  |k|
6.  \mforall{}[i:\mBbbN{}\msupplus{}a].  (\mneg{}\muparrow{}eval  k  =  x  i  in  4  <z  |k|)
7.  b  :  \mBbbN{}\msupplus{}
8.  \muparrow{}eval  k  =  y  b  in
        4  <z  |k|
9.  \mforall{}[i:\mBbbN{}\msupplus{}b].  (\mneg{}\muparrow{}eval  k  =  y  i  in  4  <z  |k|)
\mvdash{}  bdd-diff(eval  n  =  a  in
                      if  (n  =\msubz{}  1)
                      then  accelerate(5;reg-seq-inv(x))
                      else  accelerate(4  *  ((4  *  n  *  n)  +  1);reg-seq-inv(reg-seq-adjust(n;x)))
                      fi  ;eval  n  =  b  in
                              if  (n  =\msubz{}  1)
                              then  accelerate(5;reg-seq-inv(y))
                              else  accelerate(4  *  ((4  *  n  *  n)  +  1);reg-seq-inv(reg-seq-adjust(n;y)))
                              fi  )


By

---

Latex:
((CallByValueReduce  (-5)\mcdot{}  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-5)  THENA  Auto)
  THEN  InstLemma  `rnonzero-lemma1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index