TRS: { f(x, x) -> a(), f(g(x), y) -> f(x, y)} Cdiprover: Interpretation class: pizerosimplemixed Complexity bound: POLYTIME COMPUTABLE g(X2) = + 1*X2 + 1 f(X1, X0) = + 0*X1^2 + 0*X0^2 + 2*X1 + 2 + 2*X0 + 0*X0*X1 a = + 1 Qed