YES
TRS:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
DP:
Strict:
{ __#(__(X, Y), Z) -> __#(X, __(Y, Z)),
__#(__(X, Y), Z) -> __#(Y, Z),
isNeList#(V) -> activate#(V),
isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)),
isNeList#(V) -> isPalListKind#(activate(V)),
isNeList#(n____(V1, V2)) -> activate#(V1),
isNeList#(n____(V1, V2)) -> activate#(V2),
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)),
isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)),
activate#(n__nil()) -> nil#(),
activate#(n__isPalListKind(X)) -> isPalListKind#(X),
activate#(n____(X1, X2)) -> __#(X1, X2),
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#(),
U11#(tt(), V) -> U12#(isNeList(activate(V))),
U11#(tt(), V) -> isNeList#(activate(V)),
U11#(tt(), V) -> activate#(V),
U22#(tt(), V2) -> activate#(V2),
U22#(tt(), V2) -> isList#(activate(V2)),
U22#(tt(), V2) -> U23#(isList(activate(V2))),
isList#(V) -> activate#(V),
isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)),
isList#(V) -> isPalListKind#(activate(V)),
isList#(n____(V1, V2)) -> activate#(V1),
isList#(n____(V1, V2)) -> activate#(V2),
isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)),
isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)),
U21#(tt(), V1, V2) -> activate#(V1),
U21#(tt(), V1, V2) -> activate#(V2),
U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)),
U21#(tt(), V1, V2) -> isList#(activate(V1)),
U31#(tt(), V) -> activate#(V),
U31#(tt(), V) -> U32#(isQid(activate(V))),
U31#(tt(), V) -> isQid#(activate(V)),
U42#(tt(), V2) -> isNeList#(activate(V2)),
U42#(tt(), V2) -> activate#(V2),
U42#(tt(), V2) -> U43#(isNeList(activate(V2))),
U41#(tt(), V1, V2) -> activate#(V1),
U41#(tt(), V1, V2) -> activate#(V2),
U41#(tt(), V1, V2) -> isList#(activate(V1)),
U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)),
U52#(tt(), V2) -> activate#(V2),
U52#(tt(), V2) -> isList#(activate(V2)),
U52#(tt(), V2) -> U53#(isList(activate(V2))),
U51#(tt(), V1, V2) -> isNeList#(activate(V1)),
U51#(tt(), V1, V2) -> activate#(V1),
U51#(tt(), V1, V2) -> activate#(V2),
U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)),
U61#(tt(), V) -> activate#(V),
U61#(tt(), V) -> isQid#(activate(V)),
U61#(tt(), V) -> U62#(isQid(activate(V))),
isNePal#(V) -> activate#(V),
isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)),
isNePal#(V) -> isPalListKind#(activate(V)),
isNePal#(n____(I, __(P, I))) -> activate#(I),
isNePal#(n____(I, __(P, I))) -> activate#(P),
isNePal#(n____(I, __(P, I))) -> isQid#(activate(I)),
isNePal#(n____(I, __(P, I))) -> and#(isQid(activate(I)), n__isPalListKind(activate(I))),
isNePal#(n____(I, __(P, I))) -> and#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))),
isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)),
U71#(tt(), V) -> activate#(V),
U71#(tt(), V) -> U72#(isNePal(activate(V))),
U71#(tt(), V) -> isNePal#(activate(V)),
and#(tt(), X) -> activate#(X),
isPalListKind#(n____(V1, V2)) -> activate#(V1),
isPalListKind#(n____(V1, V2)) -> activate#(V2),
isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)),
isPal#(V) -> activate#(V),
isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)),
isPal#(V) -> isPalListKind#(activate(V))}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
EDG:
{
(U11#(tt(), V) -> activate#(V), activate#(n__u()) -> u#())
(U11#(tt(), V) -> activate#(V), activate#(n__o()) -> o#())
(U11#(tt(), V) -> activate#(V), activate#(n__i()) -> i#())
(U11#(tt(), V) -> activate#(V), activate#(n__e()) -> e#())
(U11#(tt(), V) -> activate#(V), activate#(n__a()) -> a#())
(U11#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U11#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(U11#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U11#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#())
(U31#(tt(), V) -> activate#(V), activate#(n__u()) -> u#())
(U31#(tt(), V) -> activate#(V), activate#(n__o()) -> o#())
(U31#(tt(), V) -> activate#(V), activate#(n__i()) -> i#())
(U31#(tt(), V) -> activate#(V), activate#(n__e()) -> e#())
(U31#(tt(), V) -> activate#(V), activate#(n__a()) -> a#())
(U31#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U31#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(U31#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U31#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#())
(isNePal#(V) -> activate#(V), activate#(n__u()) -> u#())
(isNePal#(V) -> activate#(V), activate#(n__o()) -> o#())
(isNePal#(V) -> activate#(V), activate#(n__i()) -> i#())
(isNePal#(V) -> activate#(V), activate#(n__e()) -> e#())
(isNePal#(V) -> activate#(V), activate#(n__a()) -> a#())
(isNePal#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isNePal#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(isNePal#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isNePal#(V) -> activate#(V), activate#(n__nil()) -> nil#())
(isPal#(V) -> activate#(V), activate#(n__u()) -> u#())
(isPal#(V) -> activate#(V), activate#(n__o()) -> o#())
(isPal#(V) -> activate#(V), activate#(n__i()) -> i#())
(isPal#(V) -> activate#(V), activate#(n__e()) -> e#())
(isPal#(V) -> activate#(V), activate#(n__a()) -> a#())
(isPal#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isPal#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(isPal#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isPal#(V) -> activate#(V), activate#(n__nil()) -> nil#())
(isNePal#(n____(I, __(P, I))) -> and#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))), and#(tt(), X) -> activate#(X))
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__u()) -> u#())
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__o()) -> o#())
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__i()) -> i#())
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__e()) -> e#())
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__a()) -> a#())
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2))
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isList#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#())
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__u()) -> u#())
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__o()) -> o#())
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__i()) -> i#())
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__e()) -> e#())
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__a()) -> a#())
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2))
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U41#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#())
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__u()) -> u#())
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__o()) -> o#())
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__i()) -> i#())
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__e()) -> e#())
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__a()) -> a#())
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2))
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#())
(isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), and#(tt(), X) -> activate#(X))
(isNePal#(n____(I, __(P, I))) -> and#(isQid(activate(I)), n__isPalListKind(activate(I))), and#(tt(), X) -> activate#(X))
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__u()) -> u#())
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__o()) -> o#())
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__i()) -> i#())
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__e()) -> e#())
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__a()) -> a#())
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#())
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__u()) -> u#())
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__o()) -> o#())
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__i()) -> i#())
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__e()) -> e#())
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__a()) -> a#())
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isList#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#())
(U42#(tt(), V2) -> activate#(V2), activate#(n__u()) -> u#())
(U42#(tt(), V2) -> activate#(V2), activate#(n__o()) -> o#())
(U42#(tt(), V2) -> activate#(V2), activate#(n__i()) -> i#())
(U42#(tt(), V2) -> activate#(V2), activate#(n__e()) -> e#())
(U42#(tt(), V2) -> activate#(V2), activate#(n__a()) -> a#())
(U42#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U42#(tt(), V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(U42#(tt(), V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U42#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(U52#(tt(), V2) -> activate#(V2), activate#(n__u()) -> u#())
(U52#(tt(), V2) -> activate#(V2), activate#(n__o()) -> o#())
(U52#(tt(), V2) -> activate#(V2), activate#(n__i()) -> i#())
(U52#(tt(), V2) -> activate#(V2), activate#(n__e()) -> e#())
(U52#(tt(), V2) -> activate#(V2), activate#(n__a()) -> a#())
(U52#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U52#(tt(), V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(U52#(tt(), V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U52#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__u()) -> u#())
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__o()) -> o#())
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__i()) -> i#())
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__e()) -> e#())
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__a()) -> a#())
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#())
(and#(tt(), X) -> activate#(X), activate#(n__u()) -> u#())
(and#(tt(), X) -> activate#(X), activate#(n__o()) -> o#())
(and#(tt(), X) -> activate#(X), activate#(n__i()) -> i#())
(and#(tt(), X) -> activate#(X), activate#(n__e()) -> e#())
(and#(tt(), X) -> activate#(X), activate#(n__a()) -> a#())
(and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2))
(and#(tt(), X) -> activate#(X), activate#(n____(X1, X2)) -> __#(X1, X2))
(and#(tt(), X) -> activate#(X), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(and#(tt(), X) -> activate#(X), activate#(n__nil()) -> nil#())
(isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)))
(isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> activate#(V2))
(isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> activate#(V1))
(isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> isNeList#(activate(V1)))
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__u()) -> u#())
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__o()) -> o#())
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__i()) -> i#())
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__e()) -> e#())
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__a()) -> a#())
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n____(X1, X2)) -> __#(X1, X2))
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__nil()) -> nil#())
(isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)), U31#(tt(), V) -> isQid#(activate(V)))
(isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)), U31#(tt(), V) -> U32#(isQid(activate(V))))
(isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)), U31#(tt(), V) -> activate#(V))
(U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> U23#(isList(activate(V2))))
(U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> isList#(activate(V2)))
(U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> activate#(V2))
(U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)), U52#(tt(), V2) -> U53#(isList(activate(V2))))
(U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)), U52#(tt(), V2) -> isList#(activate(V2)))
(U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)), U52#(tt(), V2) -> activate#(V2))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V2))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V1))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> isPalListKind#(activate(V)))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> activate#(V))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V2))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V1))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> isPalListKind#(activate(V)))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))
(U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> activate#(V))
(activate#(n____(X1, X2)) -> __#(X1, X2), __#(__(X, Y), Z) -> __#(Y, Z))
(activate#(n____(X1, X2)) -> __#(X1, X2), __#(__(X, Y), Z) -> __#(X, __(Y, Z)))
(isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V2))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V1))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> isPalListKind#(activate(V)))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))
(U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> activate#(V))
(isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V2))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V1))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(V) -> isPalListKind#(activate(V)))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(V) -> activate#(V))
(isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(V) -> activate#(V))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(V) -> isPalListKind#(activate(V)))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> activate#(I))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> activate#(P))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> isQid#(activate(I)))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> and#(isQid(activate(I)), n__isPalListKind(activate(I))))
(U71#(tt(), V) -> isNePal#(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)))))
(U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)))
(isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(V) -> activate#(V))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(V) -> isPalListKind#(activate(V)))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> activate#(V1))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> activate#(V2))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> activate#(V))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> isPalListKind#(activate(V)))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V1))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V2))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X))
(isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(V) -> activate#(V))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(V) -> isPalListKind#(activate(V)))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> activate#(V1))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> activate#(V2))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> activate#(V))
(isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> U72#(isNePal(activate(V))))
(isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> isNePal#(activate(V)))
(isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)), U61#(tt(), V) -> activate#(V))
(isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)), U61#(tt(), V) -> isQid#(activate(V)))
(isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)), U61#(tt(), V) -> U62#(isQid(activate(V))))
(U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U42#(tt(), V2) -> isNeList#(activate(V2)))
(U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U42#(tt(), V2) -> activate#(V2))
(U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U42#(tt(), V2) -> U43#(isNeList(activate(V2))))
(isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> U12#(isNeList(activate(V))))
(isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> isNeList#(activate(V)))
(isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> activate#(V))
(isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), isPal#(V) -> activate#(V))
(isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)))
(isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), isPal#(V) -> isPalListKind#(activate(V)))
(isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> activate#(V1))
(isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> activate#(V2))
(isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)))
(isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> isList#(activate(V1)))
(isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> activate#(V1))
(isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> activate#(V2))
(isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> isList#(activate(V1)))
(isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)))
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__nil()) -> nil#())
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n____(X1, X2)) -> __#(X1, X2))
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__a()) -> a#())
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__e()) -> e#())
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__i()) -> i#())
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__o()) -> o#())
(isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__u()) -> u#())
(activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> activate#(V1))
(activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> activate#(V2))
(activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))))
(activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)))
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__a()) -> a#())
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__e()) -> e#())
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__i()) -> i#())
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__o()) -> o#())
(U51#(tt(), V1, V2) -> activate#(V2), activate#(n__u()) -> u#())
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__a()) -> a#())
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__e()) -> e#())
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__i()) -> i#())
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__o()) -> o#())
(U41#(tt(), V1, V2) -> activate#(V2), activate#(n__u()) -> u#())
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__a()) -> a#())
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__e()) -> e#())
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__i()) -> i#())
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__o()) -> o#())
(U21#(tt(), V1, V2) -> activate#(V2), activate#(n__u()) -> u#())
(U22#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(U22#(tt(), V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U22#(tt(), V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2))
(U22#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U22#(tt(), V2) -> activate#(V2), activate#(n__a()) -> a#())
(U22#(tt(), V2) -> activate#(V2), activate#(n__e()) -> e#())
(U22#(tt(), V2) -> activate#(V2), activate#(n__i()) -> i#())
(U22#(tt(), V2) -> activate#(V2), activate#(n__o()) -> o#())
(U22#(tt(), V2) -> activate#(V2), activate#(n__u()) -> u#())
(isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), and#(tt(), X) -> activate#(X))
(isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), and#(tt(), X) -> activate#(X))
(__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(X, __(Y, Z)))
(__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(Y, Z))
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#())
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2))
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__a()) -> a#())
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__e()) -> e#())
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__i()) -> i#())
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__o()) -> o#())
(U51#(tt(), V1, V2) -> activate#(V1), activate#(n__u()) -> u#())
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#())
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2))
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__a()) -> a#())
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__e()) -> e#())
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__i()) -> i#())
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__o()) -> o#())
(U21#(tt(), V1, V2) -> activate#(V1), activate#(n__u()) -> u#())
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#())
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2))
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__a()) -> a#())
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__e()) -> e#())
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__i()) -> i#())
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__o()) -> o#())
(isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__u()) -> u#())
(__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(X, __(Y, Z)))
(__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(Y, Z))
(U71#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#())
(U71#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U71#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(U71#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U71#(tt(), V) -> activate#(V), activate#(n__a()) -> a#())
(U71#(tt(), V) -> activate#(V), activate#(n__e()) -> e#())
(U71#(tt(), V) -> activate#(V), activate#(n__i()) -> i#())
(U71#(tt(), V) -> activate#(V), activate#(n__o()) -> o#())
(U71#(tt(), V) -> activate#(V), activate#(n__u()) -> u#())
(U61#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#())
(U61#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(U61#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(U61#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(U61#(tt(), V) -> activate#(V), activate#(n__a()) -> a#())
(U61#(tt(), V) -> activate#(V), activate#(n__e()) -> e#())
(U61#(tt(), V) -> activate#(V), activate#(n__i()) -> i#())
(U61#(tt(), V) -> activate#(V), activate#(n__o()) -> o#())
(U61#(tt(), V) -> activate#(V), activate#(n__u()) -> u#())
(isList#(V) -> activate#(V), activate#(n__nil()) -> nil#())
(isList#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isList#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(isList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isList#(V) -> activate#(V), activate#(n__a()) -> a#())
(isList#(V) -> activate#(V), activate#(n__e()) -> e#())
(isList#(V) -> activate#(V), activate#(n__i()) -> i#())
(isList#(V) -> activate#(V), activate#(n__o()) -> o#())
(isList#(V) -> activate#(V), activate#(n__u()) -> u#())
(isNeList#(V) -> activate#(V), activate#(n__nil()) -> nil#())
(isNeList#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(isNeList#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2))
(isNeList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2))
(isNeList#(V) -> activate#(V), activate#(n__a()) -> a#())
(isNeList#(V) -> activate#(V), activate#(n__e()) -> e#())
(isNeList#(V) -> activate#(V), activate#(n__i()) -> i#())
(isNeList#(V) -> activate#(V), activate#(n__o()) -> o#())
(isNeList#(V) -> activate#(V), activate#(n__u()) -> u#())
}
SCCS:
Scc:
{isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)),
U71#(tt(), V) -> isNePal#(activate(V)),
isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V))}
Scc:
{activate#(n__isPalListKind(X)) -> isPalListKind#(X),
activate#(n__and(X1, X2)) -> and#(X1, X2),
and#(tt(), X) -> activate#(X),
isPalListKind#(n____(V1, V2)) -> activate#(V1),
isPalListKind#(n____(V1, V2)) -> activate#(V2),
isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))}
Scc:
{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)),
U11#(tt(), V) -> isNeList#(activate(V)),
U22#(tt(), V2) -> isList#(activate(V2)),
isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)),
isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)),
U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)),
U21#(tt(), V1, V2) -> isList#(activate(V1)),
U42#(tt(), V2) -> isNeList#(activate(V2)),
U41#(tt(), V1, V2) -> isList#(activate(V1)),
U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)),
U52#(tt(), V2) -> isList#(activate(V2)),
U51#(tt(), V1, V2) -> isNeList#(activate(V1)),
U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2))}
Scc:
{__#(__(X, Y), Z) -> __#(X, __(Y, Z)),
__#(__(X, Y), Z) -> __#(Y, Z)}
SCC:
Strict:
{isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)),
U71#(tt(), V) -> isNePal#(activate(V)),
isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V))}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
POLY:
Argument Filtering:
pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(n__u) = [], pi(n__o) = [], pi(n__i) = [], pi(n__e) = [], pi(n__a) = [], pi(isPal#) = 0, pi(isPal) = [], pi(n__and) = 1, pi(n____) = [0,1], pi(n__isPalListKind) = [], pi(n__nil) = [], pi(isPalListKind) = [], pi(and) = 1, pi(U71#) = 1, pi(U71) = [], pi(isNePal#) = 0, pi(isNePal) = [], pi(U72) = [], pi(U61) = [], pi(U62) = [], pi(U53) = [], pi(U51) = [], pi(U52) = [], pi(U43) = [], pi(U41) = [], pi(U42) = [], pi(U31) = [], pi(isQid) = [], pi(U32) = [], pi(U23) = [], pi(U21) = [], pi(isList) = [], pi(U22) = [], pi(tt) = [], pi(U11) = [], pi(activate) = 0, pi(isNeList) = [], pi(U12) = [], pi(nil) = [], pi(__) = [0,1]
Usable Rules:
{}
Interpretation:
[n____](x0, x1) = x0 + x1 + 1,
[__](x0, x1) = x0 + x1 + 1
Strict:
{U71#(tt(), V) -> isNePal#(activate(V)),
isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V))}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
EDG:
{(isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> isNePal#(activate(V)))}
SCCS:
Qed
SCC:
Strict:
{activate#(n__isPalListKind(X)) -> isPalListKind#(X),
activate#(n__and(X1, X2)) -> and#(X1, X2),
and#(tt(), X) -> activate#(X),
isPalListKind#(n____(V1, V2)) -> activate#(V1),
isPalListKind#(n____(V1, V2)) -> activate#(V2),
isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
POLY:
Argument Filtering:
pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(n__u) = [], pi(n__o) = [], pi(n__i) = [], pi(n__e) = [], pi(n__a) = [], pi(isPal) = [], pi(n__and) = 1, pi(n____) = [0,1], pi(n__isPalListKind) = 0, pi(n__nil) = [], pi(isPalListKind#) = 0, pi(isPalListKind) = 0, pi(and#) = 1, pi(and) = 1, pi(U71) = [], pi(isNePal) = [], pi(U72) = [], pi(U61) = [], pi(U62) = [], pi(U53) = [], pi(U51) = [], pi(U52) = [], pi(U43) = [], pi(U41) = [], pi(U42) = [], pi(U31) = [], pi(isQid) = [], pi(U32) = [], pi(U23) = [], pi(U21) = [], pi(isList) = [], pi(U22) = [], pi(tt) = [], pi(U11) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNeList) = [], pi(U12) = [], pi(nil) = [], pi(__) = [0,1]
Usable Rules:
{}
Interpretation:
[n____](x0, x1) = x0 + x1 + 1
Strict:
{activate#(n__isPalListKind(X)) -> isPalListKind#(X),
activate#(n__and(X1, X2)) -> and#(X1, X2),
and#(tt(), X) -> activate#(X)}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
EDG:
{(and#(tt(), X) -> activate#(X), activate#(n__isPalListKind(X)) -> isPalListKind#(X))
(and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2))
(activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X))}
SCCS:
Scc:
{activate#(n__and(X1, X2)) -> and#(X1, X2),
and#(tt(), X) -> activate#(X)}
SCC:
Strict:
{activate#(n__and(X1, X2)) -> and#(X1, X2),
and#(tt(), X) -> activate#(X)}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
SPSC:
Simple Projection:
pi(and#) = 1, pi(activate#) = 0
Strict:
{and#(tt(), X) -> activate#(X)}
EDG:
{}
SCCS:
Qed
SCC:
Strict:
{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)),
U11#(tt(), V) -> isNeList#(activate(V)),
U22#(tt(), V2) -> isList#(activate(V2)),
isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)),
isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)),
U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)),
U21#(tt(), V1, V2) -> isList#(activate(V1)),
U42#(tt(), V2) -> isNeList#(activate(V2)),
U41#(tt(), V1, V2) -> isList#(activate(V1)),
U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)),
U52#(tt(), V2) -> isList#(activate(V2)),
U51#(tt(), V1, V2) -> isNeList#(activate(V1)),
U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2))}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
POLY:
Argument Filtering:
pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(n__u) = [], pi(n__o) = [], pi(n__i) = [], pi(n__e) = [], pi(n__a) = [], pi(isPal) = [], pi(n__and) = 1, pi(n____) = [0,1], pi(n__isPalListKind) = [], pi(n__nil) = [], pi(isPalListKind) = [], pi(and) = 1, pi(U71) = [], pi(isNePal) = [], pi(U72) = [], pi(U61) = [], pi(U62) = [], pi(U53) = [], pi(U51#) = [0,1,2], pi(U51) = [], pi(U52#) = [1], pi(U52) = [], pi(U43) = [], pi(U41#) = [0,1,2], pi(U41) = [], pi(U42#) = [0,1], pi(U42) = [], pi(U31) = [], pi(isQid) = [], pi(U32) = [], pi(U23) = 0, pi(U21#) = [0,1,2], pi(U21) = [0,2], pi(isList#) = [0], pi(isList) = [0], pi(U22#) = [0,1], pi(U22) = [1], pi(tt) = [], pi(U11#) = [1], pi(U11) = [], pi(activate) = 0, pi(isNeList#) = [0], pi(isNeList) = [], pi(U12) = [], pi(nil) = [], pi(__) = [0,1]
Usable Rules:
{}
Interpretation:
[U51#](x0, x1, x2) = x0 + x1 + x2 + 1,
[U41#](x0, x1, x2) = x0 + x1 + x2 + 1,
[U21#](x0, x1, x2) = x0 + x1 + x2,
[U52#](x0) = x0 + 1,
[U42#](x0, x1) = x0 + x1 + 1,
[U22#](x0, x1) = x0 + x1,
[U11#](x0) = x0 + 1,
[isList#](x0) = x0 + 1,
[isNeList#](x0) = x0 + 1,
[n____](x0, x1) = x0 + x1 + 1,
[n__isPalListKind] = 1,
[isList](x0) = x0 + 1,
[tt] = 1
Strict:
{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)),
U11#(tt(), V) -> isNeList#(activate(V)),
U22#(tt(), V2) -> isList#(activate(V2)),
isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)),
U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)),
U21#(tt(), V1, V2) -> isList#(activate(V1)),
U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)),
U52#(tt(), V2) -> isList#(activate(V2))}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
EDG:
{(U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)))
(U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> isList#(activate(V2)))
(isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> isNeList#(activate(V)))
(isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)))
(U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))
(U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))}
SCCS:
Qed
SCC:
Strict:
{__#(__(X, Y), Z) -> __#(X, __(Y, Z)),
__#(__(X, Y), Z) -> __#(Y, Z)}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
SPSC:
Simple Projection:
pi(__#) = 0
Strict:
{__#(__(X, Y), Z) -> __#(Y, Z)}
EDG:
{(__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(Y, Z))}
SCCS:
Scc:
{__#(__(X, Y), Z) -> __#(Y, Z)}
SCC:
Strict:
{__#(__(X, Y), Z) -> __#(Y, Z)}
Weak:
{ __(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U12(tt()) -> tt(),
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)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n__isPalListKind(X)) -> isPalListKind(X),
activate(n____(X1, X2)) -> __(X1, X2),
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(),
U11(tt(), V) -> U12(isNeList(activate(V))),
U22(tt(), V2) -> U23(isList(activate(V2))),
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)),
U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)),
U23(tt()) -> tt(),
U32(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
U31(tt(), V) -> U32(isQid(activate(V))),
U42(tt(), V2) -> U43(isNeList(activate(V2))),
U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)),
U43(tt()) -> tt(),
U52(tt(), V2) -> U53(isList(activate(V2))),
U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)),
U53(tt()) -> tt(),
U62(tt()) -> tt(),
U61(tt(), V) -> U62(isQid(activate(V))),
U72(tt()) -> tt(),
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)))),
U71(tt(), V) -> U72(isNePal(activate(V))),
and(X1, X2) -> n__and(X1, X2),
and(tt(), X) -> activate(X),
isPalListKind(X) -> n__isPalListKind(X),
isPalListKind(n__nil()) -> tt(),
isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))),
isPalListKind(n__a()) -> tt(),
isPalListKind(n__e()) -> tt(),
isPalListKind(n__i()) -> tt(),
isPalListKind(n__o()) -> tt(),
isPalListKind(n__u()) -> tt(),
isPal(V) -> U71(isPalListKind(activate(V)), activate(V)),
isPal(n__nil()) -> tt(),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()}
SPSC:
Simple Projection:
pi(__#) = 0
Strict:
{}
Qed