(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: SCNP Order with the following components:
Level mapping:
Top level AFS:
__1(x0, x1, x2)  =  __1(x1)

Tags:
__1 has argument tags [2,0,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
_2 > [^12, n2]
nil > [^12, n2]

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


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: SCNP Order with the following components:
Level mapping:
Top level AFS:
U911(x0, x1, x2)  =  U911(x0)
ISPALLISTKIND(x0, x1)  =  ISPALLISTKIND(x1)

Tags:
U911 has argument tags [4,0,4] and root tag 0
ISPALLISTKIND has argument tags [0,4] and root tag 1

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
U911(x1, x2)  =  U911(x1, x2)
tt  =  tt
ISPALLISTKIND(x1)  =  ISPALLISTKIND
activate(x1)  =  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)  =  x2
U92(x1)  =  x1

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

Status:
U91^12: [1,2]
tt: []
ISPALLISTKIND: []
n2: [1,2]
nnil: []
nil: []
_2: [1,2]
na: []
a: []
ne: []
e: []
ni: []
i: []
no: []
o: []
nu: []
u: []


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: SCNP Order with the following components:
Level mapping:
Top level AFS:
ISNEPAL(x0, x1)  =  ISNEPAL(x0, x1)
U711(x0, x1, x2, x3)  =  U711(x0)
U721(x0, x1, x2)  =  U721(x0, x1)
ISPAL(x0, x1)  =  ISPAL(x1)
U811(x0, x1, x2)  =  U811(x1, x2)
U821(x0, x1, x2)  =  U821(x2)

Tags:
ISNEPAL has argument tags [0,0] and root tag 4
U711 has argument tags [24,8,16,6] and root tag 5
U721 has argument tags [24,9,27] and root tag 0
ISPAL has argument tags [6,0] and root tag 4
U811 has argument tags [16,0,0] and root tag 4
U821 has argument tags [18,11,0] and root tag 4

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ISNEPAL(x1)  =  ISNEPAL
n____(x1, x2)  =  n____(x1, x2)
__(x1, x2)  =  __(x1, x2)
U711(x1, x2, x3)  =  U711(x2, x3)
isQid(x1)  =  isQid(x1)
activate(x1)  =  x1
tt  =  tt
U721(x1, x2)  =  U721(x1, x2)
isPalListKind(x1)  =  x1
ISPAL(x1)  =  ISPAL
U811(x1, x2)  =  U811(x1)
U821(x1, x2)  =  U821(x1, x2)
n__nil  =  n__nil
nil  =  nil
n__a  =  n__a
a  =  a
n__e  =  n__e
e  =  e
n__i  =  n__i
i  =  i
n__o  =  n__o
o  =  o
n__u  =  n__u
u  =  u
U91(x1, x2)  =  U91
U92(x1)  =  U92

Lexicographic path order with status [LPO].
Quasi-Precedence:
[n2, 2] > [U71^12, U72^12] > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]
[n2, 2] > [U91, U92] > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]
isQid1 > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]
[nnil, nil] > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]
[ne, e] > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]
[ni, i] > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]
[no, o] > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]
[nu, u] > [ISNEPAL, tt, ISPAL, U81^11, U82^12, na, a]

Status:
ISNEPAL: []
n2: [1,2]
_2: [1,2]
U71^12: [1,2]
isQid1: [1]
tt: []
U72^12: [1,2]
ISPAL: []
U81^11: [1]
U82^12: [1,2]
nnil: []
nil: []
na: []
a: []
ne: []
e: []
ni: []
i: []
no: []
o: []
nu: []
u: []
U91: []
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

(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))
U241(tt, V1, V2) → ISLIST(activate(V1))
U541(tt, V1, V2) → ISNELIST(activate(V1))
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
U111(x0, x1, x2)  =  U111(x0, x2)
U121(x0, x1, x2)  =  U121(x0, x2)
ISNELIST(x0, x1)  =  ISNELIST(x0, x1)
U411(x0, x1, x2, x3)  =  U411(x0)
U421(x0, x1, x2, x3)  =  U421(x0, x3)
U431(x0, x1, x2, x3)  =  U431(x1, x2, x3)
U441(x0, x1, x2, x3)  =  U441(x0, x2, x3)
U451(x0, x1, x2)  =  U451(x0, x2)
U511(x0, x1, x2, x3)  =  U511(x0, x2, x3)
U521(x0, x1, x2, x3)  =  U521(x0, x1)
U531(x0, x1, x2, x3)  =  U531(x0, x2, x3)
U541(x0, x1, x2, x3)  =  U541(x0, x2)
U551(x0, x1, x2)  =  U551(x0, x1, x2)
ISLIST(x0, x1)  =  ISLIST(x0, x1)
U211(x0, x1, x2, x3)  =  U211(x0, x1)
U221(x0, x1, x2, x3)  =  U221(x0, x1)
U231(x0, x1, x2, x3)  =  U231(x0, x1)
U241(x0, x1, x2, x3)  =  U241(x1, x2, x3)
U251(x0, x1, x2)  =  U251(x1, x2)

