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

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

    ↳5 QDP

        ↳6 QDPOrderProof (⇔)

        ↳7 QDP

        ↳8 QDPOrderProof (⇔)

        ↳9 QDP

        ↳10 PisEmptyProof (⇔)

        ↳11 TRUE

    ↳12 QDP

        ↳13 QDPOrderProof (⇔)

        ↳14 QDP

        ↳15 QDPOrderProof (⇔)

        ↳16 QDP

        ↳17 PisEmptyProof (⇔)

        ↳18 TRUE

    ↳19 QDP

        ↳20 QDPOrderProof (⇔)

        ↳21 QDP

        ↳22 QDPOrderProof (⇔)

        ↳23 QDP

        ↳24 PisEmptyProof (⇔)

        ↳25 TRUE

    ↳26 QDP

        ↳27 QDPOrderProof (⇔)

        ↳28 QDP

        ↳29 QDPOrderProof (⇔)

        ↳30 QDP

        ↳31 PisEmptyProof (⇔)

        ↳32 TRUE

    ↳33 QDP

        ↳34 QDPOrderProof (⇔)

        ↳35 QDP

        ↳36 QDPOrderProof (⇔)

        ↳37 QDP

        ↳38 PisEmptyProof (⇔)

        ↳39 TRUE

    ↳40 QDP

        ↳41 QDPOrderProof (⇔)

        ↳42 QDP

        ↳43 QDPOrderProof (⇔)

        ↳44 QDP

        ↳45 QDPOrderProof (⇔)

        ↳46 QDP

        ↳47 QDPOrderProof (⇔)

        ↳48 QDP

        ↳49 PisEmptyProof (⇔)

        ↳50 TRUE

    ↳51 QDP

        ↳52 QDPOrderProof (⇔)

        ↳53 QDP

        ↳54 QDPOrderProof (⇔)

        ↳55 QDP

        ↳56 QDPOrderProof (⇔)

        ↳57 QDP

        ↳58 QDPOrderProof (⇔)

        ↳59 QDP

        ↳60 PisEmptyProof (⇔)

        ↳61 TRUE

    ↳62 QDP

        ↳63 QDPOrderProof (⇔)

        ↳64 QDP

        ↳65 QDPOrderProof (⇔)

        ↳66 QDP

        ↳67 QDPOrderProof (⇔)

        ↳68 QDP

        ↳69 PisEmptyProof (⇔)

        ↳70 TRUE

(0) Obligation:

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

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

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
active₁: 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, mark₁]

Status:

ISPAL: multiset
mark₁: 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
active₁: 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, mark₁]

Status:

ISNEPAL: multiset
mark₁: 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
active₁: 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, mark₁]

Status:

ISQID: multiset
mark₁: 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
active₁: 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, mark₁]

Status:

ISNELIST: multiset
mark₁: 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
active₁: 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, mark₁]

Status:

ISLIST: multiset
mark₁: 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:

active₁: 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:

[AND₂, active₁]

Status:

AND₂: [1,2]
active₁: 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:

[AND₁, mark₁]

Status:

AND₁: multiset
mark₁: 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:

mark₁ > AND

Status:

