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()))}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  v = + 1
  u = + 1
  ++(X3, X2) = + 1*X2 + 1*X3 + 1
  nil = + 1
  merge(X1, X0) = + 0*X1^2 + 0*X0^2 + 2*X1 + 0 + 2*X0 + 0*X0*X1
  
  Qed