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