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))}
 LMPO:
  Quasi-Precedence:
  sum > sqr
  empty
  
Normal:
   pi(sqr) = [1], pi(sum) = [1]
  
Safe:
   
  
Predicative System:
   {  sum(0();) -> 0(),
    sum(s(x;);) -> +(sqr(s(x;);),sum(x;);),
        sqr(x;) -> *(x,x;),
    sum(s(x;);) -> +(*(s(x;),s(x;);),sum(x;);)}
  

   
  

  Qed