YES O(n^2) TRS: { a__h(X) -> h(X), a__h(d()) -> a__g(c()), a__g(X) -> a__h(X), a__g(X) -> g(X), a__c() -> d(), a__c() -> c(), mark(d()) -> d(), mark(c()) -> a__c(), mark(g(X)) -> a__g(X), mark(h(X)) -> a__h(X) } Natural interpretation: Strict: { a__h(X) -> h(X), a__h(d()) -> a__g(c()), a__g(X) -> a__h(X), a__g(X) -> g(X), a__c() -> d(), a__c() -> c(), mark(d()) -> d(), mark(c()) -> a__c(), mark(g(X)) -> a__g(X), mark(h(X)) -> a__h(X) } Weak: {} Interpretation class: deltarestricted [h](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta [g](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 2*delta [mark](delta, X0) = + 1*X0 + 3 + 2*X0*delta + 3*delta [c](delta) = + 0 + 0*delta [a__c](delta) = + 2 + 2*delta [d](delta) = + 2 + 0*delta [a__g](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 3*delta [a__h](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 2*delta h_tau_1(delta) = delta/(0 + 1 * delta) g_tau_1(delta) = delta/(0 + 1 * delta) mark_tau_1(delta) = delta/(1 + 2 * delta) a__g_tau_1(delta) = delta/(0 + 1 * delta) a__h_tau_1(delta) = delta/(0 + 1 * delta) Qed