(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)
U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
U111(tt, V) → ISPALLISTKIND(activate(V))
U111(tt, V) → ACTIVATE(V)
U121(tt, V) → U131(isNeList(activate(V)))
U121(tt, V) → ISNELIST(activate(V))
U121(tt, V) → ACTIVATE(V)
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U211(tt, V1, V2) → ISPALLISTKIND(activate(V1))
U211(tt, V1, V2) → ACTIVATE(V1)
U211(tt, V1, V2) → ACTIVATE(V2)
U221(tt, V1, V2) → U231(isPalListKind(activate(V2)), activate(V1), activate(V2))
U221(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U221(tt, V1, V2) → ACTIVATE(V2)
U221(tt, V1, V2) → ACTIVATE(V1)
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U231(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U231(tt, V1, V2) → ACTIVATE(V2)
U231(tt, V1, V2) → ACTIVATE(V1)
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))
U241(tt, V1, V2) → ISLIST(activate(V1))
U241(tt, V1, V2) → ACTIVATE(V1)
U241(tt, V1, V2) → ACTIVATE(V2)
U251(tt, V2) → U261(isList(activate(V2)))
U251(tt, V2) → ISLIST(activate(V2))
U251(tt, V2) → ACTIVATE(V2)
U311(tt, V) → U321(isPalListKind(activate(V)), activate(V))
U311(tt, V) → ISPALLISTKIND(activate(V))
U311(tt, V) → ACTIVATE(V)
U321(tt, V) → U331(isQid(activate(V)))
U321(tt, V) → ISQID(activate(V))
U321(tt, V) → ACTIVATE(V)
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U411(tt, V1, V2) → ISPALLISTKIND(activate(V1))
U411(tt, V1, V2) → ACTIVATE(V1)
U411(tt, V1, V2) → ACTIVATE(V2)
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U421(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U421(tt, V1, V2) → ACTIVATE(V2)
U421(tt, V1, V2) → ACTIVATE(V1)
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U431(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U431(tt, V1, V2) → ACTIVATE(V2)
U431(tt, V1, V2) → ACTIVATE(V1)
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
U441(tt, V1, V2) → ISLIST(activate(V1))
U441(tt, V1, V2) → ACTIVATE(V1)
U441(tt, V1, V2) → ACTIVATE(V2)
U451(tt, V2) → U461(isNeList(activate(V2)))
U451(tt, V2) → ISNELIST(activate(V2))
U451(tt, V2) → ACTIVATE(V2)
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
U511(tt, V1, V2) → ISPALLISTKIND(activate(V1))
U511(tt, V1, V2) → ACTIVATE(V1)
U511(tt, V1, V2) → ACTIVATE(V2)
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
U521(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U521(tt, V1, V2) → ACTIVATE(V2)
U521(tt, V1, V2) → ACTIVATE(V1)
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U531(tt, V1, V2) → ISPALLISTKIND(activate(V2))
U531(tt, V1, V2) → ACTIVATE(V2)
U531(tt, V1, V2) → ACTIVATE(V1)
U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
U541(tt, V1, V2) → ISNELIST(activate(V1))
U541(tt, V1, V2) → ACTIVATE(V1)
U541(tt, V1, V2) → ACTIVATE(V2)
U551(tt, V2) → U561(isList(activate(V2)))
U551(tt, V2) → ISLIST(activate(V2))
U551(tt, V2) → ACTIVATE(V2)
U611(tt, V) → U621(isPalListKind(activate(V)), activate(V))
U611(tt, V) → ISPALLISTKIND(activate(V))
U611(tt, V) → ACTIVATE(V)
U621(tt, V) → U631(isQid(activate(V)))
U621(tt, V) → ISQID(activate(V))
U621(tt, V) → ACTIVATE(V)
U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
U711(tt, I, P) → ISPALLISTKIND(activate(I))
U711(tt, I, P) → ACTIVATE(I)
U711(tt, I, P) → ACTIVATE(P)
U721(tt, P) → U731(isPal(activate(P)), activate(P))
U721(tt, P) → ISPAL(activate(P))
U721(tt, P) → ACTIVATE(P)
U731(tt, P) → U741(isPalListKind(activate(P)))
U731(tt, P) → ISPALLISTKIND(activate(P))
U731(tt, P) → ACTIVATE(P)
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))
U811(tt, V) → ISPALLISTKIND(activate(V))
U811(tt, V) → ACTIVATE(V)
U821(tt, V) → U831(isNePal(activate(V)))
U821(tt, V) → ISNEPAL(activate(V))
U821(tt, V) → ACTIVATE(V)
U911(tt, V2) → U921(isPalListKind(activate(V2)))
U911(tt, V2) → ISPALLISTKIND(activate(V2))
U911(tt, V2) → ACTIVATE(V2)
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
ISLIST(V) → ISPALLISTKIND(activate(V))
ISLIST(V) → ACTIVATE(V)
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISLIST(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
ISLIST(n____(V1, V2)) → ACTIVATE(V1)
ISLIST(n____(V1, V2)) → ACTIVATE(V2)
ISNELIST(V) → U311(isPalListKind(activate(V)), activate(V))
ISNELIST(V) → ISPALLISTKIND(activate(V))
ISNELIST(V) → ACTIVATE(V)
ISNELIST(n____(V1, V2)) → U411(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISNELIST(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
ISNELIST(n____(V1, V2)) → ACTIVATE(V1)
ISNELIST(n____(V1, V2)) → ACTIVATE(V2)
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
ISNEPAL(V) → U611(isPalListKind(activate(V)), activate(V))
ISNEPAL(V) → ISPALLISTKIND(activate(V))
ISNEPAL(V) → ACTIVATE(V)
ISNEPAL(n____(I, __(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
ISNEPAL(n____(I, __(P, I))) → ISQID(activate(I))
ISNEPAL(n____(I, __(P, I))) → ACTIVATE(I)
ISNEPAL(n____(I, __(P, I))) → ACTIVATE(P)
ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
ISPAL(V) → ISPALLISTKIND(activate(V))
ISPAL(V) → ACTIVATE(V)
ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V1)
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V2)
ACTIVATE(n__nil) → NIL
ACTIVATE(n____(X1, X2)) → __1(X1, X2)
ACTIVATE(n__a) → A
ACTIVATE(n__e) → E
ACTIVATE(n__i) → I
ACTIVATE(n__o) → O
ACTIVATE(n__u) → U

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 97 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(Y, Z)
__1(__(X, Y), Z) → __1(X, __(Y, Z))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


__1(__(X, Y), Z) → __1(Y, Z)
__1(__(X, Y), Z) → __1(X, __(Y, Z))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
__1(x1, x2)  =  x1
__(x1, x2)  =  __(x1, x2)
nil  =  nil
n____(x1, x2)  =  n____(x1, x2)

Lexicographic Path Order [LPO].
Precedence:
nil > [2, n2]


The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(9) TRUE

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U911(tt, V2) → ISPALLISTKIND(activate(V2))
ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISPALLISTKIND(n____(V1, V2)) → U911(isPalListKind(activate(V1)), activate(V2))
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
U911(x1, x2)  =  x2
tt  =  tt
ISPALLISTKIND(x1)  =  x1
activate(x1)  =  x1
n____(x1, x2)  =  n____(x1, x2)
isPalListKind(x1)  =  isPalListKind(x1)
n__nil  =  n__nil
nil  =  nil
__(x1, x2)  =  __(x1, x2)
n__a  =  n__a
a  =  a
n__e  =  n__e
e  =  e
n__i  =  n__i
i  =  i
n__o  =  n__o
o  =  o
n__u  =  n__u
u  =  u
U91(x1, x2)  =  U91(x2)
U92(x1)  =  U92(x1)

Lexicographic Path Order [LPO].
Precedence:
[n2, 2] > [tt, isPalListKind1, nnil, nil, na, a, ne, e, ni, i, no, o, nu, u, U911, U921]


The following usable rules [FROCOS05] were oriented:

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
activate(X) → X
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(X1, X2) → n____(X1, X2)
niln__nil
an__a
en__e
in__i
on__o
un__u

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U911(tt, V2) → ISPALLISTKIND(activate(V2))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(14) TRUE

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNEPAL(n____(I, __(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
U721(tt, P) → ISPAL(activate(P))
ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))
U821(tt, V) → ISNEPAL(activate(V))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNEPAL(n____(I, __(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
U821(tt, V) → ISNEPAL(activate(V))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNEPAL(x1)  =  x1
n____(x1, x2)  =  n____(x1, x2)
__(x1, x2)  =  __(x1, x2)
U711(x1, x2, x3)  =  U711(x3)
isQid(x1)  =  isQid(x1)
activate(x1)  =  x1
tt  =  tt
U721(x1, x2)  =  U721(x2)
isPalListKind(x1)  =  isPalListKind
ISPAL(x1)  =  ISPAL(x1)
U811(x1, x2)  =  U811(x2)
U821(x1, x2)  =  U821(x2)
n__nil  =  n__nil
nil  =  nil
n__a  =  n__a
a  =  a
n__e  =  n__e
e  =  e
n__i  =  n__i
i  =  i
n__o  =  n__o
o  =  o
n__u  =  n__u
u  =  u
U91(x1, x2)  =  U91
U92(x1)  =  U92(x1)

Lexicographic Path Order [LPO].
Precedence:
isPalListKind > tt > [n2, 2, U71^11, isQid1, U72^11, ISPAL1, U81^11, U82^11, U91, U921]
[nnil, nil] > [n2, 2, U71^11, isQid1, U72^11, ISPAL1, U81^11, U82^11, U91, U921]
[na, a] > [n2, 2, U71^11, isQid1, U72^11, ISPAL1, U81^11, U82^11, U91, U921]
[ne, e] > [n2, 2, U71^11, isQid1, U72^11, ISPAL1, U81^11, U82^11, U91, U921]
[ni, i] > [n2, 2, U71^11, isQid1, U72^11, ISPAL1, U81^11, U82^11, U91, U921]
[no, o] > [n2, 2, U71^11, isQid1, U72^11, ISPAL1, U81^11, U82^11, U91, U921]
[nu, u] > [n2, 2, U71^11, isQid1, U72^11, ISPAL1, U81^11, U82^11, U91, U921]


The following usable rules [FROCOS05] were oriented:

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
activate(X) → X
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(X1, X2) → n____(X1, X2)
niln__nil
an__a
en__e
in__i
on__o
un__u

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
U721(tt, P) → ISPAL(activate(P))
ISPAL(V) → U811(isPalListKind(activate(V)), activate(V))
U811(tt, V) → U821(isPalListKind(activate(V)), activate(V))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.

(19) TRUE

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
U121(tt, V) → ISNELIST(activate(V))
ISNELIST(n____(V1, V2)) → U411(isPalListKind(activate(V1)), activate(V1), activate(V2))
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
U451(tt, V2) → ISNELIST(activate(V2))
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
U551(tt, V2) → ISLIST(activate(V2))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U221(tt, V1, V2) → U231(isPalListKind(activate(V2)), activate(V1), activate(V2))
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))
U251(tt, V2) → ISLIST(activate(V2))
U241(tt, V1, V2) → ISLIST(activate(V1))
U541(tt, V1, V2) → ISNELIST(activate(V1))
U441(tt, V1, V2) → ISLIST(activate(V1))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U111(tt, V) → U121(isPalListKind(activate(V)), activate(V))
ISNELIST(n____(V1, V2)) → U411(isPalListKind(activate(V1)), activate(V1), activate(V2))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U441(tt, V1, V2) → U451(isList(activate(V1)), activate(V2))
U451(tt, V2) → ISNELIST(activate(V2))
ISNELIST(n____(V1, V2)) → U511(isPalListKind(activate(V1)), activate(V1), activate(V2))
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
U531(tt, V1, V2) → U541(isPalListKind(activate(V2)), activate(V1), activate(V2))
U541(tt, V1, V2) → U551(isNeList(activate(V1)), activate(V2))
U551(tt, V2) → ISLIST(activate(V2))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), activate(V1), activate(V2))
U231(tt, V1, V2) → U241(isPalListKind(activate(V2)), activate(V1), activate(V2))
U251(tt, V2) → ISLIST(activate(V2))
U241(tt, V1, V2) → ISLIST(activate(V1))
U541(tt, V1, V2) → ISNELIST(activate(V1))
U441(tt, V1, V2) → ISLIST(activate(V1))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
U111(x1, x2)  =  U111(x2)
tt  =  tt
U121(x1, x2)  =  x2
isPalListKind(x1)  =  x1
activate(x1)  =  x1
ISNELIST(x1)  =  x1
n____(x1, x2)  =  n____(x1, x2)
U411(x1, x2, x3)  =  U411(x2, x3)
U421(x1, x2, x3)  =  U421(x2, x3)
U431(x1, x2, x3)  =  U431(x2, x3)
U441(x1, x2, x3)  =  U441(x2, x3)
U451(x1, x2)  =  U451(x2)
isList(x1)  =  isList
U511(x1, x2, x3)  =  U511(x2, x3)
U521(x1, x2, x3)  =  U521(x2, x3)
U531(x1, x2, x3)  =  U531(x2, x3)
U541(x1, x2, x3)  =  U541(x1, x2, x3)
U551(x1, x2)  =  U551(x2)
isNeList(x1)  =  isNeList
ISLIST(x1)  =  ISLIST(x1)
U211(x1, x2, x3)  =  U211(x2, x3)
U221(x1, x2, x3)  =  U221(x2, x3)
U231(x1, x2, x3)  =  U231(x2, x3)
U241(x1, x2, x3)  =  U241(x2, x3)
U251(x1, x2)  =  U251(x1, x2)
n__nil  =  n__nil
nil  =  nil
__(x1, x2)  =  __(x1, x2)
n__a  =  n__a
a  =  a
n__e  =  n__e
e  =  e
n__i  =  n__i
i  =  i
n__o  =  n__o
o  =  o
n__u  =  n__u
u  =  u
U91(x1, x2)  =  U91
U11(x1, x2)  =  U11
U21(x1, x2, x3)  =  U21
U31(x1, x2)  =  U31
U41(x1, x2, x3)  =  U41
U51(x1, x2, x3)  =  U51
U12(x1, x2)  =  U12
U13(x1)  =  U13
U42(x1, x2, x3)  =  U42
U43(x1, x2, x3)  =  U43
U44(x1, x2, x3)  =  U44
U45(x1, x2)  =  x1
U22(x1, x2, x3)  =  U22
U23(x1, x2, x3)  =  U23
U24(x1, x2, x3)  =  U24
U25(x1, x2)  =  x1
U26(x1)  =  U26
U46(x1)  =  U46
U52(x1, x2, x3)  =  U52
U53(x1, x2, x3)  =  U53
U54(x1, x2, x3)  =  U54
U55(x1, x2)  =  U55
U56(x1)  =  U56
U32(x1, x2)  =  U32
U33(x1)  =  U33(x1)
isQid(x1)  =  isQid(x1)
U92(x1)  =  U92

Lexicographic Path Order [LPO].
Precedence:
[n2, 2] > [U41^12, U42^12, U43^12] > U44^12 > U45^11 > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[n2, 2] > [U41^12, U42^12, U43^12] > U44^12 > ISLIST1 > U11^11 > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[n2, 2] > U51^12 > [U52^12, U53^12] > U54^13 > U55^11 > ISLIST1 > U11^11 > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[n2, 2] > U51^12 > [U52^12, U53^12] > U54^13 > isNeList > U31 > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[n2, 2] > U51^12 > [U52^12, U53^12] > U54^13 > isNeList > [U41, U42] > [U43, U44] > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[n2, 2] > U51^12 > [U52^12, U53^12] > U54^13 > isNeList > U51 > U52 > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[n2, 2] > [U21^12, U22^12, U23^12] > [U24^12, U25^12] > ISLIST1 > U11^11 > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[nnil, nil] > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[na, a] > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[ne, e] > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[ni, i] > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[no, o] > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]
[nu, u] > [tt, isList, U91, U11, U21, U12, U13, U22, U23, U24, U26, U46, U53, U54, U55, U56, U32, U331, isQid1, U92]


The following usable rules [FROCOS05] were oriented:

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
activate(X) → X
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(X1, X2) → n____(X1, X2)
niln__nil
an__a
en__e
in__i
on__o
un__u

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U121(tt, V) → ISNELIST(activate(V))
U411(tt, V1, V2) → U421(isPalListKind(activate(V1)), activate(V1), activate(V2))
U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U521(tt, V1, V2) → U531(isPalListKind(activate(V2)), activate(V1), activate(V2))
U211(tt, V1, V2) → U221(isPalListKind(activate(V1)), activate(V1), activate(V2))
U221(tt, V1, V2) → U231(isPalListKind(activate(V2)), activate(V1), activate(V2))
U241(tt, V1, V2) → U251(isList(activate(V1)), activate(V2))

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
an__a
en__e
in__i
on__o
un__u
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
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 7 less nodes.

(24) TRUE