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__isList(V) -> a__isNeList(V) a__isList(nil()) -> tt() a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a____(X1,X2) -> __(X1,X2) a__and(X1,X2) -> and(X1,X2) a__isList(X) -> isList(X) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isNePal(X) -> isNePal(X) a__isPal(X) -> isPal(X) linear polynomial interpretations on N: a_____A(x1,x2) = x1 + x2 + 8 a____#_A(x1,x2) = x1 + x2 + 8 ___A(x1,x2) = x1 + x2 + 8 __#_A(x1,x2) = x1 + x2 + 8 mark_A(x1) = x1 mark#_A(x1) = x1 nil_A = 2 nil#_A = 2 a__and_A(x1,x2) = x1 + x2 + 1 a__and#_A(x1,x2) = x1 + x2 + 1 tt_A = 1 tt#_A = 1 a__isList_A(x1) = x1 + 3 a__isList#_A(x1) = x1 + 3 a__isNeList_A(x1) = x1 + 2 a__isNeList#_A(x1) = x1 + 2 isList_A(x1) = x1 + 3 isList#_A(x1) = x1 + 3 a__isQid_A(x1) = x1 + 1 a__isQid#_A(x1) = x1 + 1 isNeList_A(x1) = x1 + 2 isNeList#_A(x1) = x1 + 2 a__isNePal_A(x1) = x1 + 2 a__isNePal#_A(x1) = x1 + 2 isPal_A(x1) = x1 + 3 isPal#_A(x1) = x1 + 3 a__isPal_A(x1) = x1 + 3 a__isPal#_A(x1) = x1 + 3 a_A = 2 a#_A = 2 e_A = 2 e#_A = 2 i_A = 2 i#_A = 2 o_A = 2 o#_A = 2 u_A = 2 u#_A = 2 and_A(x1,x2) = x1 + x2 + 1 and#_A(x1,x2) = x1 + x2 + 1 isQid_A(x1) = x1 + 1 isQid#_A(x1) = x1 + 1 isNePal_A(x1) = x1 + 2 isNePal#_A(x1) = x1 + 2 precedence: a____ = mark > __ = nil = a = e = i = o > a__and = u > tt = and > a__isNeList > a__isList > isList > a__isQid > isNeList > a__isNePal > a__isPal > isPal > isNePal > isQid