---

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


1. u : Atom
2. v : Atom List
3. ∀r:Atom List
     ((||r|| = 1 ∈ ℤ) ⇒ (str-to-nat-plus(v @ r;0) = ((str-to-nat-plus(v;0) * 10) + str-to-nat-plus(r;0)) ∈ ℤ))
4. r : Atom List
5. ||r|| = 1 ∈ ℤ
⊢ str-to-nat-plus(v @ r;str1-to-nat(u) + 0) = ((str-to-nat-plus(v;str1-to-nat(u) + 0) * 10) + str-to-nat-plus(r;0)) ∈ ℤ
BY
{ (RWO "str-to-nat-plus-property" 0 THEN Auto' THEN Unfold `str-to-nat` 0) }

1
1. u : Atom
2. v : Atom List
3. ∀r:Atom List
     ((||r|| = 1 ∈ ℤ) ⇒ (str-to-nat-plus(v @ r;0) = ((str-to-nat-plus(v;0) * 10) + str-to-nat-plus(r;0)) ∈ ℤ))
4. r : Atom List
5. ||r|| = 1 ∈ ℤ
⊢ (str-to-nat-plus(v @ r;0) + ((str1-to-nat(u) + 0) * 10^||v|| + ||r||))
= (((str-to-nat-plus(v;0) + ((str1-to-nat(u) + 0) * 10^||v||)) * 10) + str-to-nat-plus(r;0) + (0 * 10^||r||))
∈ ℤ

---

Latex:

---

Latex:

1.  u  :  Atom
2.  v  :  Atom  List
3.  \mforall{}r:Atom  List
          ((||r||  =  1)
          {}\mRightarrow{}  (str-to-nat-plus(v  @  r;0)  =  ((str-to-nat-plus(v;0)  *  10)  +  str-to-nat-plus(r;0))))
4.  r  :  Atom  List
5.  ||r||  =  1
\mvdash{}  str-to-nat-plus(v  @  r;str1-to-nat(u)  +  0)
=  ((str-to-nat-plus(v;str1-to-nat(u)  +  0)  *  10)  +  str-to-nat-plus(r;0))


By

---

Latex:
(RWO  "str-to-nat-plus-property"  0  THEN  Auto'  THEN  Unfold  `str-to-nat`  0)

---

Home Index