Termination w.r.t. Q proof of /tmp/tmpSvvQ_r/PALINDROME_nokinds_noand

Termination w.r.t. Q of the given QTRS could not be shown:

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 QDPOrderProof (⇔)

    ↳7 QDP

    ↳8 DependencyGraphProof (⇔)

    ↳9 TRUE

  ↳10 QDP

    ↳11 QDPOrderProof (⇔)

    ↳12 QDP

    ↳13 DependencyGraphProof (⇔)

    ↳14 TRUE

  ↳15 QDP

(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__U71(tt, P) → A__ISPAL(P)
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) = x1
A__ISNEPAL(x1) = x1
__(x1, x2) = __(x1, x2)
a__isQid(x1) = a__isQid
a = a
e = e
i = i
o = o
u = u
isQid(x1) = isQid(x1)

Lexicographic path order with status [LPO].
Precedence:

__₂ > A_{_U71₁}
a_{_isQid} > tt
a_{_isQid} > isQid₁
u > tt

Status:

A_{_U71₁}: [1]
tt: []
__₂: [1,2]
a_{_isQid}: []
a: []
e: []
i: []
o: []
u: []
isQid₁: [1]

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

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

A__ISPAL(V) → A__ISNEPAL(V)

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__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 remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A__U21(x1, x2) = x2
tt = tt
A__ISLIST(x1) = x1
A__ISNELIST(x1) = x1
__(x1, x2) = __(x1, x2)
A__U41(x1, x2) = A__U41(x2)
a__isList(x1) = a__isList(x1)
A__U51(x1, x2) = A__U51(x2)
a__isNeList(x1) = a__isNeList
a__U11(x1) = a__U11(x1)
nil = nil
a__U21(x1, x2) = a__U21(x1)
isList(x1) = isList(x1)
a__U31(x1) = x1
a__isQid(x1) = x1
a__U41(x1, x2) = a__U41(x1)
a__U51(x1, x2) = a__U51(x1)
isNeList(x1) = isNeList
U41(x1, x2) = U41(x1, x2)
U11(x1) = U11
U51(x1, x2) = U51(x1, x2)
a__U52(x1) = x1
U52(x1) = U52(x1)
U21(x1, x2) = U21(x1, x2)
a__U22(x1) = x1
U22(x1) = U22(x1)
a__U42(x1) = x1
U42(x1) = U42(x1)
a = a
e = e
i = i
o = o
u = u
isQid(x1) = isQid(x1)
U31(x1) = U31(x1)

Lexicographic path order with status [LPO].
Precedence:

__₂ > A_{_U41₁} > U31₁
__₂ > A_{_U51₁} > U31₁
__₂ > a_{_U41₁} > U31₁
__₂ > a_{_U51₁} > U51₂ > U31₁
a_{_isNeList} > a_{_isList₁} > tt > U31₁
a_{_isNeList} > a_{_isList₁} > a_{_U11₁} > U11 > U31₁
a_{_isNeList} > a_{_U41₁} > U31₁
a_{_isNeList} > a_{_U51₁} > U51₂ > U31₁
nil > U31₁
a_{_U21₁} > a_{_isList₁} > tt > U31₁
a_{_U21₁} > a_{_isList₁} > a_{_U11₁} > U11 > U31₁
isList₁ > U31₁
isNeList > U31₁
U41₂ > U31₁
U52₁ > U31₁
U21₂ > U31₁
U22₁ > U31₁
U42₁ > U31₁
a > U31₁
e > U31₁
i > U31₁
o > U31₁
u > U31₁
isQid₁ > U31₁

Status:

tt: []
__₂: [1,2]
A_{_U41₁}: [1]
a_{_isList₁}: [1]
A_{_U51₁}: [1]
a_{_isNeList}: []
a_{_U11₁}: [1]
nil: []
a_{_U21₁}: [1]
isList₁: [1]
a_{_U41₁}: [1]
a_{_U51₁}: [1]
isNeList: []
U41₂: [1,2]
U11: []
U51₂: [1,2]
U52₁: [1]
U21₂: [1,2]
U22₁: [1]
U42₁: [1]
a: []
e: []
i: []
o: []
u: []
isQid₁: [1]
U31₁: [1]

The following usable rules [FROCOS05] were oriented: none

(12) 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)

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