---

Step * of Lemma member-nat-to-str

∀n:ℕ. ∀s:Atom.  ((s ∈ nat-to-str(n)) ⇒ (s ∈ ``0 1 2 3 4 5 6 7 8 9``))
BY
{ (CompleteInductionOnNat
   THEN Auto
   THEN RecUnfold `nat-to-str` (-1)
   THEN RepeatFor 10 (((SplitOnHypITE -1  THENA Auto)
                       THENL [((RWW "member_singleton" (-2) THENA Auto) THEN HypSubst' (-2) 0 THEN Auto)
                             ; (PromoteHyp (-1) 2 THEN (CombineNequalWithLe⋅ THENA Auto))]
                      )⋅)) }

1
1. n : {10...}
2. ∀n:ℕn. ∀s:Atom.  ((s ∈ nat-to-str(n)) ⇒ (s ∈ ``0 1 2 3 4 5 6 7 8 9``))
3. s : Atom
4. (s ∈ nat-to-str(n ÷ 10) @ nat-to-str(n rem 10))
⊢ (s ∈ ``0 1 2 3 4 5 6 7 8 9``)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}s:Atom.    ((s  \mmember{}  nat-to-str(n))  {}\mRightarrow{}  (s  \mmember{}  ``0  1  2  3  4  5  6  7  8  9``))


By

---

Latex:
(CompleteInductionOnNat
  THEN  Auto
  THEN  RecUnfold  `nat-to-str`  (-1)
  THEN  RepeatFor  10  (((SplitOnHypITE  -1    THENA  Auto)
                                          THENL  [((RWW  "member\_singleton"  (-2)  THENA  Auto)
                                                          THEN  HypSubst'  (-2)  0
                                                          THEN  Auto)
                                                      ;  (PromoteHyp  (-1)  2  THEN  (CombineNequalWithLe\mcdot{}  THENA  Auto))]
                                        )\mcdot{}))

---

Home Index