YES O(n^2) TRS: { c(X) -> d(activate(X)), f(X) -> n__f(X), f(f(X)) -> c(n__f(g(n__f(X)))), d(X) -> n__d(X), activate(X) -> X, activate(n__f(X)) -> f(X), activate(n__d(X)) -> d(X), h(X) -> c(n__d(X)) } DUP: We consider a non-duplicating system. Trs: { c(X) -> d(activate(X)), f(X) -> n__f(X), f(f(X)) -> c(n__f(g(n__f(X)))), d(X) -> n__d(X), activate(X) -> X, activate(n__f(X)) -> f(X), activate(n__d(X)) -> d(X), h(X) -> c(n__d(X)) } Matrix Interpretation: Interpretation class: triangular [X1] [1 4][X1] [7] [h]([X0]) = [0 0][X0] + [4] [X1] [1 0][X1] [1] [n__d]([X0]) = [0 0][X0] + [0] [X1] [1 0][X1] [2] [activate]([X0]) = [0 1][X0] + [0] [X1] [1 0][X1] [2] [d]([X0]) = [0 0][X0] + [0] [X1] [1 3][X1] [1] [f]([X0]) = [0 0][X0] + [4] [X1] [1 0][X1] [3] [g]([X0]) = [0 0][X0] + [0] [X1] [1 3][X1] [0] [n__f]([X0]) = [0 0][X0] + [4] [X1] [1 0][X1] [5] [c]([X0]) = [0 0][X0] + [4] Qed