---

{ [s:Atom List]. [n:].
    (str-to-nat-plus(s;n) = (str-to-nat(s) + (n * 10^||s||))) }

{ Proof }

---

Definitions occuring in Statement :  str-to-nat: str-to-nat(s),  str-to-nat-plus: str-to-nat-plus(s;n),  length: ||as||,  nat: ,  uall: [x:A]. B[x],  list: type List,  multiply: n * m,  add: n + m,  natural_number: $n,  int: ,  atom: Atom,  equal: s = t,  exp: i^n
Definitions :  uall: [x:A]. B[x],  str-to-nat-plus: str-to-nat-plus(s;n),  str-to-nat: str-to-nat(s),  length: ||as||,  member: t  T,  ycomb: Y,  top: Top,  all: x:A. B[x],  subtype: S  T,  prop: ,  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  implies: P  Q,  nat: ,  le: A  B,  not: A,  false: False,  uimplies: b supposing a
Lemmas :  nat_wf,  str1-to-nat_wf,  str-to-nat-plus_wf,  exp_wf2,  length_wf1,  non_neg_length,  length_wf_nat,  top_wf,  str-to-nat_wf,  add_functionality_wrt_eq,  le_wf,  exp_add,  exp1

---

\mforall{}[s:Atom  List].  \mforall{}[n:\mBbbN{}].    (str-to-nat-plus(s;n)  =  (str-to-nat(s)  +  (n  *  10\^{}||s||)))


Date html generated: 2011_08_10-AM-07_42_40
Last ObjectModification: 2011_06_18-AM-08_09_44

Home Index