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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U61: {1}
U62: {1}
U71: {1}
U72: {1}
isNePal: empty set
and: {1}
isPalListKind: empty set
isPal: 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, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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}
isNeList: empty set
U21: {1}
U22: {1}
isList: empty set
U23: {1}
U31: {1}
U32: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U51: {1}
U52: {1}
U53: {1}
U61: {1}
U62: {1}
U71: {1}
U72: {1}
isNePal: empty set
and: {1}
isPalListKind: empty set
isPal: 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 {__, U12, U23, U32, U43, U53, U62, U72, __1, U121, U231, U321, U431, U531, U621, U721} are replacing on all positions.
For all symbols f in {U11, U21, U22, U31, U41, U42, U51, U52, U61, U71, and, U111, U221, U211, U311, U421, U411, U521, U511, U611, U711, AND} we have µ(f) = {1}.
The symbols in {isNeList, isList, isQid, isNePal, isPalListKind, isPal, ISNELIST, ISLIST, ISQID, ISNEPAL, ISPALLISTKIND, ISPAL, U} 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(isNeList(V))
U111(tt, V) → ISNELIST(V)
U211(tt, V1, V2) → U221(isList(V1), V2)
U211(tt, V1, V2) → ISLIST(V1)
U221(tt, V2) → U231(isList(V2))
U221(tt, V2) → ISLIST(V2)
U311(tt, V) → U321(isQid(V))
U311(tt, V) → ISQID(V)
U411(tt, V1, V2) → U421(isList(V1), V2)
U411(tt, V1, V2) → ISLIST(V1)
U421(tt, V2) → U431(isNeList(V2))
U421(tt, V2) → ISNELIST(V2)
U511(tt, V1, V2) → U521(isNeList(V1), V2)
U511(tt, V1, V2) → ISNELIST(V1)
U521(tt, V2) → U531(isList(V2))
U521(tt, V2) → ISLIST(V2)
U611(tt, V) → U621(isQid(V))
U611(tt, V) → ISQID(V)
U711(tt, V) → U721(isNePal(V))
U711(tt, V) → ISNEPAL(V)
ISLIST(V) → U111(isPalListKind(V), V)
ISLIST(V) → ISPALLISTKIND(V)
ISLIST(__(V1, V2)) → U211(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
ISLIST(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
ISLIST(__(V1, V2)) → ISPALLISTKIND(V1)
ISNELIST(V) → U311(isPalListKind(V), V)
ISNELIST(V) → ISPALLISTKIND(V)
ISNELIST(__(V1, V2)) → U411(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
ISNELIST(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
ISNELIST(__(V1, V2)) → ISPALLISTKIND(V1)
ISNELIST(__(V1, V2)) → U511(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
ISNEPAL(V) → U611(isPalListKind(V), V)
ISNEPAL(V) → ISPALLISTKIND(V)
ISNEPAL(__(I, __(P, I))) → AND(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPalListKind(I))
ISNEPAL(__(I, __(P, I))) → ISQID(I)
ISPAL(V) → U711(isPalListKind(V), V)
ISPAL(V) → ISPALLISTKIND(V)
ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)

The collapsing dependency pairs are DPc:

AND(tt, X) → X


The hidden terms of R are:

and(isPal(P), isPalListKind(P))
isPal(P)
isPalListKind(P)
isPalListKind(V2)

Every hiding context is built from:

and on positions {1}

Hence, the new unhiding pairs DPu are :

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(and(isPal(P), isPalListKind(P))) → AND(isPal(P), isPalListKind(P))
U(isPal(P)) → ISPAL(P)
U(isPalListKind(P)) → ISPALLISTKIND(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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 3 SCCs with 18 less nodes.


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

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

The TRS P consists of the following rules:

ISNEPAL(V) → ISPALLISTKIND(V)
ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(and(isPal(P), isPalListKind(P))) → AND(isPal(P), isPalListKind(P))
U(isPal(P)) → ISPAL(P)
ISPAL(V) → U711(isPalListKind(V), V)
U711(tt, V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPalListKind(I))
ISPAL(V) → ISPALLISTKIND(V)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
U(isPalListKind(P)) → ISPALLISTKIND(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(AND(x1, x2)) = x2   
POL(ISNEPAL(x1)) = 1   
POL(ISPAL(x1)) = 1   
POL(ISPALLISTKIND(x1)) = 0   
POL(U(x1)) = x1   
POL(U61(x1, x2)) = 1   
POL(U62(x1)) = 0   
POL(U71(x1, x2)) = 0   
POL(U711(x1, x2)) = 1   
POL(U72(x1)) = 0   
POL(__(x1, x2)) = x1 + x2   
POL(a) = 0   
POL(and(x1, x2)) = x1 + x2   
POL(e) = 0   
POL(i) = 0   
POL(isNePal(x1)) = 1 + x1   
POL(isPal(x1)) = 1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 0   

the following usable rules

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(V2))
and(tt, X) → X
isPal(V) → U71(isPalListKind(V), V)
isPal(nil) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

could all be oriented weakly.
Furthermore, the pairs

ISNEPAL(V) → ISPALLISTKIND(V)
U(and(isPal(P), isPalListKind(P))) → AND(isPal(P), isPalListKind(P))
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPalListKind(I))
ISPAL(V) → ISPALLISTKIND(V)

could be oriented strictly and thus removed.
The pairs

ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → U711(isPalListKind(V), V)
U711(tt, V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
U(isPalListKind(P)) → ISPALLISTKIND(P)

could only be oriented weakly and must be analyzed further.


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

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

The TRS P consists of the following rules:

ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → U711(isPalListKind(V), V)
U711(tt, V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
U(isPalListKind(P)) → ISPALLISTKIND(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(AND(x1, x2)) = 1 + x2   
POL(ISNEPAL(x1)) = x1   
POL(ISPAL(x1)) = x1   
POL(ISPALLISTKIND(x1)) = 1   
POL(U(x1)) = 1 + x1   
POL(U61(x1, x2)) = 0   
POL(U62(x1)) = 0   
POL(U71(x1, x2)) = x2   
POL(U711(x1, x2)) = x2   
POL(U72(x1)) = 0   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(a) = 0   
POL(and(x1, x2)) = x1 + x2   
POL(e) = 0   
POL(i) = 0   
POL(isNePal(x1)) = x1   
POL(isPal(x1)) = x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 0   

the following usable rules

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(V2))
and(tt, X) → X
isPal(V) → U71(isPalListKind(V), V)
isPal(nil) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

could all be oriented weakly.
Furthermore, the pairs

U(isPal(P)) → ISPAL(P)
ISNEPAL(__(I, __(P, I))) → AND(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))

could be oriented strictly and thus removed.
The pairs

ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
ISPAL(V) → U711(isPalListKind(V), V)
U711(tt, V) → ISNEPAL(V)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
U(isPalListKind(P)) → ISPALLISTKIND(P)

could only be oriented weakly and must be analyzed further.


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

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

The TRS P consists of the following rules:

ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
ISPAL(V) → U711(isPalListKind(V), V)
U711(tt, V) → ISNEPAL(V)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
U(isPalListKind(P)) → ISPALLISTKIND(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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 1 SCC with 2 less nodes.


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

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

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isPalListKind(P)) → ISPALLISTKIND(P)
ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(AND(x1, x2)) = x2   
POL(ISPALLISTKIND(x1)) = x1   
POL(U(x1)) = x1   
POL(U61(x1, x2)) = x2   
POL(U62(x1)) = 0   
POL(U71(x1, x2)) = 0   
POL(U72(x1)) = 0   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(a) = 1   
POL(and(x1, x2)) = x1 + x2   
POL(e) = 1   
POL(i) = 1   
POL(isNePal(x1)) = x1   
POL(isPal(x1)) = 0   
POL(isPalListKind(x1)) = 1 + x1   
POL(isQid(x1)) = x1   
POL(nil) = 1   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 0   

the following usable rules

and(tt, X) → X
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(V2))
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
isPal(V) → U71(isPalListKind(V), V)
isPal(nil) → tt

could all be oriented weakly.
Furthermore, the pairs

U(isPalListKind(P)) → ISPALLISTKIND(P)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))

could only be oriented weakly and must be analyzed further.


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

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

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), 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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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 1 SCC with 2 less nodes.


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

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

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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.


U(and(x_0, x_1)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U12, U23, U32, U43, U53, U62, U72} are replacing on all positions.
For all symbols f in {U11, U21, U22, U31, U41, U42, U51, U52, U61, U71, and} we have µ(f) = {1}.
The symbols in {isNeList, isList, isQid, isNePal, isPalListKind, isPal} 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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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.
Using the order
Polynomial interpretation [25]:

POL(AND(x1, x2)) = x2   
POL(ISNEPAL(x1)) = 1 + 2·x1   
POL(ISPAL(x1)) = 1 + 2·x1   
POL(ISPALLISTKIND(x1)) = 0   
POL(U(x1)) = x1   
POL(U61(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U62(x1)) = 1 + x1   
POL(U71(x1, x2)) = 1 + 2·x1 + x2   
POL(U711(x1, x2)) = 1 + x1 + 2·x2   
POL(U72(x1)) = 0   
POL(__(x1, x2)) = 2·x1 + x2   
POL(a) = 1   
POL(and(x1, x2)) = x1 + x2   
POL(e) = 1   
POL(i) = 1   
POL(isNePal(x1)) = 1 + 2·x1   
POL(isPal(x1)) = 1 + 2·x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = x1   
POL(nil) = 2   
POL(o) = 1   
POL(tt) = 0   
POL(u) = 1   

the following usable rules

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → and(isPalListKind(V1), isPalListKind(V2))
and(tt, X) → X
isPal(V) → U71(isPalListKind(V), V)
isPal(nil) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

could all be oriented weakly.
Furthermore, the pairs

ISNEPAL(V) → ISPALLISTKIND(V)
U(and(isPal(P), isPalListKind(P))) → AND(isPal(P), isPalListKind(P))
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPalListKind(I))
ISPAL(V) → ISPALLISTKIND(V)

could be oriented strictly and thus removed.
The pairs

ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → U711(isPalListKind(V), V)
U711(tt, V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
U(isPalListKind(P)) → ISPALLISTKIND(P)

could only be oriented weakly and must be analyzed further.


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

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

The TRS P consists of the following rules:

ISPALLISTKIND(__(V1, V2)) → AND(isPalListKind(V1), isPalListKind(V2))
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → U711(isPalListKind(V), V)
U711(tt, V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)
U(isPalListKind(P)) → ISPALLISTKIND(P)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.


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

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

The TRS P consists of the following rules:

ISNELIST(__(V1, V2)) → U411(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
U411(tt, V1, V2) → U421(isList(V1), V2)
U421(tt, V2) → ISNELIST(V2)
ISNELIST(__(V1, V2)) → U511(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
U511(tt, V1, V2) → U521(isNeList(V1), V2)
U521(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → ISNELIST(V)
ISLIST(__(V1, V2)) → U211(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
U211(tt, V1, V2) → U221(isList(V1), V2)
U221(tt, V2) → ISLIST(V2)
U211(tt, V1, V2) → ISLIST(V1)
U511(tt, V1, V2) → ISNELIST(V1)
U411(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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(V2))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(ISLIST(x1)) = x1   
POL(ISNELIST(x1)) = x1   
POL(U11(x1, x2)) = 0   
POL(U111(x1, x2)) = x2   
POL(U12(x1)) = 0   
POL(U21(x1, x2, x3)) = 1 + x2 + x3   
POL(U211(x1, x2, x3)) = x2 + x3   
POL(U22(x1, x2)) = 1 + x1   
POL(U221(x1, x2)) = x2   
POL(U23(x1)) = 1   
POL(U31(x1, x2)) = 0   
POL(U32(x1)) = 0   
POL(U41(x1, x2, x3)) = 0   
POL(U411(x1, x2, x3)) = x2 + x3   
POL(U42(x1, x2)) = 0   
POL(U421(x1, x2)) = x2   
POL(U43(x1)) = 0   
POL(U51(x1, x2, x3)) = 0   
POL(U511(x1, x2, x3)) = x2 + x3   
POL(U52(x1, x2)) = 0   
POL(U521(x1, x2)) = x2   
POL(U53(x1)) = 0   
POL(U61(x1, x2)) = 0   
POL(U62(x1)) = 0   
POL(U71(x1, x2)) = 0   
POL(U72(x1)) = 0   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(a) = 0   
POL(and(x1, x2)) = x2   
POL(e) = 0   
POL(i) = 0   
POL(isList(x1)) = x1   
POL(isNeList(x1)) = 0   
POL(isNePal(x1)) = 0   
POL(isPal(x1)) = 1 + x1   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 0   
POL(nil) = 0   
POL(o) = 0   
POL(tt) = 0   
POL(u) = 0   

the following usable rules

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

could all be oriented weakly.
Furthermore, the pairs

ISNELIST(__(V1, V2)) → U411(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
ISNELIST(__(V1, V2)) → U511(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
ISLIST(__(V1, V2)) → U211(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)

could be oriented strictly and thus removed.
The pairs

U411(tt, V1, V2) → U421(isList(V1), V2)
U421(tt, V2) → ISNELIST(V2)
U511(tt, V1, V2) → U521(isNeList(V1), V2)
U521(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → ISNELIST(V)
U211(tt, V1, V2) → U221(isList(V1), V2)
U221(tt, V2) → ISLIST(V2)
U211(tt, V1, V2) → ISLIST(V1)
U511(tt, V1, V2) → ISNELIST(V1)
U411(tt, V1, V2) → ISLIST(V1)

could only be oriented weakly and must be analyzed further.


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

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

The TRS P consists of the following rules:

U411(tt, V1, V2) → U421(isList(V1), V2)
U421(tt, V2) → ISNELIST(V2)
U511(tt, V1, V2) → U521(isNeList(V1), V2)
U521(tt, V2) → ISLIST(V2)
ISLIST(V) → U111(isPalListKind(V), V)
U111(tt, V) → ISNELIST(V)
U211(tt, V1, V2) → U221(isList(V1), V2)
U221(tt, V2) → ISLIST(V2)
U211(tt, V1, V2) → ISLIST(V1)
U511(tt, V1, V2) → ISNELIST(V1)
U411(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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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 10 less nodes.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U12, U23, U32, U43, U53, U62, U72, __1} are replacing on all positions.
For all symbols f in {U11, U21, U22, U31, U41, U42, U51, U52, U61, U71, and} we have µ(f) = {1}.
The symbols in {isNeList, isList, isQid, isNePal, isPalListKind, isPal} 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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U12, U23, U32, U43, U53, U62, U72} are replacing on all positions.
For all symbols f in {U11, U21, U22, U31, U41, U42, U51, U52, U61, U71, and} we have µ(f) = {1}.
The symbols in {isNeList, isList, isQid, isNePal, isPalListKind, isPal} 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(isNeList(V))
U12(tt) → tt
U21(tt, V1, V2) → U22(isList(V1), V2)
U22(tt, V2) → U23(isList(V2))
U23(tt) → tt
U31(tt, V) → U32(isQid(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isList(V1), V2)
U42(tt, V2) → U43(isNeList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNeList(V1), V2)
U52(tt, V2) → U53(isList(V2))
U53(tt) → tt
U61(tt, V) → U62(isQid(V))
U62(tt) → tt
U71(tt, V) → U72(isNePal(V))
U72(tt) → tt
and(tt, X) → X
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNeList(__(V1, V2)) → U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P)))
isPal(V) → U71(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)) → and(isPalListKind(V1), isPalListKind(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.