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, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
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, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
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 {__, U13, U26, U33, U46, U56, U63, U74, U83, U92, __1, U131, U261, U331, U461, U561, U631, U741, U831, U921} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U121, U111, U221, U211, U231, U241, U251, U321, U311, U421, U411, U431, U441, U451, U521, U511, U531, U541, U551, U621, U611, U721, U711, U731, U821, U811, U911} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISPALLISTKIND, ISNELIST, ISLIST, ISQID, ISPAL, 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)
U111(tt, V) → U121(isPalListKind(V), V)
U111(tt, V) → ISPALLISTKIND(V)
U121(tt, V) → U131(isNeList(V))
U121(tt, V) → ISNELIST(V)
U211(tt, V1, V2) → U221(isPalListKind(V1), V1, V2)
U211(tt, V1, V2) → ISPALLISTKIND(V1)
U221(tt, V1, V2) → U231(isPalListKind(V2), V1, V2)
U221(tt, V1, V2) → ISPALLISTKIND(V2)
U231(tt, V1, V2) → U241(isPalListKind(V2), V1, V2)
U231(tt, V1, V2) → ISPALLISTKIND(V2)
U241(tt, V1, V2) → U251(isList(V1), V2)
U241(tt, V1, V2) → ISLIST(V1)
U251(tt, V2) → U261(isList(V2))
U251(tt, V2) → ISLIST(V2)
U311(tt, V) → U321(isPalListKind(V), V)
U311(tt, V) → ISPALLISTKIND(V)
U321(tt, V) → U331(isQid(V))
U321(tt, V) → ISQID(V)
U411(tt, V1, V2) → U421(isPalListKind(V1), V1, V2)
U411(tt, V1, V2) → ISPALLISTKIND(V1)
U421(tt, V1, V2) → U431(isPalListKind(V2), V1, V2)
U421(tt, V1, V2) → ISPALLISTKIND(V2)
U431(tt, V1, V2) → U441(isPalListKind(V2), V1, V2)
U431(tt, V1, V2) → ISPALLISTKIND(V2)
U441(tt, V1, V2) → U451(isList(V1), V2)
U441(tt, V1, V2) → ISLIST(V1)
U451(tt, V2) → U461(isNeList(V2))
U451(tt, V2) → ISNELIST(V2)
U511(tt, V1, V2) → U521(isPalListKind(V1), V1, V2)
U511(tt, V1, V2) → ISPALLISTKIND(V1)
U521(tt, V1, V2) → U531(isPalListKind(V2), V1, V2)
U521(tt, V1, V2) → ISPALLISTKIND(V2)
U531(tt, V1, V2) → U541(isPalListKind(V2), V1, V2)
U531(tt, V1, V2) → ISPALLISTKIND(V2)
U541(tt, V1, V2) → U551(isNeList(V1), V2)
U541(tt, V1, V2) → ISNELIST(V1)
U551(tt, V2) → U561(isList(V2))
U551(tt, V2) → ISLIST(V2)
U611(tt, V) → U621(isPalListKind(V), V)
U611(tt, V) → ISPALLISTKIND(V)
U621(tt, V) → U631(isQid(V))
U621(tt, V) → ISQID(V)
U711(tt, I, P) → U721(isPalListKind(I), P)
U711(tt, I, P) → ISPALLISTKIND(I)
U721(tt, P) → U731(isPal(P), P)
U721(tt, P) → ISPAL(P)
U731(tt, P) → U741(isPalListKind(P))
U731(tt, P) → ISPALLISTKIND(P)
U811(tt, V) → U821(isPalListKind(V), V)
U811(tt, V) → ISPALLISTKIND(V)
U821(tt, V) → U831(isNePal(V))
U821(tt, V) → ISNEPAL(V)
U911(tt, V2) → U921(isPalListKind(V2))
U911(tt, V2) → ISPALLISTKIND(V2)
ISLIST(V) → U111(isPalListKind(V), V)
ISLIST(V) → ISPALLISTKIND(V)
ISLIST(__(V1, V2)) → U211(isPalListKind(V1), V1, V2)
ISLIST(__(V1, V2)) → ISPALLISTKIND(V1)
ISNELIST(V) → U311(isPalListKind(V), V)
ISNELIST(V) → ISPALLISTKIND(V)
ISNELIST(__(V1, V2)) → U411(isPalListKind(V1), V1, V2)
ISNELIST(__(V1, V2)) → ISPALLISTKIND(V1)
ISNELIST(__(V1, V2)) → U511(isPalListKind(V1), V1, V2)
ISNEPAL(V) → U611(isPalListKind(V), V)
ISNEPAL(V) → ISPALLISTKIND(V)
ISNEPAL(__(I, __(P, I))) → U711(isQid(I), I, P)
ISNEPAL(__(I, __(P, I))) → ISQID(I)
ISPAL(V) → U811(isPalListKind(V), V)
ISPAL(V) → ISPALLISTKIND(V)
ISPALLISTKIND(__(V1, V2)) → U911(isPalListKind(V1), V2)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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 4 SCCs with 38 less nodes.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U911} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISPALLISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U911(tt, V2) → ISPALLISTKIND(V2)
ISPALLISTKIND(__(V1, V2)) → U911(isPalListKind(V1), V2)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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.