Tags:
U111 has argument tags [64,15,64] and root tag 10
U121 has argument tags [83,119,60] and root tag 28
ISNELIST has argument tags [93,60] and root tag 24
U411 has argument tags [45,33,2,0] and root tag 6
U421 has argument tags [5,2,66,78] and root tag 16
U431 has argument tags [22,49,71,72] and root tag 22
U441 has argument tags [49,5,71,72] and root tag 8
U451 has argument tags [123,85,67] and root tag 30
U511 has argument tags [66,64,32,0] and root tag 4
U521 has argument tags [116,96,120,0] and root tag 7
U531 has argument tags [0,1,0,31] and root tag 11
U541 has argument tags [13,3,93,0] and root tag 16
U551 has argument tags [10,33,71] and root tag 23
ISLIST has argument tags [45,71] and root tag 8
U211 has argument tags [120,101,0,3] and root tag 4
U221 has argument tags [112,26,0,124] and root tag 29
U231 has argument tags [72,125,4,0] and root tag 5
U241 has argument tags [22,75,76,71] and root tag 26
U251 has argument tags [32,48,71] and root tag 8

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
U111(x1, x2)  =  U111
tt  =  tt
U121(x1, x2)  =  U121
isPalListKind(x1)  =  isPalListKind
activate(x1)  =  x1
ISNELIST(x1)  =  ISNELIST
n____(x1, x2)  =  n____(x1, x2)
U411(x1, x2, x3)  =  U411(x2, x3)
U421(x1, x2, x3)  =  U421(x1, x2)
U431(x1, x2, x3)  =  U431(x1)
U441(x1, x2, x3)  =  U441
U451(x1, x2)  =  U451
isList(x1)  =  isList
U511(x1, x2, x3)  =  U511(x1, x2, x3)
U521(x1, x2, x3)  =  U521(x1, x2, x3)
U531(x1, x2, x3)  =  U531(x1, x2, x3)
U541(x1, x2, x3)  =  U541(x3)
U551(x1, x2)  =  U551
isNeList(x1)  =  isNeList
ISLIST(x1)  =  ISLIST
U211(x1, x2, x3)  =  U211(x2, x3)
U221(x1, x2, x3)  =  U221(x2, x3)
U231(x1, x2, x3)  =  U231(x1, x2, x3)
U241(x1, x2, x3)  =  U241(x1, x2, x3)
U251(x1, x2)  =  U251(x1, x2)
n__nil  =  n__nil
nil  =  nil
__(x1, x2)  =  __(x1, x2)
n__a  =  n__a
a  =  a
n__e  =  n__e
e  =  e
n__i  =  n__i
i  =  i
n__o  =  n__o
o  =  o
n__u  =  n__u
u  =  u
U91(x1, x2)  =  U91
U11(x1, x2)  =  U11
U21(x1, x2, x3)  =  U21
U31(x1, x2)  =  U31
U41(x1, x2, x3)  =  U41
U51(x1, x2, x3)  =  U51
U42(x1, x2, x3)  =  U42
U12(x1, x2)  =  U12
U22(x1, x2, x3)  =  U22
U52(x1, x2, x3)  =  U52
U43(x1, x2, x3)  =  x1
U13(x1)  =  U13
U23(x1, x2, x3)  =  U23
U53(x1, x2, x3)  =  U53
U44(x1, x2, x3)  =  U44
U24(x1, x2, x3)  =  U24
U54(x1, x2, x3)  =  U54
U45(x1, x2)  =  x1
U25(x1, x2)  =  U25
U55(x1, x2)  =  U55
U46(x1)  =  U46
U26(x1)  =  U26
U56(x1)  =  U56
U32(x1, x2)  =  x1
U33(x1)  =  U33
isQid(x1)  =  isQid
U92(x1)  =  U92

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

Status:
U11^1: []
tt: []
U12^1: []
isPalListKind: []
ISNELIST: []
n2: [1,2]
U41^12: [1,2]
U42^12: [2,1]
U43^11: [1]
U44^1: []
U45^1: []
isList: []
U51^13: [1,2,3]
U52^13: [2,1,3]
U53^13: [2,1,3]
U54^11: [1]
U55^1: []
isNeList: []
ISLIST: []
U21^12: [2,1]
U22^12: [2,1]
U23^13: [3,1,2]
U24^13: [2,3,1]
U25^12: [1,2]
nnil: []
nil: []
_2: [1,2]
na: []
a: []
ne: []
e: []
ni: []
i: []
no: []
o: []
nu: []
u: []
U91: []
U11: []
U21: []
U31: []
U41: []
U51: []
U42: []
U12: []
U22: []
U52: []
U13: []
U23: []
U53: []
U44: []
U24: []
U54: []
U25: []
U55: []
U46: []
U26: []
U56: []
U33: []
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))
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V) → U13(isNeList(activate(V)))
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)))
U13(tt) → tt
U26(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(X1, X2) → n____(X1, X2)
niln__nil
an__a
en__e
in__i
on__o
un__u

(22) Obligation:

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

U251(tt, V2) → ISLIST(activate(V2))
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.

(23) DependencyGraphProof (EQUIVALENT transformation)

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

(24) TRUE