AND: multiset
mark₁: [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:

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

__¹(active(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) = __¹(x0)

Tags:
__¹ 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.
__¹(x1, x2) = x1
mark(x1) = x1
active(x1) = active(x1)

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

trivial

Status:

active₁: multiset

The following usable rules [FROCOS05] were oriented: none

(53) Obligation:

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

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

__¹(X1, active(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, x1, x2)

Tags:
__¹ 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.
__¹(x1, x2) = __¹(x1, x2)
mark(x1) = x1
active(x1) = active(x1)

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

[_{_^1₂}, active₁]

Status:

__^1₂: [1,2]
active₁: multiset

The following usable rules [FROCOS05] were oriented: none

(55) Obligation:

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

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

__¹(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) = __¹(x2)

Tags:
__¹ 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.
__¹(x1, x2) = __¹(x2)
mark(x1) = mark(x1)

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

[_{_^1₁}, mark₁]

Status:

__^1₁: multiset
mark₁: multiset

The following usable rules [FROCOS05] were oriented: none

(57) Obligation:

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

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

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

Tags:
__¹ 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.
__¹(x1, x2) = __¹
mark(x1) = mark(x1)

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

mark₁ > __^1

Status:

__^1: multiset
mark₁: [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:

[_{_₂}, and₂, isList₁, isNeList₁] > isPal₁ > tt
nil > tt
a > tt
e > tt
i > tt
o > tt
u > tt

Status:

__₂: [1,2]
and₂: [1,2]
nil: multiset
isList₁: [1]
isNeList₁: [1]
tt: multiset
isPal₁: 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:

[_{_₂}, and₂] > [isNePal₁, isPal₁] > [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:

__₂: [1,2]
ACTIVE: multiset
and₂: [1,2]
isQid: multiset
isNePal₁: multiset
isPal₁: 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:

[MARK₁, _{_₂}, ACTIVE₁] > and₁
[MARK₁, _{_₂}, ACTIVE₁] > isList₁ > isNeList₁
[MARK₁, _{_₂}, ACTIVE₁] > isList₁ > [tt, a]
nil > [tt, a]
e > [tt, a]
i > [tt, a]
o > [tt, a]
u > [tt, a]

Status:

MARK₁: [1]
__₂: [1,2]
ACTIVE₁: [1]
and₁: multiset
isList₁: multiset
isNeList₁: [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.

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) QDPOrderProof (EQUIVALENT transformation)

(7) Obligation:

(8) QDPOrderProof (EQUIVALENT transformation)

(9) Obligation:

(10) PisEmptyProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) QDPOrderProof (EQUIVALENT transformation)

(14) Obligation:

(15) QDPOrderProof (EQUIVALENT transformation)

(16) Obligation:

(17) PisEmptyProof (EQUIVALENT transformation)

(18) TRUE

(19) Obligation:

(20) QDPOrderProof (EQUIVALENT transformation)

(21) Obligation:

(22) QDPOrderProof (EQUIVALENT transformation)

(23) Obligation:

(24) PisEmptyProof (EQUIVALENT transformation)

(25) TRUE

(26) Obligation:

(27) QDPOrderProof (EQUIVALENT transformation)

(28) Obligation:

(29) QDPOrderProof (EQUIVALENT transformation)

(30) Obligation:

(31) PisEmptyProof (EQUIVALENT transformation)

(32) TRUE

(33) Obligation:

(34) QDPOrderProof (EQUIVALENT transformation)

(35) Obligation:

(36) QDPOrderProof (EQUIVALENT transformation)

(37) Obligation:

(38) PisEmptyProof (EQUIVALENT transformation)

(39) TRUE

(40) Obligation:

(41) QDPOrderProof (EQUIVALENT transformation)

(42) Obligation:

(43) QDPOrderProof (EQUIVALENT transformation)

(44) Obligation:

(45) QDPOrderProof (EQUIVALENT transformation)

(46) Obligation:

(47) QDPOrderProof (EQUIVALENT transformation)

(48) Obligation:

(49) PisEmptyProof (EQUIVALENT transformation)

(50) TRUE

(51) Obligation:

(52) QDPOrderProof (EQUIVALENT transformation)

(53) Obligation:

(54) QDPOrderProof (EQUIVALENT transformation)

(55) Obligation:

(56) QDPOrderProof (EQUIVALENT transformation)

(57) Obligation:

(58) QDPOrderProof (EQUIVALENT transformation)

(59) Obligation:

(60) PisEmptyProof (EQUIVALENT transformation)

(61) TRUE

(62) Obligation:

(63) QDPOrderProof (EQUIVALENT transformation)

(64) Obligation:

(65) QDPOrderProof (EQUIVALENT transformation)

(66) Obligation:

(67) QDPOrderProof (EQUIVALENT transformation)

(68) Obligation:

(69) PisEmptyProof (EQUIVALENT transformation)

(70) TRUE