ISPALLISTKIND(__(V1, V2)) → U911(isPalListKind(V1), V2)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
The remaining pairs can at least be oriented weakly.

U911(tt, V2) → ISPALLISTKIND(V2)
Used ordering: Combined order from the following AFS and order.
ISPALLISTKIND(x1)  =  x1
U911(x1, x2)  =  x2

Subterm Order


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U911} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISPALLISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U911(tt, V2) → ISPALLISTKIND(V2)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U711, U721, U811, U821} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISNEPAL, ISPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISNEPAL(__(I, __(P, I))) → U711(isQid(I), I, P)
U711(tt, I, P) → U721(isPalListKind(I), P)
U721(tt, P) → ISPAL(P)
ISPAL(V) → U811(isPalListKind(V), V)
U811(tt, V) → U821(isPalListKind(V), V)
U821(tt, 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, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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), I, P)
The remaining pairs can at least be oriented weakly.

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

Subterm Order


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U721, U711, U811, U821} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISPAL, ISNEPAL} are not replacing on any position.

The TRS P consists of the following rules:

U711(tt, I, P) → U721(isPalListKind(I), P)
U721(tt, P) → ISPAL(P)
ISPAL(V) → U811(isPalListKind(V), V)
U811(tt, V) → U821(isPalListKind(V), V)
U821(tt, 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, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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 5 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U121, U411, U421, U431, U441, U451, U511, U521, U531, U541, U551, U111, U211, U221, U231, U241, U251} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → U411(isPalListKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isPalListKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isPalListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isPalListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isList(V1), V2)
U451(tt, V2) → ISNELIST(V2)
ISNELIST(__(V1, V2)) → U511(isPalListKind(V1), V1, V2)
U511(tt, V1, V2) → U521(isPalListKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isPalListKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isPalListKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNeList(V1), V2)
U551(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → U121(isPalListKind(V), V)
ISLIST(__(V1, V2)) → U211(isPalListKind(V1), V1, V2)
U211(tt, V1, V2) → U221(isPalListKind(V1), V1, V2)
U221(tt, V1, V2) → U231(isPalListKind(V2), V1, V2)
U231(tt, V1, V2) → U241(isPalListKind(V2), V1, V2)
U241(tt, V1, V2) → U251(isList(V1), V2)
U251(tt, V2) → ISLIST(V2)
U241(tt, V1, V2) → ISLIST(V1)
U541(tt, V1, V2) → ISNELIST(V1)
U441(tt, V1, V2) → ISLIST(V1)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The following rules are not useable and can be deleted:

__(__(x0, x1), x2) → __(x0, __(x1, x2))
__(x0, nil) → x0
__(nil, x0) → x0
U61(tt, x0) → U62(isPalListKind(x0), x0)
U62(tt, x0) → U63(isQid(x0))
U63(tt) → tt
U71(tt, x0, x1) → U72(isPalListKind(x0), x1)
U72(tt, x0) → U73(isPal(x0), x0)
U73(tt, x0) → U74(isPalListKind(x0))
U74(tt) → tt
U81(tt, x0) → U82(isPalListKind(x0), x0)
U82(tt, x0) → U83(isNePal(x0))
U83(tt) → tt
isNePal(x0) → U61(isPalListKind(x0), x0)
isNePal(__(x0, __(x1, x0))) → U71(isQid(x0), x0, x1)
isPal(x0) → U81(isPalListKind(x0), x0)
isPal(nil) → tt


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
QCSDP
                ↳ QCSDPReductionPairProof
                ↳ QCSDPReductionPairProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U92, U13, U33, U26, U46, U56} are replacing on all positions.
