{ 
[s:Atom List]. [n:
]. (str-to-nat-plus(s;n) 
) }
{ Proof }
Definitions occuring in Statement :
str-to-nat-plus: str-to-nat-plus(s;n),
nat: ,
uall: [x:A]. B[x],
member: t T,
list: type List,
atom: Atom
Definitions :
uall: [x:A]. B[x],
member: t T,
str-to-nat-plus: str-to-nat-plus(s;n),
nat:
Lemmas :
nat_wf,
str1-to-nat_wf
\mforall{}[s:Atom List]. \mforall{}[n:\mBbbN{}]. (str-to-nat-plus(s;n) \mmember{} \mBbbN{})
Date html generated:
2011_08_10-AM-07_42_33
Last ObjectModification:
2011_06_18-AM-08_09_41
Home
Index