(0) Obligation:

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

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(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:

A____(__(X, Y), Z) → A____(mark(X), a____(mark(Y), mark(Z)))
A____(__(X, Y), Z) → MARK(X)
A____(__(X, Y), Z) → A____(mark(Y), mark(Z))
A____(__(X, Y), Z) → MARK(Y)
A____(__(X, Y), Z) → MARK(Z)
A____(X, nil) → MARK(X)
A____(nil, X) → MARK(X)
A__U21(tt, V2) → A__U22(a__isList(V2))
A__U21(tt, V2) → A__ISLIST(V2)
A__U41(tt, V2) → A__U42(a__isNeList(V2))
A__U41(tt, V2) → A__ISNELIST(V2)
A__U51(tt, V2) → A__U52(a__isList(V2))
A__U51(tt, V2) → A__ISLIST(V2)
A__U71(tt, P) → A__U72(a__isPal(P))
A__U71(tt, P) → A__ISPAL(P)
A__ISLIST(V) → A__U11(a__isNeList(V))
A__ISLIST(V) → A__ISNELIST(V)
A__ISLIST(__(V1, V2)) → A__U21(a__isList(V1), V2)
A__ISLIST(__(V1, V2)) → A__ISLIST(V1)
A__ISNELIST(V) → A__U31(a__isQid(V))
A__ISNELIST(V) → A__ISQID(V)
A__ISNELIST(__(V1, V2)) → A__U41(a__isList(V1), V2)
A__ISNELIST(__(V1, V2)) → A__ISLIST(V1)
A__ISNELIST(__(V1, V2)) → A__U51(a__isNeList(V1), V2)
A__ISNELIST(__(V1, V2)) → A__ISNELIST(V1)
A__ISNEPAL(V) → A__U61(a__isQid(V))
A__ISNEPAL(V) → A__ISQID(V)
A__ISNEPAL(__(I, __(P, I))) → A__U71(a__isQid(I), P)
A__ISNEPAL(__(I, __(P, I))) → A__ISQID(I)
A__ISPAL(V) → A__U81(a__isNePal(V))
A__ISPAL(V) → A__ISNEPAL(V)
MARK(__(X1, X2)) → A____(mark(X1), mark(X2))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → A__U11(mark(X))
MARK(U11(X)) → MARK(X)
MARK(U21(X1, X2)) → A__U21(mark(X1), X2)
MARK(U21(X1, X2)) → MARK(X1)
MARK(U22(X)) → A__U22(mark(X))
MARK(U22(X)) → MARK(X)
MARK(isList(X)) → A__ISLIST(X)
MARK(U31(X)) → A__U31(mark(X))
MARK(U31(X)) → MARK(X)
MARK(U41(X1, X2)) → A__U41(mark(X1), X2)
MARK(U41(X1, X2)) → MARK(X1)
MARK(U42(X)) → A__U42(mark(X))
MARK(U42(X)) → MARK(X)
MARK(isNeList(X)) → A__ISNELIST(X)
MARK(U51(X1, X2)) → A__U51(mark(X1), X2)
MARK(U51(X1, X2)) → MARK(X1)
MARK(U52(X)) → A__U52(mark(X))
MARK(U52(X)) → MARK(X)
MARK(U61(X)) → A__U61(mark(X))
MARK(U61(X)) → MARK(X)
MARK(U71(X1, X2)) → A__U71(mark(X1), X2)
MARK(U71(X1, X2)) → MARK(X1)
MARK(U72(X)) → A__U72(mark(X))
MARK(U72(X)) → MARK(X)
MARK(isPal(X)) → A__ISPAL(X)
MARK(U81(X)) → A__U81(mark(X))
MARK(U81(X)) → MARK(X)
MARK(isQid(X)) → A__ISQID(X)
MARK(isNePal(X)) → A__ISNEPAL(X)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(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 3 SCCs with 28 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

A__U71(tt, P) → A__ISPAL(P)
A__ISPAL(V) → A__ISNEPAL(V)
A__ISNEPAL(__(I, __(P, I))) → A__U71(a__isQid(I), P)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(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.


A__ISPAL(V) → A__ISNEPAL(V)
A__ISNEPAL(__(I, __(P, I))) → A__U71(a__isQid(I), P)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A__U71(x1, x2)  =  A__U71(x2)
tt  =  tt
A__ISPAL(x1)  =  A__ISPAL(x1)
A__ISNEPAL(x1)  =  A__ISNEPAL(x1)
__(x1, x2)  =  __(x1, x2)
a__isQid(x1)  =  x1
a____(x1, x2)  =  a____(x1, x2)
mark(x1)  =  x1
nil  =  nil
a__U11(x1)  =  x1
a__U21(x1, x2)  =  x1
a__U22(x1)  =  a__U22
a__isList(x1)  =  x1
a__U31(x1)  =  x1
a__U41(x1, x2)  =  a__U41(x1, x2)
a__U42(x1)  =  x1
a__isNeList(x1)  =  x1
a__U51(x1, x2)  =  a__U51(x1, x2)
a__U52(x1)  =  x1
a__U61(x1)  =  x1
a__U71(x1, x2)  =  a__U71(x1)
a__U72(x1)  =  a__U72
a__isPal(x1)  =  a__isPal(x1)
a__U81(x1)  =  a__U81
a__isNePal(x1)  =  x1
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
U11(x1)  =  x1
U21(x1, x2)  =  x1
U22(x1)  =  U22
isList(x1)  =  x1
U31(x1)  =  x1
U41(x1, x2)  =  U41(x1, x2)
U42(x1)  =  x1
isNeList(x1)  =  x1
U51(x1, x2)  =  U51(x1, x2)
U52(x1)  =  x1
U61(x1)  =  x1
U71(x1, x2)  =  U71(x1)
U72(x1)  =  U72
isPal(x1)  =  isPal(x1)
U81(x1)  =  U81
isQid(x1)  =  x1
isNePal(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
[2, a2, aU512, U512] > [aU412, U412]
[2, a2, aU512, U512] > [aU711, U711] > [aisPal1, isPal1] > [tt, aU22, aU72, aU81, a, U22, U72, U81] > [AU711, AISPAL1] > AISNEPAL1
nil > [tt, aU22, aU72, aU81, a, U22, U72, U81] > [AU711, AISPAL1] > AISNEPAL1
e > [tt, aU22, aU72, aU81, a, U22, U72, U81] > [AU711, AISPAL1] > AISNEPAL1
i > [tt, aU22, aU72, aU81, a, U22, U72, U81] > [AU711, AISPAL1] > AISNEPAL1
o > [tt, aU22, aU72, aU81, a, U22, U72, U81] > [AU711, AISPAL1] > AISNEPAL1
u > [tt, aU22, aU72, aU81, a, U22, U72, U81] > [AU711, AISPAL1] > AISNEPAL1

Status:
AU711: multiset
tt: multiset
AISPAL1: multiset
AISNEPAL1: [1]
_2: [1,2]
a2: [1,2]
nil: multiset
aU22: []
aU412: multiset
aU512: [1,2]
aU711: [1]
aU72: []
aisPal1: multiset
aU81: []
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
U22: []
U412: multiset
U512: [1,2]
U711: [1]
U72: []
isPal1: multiset
U81: []


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(7) Obligation:

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

A__U71(tt, P) → A__ISPAL(P)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

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

(8) DependencyGraphProof (EQUIVALENT transformation)

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

(9) TRUE

(10) Obligation:

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

A__U21(tt, V2) → A__ISLIST(V2)
A__ISLIST(V) → A__ISNELIST(V)
A__ISNELIST(__(V1, V2)) → A__U41(a__isList(V1), V2)
A__U41(tt, V2) → A__ISNELIST(V2)
A__ISNELIST(__(V1, V2)) → A__ISLIST(V1)
A__ISLIST(__(V1, V2)) → A__U21(a__isList(V1), V2)
A__ISLIST(__(V1, V2)) → A__ISLIST(V1)
A__ISNELIST(__(V1, V2)) → A__U51(a__isNeList(V1), V2)
A__U51(tt, V2) → A__ISLIST(V2)
A__ISNELIST(__(V1, V2)) → A__ISNELIST(V1)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(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.


A__U21(tt, V2) → A__ISLIST(V2)
A__ISNELIST(__(V1, V2)) → A__U41(a__isList(V1), V2)
A__ISNELIST(__(V1, V2)) → A__ISLIST(V1)
A__ISLIST(__(V1, V2)) → A__ISLIST(V1)
A__ISNELIST(__(V1, V2)) → A__U51(a__isNeList(V1), V2)
A__ISNELIST(__(V1, V2)) → A__ISNELIST(V1)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A__U21(x1, x2)  =  A__U21(x1, x2)
tt  =  tt
A__ISLIST(x1)  =  x1
A__ISNELIST(x1)  =  x1
__(x1, x2)  =  __(x1, x2)
A__U41(x1, x2)  =  x2
a__isList(x1)  =  x1
A__U51(x1, x2)  =  x2
a__isNeList(x1)  =  x1
a____(x1, x2)  =  a____(x1, x2)
mark(x1)  =  x1
nil  =  nil
a__U11(x1)  =  x1
a__U21(x1, x2)  =  a__U21(x1, x2)
a__U22(x1)  =  a__U22
a__U31(x1)  =  x1
a__U41(x1, x2)  =  x2
a__U42(x1)  =  x1
a__U51(x1, x2)  =  x2
a__U52(x1)  =  x1
a__U61(x1)  =  x1
a__U71(x1, x2)  =  x1
a__U72(x1)  =  x1
a__isPal(x1)  =  a__isPal
a__U81(x1)  =  a__U81
a__isQid(x1)  =  x1
a__isNePal(x1)  =  x1
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
U11(x1)  =  x1
U21(x1, x2)  =  U21(x1, x2)
U22(x1)  =  U22
isList(x1)  =  x1
U31(x1)  =  x1
U41(x1, x2)  =  x2
U42(x1)  =  x1
isNeList(x1)  =  x1
U51(x1, x2)  =  x2
U52(x1)  =  x1
U61(x1)  =  x1
U71(x1, x2)  =  x1
U72(x1)  =  x1
isPal(x1)  =  isPal
U81(x1)  =  U81
isQid(x1)  =  x1
isNePal(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
[AU212, 2, a2] > [aU212, U212]
nil > [tt, aU22, aisPal, aU81, a, u, U22, isPal, U81]
e > [tt, aU22, aisPal, aU81, a, u, U22, isPal, U81]
i > [tt, aU22, aisPal, aU81, a, u, U22, isPal, U81]
o > [tt, aU22, aisPal, aU81, a, u, U22, isPal, U81]

Status:
AU212: [1,2]
tt: multiset
_2: [1,2]
a2: [1,2]
nil: multiset
aU212: [1,2]
aU22: multiset
aisPal: multiset
aU81: multiset
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
U212: [1,2]
U22: multiset
isPal: multiset
U81: multiset


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(12) Obligation:

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

A__ISLIST(V) → A__ISNELIST(V)
A__U41(tt, V2) → A__ISNELIST(V2)
A__ISLIST(__(V1, V2)) → A__U21(a__isList(V1), V2)
A__U51(tt, V2) → A__ISLIST(V2)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(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 4 less nodes.

(14) TRUE

(15) Obligation:

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

A____(__(X, Y), Z) → MARK(X)
MARK(__(X1, X2)) → A____(mark(X1), mark(X2))
A____(__(X, Y), Z) → A____(mark(X), a____(mark(Y), mark(Z)))
A____(__(X, Y), Z) → A____(mark(Y), mark(Z))
A____(__(X, Y), Z) → MARK(Y)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → MARK(X2)
MARK(U11(X)) → MARK(X)
MARK(U21(X1, X2)) → MARK(X1)
MARK(U22(X)) → MARK(X)
MARK(U31(X)) → MARK(X)
MARK(U41(X1, X2)) → MARK(X1)
MARK(U42(X)) → MARK(X)
MARK(U51(X1, X2)) → MARK(X1)
MARK(U52(X)) → MARK(X)
MARK(U61(X)) → MARK(X)
MARK(U71(X1, X2)) → MARK(X1)
MARK(U72(X)) → MARK(X)
MARK(U81(X)) → MARK(X)
A____(__(X, Y), Z) → MARK(Z)
A____(X, nil) → MARK(X)
A____(nil, X) → MARK(X)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(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.


A____(__(X, Y), Z) → MARK(X)
MARK(__(X1, X2)) → A____(mark(X1), mark(X2))
A____(__(X, Y), Z) → A____(mark(X), a____(mark(Y), mark(Z)))
A____(__(X, Y), Z) → A____(mark(Y), mark(Z))
A____(__(X, Y), Z) → MARK(Y)
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → MARK(X2)
MARK(U21(X1, X2)) → MARK(X1)
MARK(U22(X)) → MARK(X)
MARK(U41(X1, X2)) → MARK(X1)
MARK(U42(X)) → MARK(X)
MARK(U51(X1, X2)) → MARK(X1)
MARK(U52(X)) → MARK(X)
MARK(U71(X1, X2)) → MARK(X1)
A____(__(X, Y), Z) → MARK(Z)
A____(X, nil) → MARK(X)
A____(nil, X) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A____(x1, x2)  =  A____(x1, x2)
__(x1, x2)  =  __(x1, x2)
MARK(x1)  =  MARK(x1)
mark(x1)  =  x1
a____(x1, x2)  =  a____(x1, x2)
U11(x1)  =  x1
U21(x1, x2)  =  U21(x1, x2)
U22(x1)  =  U22(x1)
U31(x1)  =  x1
U41(x1, x2)  =  U41(x1, x2)
U42(x1)  =  U42(x1)
U51(x1, x2)  =  U51(x1, x2)
U52(x1)  =  U52(x1)
U61(x1)  =  x1
U71(x1, x2)  =  U71(x1, x2)
U72(x1)  =  x1
U81(x1)  =  x1
nil  =  nil
a__U11(x1)  =  x1
tt  =  tt
a__U21(x1, x2)  =  a__U21(x1, x2)
a__U22(x1)  =  a__U22(x1)
a__isList(x1)  =  a__isList(x1)
a__U31(x1)  =  x1
a__U41(x1, x2)  =  a__U41(x1, x2)
a__U42(x1)  =  a__U42(x1)
a__isNeList(x1)  =  a__isNeList(x1)
a__U51(x1, x2)  =  a__U51(x1, x2)
a__U52(x1)  =  a__U52(x1)
a__U61(x1)  =  x1
a__U71(x1, x2)  =  a__U71(x1, x2)
a__U72(x1)  =  x1
a__isPal(x1)  =  a__isPal(x1)
a__U81(x1)  =  x1
a__isQid(x1)  =  a__isQid
a__isNePal(x1)  =  a__isNePal(x1)
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
isList(x1)  =  isList(x1)
isNeList(x1)  =  isNeList(x1)
isPal(x1)  =  isPal(x1)
isQid(x1)  =  isQid
isNePal(x1)  =  isNePal(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[A2, 2, a2] > [U212, aU212] > [U221, aU221] > [tt, aisQid, o, isQid] > [U421, aU421] > MARK1
[A2, 2, a2] > [U212, aU212] > [U221, aU221] > [tt, aisQid, o, isQid] > [U521, aU521]
[A2, 2, a2] > [U212, aU212] > [U412, aisList1, aU412, aisNeList1, isList1, isNeList1] > [tt, aisQid, o, isQid] > [U421, aU421] > MARK1
[A2, 2, a2] > [U212, aU212] > [U412, aisList1, aU412, aisNeList1, isList1, isNeList1] > [tt, aisQid, o, isQid] > [U521, aU521]
[A2, 2, a2] > [U512, aU512] > [U412, aisList1, aU412, aisNeList1, isList1, isNeList1] > [tt, aisQid, o, isQid] > [U421, aU421] > MARK1
[A2, 2, a2] > [U512, aU512] > [U412, aisList1, aU412, aisNeList1, isList1, isNeList1] > [tt, aisQid, o, isQid] > [U521, aU521]
[A2, 2, a2] > [U712, aU712, aisPal1, aisNePal1, isPal1, isNePal1] > [tt, aisQid, o, isQid] > [U421, aU421] > MARK1
[A2, 2, a2] > [U712, aU712, aisPal1, aisNePal1, isPal1, isNePal1] > [tt, aisQid, o, isQid] > [U521, aU521]
nil > MARK1
i > [tt, aisQid, o, isQid] > [U421, aU421] > MARK1
i > [tt, aisQid, o, isQid] > [U521, aU521]

Status:
A2: [1,2]
_2: [1,2]
MARK1: [1]
a2: [1,2]
U212: multiset
U221: multiset
U412: multiset
U421: multiset
U512: multiset
U521: multiset
U712: multiset
nil: multiset
tt: multiset
aU212: multiset
aU221: multiset
aisList1: multiset
aU412: multiset
aU421: multiset
aisNeList1: multiset
aU512: multiset
aU521: multiset
aU712: multiset
aisPal1: multiset
aisQid: []
aisNePal1: multiset
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
isList1: multiset
isNeList1: multiset
isPal1: multiset
isQid: []
isNePal1: multiset


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(17) Obligation:

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

MARK(U11(X)) → MARK(X)
MARK(U31(X)) → MARK(X)
MARK(U61(X)) → MARK(X)
MARK(U72(X)) → MARK(X)
MARK(U81(X)) → MARK(X)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(U11(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  x1
U11(x1)  =  U11(x1)
U31(x1)  =  x1
U61(x1)  =  x1
U72(x1)  =  x1
U81(x1)  =  x1
a____(x1, x2)  =  a____(x1, x2)
__(x1, x2)  =  __(x1, x2)
mark(x1)  =  x1
nil  =  nil
a__U11(x1)  =  a__U11(x1)
tt  =  tt
a__U21(x1, x2)  =  x1
a__U22(x1)  =  a__U22
a__isList(x1)  =  a__isList(x1)
a__U31(x1)  =  x1
a__U41(x1, x2)  =  a__U41(x2)
a__U42(x1)  =  x1
a__isNeList(x1)  =  a__isNeList(x1)
a__U51(x1, x2)  =  a__U51(x1, x2)
a__U52(x1)  =  a__U52
a__U61(x1)  =  x1
a__U71(x1, x2)  =  x1
a__U72(x1)  =  x1
a__isPal(x1)  =  a__isPal
a__U81(x1)  =  x1
a__isQid(x1)  =  a__isQid
a__isNePal(x1)  =  a__isNePal
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
U21(x1, x2)  =  x1
U22(x1)  =  U22
isList(x1)  =  isList(x1)
U41(x1, x2)  =  U41(x2)
U42(x1)  =  x1
isNeList(x1)  =  isNeList(x1)
U51(x1, x2)  =  U51(x1, x2)
U52(x1)  =  U52
U71(x1, x2)  =  x1
isPal(x1)  =  isPal
isQid(x1)  =  isQid
isNePal(x1)  =  isNePal

Recursive path order with status [RPO].
Quasi-Precedence:
[a2, 2]
[aisList1, isList1] > [U111, aU111] > [tt, aU22, aisPal, aisQid, aisNePal, U22, isPal, isQid, isNePal]
[aisList1, isList1] > [aU411, aisNeList1, aU512, U411, isNeList1, U512] > [aU52, U52] > [tt, aU22, aisPal, aisQid, aisNePal, U22, isPal, isQid, isNePal]
i > [tt, aU22, aisPal, aisQid, aisNePal, U22, isPal, isQid, isNePal]
o > [tt, aU22, aisPal, aisQid, aisNePal, U22, isPal, isQid, isNePal]
u > [tt, aU22, aisPal, aisQid, aisNePal, U22, isPal, isQid, isNePal]

Status:
U111: multiset
a2: [1,2]
_2: [1,2]
nil: multiset
aU111: multiset
tt: multiset
aU22: []
aisList1: [1]
aU411: [1]
aisNeList1: [1]
aU512: [2,1]
aU52: []
aisPal: []
aisQid: []
aisNePal: []
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
U22: []
isList1: [1]
U411: [1]
isNeList1: [1]
U512: [2,1]
U52: []
isPal: []
isQid: []
isNePal: []


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(19) Obligation:

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

MARK(U31(X)) → MARK(X)
MARK(U61(X)) → MARK(X)
MARK(U72(X)) → MARK(X)
MARK(U81(X)) → MARK(X)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

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

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(U81(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK(x1)
U31(x1)  =  x1
U61(x1)  =  x1
U72(x1)  =  x1
U81(x1)  =  U81(x1)
a____(x1, x2)  =  a____(x1, x2)
__(x1, x2)  =  __(x1, x2)
mark(x1)  =  x1
nil  =  nil
a__U11(x1)  =  x1
tt  =  tt
a__U21(x1, x2)  =  a__U21(x1, x2)
a__U22(x1)  =  x1
a__isList(x1)  =  a__isList(x1)
a__U31(x1)  =  x1
a__U41(x1, x2)  =  a__U41(x1, x2)
a__U42(x1)  =  a__U42
a__isNeList(x1)  =  a__isNeList(x1)
a__U51(x1, x2)  =  a__U51
a__U52(x1)  =  a__U52
a__U61(x1)  =  x1
a__U71(x1, x2)  =  a__U71(x2)
a__U72(x1)  =  x1
a__isPal(x1)  =  a__isPal(x1)
a__U81(x1)  =  a__U81(x1)
a__isQid(x1)  =  a__isQid(x1)
a__isNePal(x1)  =  a__isNePal(x1)
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
U11(x1)  =  x1
U21(x1, x2)  =  U21(x1, x2)
U22(x1)  =  x1
isList(x1)  =  isList(x1)
U41(x1, x2)  =  U41(x1, x2)
U42(x1)  =  U42
isNeList(x1)  =  isNeList(x1)
U51(x1, x2)  =  U51
U52(x1)  =  U52
U71(x1, x2)  =  U71(x2)
isPal(x1)  =  isPal(x1)
isQid(x1)  =  isQid(x1)
isNePal(x1)  =  isNePal(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[a2, 2] > [aU412, U412] > [aU42, U42] > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]
[a2, 2] > [aU51, aU52, U51, U52] > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]
[a2, 2] > [aU711, aisPal1, U711, isPal1] > [U811, aU811] > MARK1 > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]
[aU212, aisList1, aisNeList1, U212, isList1, isNeList1] > [aU412, U412] > [aU42, U42] > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]
[aU212, aisList1, aisNeList1, U212, isList1, isNeList1] > [aU51, aU52, U51, U52] > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]
a > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]
e > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]
i > [nil, tt, aisQid1, aisNePal1, o, u, isQid1, isNePal1]

Status:
MARK1: multiset
U811: [1]
a2: [1,2]
_2: [1,2]
nil: multiset
tt: multiset
aU212: [2,1]
aisList1: [1]
aU412: multiset
aU42: []
aisNeList1: [1]
aU51: []
aU52: []
aU711: multiset
aisPal1: multiset
aU811: [1]
aisQid1: [1]
aisNePal1: [1]
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
U212: [2,1]
isList1: [1]
U412: multiset
U42: []
isNeList1: [1]
U51: []
U52: []
U711: multiset
isPal1: multiset
isQid1: [1]
isNePal1: [1]


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(21) Obligation:

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

MARK(U31(X)) → MARK(X)
MARK(U61(X)) → MARK(X)
MARK(U72(X)) → MARK(X)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

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

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(U61(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  x1
U31(x1)  =  x1
U61(x1)  =  U61(x1)
U72(x1)  =  x1
a____(x1, x2)  =  a____(x1, x2)
__(x1, x2)  =  __(x1, x2)
mark(x1)  =  x1
nil  =  nil
a__U11(x1)  =  x1
tt  =  tt
a__U21(x1, x2)  =  x2
a__U22(x1)  =  x1
a__isList(x1)  =  x1
a__U31(x1)  =  x1
a__U41(x1, x2)  =  x2
a__U42(x1)  =  x1
a__isNeList(x1)  =  x1
a__U51(x1, x2)  =  a__U51(x2)
a__U52(x1)  =  x1
a__U61(x1)  =  a__U61(x1)
a__U71(x1, x2)  =  a__U71(x1, x2)
a__U72(x1)  =  x1
a__isPal(x1)  =  a__isPal
a__U81(x1)  =  a__U81
a__isQid(x1)  =  x1
a__isNePal(x1)  =  a__isNePal(x1)
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
U11(x1)  =  x1
U21(x1, x2)  =  x2
U22(x1)  =  x1
isList(x1)  =  x1
U41(x1, x2)  =  x2
U42(x1)  =  x1
isNeList(x1)  =  x1
U51(x1, x2)  =  U51(x2)
U52(x1)  =  x1
U71(x1, x2)  =  U71(x1, x2)
isPal(x1)  =  isPal
U81(x1)  =  U81
isQid(x1)  =  x1
isNePal(x1)  =  isNePal(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[a2, 2] > [aU511, U511]
[a2, 2] > [aU712, aisPal, U712, isPal] > [aU81, U81] > [nil, tt, a, i, o]
[aisNePal1, isNePal1] > [U611, aU611] > [nil, tt, a, i, o]
[aisNePal1, isNePal1] > [aU712, aisPal, U712, isPal] > [aU81, U81] > [nil, tt, a, i, o]
e > [nil, tt, a, i, o]
u > [nil, tt, a, i, o]

Status:
U611: multiset
a2: [1,2]
_2: [1,2]
nil: multiset
tt: multiset
aU511: multiset
aU611: multiset
aU712: multiset
aisPal: multiset
aU81: multiset
aisNePal1: [1]
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
U511: multiset
U712: multiset
isPal: multiset
U81: multiset
isNePal1: [1]


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(23) Obligation:

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

MARK(U31(X)) → MARK(X)
MARK(U72(X)) → MARK(X)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

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

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(U31(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK(x1)
U31(x1)  =  U31(x1)
U72(x1)  =  x1
a____(x1, x2)  =  a____(x1, x2)
__(x1, x2)  =  __(x1, x2)
mark(x1)  =  x1
nil  =  nil
a__U11(x1)  =  a__U11
tt  =  tt
a__U21(x1, x2)  =  x2
a__U22(x1)  =  x1
a__isList(x1)  =  x1
a__U31(x1)  =  a__U31(x1)
a__U41(x1, x2)  =  a__U41(x1, x2)
a__U42(x1)  =  a__U42
a__isNeList(x1)  =  a__isNeList(x1)
a__U51(x1, x2)  =  a__U51(x1, x2)
a__U52(x1)  =  x1
a__U61(x1)  =  x1
a__U71(x1, x2)  =  x2
a__U72(x1)  =  x1
a__isPal(x1)  =  x1
a__U81(x1)  =  x1
a__isQid(x1)  =  x1
a__isNePal(x1)  =  x1
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
U11(x1)  =  U11
U21(x1, x2)  =  x2
U22(x1)  =  x1
isList(x1)  =  x1
U41(x1, x2)  =  U41(x1, x2)
U42(x1)  =  U42
isNeList(x1)  =  isNeList(x1)
U51(x1, x2)  =  U51(x1, x2)
U52(x1)  =  x1
U61(x1)  =  x1
U71(x1, x2)  =  x2
isPal(x1)  =  x1
U81(x1)  =  x1
isQid(x1)  =  x1
isNePal(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
[a2, 2] > [aU412, U412] > [aU42, U42] > [MARK1, aU11, tt, a, e, u, U11]
[a2, 2] > [aU412, U412] > [aisNeList1, aU512, isNeList1, U512] > [U311, aU311] > [MARK1, aU11, tt, a, e, u, U11]
nil > [MARK1, aU11, tt, a, e, u, U11]
i > [MARK1, aU11, tt, a, e, u, U11]
o > [MARK1, aU11, tt, a, e, u, U11]

Status:
MARK1: multiset
U311: multiset
a2: [1,2]
_2: [1,2]
nil: multiset
aU11: []
tt: multiset
aU311: multiset
aU412: multiset
aU42: multiset
aisNeList1: multiset
aU512: multiset
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
U11: []
U412: multiset
U42: multiset
isNeList1: multiset
U512: multiset


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(25) Obligation:

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

MARK(U72(X)) → MARK(X)

The TRS R consists of the following rules:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(U72(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK(x1)
U72(x1)  =  U72(x1)
a____(x1, x2)  =  a____(x1, x2)
__(x1, x2)  =  __(x1, x2)
mark(x1)  =  x1
nil  =  nil
a__U11(x1)  =  x1
tt  =  tt
a__U21(x1, x2)  =  x2
a__U22(x1)  =  x1
a__isList(x1)  =  x1
a__U31(x1)  =  x1
a__U41(x1, x2)  =  x1
a__U42(x1)  =  a__U42
a__isNeList(x1)  =  x1
a__U51(x1, x2)  =  x2
a__U52(x1)  =  x1
a__U61(x1)  =  x1
a__U71(x1, x2)  =  a__U71(x1, x2)
a__U72(x1)  =  a__U72(x1)
a__isPal(x1)  =  x1
a__U81(x1)  =  x1
a__isQid(x1)  =  x1
a__isNePal(x1)  =  x1
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u
U11(x1)  =  x1
U21(x1, x2)  =  x2
U22(x1)  =  x1
isList(x1)  =  x1
U31(x1)  =  x1
U41(x1, x2)  =  x1
U42(x1)  =  U42
isNeList(x1)  =  x1
U51(x1, x2)  =  x2
U52(x1)  =  x1
U61(x1)  =  x1
U71(x1, x2)  =  U71(x1, x2)
isPal(x1)  =  x1
U81(x1)  =  x1
isQid(x1)  =  x1
isNePal(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
[a2, 2, aU712, U712] > [U721, aU721] > MARK1
[a2, 2, aU712, U712] > [U721, aU721] > [nil, tt, aU42, U42]
a > [nil, tt, aU42, U42]
e > [nil, tt, aU42, U42]
i > [nil, tt, aU42, U42]
o > [nil, tt, aU42, U42]
u > [nil, tt, aU42, U42]

Status:
MARK1: multiset
U721: [1]
a2: [1,2]
_2: [1,2]
nil: multiset
tt: multiset
aU42: multiset
aU712: [2,1]
aU721: [1]
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset
U42: multiset
U712: [2,1]


The following usable rules [FROCOS05] were oriented:

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

(27) Obligation:

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

a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__U11(tt) → tt
a__U21(tt, V2) → a__U22(a__isList(V2))
a__U22(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNeList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isList(V2))
a__U52(tt) → tt
a__U61(tt) → tt
a__U71(tt, P) → a__U72(a__isPal(P))
a__U72(tt) → tt
a__U81(tt) → tt
a__isList(V) → a__U11(a__isNeList(V))
a__isList(nil) → tt
a__isList(__(V1, V2)) → a__U21(a__isList(V1), V2)
a__isNeList(V) → a__U31(a__isQid(V))
a__isNeList(__(V1, V2)) → a__U41(a__isList(V1), V2)
a__isNeList(__(V1, V2)) → a__U51(a__isNeList(V1), V2)
a__isNePal(V) → a__U61(a__isQid(V))
a__isNePal(__(I, __(P, I))) → a__U71(a__isQid(I), P)
a__isPal(V) → a__U81(a__isNePal(V))
a__isPal(nil) → tt
a__isQid(a) → tt
a__isQid(e) → tt
a__isQid(i) → tt
a__isQid(o) → tt
a__isQid(u) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(U11(X)) → a__U11(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isList(X)) → a__isList(X)
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNeList(X)) → a__isNeList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X)) → a__U61(mark(X))
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X)) → a__U72(mark(X))
mark(isPal(X)) → a__isPal(X)
mark(U81(X)) → a__U81(mark(X))
mark(isQid(X)) → a__isQid(X)
mark(isNePal(X)) → a__isNePal(X)
mark(nil) → nil
mark(tt) → tt
mark(a) → a
mark(e) → e
mark(i) → i
mark(o) → o
mark(u) → u
a____(X1, X2) → __(X1, X2)
a__U11(X) → U11(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isList(X) → isList(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNeList(X) → isNeList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__U61(X) → U61(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X) → U72(X)
a__isPal(X) → isPal(X)
a__U81(X) → U81(X)
a__isQid(X) → isQid(X)
a__isNePal(X) → isNePal(X)

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

(28) PisEmptyProof (EQUIVALENT transformation)

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

(29) TRUE