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