---

Step * 1 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)
5. x : ℝ
⊢ x = regularize(1;λi.if i <z 1 then x 1 else x i fi ) ∈ (ℕ+ ⟶ ℤ)
BY
{ (Ext
   THEN Auto
   THEN Reduce 0
   THEN RepUR ``regularize`` 0
   THEN AutoSplit
   THEN D -1
   THEN DVar `x'
   THEN (Unhide THENA 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 : ℕ+ ⟶ ℤ
6. regular-seq(x)
7. x1 : ℕ+
⊢ ↑regular-upto(1;x1;λ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)
5.  x  :  \mBbbR{}
\mvdash{}  x  =  regularize(1;\mlambda{}i.if  i  <z  1  then  x  1  else  x  i  fi  )


By

---

Latex:
(Ext
  THEN  Auto
  THEN  Reduce  0
  THEN  RepUR  ``regularize``  0
  THEN  AutoSplit
  THEN  D  -1
  THEN  DVar  `x'
  THEN  (Unhide  THENA  Auto))

---

Home Index