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

   
  

  Qed