Termination w.r.t. Q proof of /tmp/tmpas9XS1/PALINDROME_nokinds

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 QDPOrderProof (⇔)

    ↳7 QDP

    ↳8 PisEmptyProof (⇔)

    ↳9 TRUE

  ↳10 QDP

    ↳11 QDPOrderProof (⇔)

    ↳12 QDP

    ↳13 PisEmptyProof (⇔)

    ↳14 TRUE

  ↳15 QDP

    ↳16 QDPOrderProof (⇔)

    ↳17 QDP

    ↳18 PisEmptyProof (⇔)

    ↳19 TRUE

  ↳20 QDP

    ↳21 QDPOrderProof (⇔)

    ↳22 QDP

    ↳23 PisEmptyProof (⇔)

    ↳24 TRUE

  ↳25 QDP

    ↳26 QDPOrderProof (⇔)

    ↳27 QDP

    ↳28 PisEmptyProof (⇔)

    ↳29 TRUE

  ↳30 QDP

    ↳31 QDPOrderProof (⇔)

    ↳32 QDP

    ↳33 QDPOrderProof (⇔)

    ↳34 QDP

    ↳35 PisEmptyProof (⇔)

    ↳36 TRUE

  ↳37 QDP

    ↳38 QDPOrderProof (⇔)

    ↳39 QDP

    ↳40 QDPOrderProof (⇔)

    ↳41 QDP

    ↳42 PisEmptyProof (⇔)

    ↳43 TRUE

  ↳44 QDP

    ↳45 QDPOrderProof (⇔)

    ↳46 QDP

    ↳47 QDPOrderProof (⇔)

    ↳48 QDP

    ↳49 QDPOrderProof (⇔)

    ↳50 QDP

    ↳51 PisEmptyProof (⇔)

    ↳52 TRUE

  ↳53 QDP

    ↳54 QDPOrderProof (⇔)

    ↳55 QDP

    ↳56 QDPOrderProof (⇔)

    ↳57 QDP

    ↳58 PisEmptyProof (⇔)

    ↳59 TRUE

  ↳60 QDP

    ↳61 QDPOrderProof (⇔)

    ↳62 QDP

    ↳63 QDPOrderProof (⇔)

    ↳64 QDP

    ↳65 PisEmptyProof (⇔)

    ↳66 TRUE

(0) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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:

