(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)  =  __1(x1, x2)
__(x1, x2)  =  __(x1, x2)
nil  =  nil
n____(x1, x2)  =  n____

Lexicographic path order with status [LPO].
Quasi-Precedence:
_^12 > [2, n]
nil > [2, n]

Status:
_^12: [1,2]
_2: [1,2]
nil: []
n: []


The following usable rules [FROCOS05] were oriented:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(X1, X2) → n____(X1, X2)

(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.


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(x1, x2)
tt  =  tt
ISPALLISTKIND(x1)  =  x1
activate(x1)  =  activate(x1)
n____(x1, x2)  =  n____(x1, x2)
isPalListKind(x1)  =  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)  =  x1
U92(x1)  =  U92

Lexicographic path order with status [LPO].
Quasi-Precedence:
[n2, 2] > [U91^12, activate1, nil, e] > ne > [tt, nnil, U92]
[na, a] > [tt, nnil, U92]
[ni, i] > [tt, nnil, U92]
[no, o] > [tt, nnil, U92]
[nu, u] > [tt, nnil, U92]

Status:
U91^12: [2,1]
tt: []
activate1: [1]
n2: [1,2]
nnil: []
nil: []
_2: [1,2]
na: []
a: []
ne: []
e: []
ni: []
i: []
no: []
o: []
nu: []
u: []
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))
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

(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, __(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) 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:

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))
U711(tt, I, P) → U721(isPalListKind(activate(I)), activate(P))
U721(tt, P) → ISPAL(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)
__(x1, x2)  =  __(x1, x2)
U711(x1, x2, x3)  =  U711(x1, x2, x3)
isQid(x1)  =  x1
activate(x1)  =  x1
tt  =  tt
U721(x1, x2)  =  U721(x1, x2)
isPalListKind(x1)  =  isPalListKind(x1)
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(x2)
U92(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
[n2, 2, U71^13] > [tt, U72^12, na, a, ne, e, ni, i] > [ISNEPAL1, ISPAL1, U81^11, U82^11] > [isPalListKind1, U911]
[nnil, nil] > [tt, U72^12, na, a, ne, e, ni, i] > [ISNEPAL1, ISPAL1, U81^11, U82^11] > [isPalListKind1, U911]
[no, o] > [tt, U72^12, na, a, ne, e, ni, i] > [ISNEPAL1, ISPAL1, U81^11, U82^11] > [isPalListKind1, U911]
[nu, u] > [tt, U72^12, na, a, ne, e, ni, i] > [ISNEPAL1, ISPAL1, U81^11, U82^11] > [isPalListKind1, U911]

Status:
ISNEPAL1: [1]
n2: [1,2]
_2: [1,2]
U71^13: [1,2,3]
tt: []
U72^12: [1,2]
isPalListKind1: [1]
ISPAL1: [1]
U81^11: [1]
U82^11: [1]
nnil: []
nil: []
na: []
a: []
ne: []
e: []
ni: []
i: []
no: []
o: []
nu: []
u: []
U911: [1]


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
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → 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))
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

(17) Obligation:

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

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.

