YES TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V)) U12(tt(),V) -> U13(isNeList(activate(V))) U13(tt()) -> tt() U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2)) U25(tt(),V2) -> U26(isList(activate(V2))) U26(tt()) -> tt() U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V)) U32(tt(),V) -> U33(isQid(activate(V))) U33(tt()) -> tt() U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2)) U45(tt(),V2) -> U46(isNeList(activate(V2))) U46(tt()) -> tt() U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2)) U55(tt(),V2) -> U56(isList(activate(V2))) U56(tt()) -> tt() U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V)) U62(tt(),V) -> U63(isQid(activate(V))) U63(tt()) -> tt() U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P)) U72(tt(),P) -> U73(isPal(activate(P)),activate(P)) U73(tt(),P) -> U74(isPalListKind(activate(P))) U74(tt()) -> tt() U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V)) U82(tt(),V) -> U83(isNePal(activate(V))) U83(tt()) -> tt() U91(tt(),V2) -> U92(isPalListKind(activate(V2))) U92(tt()) -> tt() isList(V) -> U11(isPalListKind(activate(V)),activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) isNeList(V) -> U31(isPalListKind(activate(V)),activate(V)) isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) isNePal(V) -> U61(isPalListKind(activate(V)),activate(V)) isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P)) isPal(V) -> U81(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)) -> U91(isPalListKind(activate(V1)),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) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(activate(X1),activate(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 + 9 __#_A(x1,x2) = 5 nil_A = 1 nil#_A = 5 U11_A(x1,x2) = x2 + 1 U11#_A(x1,x2) = x2 + 11 tt_A = 1 tt#_A = 2 U12_A(x1,x2) = x2 + 1 U12#_A(x1,x2) = x2 + 10 isPalListKind_A(x1) = 1 isPalListKind#_A(x1) = x1 + 6 activate_A(x1) = x1 activate#_A(x1) = 6 U13_A(x1) = x1 U13#_A(x1) = x1 isNeList_A(x1) = x1 + 1 isNeList#_A(x1) = x1 + 9 U21_A(x1,x2,x3) = x2 + x3 + 1 U21#_A(x1,x2,x3) = x2 + x3 + 17 U22_A(x1,x2,x3) = x3 + 1 U22#_A(x1,x2,x3) = x2 + x3 + 16 U23_A(x1,x2,x3) = x3 + 1 U23#_A(x1,x2,x3) = x2 + x3 + 15 U24_A(x1,x2,x3) = x3 + 1 U24#_A(x1,x2,x3) = x2 + x3 + 14 U25_A(x1,x2) = x2 + 1 U25#_A(x1,x2) = x2 + 13 isList_A(x1) = x1 + 1 isList#_A(x1) = x1 + 12 U26_A(x1) = x1 U26#_A(x1) = 3 U31_A(x1,x2) = x2 + 1 U31#_A(x1,x2) = x2 + 8 U32_A(x1,x2) = x1 U32#_A(x1,x2) = x2 + 7 U33_A(x1) = x1 U33#_A(x1) = 0 isQid_A(x1) = 1 isQid#_A(x1) = 3 U41_A(x1,x2,x3) = x2 + x3 + 1 U41#_A(x1,x2,x3) = x2 + x3 + 16 U42_A(x1,x2,x3) = x2 + x3 + 1 U42#_A(x1,x2,x3) = x2 + x3 + 15 U43_A(x1,x2,x3) = x2 + x3 + 1 U43#_A(x1,x2,x3) = x2 + x3 + 14 U44_A(x1,x2,x3) = x1 + x2 U44#_A(x1,x2,x3) = x2 + x3 + 13 U45_A(x1,x2) = 1 U45#_A(x1,x2) = x2 + 10 U46_A(x1) = 1 U46#_A(x1) = x1 + 2 U51_A(x1,x2,x3) = 1 U51#_A(x1,x2,x3) = x2 + x3 + 17 U52_A(x1,x2,x3) = 1 U52#_A(x1,x2,x3) = x2 + x3 + 16 U53_A(x1,x2,x3) = 1 U53#_A(x1,x2,x3) = x2 + x3 + 15 U54_A(x1,x2,x3) = 1 U54#_A(x1,x2,x3) = x2 + x3 + 14 U55_A(x1,x2) = 1 U55#_A(x1,x2) = x2 + 13 U56_A(x1) = 1 U56#_A(x1) = x1 + 2 U61_A(x1,x2) = 1 U61#_A(x1,x2) = x2 + 8 U62_A(x1,x2) = 1 U62#_A(x1,x2) = 7 U63_A(x1) = 1 U63#_A(x1) = 3 U71_A(x1,x2,x3) = 1 U71#_A(x1,x2,x3) = x2 + x3 + 14 U72_A(x1,x2) = 1 U72#_A(x1,x2) = x1 + x2 + 12 U73_A(x1,x2) = 1 U73#_A(x1,x2) = x2 + 7 isPal_A(x1) = 1 isPal#_A(x1) = x1 + 12 U74_A(x1) = 1 U74#_A(x1) = 3 U81_A(x1,x2) = x1 U81#_A(x1,x2) = x2 + 11 U82_A(x1,x2) = 1 U82#_A(x1,x2) = x2 + 10 U83_A(x1) = 1 U83#_A(x1) = x1 + 2 isNePal_A(x1) = x1 + 1 isNePal#_A(x1) = x1 + 9 U91_A(x1,x2) = x1 U91#_A(x1,x2) = x2 + 7 U92_A(x1) = 1 U92#_A(x1) = 3 n__nil_A = 1 n__nil#_A = 1 n_____A(x1,x2) = x1 + x2 + 9 n____#_A(x1,x2) = 4 n__a_A = 1 n__a#_A = 3 n__e_A = 1 n__e#_A = 3 n__i_A = 1 n__i#_A = 3 n__o_A = 1 n__o#_A = 0 n__u_A = 1 n__u#_A = 3 a_A = 1 a#_A = 4 e_A = 1 e#_A = 4 i_A = 1 i#_A = 4 o_A = 1 o#_A = 1 u_A = 1 u#_A = 4 precedence: U51 > U52 > U11 = U44 = U53 > U12 = U45 = U54 = isNePal > isNeList = U71 > U41 = U72 > U23 = U42 = isPal > U24 = U31 = U43 = U61 = U73 = U81 = U91 > isPalListKind = U25 = U55 = U82 > isList = n____ > U21 > U22 = U32 = U62 > activate = isQid = n__e > __ = nil = U26 = U46 = U56 = U63 = U74 = U83 = U92 = a = e = i = u > n__nil = n__a = n__i = n__u > tt > U13 = U33 = n__o > o