---

Step * of Lemma str-to-nat-plus_wf

∀[s:Atom List]. ∀[n:ℕ].  (str-to-nat-plus(s;n) ∈ ℕ)
BY
{ ((D 0 THENA Auto) THEN Unfold `str-to-nat-plus` 0 THEN ListInd 1 THEN Reduce 0)⋅ }

1
∀[n:ℕ]. (n ∈ ℕ)

2
1. u : Atom
2. v : Atom List
3. ∀[n:ℕ]. (rec-case(v) of [] => λx.x | fst::rest => rec.λx.(rec (str1-to-nat(fst) + (10 * x))) n ∈ ℕ)
⊢ ∀[n:ℕ]. (rec-case(v) of [] => λx.x | h::t => r.λx.(r (str1-to-nat(h) + (10 * x))) (str1-to-nat(u) + (10 * n)) ∈ ℕ)

---

Latex:

---

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


By

---

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

---

Home Index