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