YES O(n^2) TRS: { a__f(X) -> f(X), a__f(g(X)) -> g(X), a__c() -> a__f(g(c())), a__c() -> c(), mark(g(X)) -> g(X), mark(c()) -> a__c(), mark(f(X)) -> a__f(X) } Natural interpretation: Strict: { a__f(X) -> f(X), a__f(g(X)) -> g(X), a__c() -> a__f(g(c())), a__c() -> c(), mark(g(X)) -> g(X), mark(c()) -> a__c(), mark(f(X)) -> a__f(X) } Weak: {} Interpretation class: deltarestricted [f](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta [mark](delta, X0) = + 1*X0 + 2 + 0*X0*delta + 3*delta [a__c](delta) = + 0 + 2*delta [c](delta) = + 0 + 0*delta [g](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta [a__f](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 1*delta f_tau_1(delta) = delta/(0 + 1 * delta) mark_tau_1(delta) = delta/(1 + 0 * delta) g_tau_1(delta) = delta/(0 + 1 * delta) a__f_tau_1(delta) = delta/(0 + 1 * delta) Qed