Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U21: {1}
U22: {1}
isList: empty set
U31: {1}
U41: {1}
U42: {1}
isNeList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: empty set
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U21: {1}
U22: {1}
isList: empty set
U31: {1}
U41: {1}
U42: {1}
isNeList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: empty set
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U22, U31, U42, U52, U61, U72, U81, __1, U221, U421, U521, U721, U111, U311, U611, U811} are replacing on all positions.
For all symbols f in {U21, U41, U51, U71, U211, U411, U511, U711} we have µ(f) = {1}.
The symbols in {isList, isNeList, isPal, isQid, isNePal, ISLIST, ISNELIST, ISPAL, ISQID, ISNEPAL} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)
U211(tt, V2) → U221(isList(V2))
U211(tt, V2) → ISLIST(V2)
U411(tt, V2) → U421(isNeList(V2))
U411(tt, V2) → ISNELIST(V2)
U511(tt, V2) → U521(isList(V2))
U511(tt, V2) → ISLIST(V2)
U711(tt, P) → U721(isPal(P))
U711(tt, P) → ISPAL(P)
ISLIST(V) → U111(isNeList(V))
ISLIST(V) → ISNELIST(V)
ISLIST(__(V1, V2)) → U211(isList(V1), V2)
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(V) → U311(isQid(V))
ISNELIST(V) → ISQID(V)
ISNELIST(__(V1, V2)) → U411(isList(V1), V2)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → U511(isNeList(V1), V2)
ISNELIST(__(V1, V2)) → ISNELIST(V1)
ISNEPAL(V) → U611(isQid(V))
ISNEPAL(V) → ISQID(V)
ISNEPAL(__(I, __(P, I))) → U711(isQid(I), P)
ISNEPAL(__(I, __(P, I))) → ISQID(I)
ISPAL(V) → U811(isNePal(V))
ISPAL(V) → ISNEPAL(V)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 11 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U22, U31, U42, U52, U61, U72, U81} are replacing on all positions.
For all symbols f in {U21, U41, U51, U71, U711} we have µ(f) = {1}.
The symbols in {isList, isNeList, isPal, isQid, isNePal, ISNEPAL, ISPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISPAL(V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → U711(isQid(I), P)
U711(tt, P) → ISPAL(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


ISNEPAL(__(I, __(P, I))) → U711(isQid(I), P)
The remaining pairs can at least be oriented weakly.

ISPAL(V) → ISNEPAL(V)
U711(tt, P) → ISPAL(P)
Used ordering: Combined order from the following AFS and order.
ISNEPAL(x1)  =  x1
ISPAL(x1)  =  x1
U711(x1, x2)  =  x2

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U22, U31, U42, U52, U61, U72, U81} are replacing on all positions.
For all symbols f in {U21, U41, U51, U71, U711} we have µ(f) = {1}.
The symbols in {isList, isNeList, isPal, isQid, isNePal, ISNEPAL, ISPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISPAL(V) → ISNEPAL(V)
U711(tt, P) → ISPAL(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 2 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U22, U31, U42, U52, U61, U72, U81} are replacing on all positions.
For all symbols f in {U21, U41, U51, U71, U411, U211, U511} we have µ(f) = {1}.
The symbols in {isList, isNeList, isPal, isQid, isNePal, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

ISLIST(V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → U411(isList(V1), V2)
U411(tt, V2) → ISNELIST(V2)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → U211(isList(V1), V2)
U211(tt, V2) → ISLIST(V2)
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → U511(isNeList(V1), V2)
U511(tt, V2) → ISLIST(V2)
ISNELIST(__(V1, V2)) → ISNELIST(V1)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


ISNELIST(__(V1, V2)) → U411(isList(V1), V2)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → U211(isList(V1), V2)
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → U511(isNeList(V1), V2)
ISNELIST(__(V1, V2)) → ISNELIST(V1)
The remaining pairs can at least be oriented weakly.

ISLIST(V) → ISNELIST(V)
U411(tt, V2) → ISNELIST(V2)
U211(tt, V2) → ISLIST(V2)
U511(tt, V2) → ISLIST(V2)
Used ordering: Combined order from the following AFS and order.
ISNELIST(x1)  =  x1
ISLIST(x1)  =  x1
U411(x1, x2)  =  x2
U211(x1, x2)  =  x2
U511(x1, x2)  =  x2

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U22, U31, U42, U52, U61, U72, U81} are replacing on all positions.
For all symbols f in {U21, U41, U51, U71, U411, U211, U511} we have µ(f) = {1}.
The symbols in {isList, isNeList, isPal, isQid, isNePal, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

ISLIST(V) → ISNELIST(V)
U411(tt, V2) → ISNELIST(V2)
U211(tt, V2) → ISLIST(V2)
U511(tt, V2) → ISLIST(V2)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U22, U31, U42, U52, U61, U72, U81, __1} are replacing on all positions.
For all symbols f in {U21, U41, U51, U71} we have µ(f) = {1}.
The symbols in {isList, isNeList, isPal, isQid, isNePal} are not replacing on any position.

The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
__1(x1, x2)  =  x1

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U22, U31, U42, U52, U61, U72, U81} are replacing on all positions.
For all symbols f in {U21, U41, U51, U71} we have µ(f) = {1}.
The symbols in {isList, isNeList, isPal, isQid, isNePal} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(isNePal(V))
isPal(nil) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

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