(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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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, n____(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
ISNEPAL(n____(I, n____(P, I))) → ISQID(activate(I))
ISNEPAL(n____(I, n____(P, I))) → ACTIVATE(I)
ISNEPAL(n____(I, n____(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(activate(X1), activate(X2))
ACTIVATE(n____(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n____(X1, X2)) → ACTIVATE(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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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 5 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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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)  =  __1(x1)
__(x1, x2)  =  __(x1, x2)
nil  =  nil
U11(x1, x2)  =  U11
tt  =  tt
U12(x1, x2)  =  U12
isPalListKind(x1)  =  x1
activate(x1)  =  activate(x1)
U13(x1)  =  U13
isNeList(x1)  =  isNeList(x1)
U21(x1, x2, x3)  =  U21
U22(x1, x2, x3)  =  U22
U23(x1, x2, x3)  =  U23
U24(x1, x2, x3)  =  U24
U25(x1, x2)  =  U25
isList(x1)  =  isList
U26(x1)  =  U26
U31(x1, x2)  =  U31(x2)
U32(x1, x2)  =  U32
U33(x1)  =  x1
isQid(x1)  =  isQid
U41(x1, x2, x3)  =  U41(x2, x3)
U42(x1, x2, x3)  =  U42(x2, x3)
U43(x1, x2, x3)  =  U43(x2, x3)
U44(x1, x2, x3)  =  x2
U45(x1, x2)  =  U45
U46(x1)  =  U46
U51(x1, x2, x3)  =  U51(x2, x3)
U52(x1, x2, x3)  =  U52(x1, x3)
U53(x1, x2, x3)  =  x1
U54(x1, x2, x3)  =  U54
U55(x1, x2)  =  U55
U56(x1)  =  U56
U61(x1, x2)  =  U61(x1, x2)
U62(x1, x2)  =  U62(x2)
U63(x1)  =  U63(x1)
U71(x1, x2, x3)  =  U71(x2, x3)
U72(x1, x2)  =  U72(x1, x2)
U73(x1, x2)  =  U73(x1, x2)
isPal(x1)  =  isPal
U74(x1)  =  U74
U81(x1, x2)  =  U81
U82(x1, x2)  =  U82
U83(x1)  =  U83
isNePal(x1)  =  isNePal(x1)
U91(x1, x2)  =  U91
U92(x1)  =  U92
n__nil  =  n__nil
n____(x1, x2)  =  n____(x1, x2)
n__a  =  n__a
n__e  =  n__e
n__i  =  n__i
n__o  =  n__o
n__u  =  n__u
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Lexicographic Path Order [LPO].
Precedence:
_^11 > _2 > n2 > [U32, isQid] > [tt, U45, U46, U54, U55, U56]
_^11 > _2 > n2 > [U91, U92] > [tt, U45, U46, U54, U55, U56]
isNeList1 > U311 > [U32, isQid] > [tt, U45, U46, U54, U55, U56]
isNeList1 > U412 > U422 > U432 > [activate1, e] > _2 > n2 > [U32, isQid] > [tt, U45, U46, U54, U55, U56]
isNeList1 > U412 > U422 > U432 > [activate1, e] > _2 > n2 > [U91, U92] > [tt, U45, U46, U54, U55, U56]
isNeList1 > U412 > U422 > U432 > [activate1, e] > nil > nnil > [tt, U45, U46, U54, U55, U56]
isNeList1 > U412 > U422 > U432 > [activate1, e] > ne > [tt, U45, U46, U54, U55, U56]
isNeList1 > U412 > U422 > U432 > [activate1, e] > a > na > [tt, U45, U46, U54, U55, U56]
isNeList1 > U412 > U422 > U432 > [activate1, e] > i > ni > [tt, U45, U46, U54, U55, U56]
isNeList1 > U512 > U522 > [activate1, e] > _2 > n2 > [U32, isQid] > [tt, U45, U46, U54, U55, U56]
isNeList1 > U512 > U522 > [activate1, e] > _2 > n2 > [U91, U92] > [tt, U45, U46, U54, U55, U56]
isNeList1 > U512 > U522 > [activate1, e] > nil > nnil > [tt, U45, U46, U54, U55, U56]
isNeList1 > U512 > U522 > [activate1, e] > ne > [tt, U45, U46, U54, U55, U56]
isNeList1 > U512 > U522 > [activate1, e] > a > na > [tt, U45, U46, U54, U55, U56]
isNeList1 > U512 > U522 > [activate1, e] > i > ni > [tt, U45, U46, U54, U55, U56]
isList > U11 > [U12, U13] > [tt, U45, U46, U54, U55, U56]
isList > [U21, U22, U23, U24, U25] > U26 > [tt, U45, U46, U54, U55, U56]
isNePal1 > U612 > U621 > [activate1, e] > _2 > n2 > [U32, isQid] > [tt, U45, U46, U54, U55, U56]
isNePal1 > U612 > U621 > [activate1, e] > _2 > n2 > [U91, U92] > [tt, U45, U46, U54, U55, U56]
isNePal1 > U612 > U621 > [activate1, e] > nil > nnil > [tt, U45, U46, U54, U55, U56]
isNePal1 > U612 > U621 > [activate1, e] > ne > [tt, U45, U46, U54, U55, U56]
isNePal1 > U612 > U621 > [activate1, e] > a > na > [tt, U45, U46, U54, U55, U56]
isNePal1 > U612 > U621 > [activate1, e] > i > ni > [tt, U45, U46, U54, U55, U56]
isNePal1 > U612 > U621 > U631 > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > [U732, U74] > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > U82 > [activate1, e] > _2 > n2 > [U32, isQid] > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > U82 > [activate1, e] > _2 > n2 > [U91, U92] > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > U82 > [activate1, e] > nil > nnil > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > U82 > [activate1, e] > ne > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > U82 > [activate1, e] > a > na > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > U82 > [activate1, e] > i > ni > [tt, U45, U46, U54, U55, U56]
isNePal1 > U712 > [U722, isPal, U81] > U82 > U83 > [tt, U45, U46, U54, U55, U56]
[no, o] > [tt, U45, U46, U54, U55, U56]
[nu, u] > [tt, U45, U46, U54, U55, U56]


The following usable rules [FROCOS05] were oriented:

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

(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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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:

ACTIVATE(n____(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n____(X1, X2)) → ACTIVATE(X1)

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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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.


ACTIVATE(n____(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n____(X1, X2)) → ACTIVATE(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVATE(x1)  =  ACTIVATE(x1)
n____(x1, x2)  =  n____(x1, x2)
__(x1, x2)  =  __(x1, x2)
nil  =  nil
U11(x1, x2)  =  U11(x1, x2)
tt  =  tt
U12(x1, x2)  =  x2
isPalListKind(x1)  =  isPalListKind(x1)
activate(x1)  =  x1
U13(x1)  =  U13
isNeList(x1)  =  isNeList(x1)
U21(x1, x2, x3)  =  x2
U22(x1, x2, x3)  =  x2
U23(x1, x2, x3)  =  x2
U24(x1, x2, x3)  =  x2
U25(x1, x2)  =  U25
isList(x1)  =  isList(x1)
U26(x1)  =  U26
U31(x1, x2)  =  U31(x1, x2)
U32(x1, x2)  =  x1
U33(x1)  =  x1
isQid(x1)  =  isQid
U41(x1, x2, x3)  =  U41(x2, x3)
U42(x1, x2, x3)  =  U42(x2, x3)
U43(x1, x2, x3)  =  U43(x1, x2, x3)
U44(x1, x2, x3)  =  U44(x2, x3)
U45(x1, x2)  =  U45
U46(x1)  =  U46
U51(x1, x2, x3)  =  U51(x1, x2, x3)
U52(x1, x2, x3)  =  U52(x2, x3)
U53(x1, x2, x3)  =  U53(x1, x2, x3)
U54(x1, x2, x3)  =  U54(x1, x3)
U55(x1, x2)  =  U55
U56(x1)  =  U56
U61(x1, x2)  =  U61
U62(x1, x2)  =  U62
U63(x1)  =  U63
U71(x1, x2, x3)  =  x2
U72(x1, x2)  =  U72
U73(x1, x2)  =  x1
isPal(x1)  =  isPal
U74(x1)  =  U74
U81(x1, x2)  =  U81
U82(x1, x2)  =  U82
U83(x1)  =  U83
isNePal(x1)  =  x1
U91(x1, x2)  =  x1
U92(x1)  =  U92
n__nil  =  n__nil
n__a  =  n__a
n__e  =  n__e
n__i  =  n__i
n__o  =  n__o
n__u  =  n__u
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Lexicographic Path Order [LPO].
Precedence:
ACTIVATE1 > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
[n2, 2] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
[nil, nnil] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
isNeList1 > U312 > isPalListKind1 > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
isNeList1 > U412 > U422 > isPalListKind1 > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
isNeList1 > U412 > U422 > U433 > [U442, U45, U46] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
isNeList1 > U513 > U522 > U533 > isPalListKind1 > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
isNeList1 > U513 > U522 > U533 > [U542, U55, U56] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
isList1 > U112 > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
isList1 > isPalListKind1 > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
[ne, e] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
[ni, i] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
[no, o] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]
[nu, u] > [tt, U13, U25, U26, isQid, U61, U62, U63, U72, isPal, U74, U81, U82, U83, U92, na, a]


The following usable rules [FROCOS05] were oriented:

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

(12) 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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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

(13) PisEmptyProof (EQUIVALENT transformation)

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

(14) TRUE

(15) 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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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.


U911(tt, V2) → ISPALLISTKIND(activate(V2))
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)  =  U911(x2)
tt  =  tt
ISPALLISTKIND(x1)  =  ISPALLISTKIND(x1)
activate(x1)  =  x1
n____(x1, x2)  =  n____(x1, x2)
isPalListKind(x1)  =  isPalListKind
__(x1, x2)  =  __(x1, x2)
nil  =  nil
U11(x1, x2)  =  U11(x2)
U12(x1, x2)  =  x1
U13(x1)  =  U13
isNeList(x1)  =  isNeList(x1)
U21(x1, x2, x3)  =  U21(x1, x2, x3)
U22(x1, x2, x3)  =  U22(x1, x2, x3)
U23(x1, x2, x3)  =  U23(x1, x2, x3)
U24(x1, x2, x3)  =  U24(x1, x2, x3)
U25(x1, x2)  =  U25(x2)
isList(x1)  =  isList(x1)
U26(x1)  =  U26
U31(x1, x2)  =  U31(x1, x2)
U32(x1, x2)  =  U32(x1)
U33(x1)  =  U33(x1)
isQid(x1)  =  isQid
U41(x1, x2, x3)  =  U41(x1, x3)
U42(x1, x2, x3)  =  U42(x1, x3)
U43(x1, x2, x3)  =  U43(x1)
U44(x1, x2, x3)  =  U44(x1)
U45(x1, x2)  =  U45
U46(x1)  =  U46
U51(x1, x2, x3)  =  U51(x2, x3)
U52(x1, x2, x3)  =  U52(x2, x3)
U53(x1, x2, x3)  =  U53(x2, x3)
U54(x1, x2, x3)  =  U54(x1, x2, x3)
U55(x1, x2)  =  U55(x2)
U56(x1)  =  U56
U61(x1, x2)  =  x1
U62(x1, x2)  =  U62
U63(x1)  =  U63
U71(x1, x2, x3)  =  U71
U72(x1, x2)  =  U72(x1)
U73(x1, x2)  =  U73
isPal(x1)  =  isPal(x1)
U74(x1)  =  U74
U81(x1, x2)  =  U81(x2)
U82(x1, x2)  =  U82
U83(x1)  =  U83(x1)
isNePal(x1)  =  isNePal
U91(x1, x2)  =  U91
U92(x1)  =  U92
n__nil  =  n__nil
n__a  =  n__a
n__e  =  n__e
n__i  =  n__i
n__o  =  n__o
n__u  =  n__u
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Lexicographic Path Order [LPO].
Precedence:
[n2, 2] > U91^11 > ISPALLISTKIND1
[nil, nnil] > ISPALLISTKIND1
[U111, isList1] > [U213, U223, U233, U243] > [U251, U26] > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
[isNeList1, U512, U522, U532] > [U312, U321] > U331 > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
[isNeList1, U512, U522, U532] > [U312, U321] > isQid > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
[isNeList1, U512, U522, U532] > [U412, U422, U431, U441, U45] > U46 > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
[isNeList1, U512, U522, U532] > U543 > U551 > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
isPal1 > U811 > U82 > U831 > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
isPal1 > U811 > U82 > isNePal > U71 > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
[na, a] > ISPALLISTKIND1
[ne, e] > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
[ni, i] > [tt, isPalListKind, U13, U56, U62, U63, U73, U74, U91, U92] > U721 > ISPALLISTKIND1
[no, o] > ISPALLISTKIND1
[nu, u] > ISPALLISTKIND1


The following usable rules [FROCOS05] were oriented:

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

(17) 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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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

(18) PisEmptyProof (EQUIVALENT transformation)

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

(19) TRUE

(20) Obligation:

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

ISNEPAL(n____(I, n____(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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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.


ISNEPAL(n____(I, n____(P, I))) → U711(isQid(activate(I)), activate(I), activate(P))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNEPAL(x1)  =  ISNEPAL(x1)
n____(x1, x2)  =  n____(x1, x2)
U711(x1, x2, x3)  =  U711(x3)
isQid(x1)  =  isQid
activate(x1)  =  x1
tt  =  tt
U721(x1, x2)  =  U721(x2)
isPalListKind(x1)  =  isPalListKind(x1)
ISPAL(x1)  =  ISPAL(x1)
U811(x1, x2)  =  U811(x2)
U821(x1, x2)  =  U821(x2)
__(x1, x2)  =  __(x1, x2)
nil  =  nil
U11(x1, x2)  =  U11
U12(x1, x2)  =  U12
U13(x1)  =  x1
isNeList(x1)  =  isNeList
U21(x1, x2, x3)  =  U21
U22(x1, x2, x3)  =  U22
U23(x1, x2, x3)  =  U23
U24(x1, x2, x3)  =  U24
U25(x1, x2)  =  U25
isList(x1)  =  isList
U26(x1)  =  x1
U31(x1, x2)  =  U31
U32(x1, x2)  =  U32
U33(x1)  =  U33(x1)
U41(x1, x2, x3)  =  U41
U42(x1, x2, x3)  =  U42
U43(x1, x2, x3)  =  U43
U44(x1, x2, x3)  =  U44
U45(x1, x2)  =  U45
U46(x1)  =  U46
U51(x1, x2, x3)  =  U51
U52(x1, x2, x3)  =  U52
U53(x1, x2, x3)  =  U53
U54(x1, x2, x3)  =  U54
U55(x1, x2)  =  U55
U56(x1)  =  U56
U61(x1, x2)  =  U61
U62(x1, x2)  =  U62
U63(x1)  =  U63
U71(x1, x2, x3)  =  U71
U72(x1, x2)  =  U72
U73(x1, x2)  =  U73
isPal(x1)  =  isPal
U74(x1)  =  U74
U81(x1, x2)  =  U81
U82(x1, x2)  =  U82
U83(x1)  =  U83
isNePal(x1)  =  isNePal
U91(x1, x2)  =  U91(x1, x2)
U92(x1)  =  x1
n__nil  =  n__nil
n__a  =  n__a
n__e  =  n__e
n__i  =  n__i
n__o  =  n__o
n__u  =  n__u
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Lexicographic Path Order [LPO].
Precedence:
[ISNEPAL1, U71^11, U72^11, ISPAL1, U81^11, U82^11] > isQid > [tt, isPalListKind1, U63, na, a]
[n2, 2] > [U51, U52, U53] > U54 > [U55, U56] > [tt, isPalListKind1, U63, na, a]
[n2, 2] > U912 > [tt, isPalListKind1, U63, na, a]
[nil, nnil]
[U21, U22, U23, U24, U25, isList] > U11 > [U12, isNeList, U31, U32, U41, U42] > isQid > [tt, isPalListKind1, U63, na, a]
[U21, U22, U23, U24, U25, isList] > U11 > [U12, isNeList, U31, U32, U41, U42] > U331 > [tt, isPalListKind1, U63, na, a]
[U21, U22, U23, U24, U25, isList] > U11 > [U12, isNeList, U31, U32, U41, U42] > [U43, U44] > [U45, U46] > [tt, isPalListKind1, U63, na, a]
[U21, U22, U23, U24, U25, isList] > U11 > [U12, isNeList, U31, U32, U41, U42] > [U51, U52, U53] > U54 > [U55, U56] > [tt, isPalListKind1, U63, na, a]
[U71, isNePal] > isQid > [tt, isPalListKind1, U63, na, a]
[U71, isNePal] > U61 > U62 > [tt, isPalListKind1, U63, na, a]
[U71, isNePal] > U72 > [U73, U74] > [tt, isPalListKind1, U63, na, a]
isPal > [U81, U82, U83] > [tt, isPalListKind1, U63, na, a]
[ne, e]
[ni, i]
[no, o]
[nu, u]


The following usable rules [FROCOS05] were oriented:

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

(22) 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))
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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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 5 less nodes.

(24) TRUE

(25) 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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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

(26) 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))
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))
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))
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))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
ISLIST(n____(V1, V2)) → U211(isPalListKind(activate(V1)), 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 remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
U111(x1, x2)  =  U111(x1, x2)
tt  =  tt
U121(x1, x2)  =  U121(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(x1)
U511(x1, x2, x3)  =  U511(x2, x3)
U521(x1, x2, x3)  =  U521(x2, x3)
U531(x1, x2, x3)  =  U531(x1, x2, x3)
U541(x1, x2, x3)  =  U541(x2, x3)
U551(x1, x2)  =  U551(x2)
isNeList(x1)  =  isNeList(x1)
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(x2)
__(x1, x2)  =  __(x1, x2)
nil  =  nil
U11(x1, x2)  =  U11(x2)
U12(x1, x2)  =  x1
U13(x1)  =  U13
U21(x1, x2, x3)  =  U21(x2, x3)
U22(x1, x2, x3)  =  U22(x2, x3)
U23(x1, x2, x3)  =  U23(x2, x3)
U24(x1, x2, x3)  =  U24(x1, x2, x3)
U25(x1, x2)  =  U25(x1, x2)
U26(x1)  =  U26
U31(x1, x2)  =  U31(x2)
U32(x1, x2)  =  U32(x1)
U33(x1)  =  U33
isQid(x1)  =  isQid(x1)
U41(x1, x2, x3)  =  x3
U42(x1, x2, x3)  =  x3
U43(x1, x2, x3)  =  x3
U44(x1, x2, x3)  =  x1
U45(x1, x2)  =  U45
U46(x1)  =  U46
U51(x1, x2, x3)  =  U51(x1, x3)
U52(x1, x2, x3)  =  x3
U53(x1, x2, x3)  =  x1
U54(x1, x2, x3)  =  U54
U55(x1, x2)  =  U55
U56(x1)  =  U56
U61(x1, x2)  =  U61(x1, x2)
U62(x1, x2)  =  U62(x1, x2)
U63(x1)  =  U63(x1)
U71(x1, x2, x3)  =  U71(x2, x3)
U72(x1, x2)  =  U72(x2)
U73(x1, x2)  =  U73(x2)
isPal(x1)  =  x1
U74(x1)  =  U74
U81(x1, x2)  =  x2
U82(x1, x2)  =  x1
U83(x1)  =  U83
isNePal(x1)  =  isNePal(x1)
U91(x1, x2)  =  U91(x1, x2)
U92(x1)  =  x1
n__nil  =  n__nil
n__a  =  n__a
n__e  =  n__e
n__i  =  n__i
n__o  =  n__o
n__u  =  n__u
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Lexicographic Path Order [LPO].
Precedence:
[n2, 2, U212, U222] > U41^12 > [U42^12, U43^12, U44^12] > U45^11
[n2, 2, U212, U222] > U41^12 > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > U45^11
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U51^12, U52^12] > U53^13 > U54^12 > [U55^11, ISLIST1] > U11^12 > U12^11
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U21^12, U22^12, U23^12, U24^12] > U25^11 > [U55^11, ISLIST1] > U11^12 > U12^11
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U252
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U321
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > isQid1
[n2, 2, U212, U222] > U232 > U243 > [isList1, U111] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > U631
[n2, 2, U212, U222] > U512
[n2, 2, U212, U222] > U912
isNeList1 > U311 > U321
isNeList1 > U512
[U712, isNePal1] > U612 > U622 > isQid1
[U712, isNePal1] > U612 > U622 > U631
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > U45^11
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U51^12, U52^12] > U53^13 > U54^12 > [U55^11, ISLIST1] > U11^12 > U12^11
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U21^12, U22^12, U23^12, U24^12] > U25^11 > [U55^11, ISLIST1] > U11^12 > U12^11
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U252
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U321
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > isQid1
[U712, isNePal1] > [U721, U731] > U74 > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > U631
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > U45^11
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U51^12, U52^12] > U53^13 > U54^12 > [U55^11, ISLIST1] > U11^12 > U12^11
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U21^12, U22^12, U23^12, U24^12] > U25^11 > [U55^11, ISLIST1] > U11^12 > U12^11
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U252
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U321
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > isQid1
[na, a] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > U631
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > U45^11
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U51^12, U52^12] > U53^13 > U54^12 > [U55^11, ISLIST1] > U11^12 > U12^11
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U21^12, U22^12, U23^12, U24^12] > U25^11 > [U55^11, ISLIST1] > U11^12 > U12^11
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U252
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U321
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > isQid1
[ne, e] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > U631
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > U45^11
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U51^12, U52^12] > U53^13 > U54^12 > [U55^11, ISLIST1] > U11^12 > U12^11
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U21^12, U22^12, U23^12, U24^12] > U25^11 > [U55^11, ISLIST1] > U11^12 > U12^11
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U252
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U321
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > isQid1
[ni, i] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > U631
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > U45^11
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U51^12, U52^12] > U53^13 > U54^12 > [U55^11, ISLIST1] > U11^12 > U12^11
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U21^12, U22^12, U23^12, U24^12] > U25^11 > [U55^11, ISLIST1] > U11^12 > U12^11
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U252
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U321
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > isQid1
[no, o] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > U631
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > U45^11
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U42^12, U43^12, U44^12] > [U55^11, ISLIST1] > U11^12 > U12^11
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U51^12, U52^12] > U53^13 > U54^12 > [U55^11, ISLIST1] > U11^12 > U12^11
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > [U21^12, U22^12, U23^12, U24^12] > U25^11 > [U55^11, ISLIST1] > U11^12 > U12^11
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U252
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U321
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > isQid1
[nu, u] > [tt, nil, U13, U26, U33, U45, U46, U54, U55, U56, U83, nnil] > U622 > U631


The following usable rules [FROCOS05] were oriented:

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

(27) Obligation:

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

U421(tt, V1, V2) → U431(isPalListKind(activate(V2)), activate(V1), activate(V2))
U431(tt, V1, V2) → U441(isPalListKind(activate(V2)), activate(V1), activate(V2))
U511(tt, V1, V2) → U521(isPalListKind(activate(V1)), activate(V1), activate(V2))
U551(tt, V2) → ISLIST(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))

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, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
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)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) TRUE