---

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

.....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 ∈ ℕ)
⊢ ℕ ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
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{})
\mvdash{}  \mBbbN{}  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index