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()))}
 RPO Product:
  Quasi-Precedence:
  empty
  
  Qed


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: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  v = + 0
  u = + 0
  ++(X3, X2) = + 1*X2 + 1*X3 + 1
  nil = + 0
  merge(X1, X0) = + 0*X1^2 + 0*X0^2 + 2*X1 + 0 + 2*X0 + 0*X0*X1
  
  Qed