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