(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(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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(isNeList(activate(V)))
U111(tt, V) → ISNELIST(activate(V))
U111(tt, V) → ACTIVATE(V)
U211(tt, V1, V2) → U221(isList(activate(V1)), activate(V2))
U211(tt, V1, V2) → ISLIST(activate(V1))
U211(tt, V1, V2) → ACTIVATE(V1)
U211(tt, V1, V2) → ACTIVATE(V2)
U221(tt, V2) → U231(isList(activate(V2)))
U221(tt, V2) → ISLIST(activate(V2))
U221(tt, V2) → ACTIVATE(V2)
U311(tt, V) → U321(isQid(activate(V)))
U311(tt, V) → ISQID(activate(V))
U311(tt, V) → ACTIVATE(V)
U411(tt, V1, V2) → U421(isList(activate(V1)), activate(V2))
U411(tt, V1, V2) → ISLIST(activate(V1))
U411(tt, V1, V2) → ACTIVATE(V1)
U411(tt, V1, V2) → ACTIVATE(V2)
U421(tt, V2) → U431(isNeList(activate(V2)))
U421(tt, V2) → ISNELIST(activate(V2))
U421(tt, V2) → ACTIVATE(V2)
U511(tt, V1, V2) → U521(isNeList(activate(V1)), activate(V2))
U511(tt, V1, V2) → ISNELIST(activate(V1))
U511(tt, V1, V2) → ACTIVATE(V1)
U511(tt, V1, V2) → ACTIVATE(V2)
U521(tt, V2) → U531(isList(activate(V2)))
U521(tt, V2) → ISLIST(activate(V2))
U521(tt, V2) → ACTIVATE(V2)
U611(tt, V) → U621(isQid(activate(V)))
U611(tt, V) → ISQID(activate(V))
U611(tt, V) → ACTIVATE(V)
U711(tt, V) → U721(isNePal(activate(V)))
U711(tt, V) → ISNEPAL(activate(V))
U711(tt, V) → ACTIVATE(V)
AND(tt, X) → ACTIVATE(X)
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
ISLIST(V) → ISPALLISTKIND(activate(V))
ISLIST(V) → ACTIVATE(V)
ISLIST(n____(V1, V2)) → U211(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
ISLIST(n____(V1, V2)) → AND(isPalListKind(activate(V1)), n__isPalListKind(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(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
ISNELIST(n____(V1, V2)) → AND(isPalListKind(activate(V1)), n__isPalListKind(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(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), 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))) → AND(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
ISNEPAL(n____(I, __(P, I))) → AND(isQid(activate(I)), n__isPalListKind(activate(I)))
ISNEPAL(n____(I, __(P, I))) → ISQID(activate(I))
ISNEPAL(n____(I, __(P, I))) → ACTIVATE(I)
ISNEPAL(n____(I, __(P, I))) → ISPAL(activate(P))
ISNEPAL(n____(I, __(P, I))) → ACTIVATE(P)
ISPAL(V) → U711(isPalListKind(activate(V)), activate(V))
ISPAL(V) → ISPALLISTKIND(activate(V))
ISPAL(V) → ACTIVATE(V)
ISPALLISTKIND(n____(V1, V2)) → AND(isPalListKind(activate(V1)), n__isPalListKind(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__isPalListKind(X)) → ISPALLISTKIND(X)
ACTIVATE(n__and(X1, X2)) → AND(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(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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 52 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(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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: Recursive path order with status [RPO].
Quasi-Precedence:
_^12 > [2, n2]

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


The following usable rules [FROCOS05] were oriented:

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

(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(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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:

ACTIVATE(n__isPalListKind(X)) → ISPALLISTKIND(X)
ISPALLISTKIND(n____(V1, V2)) → AND(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISPALLISTKIND(n____(V1, V2)) → ISPALLISTKIND(activate(V1))
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V1)
ISPALLISTKIND(n____(V1, V2)) → ACTIVATE(V2)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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

Recursive path order with status [RPO].
Quasi-Precedence:
[nisPalListKind1, ISPALLISTKIND1, isPalListKind1] > [AND2, nand2, and2] > [activate1, e] > nil > [tt, nnil]
[nisPalListKind1, ISPALLISTKIND1, isPalListKind1] > [AND2, nand2, and2] > [activate1, e] > ne > [tt, nnil]
[n2, 2] > [activate1, e] > nil > [tt, nnil]
[n2, 2] > [activate1, e] > ne > [tt, nnil]
[nu, u] > [tt, nnil]
[no, o] > [tt, nnil]
[na, a] > [tt, nnil]
[ni, i] > [tt, nnil]

Status:
i: multiset
a: multiset
_2: [1,2]
nu: multiset
e: multiset
ni: multiset
ne: multiset
activate1: multiset
nnil: multiset
and2: multiset
n2: [1,2]
o: multiset
na: multiset
nand2: multiset
no: multiset
tt: multiset
isPalListKind1: [1]
ISPALLISTKIND1: [1]
AND2: multiset
u: multiset
nisPalListKind1: [1]
nil: multiset


The following usable rules [FROCOS05] were oriented:

__(nil, X) → X
activate(X) → X
__(X, nil) → X
activate(n__u) → u
__(__(X, Y), Z) → __(X, __(Y, Z))
activate(n__o) → o
isPalListKind(n__e) → tt
isPalListKind(n__a) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__i) → tt
isPalListKind(n__u) → tt
isPalListKind(n__o) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
and(tt, X) → activate(X)
activate(n__and(X1, X2)) → and(X1, X2)
isPalListKind(n____(V1, V2)) → and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i

(12) Obligation:

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

ACTIVATE(n__isPalListKind(X)) → ISPALLISTKIND(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X

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

(13) DependencyGraphProof (EQUIVALENT transformation)

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

(14) TRUE

(15) Obligation:

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

ISNEPAL(n____(I, __(P, I))) → ISPAL(activate(P))
ISPAL(V) → U711(isPalListKind(activate(V)), activate(V))
U711(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(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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))) → ISPAL(activate(P))
ISPAL(V) → U711(isPalListKind(activate(V)), activate(V))
U711(tt, V) → ISNEPAL(activate(V))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNEPAL(x1)  =  ISNEPAL(x1)
n____(x1, x2)  =  n____(x1, x2)
__(x1, x2)  =  __(x1, x2)
ISPAL(x1)  =  ISPAL(x1)
activate(x1)  =  x1
U711(x1, x2)  =  U711(x1, x2)
isPalListKind(x1)  =  isPalListKind
tt  =  tt
nil  =  nil
n__u  =  n__u
u  =  u
n__o  =  n__o
o  =  o
n__e  =  n__e
n__a  =  n__a
n__nil  =  n__nil
n__i  =  n__i
n__isPalListKind(x1)  =  n__isPalListKind
and(x1, x2)  =  x2
n__and(x1, x2)  =  x2
a  =  a
e  =  e
i  =  i

Recursive path order with status [RPO].
Quasi-Precedence:
[n2, 2, ISPAL1] > [ISNEPAL1, U71^12, isPalListKind, tt, nisPalListKind]
[nil, nnil] > [ISNEPAL1, U71^12, isPalListKind, tt, nisPalListKind]
[nu, u] > [ISNEPAL1, U71^12, isPalListKind, tt, nisPalListKind]
[no, o] > [ISNEPAL1, U71^12, isPalListKind, tt, nisPalListKind]
[ne, e] > [ISNEPAL1, U71^12, isPalListKind, tt, nisPalListKind]
[na, a] > [ISNEPAL1, U71^12, isPalListKind, tt, nisPalListKind]
[ni, i] > [ISNEPAL1, U71^12, isPalListKind, tt, nisPalListKind]

Status:
i: multiset
a: multiset
_2: [1,2]
nu: multiset
e: multiset
U71^12: [2,1]
isPalListKind: multiset
ni: multiset
ne: multiset
nnil: multiset
n2: [1,2]
o: multiset
na: multiset
no: multiset
tt: multiset
ISPAL1: [1]
u: multiset
nisPalListKind: multiset
nil: multiset
ISNEPAL1: [1]


The following usable rules [FROCOS05] were oriented:

__(nil, X) → X
activate(X) → X
__(X, nil) → X
activate(n__u) → u
__(__(X, Y), Z) → __(X, __(Y, Z))
activate(n__o) → o
isPalListKind(n__e) → tt
isPalListKind(n__a) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__i) → tt
isPalListKind(n__u) → tt
isPalListKind(n__o) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
and(tt, X) → activate(X)
activate(n__and(X1, X2)) → and(X1, X2)
isPalListKind(n____(V1, V2)) → and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i

(17) Obligation:

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

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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) PisEmptyProof (EQUIVALENT transformation)

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

(19) TRUE

(20) Obligation:

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

U111(tt, V) → ISNELIST(activate(V))
ISNELIST(n____(V1, V2)) → U411(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
U411(tt, V1, V2) → U421(isList(activate(V1)), activate(V2))
U421(tt, V2) → ISNELIST(activate(V2))
ISNELIST(n____(V1, V2)) → U511(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
U511(tt, V1, V2) → U521(isNeList(activate(V1)), activate(V2))
U521(tt, V2) → ISLIST(activate(V2))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
ISLIST(n____(V1, V2)) → U211(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
U211(tt, V1, V2) → U221(isList(activate(V1)), activate(V2))
U221(tt, V2) → ISLIST(activate(V2))
U211(tt, V1, V2) → ISLIST(activate(V1))
U511(tt, V1, V2) → ISNELIST(activate(V1))
U411(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(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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) → ISNELIST(activate(V))
ISNELIST(n____(V1, V2)) → U411(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
U411(tt, V1, V2) → U421(isList(activate(V1)), activate(V2))
U421(tt, V2) → ISNELIST(activate(V2))
ISNELIST(n____(V1, V2)) → U511(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
U511(tt, V1, V2) → U521(isNeList(activate(V1)), activate(V2))
U521(tt, V2) → ISLIST(activate(V2))
ISLIST(V) → U111(isPalListKind(activate(V)), activate(V))
ISLIST(n____(V1, V2)) → U211(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
U211(tt, V1, V2) → U221(isList(activate(V1)), activate(V2))
U221(tt, V2) → ISLIST(activate(V2))
U211(tt, V1, V2) → ISLIST(activate(V1))
U511(tt, V1, V2) → ISNELIST(activate(V1))
U411(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
ISNELIST(x1)  =  ISNELIST(x1)
activate(x1)  =  activate(x1)
n____(x1, x2)  =  n____(x1, x2)
U411(x1, x2, x3)  =  U411(x2, x3)
and(x1, x2)  =  and(x1, x2)
isPalListKind(x1)  =  isPalListKind(x1)
n__isPalListKind(x1)  =  n__isPalListKind(x1)
U421(x1, x2)  =  U421(x2)
isList(x1)  =  isList
U511(x1, x2, x3)  =  U511(x1, x2, x3)
U521(x1, x2)  =  U521(x1, x2)
isNeList(x1)  =  x1
ISLIST(x1)  =  ISLIST(x1)
U211(x1, x2, x3)  =  U211(x2, x3)
U221(x1, x2)  =  U221(x2)
__(x1, x2)  =  __(x1, x2)
nil  =  nil
U22(x1, x2)  =  x1
U23(x1)  =  U23
U21(x1, x2, x3)  =  U21
U12(x1)  =  U12
U11(x1, x2)  =  U11
U41(x1, x2, x3)  =  U41(x1, x2, x3)
U42(x1, x2)  =  U42(x1, x2)
U32(x1)  =  x1
U31(x1, x2)  =  U31
isQid(x1)  =  isQid
U51(x1, x2, x3)  =  U51(x2, x3)
U52(x1, x2)  =  U52
U53(x1)  =  U53
U43(x1)  =  x1
n__nil  =  n__nil
n__e  =  n__e
n__a  =  n__a
n__i  =  n__i
n__u  =  n__u
n__o  =  n__o
n__and(x1, x2)  =  n__and(x1, x2)
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Recursive path order with status [RPO].
Quasi-Precedence:
[n2, 2] > U41^12 > U42^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > nisPalListKind1 > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U41^12 > U42^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > ne > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U41^12 > ISLIST1 > U11^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > nisPalListKind1 > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U41^12 > ISLIST1 > U11^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > ne > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U51^13 > U52^12 > ISLIST1 > U11^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > nisPalListKind1 > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U51^13 > U52^12 > ISLIST1 > U11^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > ne > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U21^12 > U22^11 > ISLIST1 > U11^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > nisPalListKind1 > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U21^12 > U22^11 > ISLIST1 > U11^11 > ISNELIST1 > [activate1, and2, isPalListKind1, nil, nand2, e] > ne > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U413 > [isList, U21] > U11 > [activate1, and2, isPalListKind1, nil, nand2, e] > nisPalListKind1 > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U413 > [isList, U21] > U11 > [activate1, and2, isPalListKind1, nil, nand2, e] > ne > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U413 > U422 > [activate1, and2, isPalListKind1, nil, nand2, e] > nisPalListKind1 > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > U413 > U422 > [activate1, and2, isPalListKind1, nil, nand2, e] > ne > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > [U512, U52, U53] > [isList, U21] > U11 > [activate1, and2, isPalListKind1, nil, nand2, e] > nisPalListKind1 > [tt, U23, U12, U31, isQid, nnil, na, a]
[n2, 2] > [U512, U52, U53] > [isList, U21] > U11 > [activate1, and2, isPalListKind1, nil, nand2, e] > ne > [tt, U23, U12, U31, isQid, nnil, na, a]
[ni, i] > [tt, U23, U12, U31, isQid, nnil, na, a]
[nu, u] > [tt, U23, U12, U31, isQid, nnil, na, a]
[no, o] > [tt, U23, U12, U31, isQid, nnil, na, a]

Status:
i: multiset
U52^12: multiset
U11^11: multiset
_2: [1,2]
nu: multiset
U413: multiset
U31: []
ni: multiset
U21^12: multiset
U11: multiset
activate1: multiset
and2: multiset
nnil: multiset
U512: [2,1]
na: multiset
isList: []
tt: multiset
isPalListKind1: multiset
U22^11: [1]
U23: []
isQid: []
nil: multiset
U21: []
a: multiset
ISNELIST1: [1]
U422: [1,2]
e: multiset
U52: []
U53: []
U12: []
ne: multiset
n2: [1,2]
o: multiset
U51^13: multiset
nand2: multiset
no: multiset
U41^12: multiset
u: multiset
nisPalListKind1: multiset
ISLIST1: multiset
U42^11: multiset


The following usable rules [FROCOS05] were oriented:

__(nil, X) → X
__(X, nil) → X
__(__(X, Y), Z) → __(X, __(Y, Z))
U22(tt, V2) → U23(isList(activate(V2)))
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U12(tt) → tt
U11(tt, V) → U12(isNeList(activate(V)))
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U32(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U23(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U53(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isPalListKind(n__e) → tt
isPalListKind(n__a) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__i) → tt
isPalListKind(n__u) → tt
isPalListKind(n__o) → tt
isQid(n__a) → tt
isQid(n__i) → tt
isQid(n__e) → tt
isQid(n__u) → tt
isQid(n__o) → tt
niln__nil
__(X1, X2) → n____(X1, X2)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
and(tt, X) → activate(X)
activate(n__and(X1, X2)) → and(X1, X2)
isPalListKind(n____(V1, V2)) → and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(X) → X
activate(n__u) → u
activate(n__o) → o

(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(isNeList(activate(V)))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(activate(V1)), activate(V2))
U22(tt, V2) → U23(isList(activate(V2)))
U23(tt) → tt
U31(tt, V) → U32(isQid(activate(V)))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(activate(V1)), activate(V2))
U42(tt, V2) → U43(isNeList(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(activate(V1)), activate(V2))
U52(tt, V2) → U53(isList(activate(V2)))
U53(tt) → tt
U61(tt, V) → U62(isQid(activate(V)))
U62(tt) → tt
U71(tt, V) → U72(isNePal(activate(V)))
U72(tt) → tt
and(tt, X) → activate(X)
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, __(P, I))) → and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P))))
isPal(V) → U71(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)) → and(isPalListKind(activate(V1)), n__isPalListKind(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)
isPalListKind(X) → n__isPalListKind(X)
and(X1, X2) → n__and(X1, X2)
an__a
en__e
in__i
on__o
un__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(X1, X2)
activate(n__isPalListKind(X)) → isPalListKind(X)
activate(n__and(X1, X2)) → and(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