---

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

∀[s:Atom List]. ∀[n:ℕ].  (str-to-nat-plus(s;n) = (str-to-nat(s) + (n * 10^||s||)) ∈ ℤ)
BY
{ (InductionOnList
   THEN RepUR ``str-to-nat-plus str-to-nat`` 0
   THEN Try (Fold `str-to-nat-plus` 0)
   THEN Auto
   THEN RWO "-2" 0
   THEN Auto'
   THEN RW IntNormC 0
   THEN Auto'
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[s:Atom  List].  \mforall{}[n:\mBbbN{}].    (str-to-nat-plus(s;n)  =  (str-to-nat(s)  +  (n  *  10\^{}||s||)))


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``str-to-nat-plus  str-to-nat``  0
  THEN  Try  (Fold  `str-to-nat-plus`  0)
  THEN  Auto
  THEN  RWO  "-2"  0
  THEN  Auto'
  THEN  RW  IntNormC  0
  THEN  Auto'
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index