YES TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X U11(tt()) -> U12(tt()) U12(tt()) -> tt() isNePal(__(I,__(P,I))) -> U11(tt()) max/plus interpretations on N: ___A(x1,x2) = max{1, 1 + x1, x2} __#_A(x1,x2) = max{2, 2, 2} nil_A = 0 nil#_A = 0 U11_A(x1) = max{1, -1} U11#_A(x1) = max{3, 5} tt_A = 1 tt#_A = 1 U12_A(x1) = max{0, 1} U12#_A(x1) = max{4, 2} isNePal_A(x1) = max{1, -2} isNePal#_A(x1) = max{0, 6} precedence: __ = nil = U12 = isNePal > U11 > tt