(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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)) → MARK(__(X, __(Y, Z)))
ACTIVE(__(__(X, Y), Z)) → __1(X, __(Y, Z))
ACTIVE(__(__(X, Y), Z)) → __1(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(V)) → ISNELIST(V)
ACTIVE(isList(nil)) → MARK(tt)
ACTIVE(isList(__(V1, V2))) → MARK(and(isList(V1), isList(V2)))
ACTIVE(isList(__(V1, V2))) → AND(isList(V1), isList(V2))
ACTIVE(isList(__(V1, V2))) → ISLIST(V1)
ACTIVE(isList(__(V1, V2))) → ISLIST(V2)
ACTIVE(isNeList(V)) → MARK(isQid(V))
ACTIVE(isNeList(V)) → ISQID(V)
ACTIVE(isNeList(__(V1, V2))) → MARK(and(isList(V1), isNeList(V2)))
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))) → MARK(and(isNeList(V1), isList(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)) → MARK(isQid(V))
ACTIVE(isNePal(V)) → ISQID(V)
ACTIVE(isNePal(__(I, __(P, I)))) → MARK(and(isQid(I), isPal(P)))
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)) → MARK(isNePal(V))
ACTIVE(isPal(V)) → 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)
MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
MARK(__(X1, X2)) → __1(mark(X1), mark(X2))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → MARK(X2)
MARK(nil) → ACTIVE(nil)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(and(X1, X2)) → AND(mark(X1), X2)
MARK(and(X1, X2)) → MARK(X1)
MARK(tt) → ACTIVE(tt)
MARK(isList(X)) → ACTIVE(isList(X))
MARK(isNeList(X)) → ACTIVE(isNeList(X))
MARK(isQid(X)) → ACTIVE(isQid(X))
MARK(isNePal(X)) → ACTIVE(isNePal(X))
MARK(isPal(X)) → ACTIVE(isPal(X))
MARK(a) → ACTIVE(a)
MARK(e) → ACTIVE(e)
MARK(i) → ACTIVE(i)
MARK(o) → ACTIVE(o)
MARK(u) → ACTIVE(u)
__1(mark(X1), X2) → __1(X1, X2)
__1(X1, mark(X2)) → __1(X1, X2)
__1(active(X1), X2) → __1(X1, X2)
__1(X1, active(X2)) → __1(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(X1, mark(X2)) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
ISLIST(mark(X)) → ISLIST(X)
ISLIST(active(X)) → ISLIST(X)
ISNELIST(mark(X)) → ISNELIST(X)
ISNELIST(active(X)) → ISNELIST(X)
ISQID(mark(X)) → ISQID(X)
ISQID(active(X)) → ISQID(X)
ISNEPAL(mark(X)) → ISNEPAL(X)
ISNEPAL(active(X)) → ISNEPAL(X)
ISPAL(mark(X)) → ISPAL(X)
ISPAL(active(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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 8 SCCs with 34 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

ISPAL(active(X)) → ISPAL(X)
ISPAL(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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(active(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,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.
ISPAL(x1)  =  ISPAL
active(x1)  =  active(x1)
mark(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
trivial

Status:
ISPAL: multiset
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

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

ISPAL(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISPAL(mark(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,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.
ISPAL(x1)  =  ISPAL
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[ISPAL, mark1]

Status:
ISPAL: multiset
mark1: multiset


The following usable rules [FROCOS05] were oriented: none

(9) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(10) PisEmptyProof (EQUIVALENT transformation)

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

(11) TRUE

(12) Obligation:

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

ISNEPAL(active(X)) → ISNEPAL(X)
ISNEPAL(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNEPAL(active(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,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.
ISNEPAL(x1)  =  ISNEPAL
active(x1)  =  active(x1)
mark(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
trivial

Status:
ISNEPAL: multiset
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

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

ISNEPAL(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNEPAL(mark(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,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.
ISNEPAL(x1)  =  ISNEPAL
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[ISNEPAL, mark1]

Status:
ISNEPAL: multiset
mark1: multiset


The following usable rules [FROCOS05] were oriented: none

(16) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(17) PisEmptyProof (EQUIVALENT transformation)

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

(18) TRUE

(19) Obligation:

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

ISQID(active(X)) → ISQID(X)
ISQID(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISQID(active(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,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.
ISQID(x1)  =  ISQID
active(x1)  =  active(x1)
mark(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
trivial

Status:
ISQID: multiset
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(21) Obligation:

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

ISQID(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISQID(mark(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,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.
ISQID(x1)  =  ISQID
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[ISQID, mark1]

Status:
ISQID: multiset
mark1: multiset


The following usable rules [FROCOS05] were oriented: none

(23) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(24) PisEmptyProof (EQUIVALENT transformation)

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

(25) TRUE

(26) Obligation:

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

ISNELIST(active(X)) → ISNELIST(X)
ISNELIST(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNELIST(active(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,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.
ISNELIST(x1)  =  ISNELIST
active(x1)  =  active(x1)
mark(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
trivial

Status:
ISNELIST: multiset
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(28) Obligation:

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

ISNELIST(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNELIST(mark(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,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.
ISNELIST(x1)  =  ISNELIST
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[ISNELIST, mark1]

Status:
ISNELIST: multiset
mark1: multiset


The following usable rules [FROCOS05] were oriented: none

(30) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(31) PisEmptyProof (EQUIVALENT transformation)

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

(32) TRUE

(33) Obligation:

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

ISLIST(active(X)) → ISLIST(X)
ISLIST(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(34) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISLIST(active(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,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.
ISLIST(x1)  =  ISLIST
active(x1)  =  active(x1)
mark(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:
trivial

Status:
ISLIST: multiset
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(35) Obligation:

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

ISLIST(mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(36) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISLIST(mark(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,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.
ISLIST(x1)  =  ISLIST
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[ISLIST, mark1]

Status:
ISLIST: multiset
mark1: multiset


The following usable rules [FROCOS05] were oriented: none

(37) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(38) PisEmptyProof (EQUIVALENT transformation)

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

(39) TRUE

(40) Obligation:

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

AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(41) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


AND(active(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(x0)

Tags:
AND has argument tags [0,0,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)  =  x1
mark(x1)  =  x1
active(x1)  =  active(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
trivial

Status:
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(42) Obligation:

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

AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(X1, active(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(43) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


AND(X1, active(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(x0, x1, x2)

Tags:
AND has argument tags [1,2,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.
AND(x1, x2)  =  AND(x1, x2)
mark(x1)  =  x1
active(x1)  =  active(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[AND2, active1]

Status:
AND2: [1,2]
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(44) Obligation:

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

AND(X1, mark(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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.


AND(X1, mark(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,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)  =  AND(x2)
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[AND1, mark1]

Status:
AND1: multiset
mark1: multiset


The following usable rules [FROCOS05] were oriented: none

(46) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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.


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(x0, x1)

Tags:
AND has argument tags [0,0,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)  =  AND
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
mark1 > AND

Status:
AND: multiset
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(48) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(49) PisEmptyProof (EQUIVALENT transformation)

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

(50) TRUE

(51) Obligation:

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

__1(X1, mark(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)
__1(active(X1), X2) → __1(X1, X2)
__1(X1, active(X2)) → __1(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(52) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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

Tags:
__1 has argument tags [0,0,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.
__1(x1, x2)  =  x1
mark(x1)  =  x1
active(x1)  =  active(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
trivial

Status:
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(53) Obligation:

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

__1(X1, mark(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(X1, X2)
__1(X1, active(X2)) → __1(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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.


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

Tags:
__1 has argument tags [1,2,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.
__1(x1, x2)  =  __1(x1, x2)
mark(x1)  =  x1
active(x1)  =  active(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[^12, active1]

Status:
_^12: [1,2]
active1: multiset


The following usable rules [FROCOS05] were oriented: none

(55) Obligation:

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

__1(X1, mark(X2)) → __1(X1, X2)
__1(mark(X1), X2) → __1(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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.


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

Tags:
__1 has argument tags [2,1,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.
__1(x1, x2)  =  __1(x2)
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
[^11, mark1]

Status:
_^11: multiset
mark1: multiset


The following usable rules [FROCOS05] were oriented: none

(57) Obligation:

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

__1(mark(X1), X2) → __1(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(58) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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

Tags:
__1 has argument tags [0,0,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.
__1(x1, x2)  =  __1
mark(x1)  =  mark(x1)

Recursive path order with status [RPO].
Quasi-Precedence:
mark1 > _^1

Status:
_^1: multiset
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(59) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(60) PisEmptyProof (EQUIVALENT transformation)

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

(61) TRUE

(62) Obligation:

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

MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → MARK(X2)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(__(X, nil)) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
MARK(isList(X)) → ACTIVE(isList(X))
ACTIVE(__(nil, X)) → MARK(X)
MARK(isNeList(X)) → ACTIVE(isNeList(X))
ACTIVE(and(tt, X)) → MARK(X)
MARK(isQid(X)) → ACTIVE(isQid(X))
ACTIVE(isList(V)) → MARK(isNeList(V))
MARK(isNePal(X)) → ACTIVE(isNePal(X))
ACTIVE(isList(__(V1, V2))) → MARK(and(isList(V1), isList(V2)))
MARK(isPal(X)) → ACTIVE(isPal(X))
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))

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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(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.


ACTIVE(__(__(X, Y), Z)) → MARK(__(X, __(Y, Z)))
MARK(__(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → MARK(X2)
ACTIVE(__(X, nil)) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
ACTIVE(__(nil, X)) → MARK(X)
ACTIVE(and(tt, X)) → MARK(X)
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(__(I, __(P, I)))) → MARK(and(isQid(I), isPal(P)))
ACTIVE(isPal(V)) → MARK(isNePal(V))
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
MARK(x0, x1)  =  MARK(x0, x1)
ACTIVE(x0, x1)  =  ACTIVE(x1)

Tags:
MARK has argument tags [0,2] and root tag 0
ACTIVE has argument tags [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.
MARK(x1)  =  x1
__(x1, x2)  =  __(x1, x2)
ACTIVE(x1)  =  x1
mark(x1)  =  x1
and(x1, x2)  =  and(x1, x2)
nil  =  nil
isList(x1)  =  isList(x1)
isNeList(x1)  =  isNeList(x1)
tt  =  tt
isQid(x1)  =  x1
isNePal(x1)  =  x1
isPal(x1)  =  isPal(x1)
active(x1)  =  x1
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Recursive path order with status [RPO].
Quasi-Precedence:
[2, and2, isList1, isNeList1] > isPal1 > tt
nil > tt
a > tt
e > tt
i > tt
o > tt
u > tt

Status:
_2: [1,2]
and2: [1,2]
nil: multiset
isList1: [1]
isNeList1: [1]
tt: multiset
isPal1: multiset
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset


The following usable rules [FROCOS05] were oriented:

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

(64) Obligation:

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

MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(isList(X)) → ACTIVE(isList(X))
MARK(isNeList(X)) → ACTIVE(isNeList(X))
MARK(isQid(X)) → ACTIVE(isQid(X))
ACTIVE(isList(V)) → MARK(isNeList(V))
MARK(isNePal(X)) → ACTIVE(isNePal(X))
MARK(isPal(X)) → ACTIVE(isPal(X))
ACTIVE(isNePal(V)) → MARK(isQid(V))

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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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

Tags:
MARK has argument tags [1,0] and root tag 0
ACTIVE has argument tags [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.
MARK(x1)  =  x1
__(x1, x2)  =  __(x1, x2)
ACTIVE(x1)  =  ACTIVE
mark(x1)  =  x1
and(x1, x2)  =  and(x1, x2)
isList(x1)  =  x1
isNeList(x1)  =  x1
isQid(x1)  =  isQid
isNePal(x1)  =  isNePal(x1)
isPal(x1)  =  isPal(x1)
active(x1)  =  x1
nil  =  nil
tt  =  tt
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Recursive path order with status [RPO].
Quasi-Precedence:
[2, and2] > [isNePal1, isPal1] > [isQid, tt, e]
ACTIVE > [isQid, tt, e]
nil > [isQid, tt, e]
a > [isQid, tt, e]
i > [isQid, tt, e]
o > [isQid, tt, e]
u > [isQid, tt, e]

Status:
_2: [1,2]
ACTIVE: multiset
and2: [1,2]
isQid: multiset
isNePal1: multiset
isPal1: multiset
nil: multiset
tt: multiset
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset


The following usable rules [FROCOS05] were oriented:

isNeList(active(X)) → isNeList(X)
isNeList(mark(X)) → isNeList(X)
isQid(active(X)) → isQid(X)
isQid(mark(X)) → isQid(X)

(66) Obligation:

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

MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(isList(X)) → ACTIVE(isList(X))
MARK(isNeList(X)) → ACTIVE(isNeList(X))
MARK(isQid(X)) → ACTIVE(isQid(X))
ACTIVE(isList(V)) → MARK(isNeList(V))
MARK(isNePal(X)) → ACTIVE(isNePal(X))
MARK(isPal(X)) → ACTIVE(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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(67) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(__(X1, X2)) → ACTIVE(__(mark(X1), mark(X2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(isList(X)) → ACTIVE(isList(X))
MARK(isNeList(X)) → ACTIVE(isNeList(X))
MARK(isQid(X)) → ACTIVE(isQid(X))
ACTIVE(isList(V)) → MARK(isNeList(V))
MARK(isNePal(X)) → ACTIVE(isNePal(X))
MARK(isPal(X)) → ACTIVE(isPal(X))
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
MARK(x0, x1)  =  MARK(x0)
ACTIVE(x0, x1)  =  ACTIVE(x0, x1)

Tags:
MARK has argument tags [0,0] and root tag 1
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.
MARK(x1)  =  MARK(x1)
__(x1, x2)  =  __(x1, x2)
ACTIVE(x1)  =  ACTIVE(x1)
mark(x1)  =  x1
and(x1, x2)  =  and(x2)
isList(x1)  =  isList(x1)
isNeList(x1)  =  isNeList(x1)
isQid(x1)  =  x1
isNePal(x1)  =  x1
isPal(x1)  =  x1
active(x1)  =  x1
nil  =  nil
tt  =  tt
a  =  a
e  =  e
i  =  i
o  =  o
u  =  u

Recursive path order with status [RPO].
Quasi-Precedence:
[MARK1, 2, ACTIVE1] > and1
[MARK1, 2, ACTIVE1] > isList1 > isNeList1
[MARK1, 2, ACTIVE1] > isList1 > [tt, a]
nil > [tt, a]
e > [tt, a]
i > [tt, a]
o > [tt, a]
u > [tt, a]

Status:
MARK1: [1]
_2: [1,2]
ACTIVE1: [1]
and1: multiset
isList1: multiset
isNeList1: [1]
nil: multiset
tt: multiset
a: multiset
e: multiset
i: multiset
o: multiset
u: multiset


The following usable rules [FROCOS05] were oriented:

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

(68) 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)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

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

(69) PisEmptyProof (EQUIVALENT transformation)

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

(70) TRUE