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