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)))}
 POP*:
  Precedence:
  sqr > +, 
  sqr > s, 
  sqr > double, 
  + > s, 
  double > s
  empty
  
Normal:
   pi(double) = [1], pi(+) = [2], pi(sqr) = [1]
  
Safe:
   pi(s) = [1], 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