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