TRS:
 {  +(0(), y) -> y,
   +(s(x), y) -> s(+(x, y)),
   +(p(x), y) -> p(+(x, y)),
   minus(0()) -> 0(),
  minus(s(x)) -> p(minus(x)),
  minus(p(x)) -> s(minus(x)),
    *(0(), y) -> 0(),
   *(s(x), y) -> +(*(x, y), y),
   *(p(x), y) -> +(*(x, y), minus(y))}
 RPO Product:
  Quasi-Precedence:
  * > minus, 
  * > +
  empty
  
  Qed


TRS:
 {  +(0(), y) -> y,
   +(s(x), y) -> s(+(x, y)),
   +(p(x), y) -> p(+(x, y)),
   minus(0()) -> 0(),
  minus(s(x)) -> p(minus(x)),
  minus(p(x)) -> s(minus(x)),
    *(0(), y) -> 0(),
   *(s(x), y) -> +(*(x, y), y),
   *(p(x), y) -> +(*(x, y), minus(y))}
 Cdiprover:
  Interpretation class: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  *(X6, X5) = + 0*X6^2 + 0*X5^2 + 2*X6 + 0 + 2*X5 + 2*X5*X6
  minus(X4) = + 0*X4^2 + 0 + 1*X4
  p(X3) = + 1*X3 + 1
  s(X2) = + 1*X2 + 1
  0 = + 0
  +(X1, X0) = + 0*X1^2 + 0*X0^2 + 1*X1 + 0 + 1*X0 + 0*X0*X1
  
  Qed