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