---

Step * 2 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 ∈ ℕ)
⊢ ∀[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
{ D 0 }

1
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)) ∈ ℕ

2
.....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

---

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{})
\mvdash{}  \mforall{}[n:\mBbbN{}]
        (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:
D  0

---

Home Index