YES Problem: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isNePal(__(I,__(P,I))) -> tt() activate(X) -> X Proof: DP Processor: DPs: __#(__(X,Y),Z) -> __#(Y,Z) __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and#(tt(),X) -> activate#(X) TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isNePal(__(I,__(P,I))) -> tt() activate(X) -> X Matrix Interpretation Processor: dim=1 interpretation: [activate#](x0) = 0, [and#](x0, x1) = 4x0 + 2x1 + 1, [__#](x0, x1) = 3x0 + 2, [isNePal](x0) = x0, [activate](x0) = 4x0, [and](x0, x1) = 4x1 + 4, [tt] = 6, [nil] = 0, [__](x0, x1) = 3x0 + x1 + 3 orientation: __#(__(X,Y),Z) = 9X + 3Y + 11 >= 3Y + 2 = __#(Y,Z) __#(__(X,Y),Z) = 9X + 3Y + 11 >= 3X + 2 = __#(X,__(Y,Z)) and#(tt(),X) = 2X + 25 >= 0 = activate#(X) __(__(X,Y),Z) = 9X + 3Y + Z + 12 >= 3X + 3Y + Z + 6 = __(X,__(Y,Z)) __(X,nil()) = 3X + 3 >= X = X __(nil(),X) = X + 3 >= X = X and(tt(),X) = 4X + 4 >= 4X = activate(X) isNePal(__(I,__(P,I))) = 4I + 3P + 6 >= 6 = tt() activate(X) = 4X >= X = X problem: DPs: TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isNePal(__(I,__(P,I))) -> tt() activate(X) -> X Qed