YES TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X U11(tt(),V) -> U12(isNeList(activate(V))) U12(tt()) -> tt() U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2)) U22(tt(),V2) -> U23(isList(activate(V2))) U23(tt()) -> tt() U31(tt(),V) -> U32(isQid(activate(V))) U32(tt()) -> tt() U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2)) U42(tt(),V2) -> U43(isNeList(activate(V2))) U43(tt()) -> tt() U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2)) U52(tt(),V2) -> U53(isList(activate(V2))) U53(tt()) -> tt() U61(tt(),V) -> U62(isQid(activate(V))) U62(tt()) -> tt() U71(tt(),V) -> U72(isNePal(activate(V))) U72(tt()) -> tt() and(tt(),X) -> activate(X) isList(V) -> U11(isPalListKind(activate(V)),activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) isNePal(n____(I,__(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(isPal(activate(P)),n__isPalListKind(activate(P)))) isPal(V) -> U71(isPalListKind(activate(V)),activate(V)) isPal(n__nil()) -> tt() isPalListKind(n__a()) -> tt() isPalListKind(n__e()) -> tt() isPalListKind(n__i()) -> tt() isPalListKind(n__nil()) -> tt() isPalListKind(n__o()) -> tt() isPalListKind(n__u()) -> tt() isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isPalListKind(X) -> n__isPalListKind(X) and(X1,X2) -> n__and(X1,X2) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(X1,X2) activate(n__isPalListKind(X)) -> isPalListKind(X) activate(n__and(X1,X2)) -> and(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__o()) -> o() activate(n__u()) -> u() activate(X) -> X linear polynomial interpretations on N: ___A(x1,x2) = x1 + x2 + 23 __#_A(x1,x2) = x1 + x2 + 25 nil_A = 1 nil#_A = 3 U11_A(x1,x2) = 2 U11#_A(x1,x2) = x2 + 10 tt_A = 2 tt#_A = 1 U12_A(x1) = 2 U12#_A(x1) = 2 isNeList_A(x1) = 2 isNeList#_A(x1) = x1 + 7 activate_A(x1) = x1 + 2 activate#_A(x1) = x1 + 3 U21_A(x1,x2,x3) = x2 + 2 U21#_A(x1,x2,x3) = x1 + x2 + x3 + 17 U22_A(x1,x2) = 2 U22#_A(x1,x2) = x2 + 16 isList_A(x1) = x1 + 2 isList#_A(x1) = x1 + 13 U23_A(x1) = 2 U23#_A(x1) = x1 U31_A(x1,x2) = 2 U31#_A(x1,x2) = x2 + 4 U32_A(x1) = x1 U32#_A(x1) = 2 isQid_A(x1) = 2 isQid#_A(x1) = 2 U41_A(x1,x2,x3) = 2 U41#_A(x1,x2,x3) = x2 + x3 + 16 U42_A(x1,x2) = 2 U42#_A(x1,x2) = x2 + 10 U43_A(x1) = 2 U43#_A(x1) = 0 U51_A(x1,x2,x3) = 2 U51#_A(x1,x2,x3) = x2 + x3 + 19 U52_A(x1,x2) = x1 U52#_A(x1,x2) = x2 + 16 U53_A(x1) = 2 U53#_A(x1) = x1 U61_A(x1,x2) = 2 U61#_A(x1,x2) = x2 + 3 U62_A(x1) = 2 U62#_A(x1) = 2 U71_A(x1,x2) = 2 U71#_A(x1,x2) = x2 + 9 U72_A(x1) = 2 U72#_A(x1) = x1 isNePal_A(x1) = x1 + 2 isNePal#_A(x1) = x1 + 6 and_A(x1,x2) = x1 + x2 and#_A(x1,x2) = x1 + x2 + 2 isPalListKind_A(x1) = 2 isPalListKind#_A(x1) = 2 n__nil_A = 1 n__nil#_A = 2 n_____A(x1,x2) = x1 + x2 + 23 n____#_A(x1,x2) = x1 + x2 + 24 n__isPalListKind_A(x1) = 0 n__isPalListKind#_A(x1) = 0 n__and_A(x1,x2) = x1 + x2 n__and#_A(x1,x2) = x1 + 1 isPal_A(x1) = x1 + 40 isPal#_A(x1) = x1 + 22 n__a_A = 1 n__a#_A = 2 n__e_A = 1 n__e#_A = 2 n__i_A = 1 n__i#_A = 2 n__o_A = 1 n__o#_A = 2 n__u_A = 1 n__u#_A = 0 a_A = 1 a#_A = 3 e_A = 1 e#_A = 3 i_A = 1 i#_A = 3 o_A = 1 o#_A = 3 u_A = 1 u#_A = 1 precedence: isNeList = U21 > U22 = U31 = U41 = U52 > isList = U42 = isNePal > U11 = U43 = U61 = a > activate = U62 > __ = nil = i = o > n____ = n__i = n__o > isQid = U51 = n__and = isPal > U12 = U71 = isPalListKind = n__a = e = u > U23 = U32 = U72 = and = n__nil = n__isPalListKind = n__e = n__u > tt > U53