For all symbols f in {U91, U11, U12, U31, U32, U41, U42, U43, U44, U45, U21, U22, U23, U24, U25, U51, U52, U53, U54, U55, U121, U411, U421, U431, U441, U451, U511, U521, U531, U541, U551, U111, U211, U221, U231, U241, U251} we have µ(f) = {1}.
The symbols in {isPalListKind, isList, isNeList, isQid, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → U411(isPalListKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isPalListKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isPalListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isPalListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isList(V1), V2)
U451(tt, V2) → ISNELIST(V2)
ISNELIST(__(V1, V2)) → U511(isPalListKind(V1), V1, V2)
U511(tt, V1, V2) → U521(isPalListKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isPalListKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isPalListKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNeList(V1), V2)
U551(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → U121(isPalListKind(V), V)
ISLIST(__(V1, V2)) → U211(isPalListKind(V1), V1, V2)
U211(tt, V1, V2) → U221(isPalListKind(V1), V1, V2)
U221(tt, V1, V2) → U231(isPalListKind(V2), V1, V2)
U231(tt, V1, V2) → U241(isPalListKind(V2), V1, V2)
U241(tt, V1, V2) → U251(isList(V1), V2)
U251(tt, V2) → ISLIST(V2)
U241(tt, V1, V2) → ISLIST(V1)
U541(tt, V1, V2) → ISNELIST(V1)
U441(tt, V1, V2) → ISLIST(V1)

The TRS R consists of the following rules:

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
isNeList(V) → U31(isPalListKind(V), V)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U33(tt) → tt
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U45(tt, V2) → U46(isNeList(V2))
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U46(tt) → tt
U13(tt) → tt

Q is empty.

Using the order
Polynomial Order [21,25] with Interpretation:

POL( i ) = 2


POL( U121(x1, x2) ) = x2 + 1


POL( U41(x1, ..., x3) ) = 2x2 + 2x3


POL( U32(x1, x2) ) = 1


POL( U25(x1, x2) ) = 1


POL( U24(x1, ..., x3) ) = 1


POL( U551(x1, x2) ) = x1 + x2


POL( U12(x1, x2) ) = 2


POL( U541(x1, ..., x3) ) = x2 + x3 + 1


POL( U56(x1) ) = 2


POL( U441(x1, ..., x3) ) = x2 + x3 + 1


POL( U521(x1, ..., x3) ) = 2x2 + x3 + 1


POL( tt ) = 1


POL( isPalListKind(x1) ) = max{0, x1 - 1}


POL( U22(x1, ..., x3) ) = 1


POL( U211(x1, ..., x3) ) = 2x2 + x3


POL( U21(x1, ..., x3) ) = 2x2 + x3 + 1


POL( nil ) = 2


POL( U54(x1, ..., x3) ) = x2 + 2


POL( U55(x1, x2) ) = 2


POL( U31(x1, x2) ) = 1


POL( e ) = 2


POL( o ) = 2


POL( U53(x1, ..., x3) ) = 2x1 + x2


POL( U411(x1, ..., x3) ) = 2x2 + 2x3 + 2


POL( U511(x1, ..., x3) ) = 2x2 + x3 + 1


POL( U23(x1, ..., x3) ) = 1


POL( U44(x1, ..., x3) ) = max{0, 2x1 + 2x2 - 1}


POL( U33(x1) ) = max{0, 2x1 - 1}


POL( U91(x1, x2) ) = x2


POL( U421(x1, ..., x3) ) = x1 + x2 + 2x3 + 2


POL( U431(x1, ..., x3) ) = x2 + x3 + 1


POL( __(x1, x2) ) = 2x1 + 2x2 + 1


POL( U251(x1, x2) ) = x2 + 1


POL( U231(x1, ..., x3) ) = x2 + x3 + 1


POL( U43(x1, ..., x3) ) = 2x2 + 2x3


POL( U26(x1) ) = 1


POL( U451(x1, x2) ) = x2 + 1


POL( U111(x1, x2) ) = x2 + 1


POL( U42(x1, ..., x3) ) = 2x2 + 2x3


POL( U92(x1) ) = x1


POL( U45(x1, x2) ) = 1


POL( U51(x1, ..., x3) ) = x2 + 2x3 + 1


POL( a ) = 2


POL( isList(x1) ) = 2x1 + 2


POL( ISNELIST(x1) ) = x1 + 1


POL( U531(x1, ..., x3) ) = 2x2 + x3 + 1


POL( U11(x1, x2) ) = x1 + x2 + 1


POL( isQid(x1) ) = 1


POL( U52(x1, ..., x3) ) = x2 + 2x3


POL( u ) = 2


POL( U46(x1) ) = 1


POL( isNeList(x1) ) = x1 + 1


POL( U221(x1, ..., x3) ) = x1 + x2 + x3


POL( U13(x1) ) = 2


POL( ISLIST(x1) ) = x1 + 1


POL( U241(x1, ..., x3) ) = x2 + x3 + 1



the following usable rules

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

U421(tt, V1, V2) → U431(isPalListKind(V2), V1, V2)
ISNELIST(__(V1, V2)) → U511(isPalListKind(V1), V1, V2)
ISLIST(__(V1, V2)) → U211(isPalListKind(V1), V1, V2)

could be oriented strictly and thus removed.
The pairs

U121(tt, V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → U411(isPalListKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isPalListKind(V1), V1, V2)
U431(tt, V1, V2) → U441(isPalListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isList(V1), V2)
U451(tt, V2) → ISNELIST(V2)
U511(tt, V1, V2) → U521(isPalListKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isPalListKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isPalListKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNeList(V1), V2)
U551(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → U121(isPalListKind(V), V)
U211(tt, V1, V2) → U221(isPalListKind(V1), V1, V2)
U221(tt, V1, V2) → U231(isPalListKind(V2), V1, V2)
U231(tt, V1, V2) → U241(isPalListKind(V2), V1, V2)
U241(tt, V1, V2) → U251(isList(V1), V2)
U251(tt, V2) → ISLIST(V2)
U241(tt, V1, V2) → ISLIST(V1)
U541(tt, V1, V2) → ISNELIST(V1)
U441(tt, V1, V2) → ISLIST(V1)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
QCSDP
                    ↳ QCSDependencyGraphProof
                ↳ QCSDPReductionPairProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U92, U13, U33, U26, U46, U56} are replacing on all positions.
For all symbols f in {U91, U11, U12, U31, U32, U41, U42, U43, U44, U45, U21, U22, U23, U24, U25, U51, U52, U53, U54, U55, U121, U411, U421, U441, U431, U451, U521, U511, U531, U541, U551, U111, U221, U211, U231, U241, U251} we have µ(f) = {1}.
The symbols in {isPalListKind, isList, isNeList, isQid, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → U411(isPalListKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isPalListKind(V1), V1, V2)
U431(tt, V1, V2) → U441(isPalListKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isList(V1), V2)
U451(tt, V2) → ISNELIST(V2)
U511(tt, V1, V2) → U521(isPalListKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isPalListKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isPalListKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNeList(V1), V2)
U551(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → U121(isPalListKind(V), V)
U211(tt, V1, V2) → U221(isPalListKind(V1), V1, V2)
U221(tt, V1, V2) → U231(isPalListKind(V2), V1, V2)
U231(tt, V1, V2) → U241(isPalListKind(V2), V1, V2)
U241(tt, V1, V2) → U251(isList(V1), V2)
U251(tt, V2) → ISLIST(V2)
U241(tt, V1, V2) → ISLIST(V1)
U541(tt, V1, V2) → ISNELIST(V1)
U441(tt, V1, V2) → ISLIST(V1)

The TRS R consists of the following rules:

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
isNeList(V) → U31(isPalListKind(V), V)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U33(tt) → tt
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U45(tt, V2) → U46(isNeList(V2))
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U46(tt) → tt
U13(tt) → tt

Q is empty.

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

Using the order
Polynomial interpretation [25]:

POL(ISLIST(x1)) = 2·x1   
POL(ISNELIST(x1)) = 2·x1   
POL(U11(x1, x2)) = 2·x1   
POL(U111(x1, x2)) = 2·x1 + 2·x2   
POL(U12(x1, x2)) = 2·x1   
POL(U121(x1, x2)) = 2·x1 + 2·x2   
POL(U13(x1)) = 0   
POL(U21(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U211(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3   
POL(U22(x1, x2, x3)) = x2 + 2·x3   
POL(U221(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3   
POL(U23(x1, x2, x3)) = 2·x1 + 2·x3   
POL(U231(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U24(x1, x2, x3)) = 2·x1 + x3   
POL(U241(x1, x2, x3)) = x1 + 2·x2 + 2·x3   
POL(U25(x1, x2)) = 0   
POL(U251(x1, x2)) = x1 + 2·x2   
POL(U26(x1)) = 0   
POL(U31(x1, x2)) = 2   
POL(U32(x1, x2)) = 1 + 2·x1   
POL(U33(x1)) = 1   
POL(U41(x1, x2, x3)) = 2 + 2·x1   
POL(U411(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U42(x1, x2, x3)) = 0   
POL(U421(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U43(x1, x2, x3)) = 2·x1   
POL(U431(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U44(x1, x2, x3)) = x1   
POL(U441(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U45(x1, x2)) = 0   
POL(U451(x1, x2)) = 2·x2   
POL(U46(x1)) = 0   
POL(U51(x1, x2, x3)) = 2 + x1   
POL(U511(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U52(x1, x2, x3)) = 1   
POL(U521(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U53(x1, x2, x3)) = 1   
POL(U531(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U54(x1, x2, x3)) = x1   
POL(U541(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U55(x1, x2)) = 0   
POL(U551(x1, x2)) = 2·x2   
POL(U56(x1)) = 0   
POL(U91(x1, x2)) = 2·x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 2   
POL(e) = 2   
POL(i) = 1   
POL(isList(x1)) = 2·x1   
POL(isNeList(x1)) = 2   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 2·x1   
POL(nil) = 0   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 0   

the following usable rules

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNELIST(__(V1, V2)) → U411(isPalListKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isPalListKind(V1), V1, V2)
U441(tt, V1, V2) → U451(isList(V1), V2)
ISNELIST(__(V1, V2)) → U511(isPalListKind(V1), V1, V2)
U511(tt, V1, V2) → U521(isPalListKind(V1), V1, V2)
U531(tt, V1, V2) → U541(isPalListKind(V2), V1, V2)
ISLIST(__(V1, V2)) → U211(isPalListKind(V1), V1, V2)
U231(tt, V1, V2) → U241(isPalListKind(V2), V1, V2)
U441(tt, V1, V2) → ISLIST(V1)

could be oriented strictly and thus removed.
The pairs

U121(tt, V) → ISNELIST(V)
U421(tt, V1, V2) → U431(isPalListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isPalListKind(V2), V1, V2)
U451(tt, V2) → ISNELIST(V2)
U521(tt, V1, V2) → U531(isPalListKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNeList(V1), V2)
U551(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → U121(isPalListKind(V), V)
U211(tt, V1, V2) → U221(isPalListKind(V1), V1, V2)
U221(tt, V1, V2) → U231(isPalListKind(V2), V1, V2)
U241(tt, V1, V2) → U251(isList(V1), V2)
U251(tt, V2) → ISLIST(V2)
U241(tt, V1, V2) → ISLIST(V1)
U541(tt, V1, V2) → ISNELIST(V1)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                ↳ QCSDPReductionPairProof
QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U92, U13, U33, U26, U46, U56} are replacing on all positions.
For all symbols f in {U91, U11, U12, U31, U32, U41, U42, U43, U44, U45, U21, U22, U23, U24, U25, U51, U52, U53, U54, U55, U121, U431, U421, U441, U451, U531, U521, U551, U541, U111, U221, U211, U231, U251, U241} we have µ(f) = {1}.
The symbols in {isPalListKind, isList, isNeList, isQid, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

U121(tt, V) → ISNELIST(V)
U421(tt, V1, V2) → U431(isPalListKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isPalListKind(V2), V1, V2)
U451(tt, V2) → ISNELIST(V2)
U521(tt, V1, V2) → U531(isPalListKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNeList(V1), V2)
U551(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → U121(isPalListKind(V), V)
U211(tt, V1, V2) → U221(isPalListKind(V1), V1, V2)
U221(tt, V1, V2) → U231(isPalListKind(V2), V1, V2)
U241(tt, V1, V2) → U251(isList(V1), V2)
U251(tt, V2) → ISLIST(V2)
U241(tt, V1, V2) → ISLIST(V1)
U541(tt, V1, V2) → ISNELIST(V1)

The TRS R consists of the following rules:

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
isNeList(V) → U31(isPalListKind(V), V)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U33(tt) → tt
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U45(tt, V2) → U46(isNeList(V2))
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U46(tt) → tt
U13(tt) → tt

Q is empty.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92, __1} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, 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, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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
          ↳ QCSDP
            ↳ QCSDPSubtermProof
QCSDP
                ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, 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, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
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.