TRS:
 {              merge(x, nil()) -> x,
                merge(nil(), y) -> y,
  merge(++(x, y), ++(u(), v())) -> ++(x, merge(y, ++(u(), v()))),
  merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v()))}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(merge_sl=1) = [1,2], pi(merge_sl=0) = [1,2]
  
Safe positions:
   pi(++_sl=1) = [1,2], pi(++_sl=0) = [1,2]
  
Precedence:
   merge_sl=0 > u_sl=1, 
   merge_sl=0 > ++_sl=0
   empty
  
Interpretation:
   merge^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 1
   nil^(0):
    | 1
   ++^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   u^(0):
    | 0
   v^(0):
    | 0
   
  
Labelling:
   merge^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   nil^(0):
    | 0
   ++^(2):
   00 | 0
   01 | 0
   10 | 0
   11 | 0
   u^(0):
    | 1
   v^(0):
    | 0
   
  
Labelled predicative System:
   {                             merge_sl=0(x,nil_sl=0();) -> x,
                                 merge_sl=0(x,nil_sl=0();) -> x,
                                 merge_sl=0(nil_sl=0(),y;) -> y,
                                 merge_sl=0(nil_sl=0(),y;) -> y,
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;x,merge_sl=0(y,++_sl=0(;u_sl=1(),v_sl=0());)),
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;x,merge_sl=0(y,++_sl=0(;u_sl=1(),v_sl=0());)),
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;x,merge_sl=0(y,++_sl=0(;u_sl=1(),v_sl=0());)),
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;x,merge_sl=0(y,++_sl=0(;u_sl=1(),v_sl=0());)),
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;u_sl=1(),merge_sl=0(++_sl=0(;x,y),v_sl=0();)),
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;u_sl=1(),merge_sl=0(++_sl=0(;x,y),v_sl=0();)),
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;u_sl=1(),merge_sl=0(++_sl=0(;x,y),v_sl=0();)),
    merge_sl=0(++_sl=0(;x,y),++_sl=0(;u_sl=1(),v_sl=0());) -> ++_sl=0(;u_sl=1(),merge_sl=0(++_sl=0(;x,y),v_sl=0();))}
  

  Qed