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