---

Step * 1 1 2 1 1 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 ∈ ℤ
6. v1 : ℕ
7. str-to-nat-plus(v;0) = v1 ∈ ℕ
8. v2 : ℕ
9. str-to-nat-plus(r;0) = v2 ∈ ℕ
10. v3 : ℕ
11. str1-to-nat(u) = v3 ∈ ℕ
⊢ (((v1 * 10) + v2) + ((v3 + 0) * 10^||v|| + ||r||)) = (((v1 + ((v3 + 0) * 10^||v||)) * 10) + v2 + (0 * 10^||r||)) ∈ ℤ
BY
{ ((RW IntNormC 0 THENA Auto) THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
2:n
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 ∈ ℤ
6. v1 : ℕ
7. str-to-nat-plus(v;0) = v1 ∈ ℕ
8. v2 : ℕ
9. str-to-nat-plus(r;0) = v2 ∈ ℕ
10. v3 : ℕ
11. str1-to-nat(u) = v3 ∈ ℕ
⊢ (v3 * 10^||r|| + ||v||) = (10 * v3 * 10^||v||) ∈ ℤ

---

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
6.  v1  :  \mBbbN{}
7.  str-to-nat-plus(v;0)  =  v1
8.  v2  :  \mBbbN{}
9.  str-to-nat-plus(r;0)  =  v2
10.  v3  :  \mBbbN{}
11.  str1-to-nat(u)  =  v3
\mvdash{}  (((v1  *  10)  +  v2)  +  ((v3  +  0)  *  10\^{}||v||  +  ||r||))
=  (((v1  +  ((v3  +  0)  *  10\^{}||v||))  *  10)  +  v2  +  (0  *  10\^{}||r||))


By

---

Latex:
((RW  IntNormC  0  THENA  Auto)  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index