---

Step * 1 of Lemma int-int-retraction-reals-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 )) ∈ ℝ)
BY
{ (With ⌜λz.accelerate(k;regularize(1;z))⌝ (D 0)⋅ THEN Auto THEN Reduce 0 THEN EqCDA THEN EqTypeCD 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)
5. x : ℝ
⊢ x = regularize(1;λi.if i <z 1 then x 1 else x i fi ) ∈ (ℕ+ ⟶ ℤ)

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  \mforall{}x:\mBbbR{}.  (\mlambda{}i.if  i  <z  1  then  x  1  else  x  i  fi    \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})
3.  \mforall{}z:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  k-regular-seq(regularize(1;z))
4.  \mforall{}x:\mBbbR{}.  k-regular-seq(x)
\mvdash{}  \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:
(With  \mkleeneopen{}\mlambda{}z.accelerate(k;regularize(1;z))\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  EqCDA
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index