---

{ [s:Atom List]. (str-to-nat(s)  ) }

{ Proof }

---

Definitions occuring in Statement :  str-to-nat: str-to-nat(s),  nat: ,  uall: [x:A]. B[x],  member: t  T,  list: type List,  atom: Atom
Definitions :  uall: [x:A]. B[x],  member: t  T,  nat: ,  str-to-nat: str-to-nat(s),  le: A  B,  not: A,  implies: P  Q,  false: False,  prop:
Lemmas :  str-to-nat-plus_wf,  le_wf

---

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


Date html generated: 2011_08_10-AM-07_42_36
Last ObjectModification: 2011_06_18-AM-08_09_43

Home Index