---

Step * 1 of Lemma rinv_functionality


1. x : ℝ
2. y : ℝ
3. x = y
4. m : {1...}
5. ↑((λn.eval k = x n in 4 <z |k|) m)
6. a : ℕ+
7. mu-ge(λn.eval k = x n in 4 <z |k|;1) = a ∈ ℕ+
8. ↑eval k = x a in
    4 <z |k|
9. ∀[i:ℕ+a]. (¬↑eval k = x i in 4 <z |k|)
10. m1 : {1...}
11. ↑((λn.eval k = y n in 4 <z |k|) m1)
12. b : ℕ+
13. mu-ge(λn.eval k = y n in 4 <z |k|;1) = b ∈ ℕ+
14. ↑eval k = y b in
     4 <z |k|
15. ∀[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
{ (Thin (-3) THEN ThinVar `m1' THEN ThinVar `m' THEN Thin (-6)) }

1
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 )

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  x  =  y
4.  m  :  \{1...\}
5.  \muparrow{}((\mlambda{}n.eval  k  =  x  n  in  4  <z  |k|)  m)
6.  a  :  \mBbbN{}\msupplus{}
7.  mu-ge(\mlambda{}n.eval  k  =  x  n  in  4  <z  |k|;1)  =  a
8.  \muparrow{}eval  k  =  x  a  in
        4  <z  |k|
9.  \mforall{}[i:\mBbbN{}\msupplus{}a].  (\mneg{}\muparrow{}eval  k  =  x  i  in  4  <z  |k|)
10.  m1  :  \{1...\}
11.  \muparrow{}((\mlambda{}n.eval  k  =  y  n  in  4  <z  |k|)  m1)
12.  b  :  \mBbbN{}\msupplus{}
13.  mu-ge(\mlambda{}n.eval  k  =  y  n  in  4  <z  |k|;1)  =  b
14.  \muparrow{}eval  k  =  y  b  in
          4  <z  |k|
15.  \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:
(Thin  (-3)  THEN  ThinVar  `m1'  THEN  ThinVar  `m'  THEN  Thin  (-6))

---

Home Index