YES TRS: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isNePal(__(I,__(P,I))) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isNePal(X)) -> a__isNePal(mark(X)) mark(nil()) -> nil() mark(tt()) -> tt() a____(X1,X2) -> __(X1,X2) a__and(X1,X2) -> and(X1,X2) a__isNePal(X) -> isNePal(X) linear polynomial interpretations on N: a_____A(x1,x2) = x1 + x2 + 3 a____#_A(x1,x2) = x1 + x2 + 3 ___A(x1,x2) = x1 + x2 + 3 __#_A(x1,x2) = x1 + x2 + 2 mark_A(x1) = x1 mark#_A(x1) = x1 + 1 nil_A = 1 nil#_A = 0 a__and_A(x1,x2) = x1 + x2 + 2 a__and#_A(x1,x2) = x2 + 2 tt_A = 3 tt#_A = 3 a__isNePal_A(x1) = x1 + 4 a__isNePal#_A(x1) = 4 and_A(x1,x2) = x1 + x2 + 2 and#_A(x1,x2) = 0 isNePal_A(x1) = x1 + 4 isNePal#_A(x1) = 0 precedence: a____ > __ = and > mark > nil = a__and = tt > a__isNePal > isNePal