---

Step * of Lemma nat-to-str_wf

∀[n:ℕ]. (nat-to-str(n) ∈ Atom List)
BY
{ (CompleteInductionOnNat
   THEN D 1
   THEN RecUnfold `nat-to-str` 0⋅
   THEN (Decide ⌜n < 10⌝⋅ THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜n⌝;⌜10⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜n⌝;⌜10⌝]⋅ THENA Auto)
   THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (nat-to-str(n)  \mmember{}  Atom  List)


By

---

Latex:
(CompleteInductionOnNat
  THEN  D  1
  THEN  RecUnfold  `nat-to-str`  0\mcdot{}
  THEN  (Decide  \mkleeneopen{}n  <  10\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}10\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}10\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Auto)\mcdot{}

---

Home Index