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)}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(+_sl=1) = [1,2], pi(+_sl=0) = [1,2], pi(double_sl=1) = [1], pi(double_sl=0) = [1]
  
Safe positions:
   pi(s_sl=1) = [1], pi(s_sl=0) = [1]
  
Precedence:
   +_sl=0 > s_sl=0, 
   +_sl=0 > +_sl=1, 
   double_sl=1 > s_sl=0, 
   double_sl=1 > +_sl=0, 
   double_sl=1 > +_sl=1
   empty
  
Interpretation:
   0^(0):
    | 1
   double^(1):
   0 | 0
   1 | 1
   s^(1):
   0 | 0
   1 | 0
   +^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 1
   
  
Labelling:
   0^(0):
    | 0
   double^(1):
   0 | 1
   1 | 1
   s^(1):
   0 | 0
   1 | 0
   +^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 1
   
  
Labelled predicative System:
   {  double_sl=1(0_sl=0();) -> 0_sl=0(),
    double_sl=1(s_sl=0(;x);) -> s_sl=0(;s_sl=0(;double_sl=1(x;))),
    double_sl=1(s_sl=0(;x);) -> s_sl=0(;s_sl=0(;double_sl=1(x;))),
         +_sl=0(x,0_sl=0();) -> x,
         +_sl=1(x,0_sl=0();) -> x,
       +_sl=0(x,s_sl=0(;y);) -> s_sl=0(;+_sl=0(x,y;)),
       +_sl=0(x,s_sl=0(;y);) -> s_sl=0(;+_sl=0(x,y;)),
       +_sl=0(x,s_sl=0(;y);) -> s_sl=0(;+_sl=0(x,y;)),
       +_sl=0(x,s_sl=0(;y);) -> s_sl=0(;+_sl=1(x,y;)),
       +_sl=0(s_sl=0(;x),y;) -> s_sl=0(;+_sl=0(x,y;)),
       +_sl=0(s_sl=0(;x),y;) -> s_sl=0(;+_sl=0(x,y;)),
       +_sl=0(s_sl=0(;x),y;) -> s_sl=0(;+_sl=0(x,y;)),
       +_sl=0(s_sl=0(;x),y;) -> s_sl=0(;+_sl=1(x,y;)),
             double_sl=1(x;) -> +_sl=0(x,x;),
             double_sl=1(x;) -> +_sl=1(x,x;)}
  

  Qed