---

Step * 1 1 2 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 ∈ ℤ
⊢ (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||))
∈ ℤ
BY
{ ((RWO "-3" 0 THEN Auto) THEN GenConclTerms Auto [str-to-nat-plus(v;0);str-to-nat-plus(r;0);str1-to-nat(u)]⋅) }

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 ∈ ℤ
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||)) ∈ ℤ

---

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;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||))


By

---

Latex:
((RWO  "-3"  0  THEN  Auto)
  THEN  GenConclTerms  Auto  [str-to-nat-plus(v;0);str-to-nat-plus(r;0);str1-to-nat(u)]\mcdot{}
  )

---

Home Index