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()))}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(merge) = [1,2]
  
Safe:
   
  
Predicative System:
   {              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(););)}
  

   
  

  Qed