---

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


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 ∈ ℕ)
4. n : ℕ
⊢ rec-case(v) of [] => λx.x | h::t => r.λx.(r (str1-to-nat(h) + (10 * x))) (str1-to-nat(u) + (10 * n)) ∈ ℕ
BY
{ (BHyp (-2) THEN Auto') }

---

Latex:

---

Latex:

1.  u  :  Atom
2.  v  :  Atom  List
3.  \mforall{}[n:\mBbbN{}]
          (rec-case(v)  of  []  =>  \mlambda{}x.x  |  fst::rest  =>  rec.\mlambda{}x.(rec  (str1-to-nat(fst)  +  (10  *  x)))  n  \mmember{}  \mBbbN{})
4.  n  :  \mBbbN{}
\mvdash{}  rec-case(v)  of
    []  =>  \mlambda{}x.x
    h::t  =>
      r.\mlambda{}x.(r  (str1-to-nat(h)  +  (10  *  x))) 
    (str1-to-nat(u)  +  (10  *  n))  \mmember{}  \mBbbN{}


By

---

Latex:
(BHyp  (-2)  THEN  Auto')

---

Home Index