ACTIVE(__(__(X, Y), Z)) → __¹(X, __(Y, Z))
ACTIVE(__(__(X, Y), Z)) → __¹(Y, Z)
ACTIVE(isList(V)) → ISNELIST(V)
ACTIVE(isList(__(V1, V2))) → AND(isList(V1), isList(V2))
ACTIVE(isList(__(V1, V2))) → ISLIST(V1)
ACTIVE(isList(__(V1, V2))) → ISLIST(V2)
ACTIVE(isNeList(V)) → ISQID(V)
ACTIVE(isNeList(__(V1, V2))) → AND(isList(V1), isNeList(V2))
ACTIVE(isNeList(__(V1, V2))) → ISLIST(V1)
ACTIVE(isNeList(__(V1, V2))) → ISNELIST(V2)
ACTIVE(isNeList(__(V1, V2))) → AND(isNeList(V1), isList(V2))
ACTIVE(isNeList(__(V1, V2))) → ISNELIST(V1)
ACTIVE(isNeList(__(V1, V2))) → ISLIST(V2)
ACTIVE(isNePal(V)) → ISQID(V)
ACTIVE(isNePal(__(I, __(P, I)))) → AND(isQid(I), isPal(P))
ACTIVE(isNePal(__(I, __(P, I)))) → ISQID(I)
ACTIVE(isNePal(__(I, __(P, I)))) → ISPAL(P)
ACTIVE(isPal(V)) → ISNEPAL(V)
ACTIVE(__(X1, X2)) → __¹(active(X1), X2)
ACTIVE(__(X1, X2)) → ACTIVE(X1)
ACTIVE(__(X1, X2)) → __¹(X1, active(X2))
ACTIVE(__(X1, X2)) → ACTIVE(X2)
ACTIVE(and(X1, X2)) → AND(active(X1), X2)
ACTIVE(and(X1, X2)) → ACTIVE(X1)
__¹(mark(X1), X2) → __¹(X1, X2)
__¹(X1, mark(X2)) → __¹(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
PROPER(__(X1, X2)) → __¹(proper(X1), proper(X2))
PROPER(__(X1, X2)) → PROPER(X1)
PROPER(__(X1, X2)) → PROPER(X2)
PROPER(and(X1, X2)) → AND(proper(X1), proper(X2))
PROPER(and(X1, X2)) → PROPER(X1)
PROPER(and(X1, X2)) → PROPER(X2)
PROPER(isList(X)) → ISLIST(proper(X))
PROPER(isList(X)) → PROPER(X)
PROPER(isNeList(X)) → ISNELIST(proper(X))
PROPER(isNeList(X)) → PROPER(X)
PROPER(isQid(X)) → ISQID(proper(X))
PROPER(isQid(X)) → PROPER(X)
PROPER(isNePal(X)) → ISNEPAL(proper(X))
PROPER(isNePal(X)) → PROPER(X)
PROPER(isPal(X)) → ISPAL(proper(X))
PROPER(isPal(X)) → PROPER(X)
__¹(ok(X1), ok(X2)) → __¹(X1, X2)
AND(ok(X1), ok(X2)) → AND(X1, X2)
ISLIST(ok(X)) → ISLIST(X)
ISNELIST(ok(X)) → ISNELIST(X)
ISQID(ok(X)) → ISQID(X)
ISNEPAL(ok(X)) → ISNEPAL(X)
ISPAL(ok(X)) → ISPAL(X)
TOP(mark(X)) → TOP(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
TOP(ok(X)) → ACTIVE(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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 10 SCCs with 30 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

ISPAL(ok(X)) → ISPAL(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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.

ISPAL(ok(X)) → ISPAL(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISPAL(x1) = ISPAL(x1)
ok(x1) = ok(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
mark(x1) = x1
nil = nil
and(x1, x2) = x2
tt = tt
isList(x1) = x1
isNeList(x1) = isNeList(x1)
isQid(x1) = x1
isNePal(x1) = x1
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

u > [ISPAL₁, ok₁, isNeList₁]
u > [tt, a]
top > active₁ > __₂ > [ISPAL₁, ok₁, isNeList₁]
top > active₁ > [tt, a]
top > proper₁ > __₂ > [ISPAL₁, ok₁, isNeList₁]
top > proper₁ > nil > [tt, a]
top > proper₁ > e > [tt, a]
top > proper₁ > i > [ISPAL₁, ok₁, isNeList₁]
top > proper₁ > i > [tt, a]
top > proper₁ > o > [ISPAL₁, ok₁, isNeList₁]
top > proper₁ > o > [tt, a]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(7) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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:

ISNEPAL(ok(X)) → ISNEPAL(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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.

ISNEPAL(ok(X)) → ISNEPAL(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNEPAL(x1) = ISNEPAL(x1)
ok(x1) = ok(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
mark(x1) = x1
nil = nil
and(x1, x2) = x2
tt = tt
isList(x1) = x1
isNeList(x1) = isNeList(x1)
isQid(x1) = x1
isNePal(x1) = x1
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

u > [ISNEPAL₁, ok₁, isNeList₁]
u > [tt, a]
top > active₁ > __₂ > [ISNEPAL₁, ok₁, isNeList₁]
top > active₁ > [tt, a]
top > proper₁ > __₂ > [ISNEPAL₁, ok₁, isNeList₁]
top > proper₁ > nil > [tt, a]
top > proper₁ > e > [tt, a]
top > proper₁ > i > [ISNEPAL₁, ok₁, isNeList₁]
top > proper₁ > i > [tt, a]
top > proper₁ > o > [ISNEPAL₁, ok₁, isNeList₁]
top > proper₁ > o > [tt, a]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(12) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(13) PisEmptyProof (EQUIVALENT transformation)

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

(14) TRUE

(15) Obligation:

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

ISQID(ok(X)) → ISQID(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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.

ISQID(ok(X)) → ISQID(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISQID(x1) = ISQID(x1)
ok(x1) = ok(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
mark(x1) = x1
nil = nil
and(x1, x2) = x2
tt = tt
isList(x1) = x1
isNeList(x1) = isNeList(x1)
isQid(x1) = x1
isNePal(x1) = x1
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

u > [ISQID₁, ok₁, isNeList₁]
u > [tt, a]
top > active₁ > __₂ > [ISQID₁, ok₁, isNeList₁]
top > active₁ > [tt, a]
top > proper₁ > __₂ > [ISQID₁, ok₁, isNeList₁]
top > proper₁ > nil > [tt, a]
top > proper₁ > e > [tt, a]
top > proper₁ > i > [ISQID₁, ok₁, isNeList₁]
top > proper₁ > i > [tt, a]
top > proper₁ > o > [ISQID₁, ok₁, isNeList₁]
top > proper₁ > o > [tt, a]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(17) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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:

ISNELIST(ok(X)) → ISNELIST(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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.

ISNELIST(ok(X)) → ISNELIST(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISNELIST(x1) = ISNELIST(x1)
ok(x1) = ok(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
mark(x1) = x1
nil = nil
and(x1, x2) = x2
tt = tt
isList(x1) = x1
isNeList(x1) = isNeList(x1)
isQid(x1) = x1
isNePal(x1) = x1
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

u > [ISNELIST₁, ok₁, isNeList₁]
u > [tt, a]
top > active₁ > __₂ > [ISNELIST₁, ok₁, isNeList₁]
top > active₁ > [tt, a]
top > proper₁ > __₂ > [ISNELIST₁, ok₁, isNeList₁]
top > proper₁ > nil > [tt, a]
top > proper₁ > e > [tt, a]
top > proper₁ > i > [ISNELIST₁, ok₁, isNeList₁]
top > proper₁ > i > [tt, a]
top > proper₁ > o > [ISNELIST₁, ok₁, isNeList₁]
top > proper₁ > o > [tt, a]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(22) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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

(25) Obligation:

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

ISLIST(ok(X)) → ISLIST(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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.

ISLIST(ok(X)) → ISLIST(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ISLIST(x1) = ISLIST(x1)
ok(x1) = ok(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
mark(x1) = x1
nil = nil
and(x1, x2) = x2
tt = tt
isList(x1) = x1
isNeList(x1) = isNeList(x1)
isQid(x1) = x1
isNePal(x1) = x1
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

u > [ISLIST₁, ok₁, isNeList₁]
u > [tt, a]
top > active₁ > __₂ > [ISLIST₁, ok₁, isNeList₁]
top > active₁ > [tt, a]
top > proper₁ > __₂ > [ISLIST₁, ok₁, isNeList₁]
top > proper₁ > nil > [tt, a]
top > proper₁ > e > [tt, a]
top > proper₁ > i > [ISLIST₁, ok₁, isNeList₁]
top > proper₁ > i > [tt, a]
top > proper₁ > o > [ISLIST₁, ok₁, isNeList₁]
top > proper₁ > o > [tt, a]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(27) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(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

(30) Obligation:

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

AND(ok(X1), ok(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(31) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

AND(ok(X1), ok(X2)) → AND(X1, X2)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
AND(x1, x2) = AND(x2)
ok(x1) = ok(x1)
mark(x1) = mark
active(x1) = active(x1)
__(x1, x2) = x2
nil = nil
and(x1, x2) = and(x2)
tt = tt
isList(x1) = x1
isNeList(x1) = x1
isQid(x1) = isQid(x1)
isNePal(x1) = isNePal(x1)
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

nil > [AND₁, ok₁, isQid₁, isNePal₁] > top > active₁ > [mark, a]
[and₁, proper₁] > [AND₁, ok₁, isQid₁, isNePal₁] > top > active₁ > [mark, a]
[and₁, proper₁] > o > [mark, a]
[and₁, proper₁] > u > [mark, a]
tt > [AND₁, ok₁, isQid₁, isNePal₁] > top > active₁ > [mark, a]
e > [AND₁, ok₁, isQid₁, isNePal₁] > top > active₁ > [mark, a]
i > [AND₁, ok₁, isQid₁, isNePal₁] > top > active₁ > [mark, a]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(32) Obligation:

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

AND(mark(X1), X2) → AND(X1, X2)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

AND(mark(X1), X2) → AND(X1, X2)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
AND(x1, x2) = AND(x1)
mark(x1) = mark(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
nil = nil
and(x1, x2) = and(x1, x2)
tt = tt
isList(x1) = isList
isNeList(x1) = isNeList
isQid(x1) = isQid
isNePal(x1) = x1
isPal(x1) = isPal(x1)
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
ok(x1) = x1
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

[active₁, tt] > isNeList > isList > [a, proper₁] > __₂ > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isNeList > isList > [a, proper₁] > and₂ > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isNeList > isList > [a, proper₁] > e > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isNeList > isList > [a, proper₁] > i > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isNeList > isList > [a, proper₁] > o > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isNeList > isList > [a, proper₁] > u > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isQid > [a, proper₁] > __₂ > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isQid > [a, proper₁] > and₂ > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isQid > [a, proper₁] > e > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isQid > [a, proper₁] > i > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isQid > [a, proper₁] > o > [AND₁, mark₁, nil, isPal₁, top]
[active₁, tt] > isQid > [a, proper₁] > u > [AND₁, mark₁, nil, isPal₁, top]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(34) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(35) PisEmptyProof (EQUIVALENT transformation)

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

(36) TRUE

(37) Obligation:

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

__¹(X1, mark(X2)) → __¹(X1, X2)
__¹(mark(X1), X2) → __¹(X1, X2)
__¹(ok(X1), ok(X2)) → __¹(X1, X2)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

__¹(mark(X1), X2) → __¹(X1, X2)
__¹(ok(X1), ok(X2)) → __¹(X1, X2)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
__¹(x1, x2) = __¹(x1)
mark(x1) = mark(x1)
ok(x1) = ok(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
nil = nil
and(x1, x2) = and(x1, x2)
tt = tt
isList(x1) = isList(x1)
isNeList(x1) = x1
isQid(x1) = isQid(x1)
isNePal(x1) = isNePal(x1)
isPal(x1) = isPal(x1)
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

i > [active₁, and₂, tt, isPal₁, e, o, proper₁] > [_{_₂}, isList₁] > [ok₁, nil, isQid₁, u] > mark₁
i > [active₁, and₂, tt, isPal₁, e, o, proper₁] > isNePal₁ > [ok₁, nil, isQid₁, u] > mark₁
i > [active₁, and₂, tt, isPal₁, e, o, proper₁] > a

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(39) Obligation:

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

__¹(X1, mark(X2)) → __¹(X1, X2)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

__¹(X1, mark(X2)) → __¹(X1, X2)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
__¹(x1, x2) = __¹(x1, x2)
mark(x1) = mark(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
nil = nil
and(x1, x2) = and(x1, x2)
tt = tt
isList(x1) = isList
isNeList(x1) = isNeList
isQid(x1) = isQid
isNePal(x1) = isNePal
isPal(x1) = isPal
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

active₁ > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isList > [tt, a, e, o]
active₁ > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isList > [ok, top]
active₁ > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isQid > [tt, a, e, o]
active₁ > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isQid > [ok, top]
active₁ > [and₂, proper₁] > nil > [tt, a, e, o]
active₁ > [and₂, proper₁] > nil > [ok, top]
active₁ > [and₂, proper₁] > u > [tt, a, e, o]
active₁ > [and₂, proper₁] > u > [ok, top]
[isNePal, isPal] > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isList > [tt, a, e, o]
[isNePal, isPal] > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isList > [ok, top]
[isNePal, isPal] > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isQid > [tt, a, e, o]
[isNePal, isPal] > [and₂, proper₁] > __₂ > [mark₁, isNeList] > isQid > [ok, top]
[isNePal, isPal] > [and₂, proper₁] > nil > [tt, a, e, o]
[isNePal, isPal] > [and₂, proper₁] > nil > [ok, top]
[isNePal, isPal] > [and₂, proper₁] > u > [tt, a, e, o]
[isNePal, isPal] > [and₂, proper₁] > u > [ok, top]
i > [mark₁, isNeList] > isList > [tt, a, e, o]
i > [mark₁, isNeList] > isList > [ok, top]
i > [mark₁, isNeList] > isQid > [tt, a, e, o]
i > [mark₁, isNeList] > isQid > [ok, top]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(41) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(42) PisEmptyProof (EQUIVALENT transformation)

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

(43) TRUE

(44) Obligation:

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

PROPER(__(X1, X2)) → PROPER(X2)
PROPER(__(X1, X2)) → PROPER(X1)
PROPER(and(X1, X2)) → PROPER(X1)
PROPER(and(X1, X2)) → PROPER(X2)
PROPER(isList(X)) → PROPER(X)
PROPER(isNeList(X)) → PROPER(X)
PROPER(isQid(X)) → PROPER(X)
PROPER(isNePal(X)) → PROPER(X)
PROPER(isPal(X)) → PROPER(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(__(X1, X2)) → PROPER(X2)
PROPER(__(X1, X2)) → PROPER(X1)
PROPER(and(X1, X2)) → PROPER(X1)
PROPER(and(X1, X2)) → PROPER(X2)
PROPER(isList(X)) → PROPER(X)
PROPER(isPal(X)) → PROPER(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PROPER(x1) = PROPER(x1)
__(x1, x2) = __(x1, x2)
and(x1, x2) = and(x1, x2)
isList(x1) = isList(x1)
isNeList(x1) = x1
isQid(x1) = x1
isNePal(x1) = x1
isPal(x1) = isPal(x1)
active(x1) = active(x1)
mark(x1) = mark
nil = nil
tt = tt
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

active₁ > __₂ > isList₁
active₁ > __₂ > isPal₁ > tt
active₁ > __₂ > mark > and₂
active₁ > __₂ > mark > top
[a, e, proper₁] > nil
[a, e, proper₁] > i > mark > and₂
[a, e, proper₁] > i > mark > top
[a, e, proper₁] > i > tt
[a, e, proper₁] > ok > __₂ > isList₁
[a, e, proper₁] > ok > __₂ > isPal₁ > tt
[a, e, proper₁] > ok > __₂ > mark > and₂
[a, e, proper₁] > ok > __₂ > mark > top
o > ok > __₂ > isList₁
o > ok > __₂ > isPal₁ > tt
o > ok > __₂ > mark > and₂
o > ok > __₂ > mark > top
u > ok > __₂ > isList₁
u > ok > __₂ > isPal₁ > tt
u > ok > __₂ > mark > and₂
u > ok > __₂ > mark > top

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(46) Obligation:

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

PROPER(isNeList(X)) → PROPER(X)
PROPER(isQid(X)) → PROPER(X)
PROPER(isNePal(X)) → PROPER(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(47) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(isQid(X)) → PROPER(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PROPER(x1) = PROPER(x1)
isNeList(x1) = x1
isQid(x1) = isQid(x1)
isNePal(x1) = x1
active(x1) = active(x1)
__(x1, x2) = x1
mark(x1) = mark
nil = nil
and(x1, x2) = and
tt = tt
isList(x1) = isList(x1)
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = x1
ok(x1) = x1
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

[PROPER₁, isQid₁] > tt > [active₁, mark, and, i, top]
nil > [active₁, mark, and, i, top]
isList₁ > [active₁, mark, and, i, top]
a > tt > [active₁, mark, and, i, top]
e > [active₁, mark, and, i, top]
o > [active₁, mark, and, i, top]
u > tt > [active₁, mark, and, i, top]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(48) Obligation:

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

PROPER(isNeList(X)) → PROPER(X)
PROPER(isNePal(X)) → PROPER(X)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(isNeList(X)) → PROPER(X)
PROPER(isNePal(X)) → PROPER(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PROPER(x1) = x1
isNeList(x1) = isNeList(x1)
isNePal(x1) = isNePal(x1)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
mark(x1) = mark
nil = nil
and(x1, x2) = and
tt = tt
isList(x1) = x1
isQid(x1) = isQid(x1)
isPal(x1) = isPal(x1)
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

tt > mark > __₂ > isNeList₁ > [a, u, ok, top] > isNePal₁
tt > mark > __₂ > isQid₁ > [a, u, ok, top] > isNePal₁
[i, o, proper₁] > [active₁, and] > mark > __₂ > isNeList₁ > [a, u, ok, top] > isNePal₁
[i, o, proper₁] > [active₁, and] > mark > __₂ > isQid₁ > [a, u, ok, top] > isNePal₁
[i, o, proper₁] > [active₁, and] > isPal₁ > [a, u, ok, top] > isNePal₁
[i, o, proper₁] > nil
[i, o, proper₁] > e

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(50) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(51) PisEmptyProof (EQUIVALENT transformation)

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

(52) TRUE

(53) Obligation:

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

ACTIVE(__(X1, X2)) → ACTIVE(X2)
ACTIVE(__(X1, X2)) → ACTIVE(X1)
ACTIVE(and(X1, X2)) → ACTIVE(X1)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVE(__(X1, X2)) → ACTIVE(X2)
ACTIVE(__(X1, X2)) → ACTIVE(X1)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1) = ACTIVE(x1)
__(x1, x2) = __(x1, x2)
and(x1, x2) = x1
active(x1) = active(x1)
mark(x1) = mark
nil = nil
tt = tt
isList(x1) = isList
isNeList(x1) = isNeList
isQid(x1) = isQid(x1)
isNePal(x1) = x1
isPal(x1) = isPal(x1)
a = a
e = e
i = i
o = o
u = u
proper(x1) = x1
ok(x1) = x1
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

nil > [_{_₂}, active₁, mark, isNeList] > isList > [tt, isQid₁]
nil > [_{_₂}, active₁, mark, isNeList] > isPal₁
nil > [_{_₂}, active₁, mark, isNeList] > top
a > [_{_₂}, active₁, mark, isNeList] > isList > [tt, isQid₁]
a > [_{_₂}, active₁, mark, isNeList] > isPal₁
a > [_{_₂}, active₁, mark, isNeList] > top
e > [tt, isQid₁]
i > [tt, isQid₁]
u > [_{_₂}, active₁, mark, isNeList] > isList > [tt, isQid₁]
u > [_{_₂}, active₁, mark, isNeList] > isPal₁
u > [_{_₂}, active₁, mark, isNeList] > top

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(55) Obligation:

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

ACTIVE(and(X1, X2)) → ACTIVE(X1)

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(56) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVE(and(X1, X2)) → ACTIVE(X1)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1) = ACTIVE(x1)
and(x1, x2) = and(x1, x2)
active(x1) = active(x1)
__(x1, x2) = __(x1, x2)
mark(x1) = x1
nil = nil
tt = tt
isList(x1) = isList(x1)
isNeList(x1) = x1
isQid(x1) = isQid
isNePal(x1) = isNePal(x1)
isPal(x1) = isPal(x1)
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
ok(x1) = ok
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

[active₁, tt, i] > [nil, isQid, a, e, o, u, ok, top] > [and₂, _{_₂}, isList₁, proper₁] > ACTIVE₁
[active₁, tt, i] > [nil, isQid, a, e, o, u, ok, top] > [and₂, _{_₂}, isList₁, proper₁] > isPal₁ > isNePal₁

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(57) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(58) PisEmptyProof (EQUIVALENT transformation)

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

(59) TRUE

(60) Obligation:

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

TOP(ok(X)) → TOP(active(X))
TOP(mark(X)) → TOP(proper(X))

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(61) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

TOP(mark(X)) → TOP(proper(X))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
TOP(x1) = TOP(x1)
ok(x1) = x1
active(x1) = x1
mark(x1) = mark(x1)
proper(x1) = x1
__(x1, x2) = __(x1, x2)
nil = nil
and(x1, x2) = and(x1, x2)
tt = tt
isList(x1) = isList(x1)
isNeList(x1) = isNeList(x1)
isQid(x1) = x1
isNePal(x1) = isNePal(x1)
isPal(x1) = isPal(x1)
a = a
e = e
i = i
o = o
u = u
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

__₂ > [and₂, isList₁] > [TOP₁, mark₁, isNeList₁, isNePal₁] > top
__₂ > [and₂, isList₁] > tt > top
__₂ > isPal₁ > [TOP₁, mark₁, isNeList₁, isNePal₁] > top
__₂ > isPal₁ > tt > top
nil > top
a > [TOP₁, mark₁, isNeList₁, isNePal₁] > top
a > tt > top
e > [TOP₁, mark₁, isNeList₁, isNePal₁] > top
e > tt > top
i > [TOP₁, mark₁, isNeList₁, isNePal₁] > top
i > tt > top
o > [TOP₁, mark₁, isNeList₁, isNePal₁] > top
o > tt > top
u > [TOP₁, mark₁, isNeList₁, isNePal₁] > top
u > tt > top

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(62) Obligation:

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

TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(63) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

TOP(ok(X)) → TOP(active(X))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
TOP(x1) = TOP(x1)
ok(x1) = ok(x1)
active(x1) = x1
__(x1, x2) = x2
mark(x1) = mark
nil = nil
and(x1, x2) = and(x1, x2)
tt = tt
isList(x1) = isList(x1)
isNeList(x1) = isNeList(x1)
isQid(x1) = isQid(x1)
isNePal(x1) = isNePal(x1)
isPal(x1) = x1
a = a
e = e
i = i
o = o
u = u
proper(x1) = proper(x1)
top(x1) = top

Lexicographic Path Order [LPO].
Precedence:

[isNeList₁, proper₁] > isList₁ > and₂ > [TOP₁, ok₁, i] > tt > [mark, nil, e]
[isNeList₁, proper₁] > isList₁ > and₂ > [TOP₁, ok₁, i] > top > [mark, nil, e]
[isNeList₁, proper₁] > isQid₁ > [TOP₁, ok₁, i] > tt > [mark, nil, e]
[isNeList₁, proper₁] > isQid₁ > [TOP₁, ok₁, i] > top > [mark, nil, e]
[isNeList₁, proper₁] > isNePal₁ > [TOP₁, ok₁, i] > tt > [mark, nil, e]
[isNeList₁, proper₁] > isNePal₁ > [TOP₁, ok₁, i] > top > [mark, nil, e]
[isNeList₁, proper₁] > u > [TOP₁, ok₁, i] > tt > [mark, nil, e]
[isNeList₁, proper₁] > u > [TOP₁, ok₁, i] > top > [mark, nil, e]
a > [TOP₁, ok₁, i] > tt > [mark, nil, e]
a > [TOP₁, ok₁, i] > top > [mark, nil, e]
o > [TOP₁, ok₁, i] > tt > [mark, nil, e]
o > [TOP₁, ok₁, i] > top > [mark, nil, e]

The following usable rules [FROCOS05] were oriented:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

(64) Obligation:

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

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
active(__(X1, X2)) → __(active(X1), X2)
active(__(X1, X2)) → __(X1, active(X2))
active(and(X1, X2)) → and(active(X1), X2)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
proper(__(X1, X2)) → __(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isList(X)) → isList(proper(X))
proper(isNeList(X)) → isNeList(proper(X))
proper(isQid(X)) → isQid(proper(X))
proper(isNePal(X)) → isNePal(proper(X))
proper(isPal(X)) → isPal(proper(X))
proper(a) → ok(a)
proper(e) → ok(e)
proper(i) → ok(i)
proper(o) → ok(o)
proper(u) → ok(u)
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isList(ok(X)) → ok(isList(X))
isNeList(ok(X)) → ok(isNeList(X))
isQid(ok(X)) → ok(isQid(X))
isNePal(ok(X)) → ok(isNePal(X))
isPal(ok(X)) → ok(isPal(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

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

(65) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) QDPOrderProof (EQUIVALENT transformation)

(7) Obligation:

(8) PisEmptyProof (EQUIVALENT transformation)

(9) TRUE

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) PisEmptyProof (EQUIVALENT transformation)

(14) TRUE

(15) Obligation:

(16) QDPOrderProof (EQUIVALENT transformation)

(17) Obligation:

(18) PisEmptyProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) QDPOrderProof (EQUIVALENT transformation)

(22) Obligation:

(23) PisEmptyProof (EQUIVALENT transformation)

(24) TRUE

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) PisEmptyProof (EQUIVALENT transformation)

(29) TRUE

(30) Obligation:

(31) QDPOrderProof (EQUIVALENT transformation)

(32) Obligation:

(33) QDPOrderProof (EQUIVALENT transformation)

(34) Obligation:

(35) PisEmptyProof (EQUIVALENT transformation)

(36) TRUE

(37) Obligation:

(38) QDPOrderProof (EQUIVALENT transformation)

(39) Obligation:

(40) QDPOrderProof (EQUIVALENT transformation)

(41) Obligation:

(42) PisEmptyProof (EQUIVALENT transformation)

(43) TRUE

(44) Obligation:

(45) QDPOrderProof (EQUIVALENT transformation)

(46) Obligation:

(47) QDPOrderProof (EQUIVALENT transformation)

(48) Obligation:

(49) QDPOrderProof (EQUIVALENT transformation)

(50) Obligation:

(51) PisEmptyProof (EQUIVALENT transformation)

(52) TRUE

(53) Obligation:

(54) QDPOrderProof (EQUIVALENT transformation)

(55) Obligation:

(56) QDPOrderProof (EQUIVALENT transformation)

(57) Obligation:

(58) PisEmptyProof (EQUIVALENT transformation)

(59) TRUE

(60) Obligation:

(61) QDPOrderProof (EQUIVALENT transformation)

(62) Obligation:

(63) QDPOrderProof (EQUIVALENT transformation)

(64) Obligation:

(65) PisEmptyProof (EQUIVALENT transformation)

(66) TRUE