---

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


1. q : Atom List
2. r : Atom List
⊢ (||r|| = 1 ∈ ℤ) ⇒ (str-to-nat(q @ r) = ((str-to-nat(q) * 10) + str-to-nat(r)) ∈ ℤ)
BY
{ (Unfold `str-to-nat` 0
   THEN MoveToConcl (-1)
   THEN ListInd 1
   THEN (Reduce 0 THEN Unfold `str-to-nat-plus` 0 THEN Reduce 0 THEN Fold `str-to-nat-plus` 0 THEN Auto)⋅) }

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;str1-to-nat(u) + 0) = ((str-to-nat-plus(v;str1-to-nat(u) + 0) * 10) + str-to-nat-plus(r;0)) ∈ ℤ

---

Latex:

---

Latex:

1.  q  :  Atom  List
2.  r  :  Atom  List
\mvdash{}  (||r||  =  1)  {}\mRightarrow{}  (str-to-nat(q  @  r)  =  ((str-to-nat(q)  *  10)  +  str-to-nat(r)))


By

---

Latex:
(Unfold  `str-to-nat`  0
  THEN  MoveToConcl  (-1)
  THEN  ListInd  1
  THEN  (Reduce  0
              THEN  Unfold  `str-to-nat-plus`  0
              THEN  Reduce  0
              THEN  Fold  `str-to-nat-plus`  0
              THEN  Auto)\mcdot{})

---

Home Index