---

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


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``)
BY
{ (((RWO "member_append" (-1) THENM D -1) THENA Auto)
   THEN FHyp 2 [-1]
   THEN Auto
   THEN (InstLemma `rem_bounds_1` [⌜n⌝;⌜10⌝]⋅ THENA Auto)
   THEN InstLemma `div_rem_sum` [⌜n⌝;⌜10⌝]⋅
   THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
(((RWO  "member\_append"  (-1)  THENM  D  -1)  THENA  Auto)
  THEN  FHyp  2  [-1]
  THEN  Auto
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}10\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `div\_rem\_sum`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}10\mkleeneclose{}]\mcdot{}
  THEN  Auto')

---

Home Index