---

Step * of Lemma nat-int-retraction-reals

∃r:(ℕ ⟶ ℤ) ⟶ ℝ. ∀x:ℝ. (x = (r (λn.(x (n + 1)))))
BY
{ ((Assert ∀x:ℝ. 2-regular-seq(x) BY
          (Auto THEN BLemma `real-regular` THEN Auto))
   THEN (InstLemma `nat-int-retraction-reals-1` [⌜2⌝]⋅ THENA Auto)
   THEN (ParallelLast THENA Auto)
   THEN RWO "-1<" 0
   THEN Auto
   THEN BLemma `req-iff-bdd-diff`
   THEN Auto
   THEN RWO "accelerate-bdd-diff" 0
   THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
((Assert  \mforall{}x:\mBbbR{}.  2-regular-seq(x)  BY
                (Auto  THEN  BLemma  `real-regular`  THEN  Auto))
  THEN  (InstLemma  `nat-int-retraction-reals-1`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ParallelLast  THENA  Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto
  THEN  BLemma  `req-iff-bdd-diff`
  THEN  Auto
  THEN  RWO  "accelerate-bdd-diff"  0
  THEN  EAuto  1)

---

Home Index