TRS: {a__f(f(a())) -> c(f(g(f(a())))), mark(f(X)) -> a__f(mark(X)), mark(a()) -> a(), mark(c(X)) -> c(X), mark(g(X)) -> g(mark(X)), a__f(X) -> f(X)} RPO Product: Quasi-Precedence: mark > a__f empty Qed TRS: {a__f(f(a())) -> c(f(g(f(a())))), mark(f(X)) -> a__f(mark(X)), mark(a()) -> a(), mark(c(X)) -> c(X), mark(g(X)) -> g(mark(X)), a__f(X) -> f(X)} Cdiprover: Interpretation class: quasisimplemixed Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING mark(X4) = + 2*X4^2 + 2 + 1*X4 a__f(X3) = + 0*X3^2 + 3 + 1*X3 a = + 0 g(X2) = + 1*X2 + 1 f(X1) = + 1*X1 + 1 c(X0) = + 1*X0 + 1 Qed