TRS:
 { sum(0()) -> 0(),
  sum(s(x)) -> +(sqr(s(x)), sum(x)),
     sqr(x) -> *(x, x),
  sum(s(x)) -> +(*(s(x), s(x)), sum(x))}
 MPO:
  Prec:
   sqr > *, 
   sum > +, 
   sum > sqr, 
   sum > *
   empty
  Strict:
   {}
   Weak:
    {}
  Qed