---

Step * 1 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 : ℕ+ ⟶ ℤ
6. regular-seq(x)
7. x1 : ℕ+
⊢ ↑regular-upto(1;x1;λi.if i <z 1 then x 1 else x i fi )
BY
{ (Unfold `regular-int-seq` -2 THEN (RWO "assert-regular-upto" 0 THEN Auto) THEN Reduce 0 THEN AutoSplit) }

---

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  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
6.  regular-seq(x)
7.  x1  :  \mBbbN{}\msupplus{}
\mvdash{}  \muparrow{}regular-upto(1;x1;\mlambda{}i.if  i  <z  1  then  x  1  else  x  i  fi  )


By

---

Latex:
(Unfold  `regular-int-seq`  -2
  THEN  (RWO  "assert-regular-upto"  0  THEN  Auto)
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index