TRS: { a__f(a(), X, X) -> a__f(X, a__b(), b()), a__b() -> a(), mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3), mark(b()) -> a__b(), mark(a()) -> a(), a__f(X1, X2, X3) -> f(X1, X2, X3), a__b() -> b()} Cdiprover: Interpretation class: pizerosimplemixed Complexity bound: POLYTIME COMPUTABLE f(X6, X5, X4) = + 1*X4 + 1*X5 + 1*X6 + 2 mark(X3) = + 2*X3^2 + 0 + 2*X3 a = + 2 b = + 1 a__b = + 3 a__f(X2, X1, X0) = + 2*X2^2 + 0*X1^2 + 2*X0^2 + 0*X1*X2 + 1*X1 + 3 + 1*X2 + 0*X0*X2 + 1*X0 + 0*X0*X1 + 0*X0*X1*X2 Qed