---

Step * of Lemma str-to-nat-to-str

∀[n:ℕ]. (str-to-nat(nat-to-str(n)) = n ∈ ℤ)
BY
{ ((CompleteInductionOnNat THENA Auto)
   THEN D 1
   THEN RecUnfold `nat-to-str` 0
   THEN RepeatFor 10 ((AutoSplit
                       THENL [((RepUR ``str-to-nat str-to-nat-plus`` 0 THEN Reduce 0)
                               THEN RepUR ``str1-to-nat`` 0
                               THEN Reduce 0
                               THEN Auto)
                             ; Id]
                      ))) }

1
1. n : ℤ
2. 10 ≤ n
3. ∀n:ℕn. (str-to-nat(nat-to-str(n)) = n ∈ ℤ)
⊢ str-to-nat(nat-to-str(n ÷ 10) @ nat-to-str(n rem 10)) = n ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (str-to-nat(nat-to-str(n))  =  n)


By

---

Latex:
((CompleteInductionOnNat  THENA  Auto)
  THEN  D  1
  THEN  RecUnfold  `nat-to-str`  0
  THEN  RepeatFor  10  ((AutoSplit
                                          THENL  [((RepUR  ``str-to-nat  str-to-nat-plus``  0  THEN  Reduce  0)
                                                          THEN  RepUR  ``str1-to-nat``  0
                                                          THEN  Reduce  0
                                                          THEN  Auto)
                                                      ;  Id]
                                        )))

---

Home Index