YES(?,O(n^3)) TRS: { f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))), f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x)) } DUP: We consider a non-duplicating system. Trs: { f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))), f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x)) } RLAB: Strict: { f([a,f])(a(), f([b,f])(b(), f([a,f])(a(), x))) -> f([a,f])(a(), f([b,f])(b(), f([b,f])(b(), f([a,f])(a(), x)))), f([a,f])(a(), f([b,f])(b(), f([a,a])(a(), x))) -> f([a,f])(a(), f([b,f])(b(), f([b,f])(b(), f([a,a])(a(), x)))), f([a,f])(a(), f([b,f])(b(), f([a,b])(a(), x))) -> f([a,f])(a(), f([b,f])(b(), f([b,f])(b(), f([a,b])(a(), x)))), f([b,f])(b(), f([b,f])(b(), f([b,f])(b(), x))) -> f([b,f])(b(), f([b,f])(b(), x)), f([b,f])(b(), f([b,f])(b(), f([b,a])(b(), x))) -> f([b,f])(b(), f([b,a])(b(), x)), f([b,f])(b(), f([b,f])(b(), f([b,b])(b(), x))) -> f([b,f])(b(), f([b,b])(b(), x)) } Weak: {} Matrix Interpretation: Interpretation class: triangular [1] [b] = [1] [2] [4] [a] = [1] [3] [X5] [X2] [1 2 0][X5] [1 0 0][X2] [4] [f(5)]([X4], [X1]) = [0 0 0][X4] + [0 0 0][X1] + [0] [X3] [X0] [0 0 0][X3] [0 0 0][X0] [0] [X5] [X2] [1 1 6][X5] [1 0 2][X2] [0] [f(4)]([X4], [X1]) = [0 0 0][X4] + [0 0 0][X1] + [0] [X3] [X0] [0 0 0][X3] [0 0 0][X0] [0] [X5] [X2] [1 0 4][X5] [1 0 4][X2] [0] [f(3)]([X4], [X1]) = [0 0 0][X4] + [0 0 0][X1] + [0] [X3] [X0] [0 0 0][X3] [0 0 0][X0] [4] [X5] [X2] [1 1 7][X5] [1 0 0][X2] [7] [f(2)]([X4], [X1]) = [0 0 0][X4] + [0 0 0][X1] + [0] [X3] [X0] [0 0 0][X3] [0 0 1][X0] [4] [X5] [X2] [1 3 0][X5] [1 0 4][X2] [2] [f(1)]([X4], [X1]) = [0 0 4][X4] + [0 0 4][X1] + [0] [X3] [X0] [0 0 1][X3] [0 0 0][X0] [0] [X5] [X2] [1 6 0][X5] [1 2 0][X2] [4] [f(0)]([X4], [X1]) = [0 0 5][X4] + [0 0 0][X1] + [0] [X3] [X0] [0 0 0][X3] [0 0 0][X0] [4] Qed