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