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

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ISPAL(x1)  =  ISPAL
ok(x1)  =  ok(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ISPAL: []
ok₁: [1]

The following usable rules [FROCOS05] were oriented: none

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ISNEPAL(x1)  =  ISNEPAL
ok(x1)  =  ok(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ISNEPAL: []
ok₁: [1]

The following usable rules [FROCOS05] were oriented: none

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ISQID(x1)  =  ISQID
ok(x1)  =  ok(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ISQID: []
ok₁: [1]

The following usable rules [FROCOS05] were oriented: none

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ISNELIST(x1)  =  ISNELIST
ok(x1)  =  ok(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ISNELIST: []
ok₁: [1]

The following usable rules [FROCOS05] were oriented: none

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ISLIST(x1)  =  ISLIST
ok(x1)  =  ok(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ISLIST: []
ok₁: [1]

The following usable rules [FROCOS05] were oriented: none

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
AND(x1, x2)  =  x2
ok(x1)  =  ok(x1)
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ok₁: [1]
mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

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

Tags:
AND has argument tags [3,3,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
AND(x1, x2)  =  x2
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
__¹(x0, x1, x2)  =  __¹(x1)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
__¹(x1, x2)  =  x1
mark(x1)  =  mark(x1)
ok(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

(39) Obligation:

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

__¹(X1, mark(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.

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
__¹(x0, x1, x2)  =  __¹(x1)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
__¹(x1, x2)  =  __¹
mark(x1)  =  mark(x1)
ok(x1)  =  ok(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

__^1: []
mark₁: [1]
ok₁: [1]

The following usable rules [FROCOS05] were oriented: none

(41) 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.

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
__¹(x1, x2)  =  __¹(x2)
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

__^11: [1]
mark₁: [1]

The following usable rules [FROCOS05] were oriented: none

(43) 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.

(44) PisEmptyProof (EQUIVALENT transformation)

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

(45) TRUE

(46) 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.

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
PROPER(x1)  =  PROPER
__(x1, x2)  =  __(x1, x2)
and(x1, x2)  =  and(x1, x2)
isList(x1)  =  x1
isNeList(x1)  =  x1
isQid(x1)  =  isQid(x1)
isNePal(x1)  =  x1
isPal(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

isQid₁ > PROPER

Status:

PROPER: []
_₂: [2,1]
and₂: [2,1]
isQid₁: [1]

The following usable rules [FROCOS05] were oriented: none

(48) 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(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.

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(isList(X)) → PROPER(X)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
PROPER(x0, x1)  =  PROPER(x0, x1)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
PROPER(x1)  =  PROPER
__(x1, x2)  =  __(x1, x2)
and(x1, x2)  =  and(x1, x2)
isList(x1)  =  isList(x1)
isNeList(x1)  =  x1
isNePal(x1)  =  x1
isPal(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

[PROPER, isList₁]

Status:

PROPER: []
_₂: [1,2]
and₂: [1,2]
isList₁: [1]

The following usable rules [FROCOS05] were oriented: none

(50) 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(isNeList(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.

(51) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(and(X1, X2)) → PROPER(X1)
PROPER(and(X1, X2)) → PROPER(X2)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
PROPER(x0, x1)  =  PROPER(x0, x1)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
PROPER(x1)  =  PROPER
__(x1, x2)  =  __(x1, x2)
and(x1, x2)  =  and(x1, x2)
isNeList(x1)  =  isNeList(x1)
isNePal(x1)  =  x1
isPal(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

and₂ > PROPER

Status:

PROPER: []
_₂: [2,1]
and₂: [1,2]
isNeList₁: [1]

The following usable rules [FROCOS05] were oriented: none

(52) Obligation:

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

PROPER(__(X1, X2)) → PROPER(X2)
PROPER(__(X1, X2)) → PROPER(X1)
PROPER(isNeList(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.

(53) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
PROPER(x0, x1)  =  PROPER(x0, x1)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
PROPER(x1)  =  PROPER
__(x1, x2)  =  __(x1, x2)
isNeList(x1)  =  x1
isNePal(x1)  =  isNePal(x1)
isPal(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

isNePal₁ > PROPER

Status:

PROPER: []
_₂: [1,2]
isNePal₁: [1]

The following usable rules [FROCOS05] were oriented: none

(54) Obligation:

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

PROPER(__(X1, X2)) → PROPER(X2)
PROPER(__(X1, X2)) → PROPER(X1)
PROPER(isNeList(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.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
PROPER(x0, x1)  =  PROPER(x0, x1)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
PROPER(x1)  =  PROPER
__(x1, x2)  =  __(x1, x2)
isNeList(x1)  =  isNeList(x1)
isPal(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

[PROPER, isNeList₁]

Status:

PROPER: []
_₂: [2,1]
isNeList₁: [1]

The following usable rules [FROCOS05] were oriented: none

(56) Obligation:

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

PROPER(__(X1, X2)) → PROPER(X2)
PROPER(__(X1, X2)) → PROPER(X1)
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.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
PROPER(x0, x1)  =  PROPER(x0)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
PROPER(x1)  =  PROPER(x1)
__(x1, x2)  =  __(x1, x2)
isPal(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

PROPER₁: [1]
_₂: [1,2]

The following usable rules [FROCOS05] were oriented: none

(58) Obligation:

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

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.

(59) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROPER(isPal(X)) → PROPER(X)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
PROPER(x0, x1)  =  PROPER(x1)

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
PROPER(x1)  =  PROPER
isPal(x1)  =  isPal(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

PROPER: []
isPal₁: [1]

The following usable rules [FROCOS05] were oriented: none

(60) 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.

(61) PisEmptyProof (EQUIVALENT transformation)

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

(62) TRUE

(63) 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.

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ACTIVE(x1)  =  ACTIVE(x1)
__(x1, x2)  =  __(x1, x2)
and(x1, x2)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ACTIVE₁: [1]
_₂: [2,1]

The following usable rules [FROCOS05] were oriented: none

(65) 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.

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
ACTIVE(x1)  =  ACTIVE
and(x1, x2)  =  and(x1, x2)

Lexicographic path order with status [LPO].
Quasi-Precedence:

trivial

Status:

ACTIVE: []
and₂: [1,2]

The following usable rules [FROCOS05] were oriented: none

(67) 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.

(68) PisEmptyProof (EQUIVALENT transformation)

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

(69) TRUE

(70) 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.

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
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

Lexicographic path order with status [LPO].
Quasi-Precedence:

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

Status:

TOP₁: [1]
mark₁: [1]
_₂: [1,2]
nil: []
and₂: [2,1]
tt: []
isList₁: [1]
isNeList₁: [1]
isNePal₁: [1]
isPal₁: [1]
a: []
e: []
i: []
o: []
u: []

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)
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)
__(mark(X1), X2) → mark(__(X1, X2))
__(X1, mark(X2)) → mark(__(X1, X2))
__(ok(X1), ok(X2)) → ok(__(X1, X2))
and(mark(X1), X2) → mark(and(X1, X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNeList(ok(X)) → ok(isNeList(X))
isList(ok(X)) → ok(isList(X))
isQid(ok(X)) → ok(isQid(X))
isPal(ok(X)) → ok(isPal(X))
isNePal(ok(X)) → ok(isNePal(X))

(72) 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.

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

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

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
TOP(x1)  =  TOP
ok(x1)  =  ok(x1)
active(x1)  =  x1
__(x1, x2)  =  __(x1)
mark(x1)  =  mark
nil  =  nil
and(x1, x2)  =  x2
tt  =  tt
isList(x1)  =  x1
isNeList(x1)  =  x1
isQid(x1)  =  x1
isNePal(x1)  =  isNePal
isPal(x1)  =  x1
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Lexicographic path order with status [LPO].
Quasi-Precedence:

TOP > [mark, nil, tt, isNePal, e, i, o]
[ok₁, ₁] > [mark, nil, tt, isNePal, e, i, o]
a > [mark, nil, tt, isNePal, e, i, o]
u > [mark, nil, tt, isNePal, e, i, o]

Status:

TOP: []
ok₁: [1]
_₁: [1]
mark: []
nil: []
tt: []
isNePal: []
a: []
e: []
i: []
o: []
u: []

The following usable rules [FROCOS05] were oriented: none

(74) 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.

(75) PisEmptyProof (EQUIVALENT transformation)

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

(76) TRUE