TRS: { zeros() -> cons(0(), n__zeros()), tail(cons(X, XS)) -> activate(XS), zeros() -> n__zeros(), activate(n__zeros()) -> zeros(), activate(X) -> X} RPO Product: Quasi-Precedence: activate > zeros, tail > activate empty Qed TRS: { zeros() -> cons(0(), n__zeros()), tail(cons(X, XS)) -> activate(XS), zeros() -> n__zeros(), activate(n__zeros()) -> zeros(), activate(X) -> X} Cdiprover: Interpretation class: quasisimplemixed Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING tail(X3) = + 0*X3^2 + 0 + 3*X3 activate(X2) = + 0*X2^2 + 2 + 1*X2 zeros = + 2 n__zeros = + 0 0 = + 0 cons(X1, X0) = + 1*X0 + 1*X1 + 1 Qed