---

Step * of Lemma nat-int-retraction-reals-1

∀k:{2...}. ∃r:(ℕ ⟶ ℤ) ⟶ ℝ. ∀x:ℝ. (accelerate(k;x) = (r (λn.(x (n + 1)))) ∈ ℝ)
BY
{ (InstLemma `int-int-retraction-reals-1` []
   THEN (ParallelLast' THEN ExRepD)
   THEN (Assert ∀x:ℝ. k-regular-seq(x) BY
               (Auto THEN BLemma `real-regular` THEN Auto))
   THEN (D 0 With ⌜λf.(r (λi.if i <z 1 then f 0 else f (i - 1) fi ))⌝  THEN Auto)
   THEN Reduce 0) }

1
1. k : {2...}
2. r : (ℤ ⟶ ℤ) ⟶ ℝ
3. ∀x:ℝ. (accelerate(k;x) = (r (λi.if i <z 1 then x 1 else x i fi )) ∈ ℝ)
4. ∀x:ℝ. k-regular-seq(x)
5. x : ℝ
⊢ accelerate(k;x) = (r (λi.if i <z 1 then x 1 else x ((i - 1) + 1) fi )) ∈ ℝ

---

Latex:

---

Latex:
\mforall{}k:\{2...\}.  \mexists{}r:(\mBbbN{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbR{}.  \mforall{}x:\mBbbR{}.  (accelerate(k;x)  =  (r  (\mlambda{}n.(x  (n  +  1)))))


By

---

Latex:
(InstLemma  `int-int-retraction-reals-1`  []
  THEN  (ParallelLast'  THEN  ExRepD)
  THEN  (Assert  \mforall{}x:\mBbbR{}.  k-regular-seq(x)  BY
                          (Auto  THEN  BLemma  `real-regular`  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}f.(r  (\mlambda{}i.if  i  <z  1  then  f  0  else  f  (i  -  1)  fi  ))\mkleeneclose{}    THEN  Auto)
  THEN  Reduce  0)

---

Home Index