---

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

No Annotations
∀k:{2...}. ∃r:(ℤ ⟶ ℤ) ⟶ ℝ. ∀x:ℝ. (accelerate(k;x) = (r (λi.if i <z 1 then x 1 else x i fi )) ∈ ℝ)
BY
{ (Intro
   THEN (Assert ∀x:ℝ. (λi.if i <z 1 then x 1 else x i fi  ∈ ℤ ⟶ ℤ) BY
               Auto)
   THEN (Assert ⌜∀z:ℤ ⟶ ℤ. k-regular-seq(regularize(1;z))⌝ BY
               (Auto THEN InstLemma `regular-int-seq-weakening` [⌜1⌝;⌜k⌝;⌜regularize(1;z)⌝]⋅ THEN Auto))
   THEN (Assert ∀x:ℝ. k-regular-seq(x) BY
               (Auto THEN BLemma `real-regular` THEN Auto))) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\{2...\}.  \mexists{}r:(\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbR{}.  \mforall{}x:\mBbbR{}.  (accelerate(k;x)  =  (r  (\mlambda{}i.if  i  <z  1  then  x  1  else  x  i  fi  )))


By

---

Latex:
(Intro
  THEN  (Assert  \mforall{}x:\mBbbR{}.  (\mlambda{}i.if  i  <z  1  then  x  1  else  x  i  fi    \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})  BY
                          Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}z:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  k-regular-seq(regularize(1;z))\mkleeneclose{}  BY
                          (Auto
                            THEN  InstLemma  `regular-int-seq-weakening`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}regularize(1;z)\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  k-regular-seq(x)  BY
                          (Auto  THEN  BLemma  `real-regular`  THEN  Auto)))

---

Home Index