---

Step * of Lemma accelerate-req

∀[k:ℕ+]. ∀[x:ℝ].  ((accelerate(k;x) ∈ ℝ) ∧ (accelerate(k;x) = x))
BY
{ (Auto
   THEN (Assert k-regular-seq(x) BY
               (DVar `x'
                THEN Unhide
                THEN Auto
                THEN RepeatFor 2 (ParallelOp 3)
                THEN ParallelLast
                THEN Auto
                THEN RWO "-1" 0
                THEN Auto
                THEN (Assert 1 ≤ k BY
                            Auto)
                THEN Mul ⌜n + m⌝ (-1)⋅
                THEN Auto))
   ) }

1
1. k : ℕ+
2. x : ℝ
3. accelerate(k;x) ∈ ℝ
4. k-regular-seq(x)
⊢ accelerate(k;x) = x

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbR{}].    ((accelerate(k;x)  \mmember{}  \mBbbR{})  \mwedge{}  (accelerate(k;x)  =  x))


By

---

Latex:
(Auto
  THEN  (Assert  k-regular-seq(x)  BY
                          (DVar  `x'
                            THEN  Unhide
                            THEN  Auto
                            THEN  RepeatFor  2  (ParallelOp  3)
                            THEN  ParallelLast
                            THEN  Auto
                            THEN  RWO  "-1"  0
                            THEN  Auto
                            THEN  (Assert  1  \mleq{}  k  BY
                                                    Auto)
                            THEN  Mul  \mkleeneopen{}n  +  m\mkleeneclose{}  (-1)\mcdot{}
                            THEN  Auto))
  )

---

Home Index