TRS:
 {    sqr(0()) -> 0(),
     sqr(s(x)) -> +(sqr(x), s(double(x))),
   double(0()) -> 0(),
  double(s(x)) -> s(s(double(x))),
     +(x, 0()) -> x,
    +(x, s(y)) -> s(+(x, y)),
     sqr(s(x)) -> s(+(sqr(x), double(x)))}
 LMPO:
  Quasi-Precedence:
  sqr > +, 
  sqr > s, 
  sqr > double
  empty
  
Normal:
   pi(double) = [1], pi(+) = [2], pi(sqr) = [1]
  
Safe:
   pi(+) = [1]
  
Predicative System:
   {     sqr(0();) -> 0(),
       sqr(s(x;);) -> +(s(double(x;););sqr(x;)),
      double(0();) -> 0(),
    double(s(x;);) -> s(s(double(x;););),
          +(0();x) -> x,
        +(s(y;);x) -> s(+(y;x);),
       sqr(s(x;);) -> s(+(double(x;);sqr(x;));)}
  

   
  

  Qed