(18) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 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))
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 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)  =  U121(x2)
isPalListKind(x1)  =  isPalListKind
activate(x1)  =  activate(x1)
ISNELIST(x1)  =  x1
n____(x1, x2)  =  n____(x1, x2)
U411(x1, x2, x3)  =  U411(x1, x2, x3)
U421(x1, x2, x3)  =  U421(x1, x2, x3)
U431(x1, x2, x3)  =  U431(x1, x2, x3)
U441(x1, x2, x3)  =  U441(x1, x2, x3)
U451(x1, x2)  =  U451(x1, x2)
isList(x1)  =  isList
U511(x1, x2, x3)  =  U511(x1, x2, x3)
U521(x1, x2, x3)  =  U521(x1, 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(x1, x2, x3)
U221(x1, x2, x3)  =  U221(x2, x3)
U231(x1, x2, x3)  =  U231(x1, x2, x3)
U241(x1, x2, x3)  =  U241(x2, x3)
U251(x1, x2)  =  U251(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)  =  x1
U11(x1, x2)  =  U11
U21(x1, x2, x3)  =  U21
U31(x1, x2)  =  U31
U41(x1, x2, x3)  =  U41
U51(x1, x2, x3)  =  x1
U42(x1, x2, x3)  =  U42
U12(x1, x2)  =  U12
U22(x1, x2, x3)  =  U22
U52(x1, x2, x3)  =  U52
U43(x1, x2, x3)  =  U43
U13(x1)  =  x1
U23(x1, x2, x3)  =  U23
U53(x1, x2, x3)  =  U53
U44(x1, x2, x3)  =  U44
U24(x1, x2, x3)  =  x1
U54(x1, x2, x3)  =  U54
U45(x1, x2)  =  U45
U25(x1, x2)  =  U25
U55(x1, x2)  =  U55
U46(x1)  =  U46
U26(x1)  =  U26
U56(x1)  =  U56
U32(x1, x2)  =  U32
U33(x1)  =  x1
isQid(x1)  =  isQid
U92(x1)  =  U92

Lexicographic path order with status [LPO].
Quasi-Precedence:
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > U45^12 > [activate1, a, e, o] > na
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > U45^12 > [activate1, a, e, o] > ne
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > U45^12 > [activate1, a, e, o] > i > ni
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > U45^12 > [activate1, a, e, o] > no
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U41^13 > U42^13 > U43^13 > U44^13 > [isList, U11, U21] > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U51^13 > U52^13 > U53^12 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > [U45, U46] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U21^13 > U22^12 > U23^13 > [isPalListKind, isNeList, U31, U41, U42, U12, U22, U43, U23, U44, U32] > isQid > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[n2, 2] > U21^13 > U22^12 > U23^13 > U24^12 > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[n2, 2] > U21^13 > U22^12 > U23^13 > U24^12 > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[n2, 2] > U21^13 > U22^12 > U23^13 > U24^12 > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[n2, 2] > U21^13 > U22^12 > U23^13 > U24^12 > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U54^13 > U55^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > na
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > ne
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > i > ni
[nnil, nil] > [tt, U52, U53, U54, U25, U55, U26, U56, U92] > U25^11 > ISLIST1 > U11^11 > U12^11 > [activate1, a, e, o] > no
[nu, u]

Status:
U11^11: [1]
tt: []
U12^11: [1]
isPalListKind: []
activate1: [1]
n2: [1,2]
U41^13: [1,3,2]
U42^13: [3,1,2]
U43^13: [1,2,3]
U44^13: [3,2,1]
U45^12: [1,2]
isList: []
U51^13: [3,2,1]
U52^13: [2,1,3]
U53^12: [2,1]
U54^13: [1,2,3]
U55^11: [1]
isNeList: []
ISLIST1: [1]
U21^13: [3,2,1]
U22^12: [2,1]
U23^13: [1,3,2]
U24^12: [2,1]
U25^11: [1]
nnil: []
nil: []
_2: [1,2]
na: []
a: []
ne: []
e: []
ni: []
i: []
no: []
o: []
nu: []
u: []
U11: []
U21: []
U31: []
U41: []
U42: []
U12: []
U22: []
U52: []
U43: []
U23: []
U53: []
U44: []
U54: []
U45: []
U25: []
U55: []
U46: []
U26: []
U56: []
U32: []
isQid: []
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(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))
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), 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))
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U12(tt, V) → U13(isNeList(activate(V)))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U25(tt, V2) → U26(isList(activate(V2)))
U55(tt, V2) → U56(isList(activate(V2)))
U13(tt) → tt
U26(tt) → tt
U46(tt) → tt
U56(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
U33(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:
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.

(23) PisEmptyProof (EQUIVALENT transformation)

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

(24) TRUE