YES Termination proof of ../tpdb/TRS/CSR_Maude/palindrome/PALINDROME_complete-noand.trs
Termination of the following Term Rewriting System could be proven:

Q restricted 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
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation

Q restricted 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

We applied the Lucas [26] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
  ↳ Zantema-Transformation

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

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

Q is empty.

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

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

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

__(X, nil) → X
__(nil, X) → X
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U12(x1)) = x1   
POL(U13(x1)) = x1   
POL(U21(x1)) = x1   
POL(U22(x1)) = x1   
POL(U23(x1)) = x1   
POL(U24(x1)) = x1   
POL(U25(x1)) = 2·x1   
POL(U26(x1)) = x1   
POL(U31(x1)) = x1   
POL(U32(x1)) = 2·x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1)) = x1   
POL(U42(x1)) = 2·x1   
POL(U43(x1)) = 2·x1   
POL(U44(x1)) = x1   
POL(U45(x1)) = 2·x1   
POL(U46(x1)) = x1   
POL(U51(x1)) = x1   
POL(U52(x1)) = x1   
POL(U53(x1)) = 2·x1   
POL(U54(x1)) = 2·x1   
POL(U55(x1)) = 2·x1   
POL(U56(x1)) = x1   
POL(U61(x1)) = 2·x1   
POL(U62(x1)) = 2·x1   
POL(U63(x1)) = 2·x1   
POL(U71(x1)) = 2·x1   
POL(U72(x1)) = 2·x1   
POL(U73(x1)) = 2·x1   
POL(U74(x1)) = x1   
POL(U81(x1)) = 2·x1   
POL(U82(x1)) = 2·x1   
POL(U83(x1)) = 2·x1   
POL(U91(x1)) = x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + x1 + x2   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 0   
POL(isPal) = 0   
POL(isPalListKind) = 0   
POL(isQid) = 0   
POL(nil) = 1   
POL(tt) = 0   




↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
  ↳ Zantema-Transformation

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

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

Q is empty.

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

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

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

__(__(X, Y), Z) → __(X, __(Y, Z))
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U12(x1)) = x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1)) = 2·x1   
POL(U22(x1)) = x1   
POL(U23(x1)) = 2·x1   
POL(U24(x1)) = x1   
POL(U25(x1)) = 2·x1   
POL(U26(x1)) = 2·x1   
POL(U31(x1)) = 2·x1   
POL(U32(x1)) = 2·x1   
POL(U33(x1)) = x1   
POL(U41(x1)) = 2·x1   
POL(U42(x1)) = x1   
POL(U43(x1)) = 2·x1   
POL(U44(x1)) = 2·x1   
POL(U45(x1)) = x1   
POL(U46(x1)) = 2·x1   
POL(U51(x1)) = x1   
POL(U52(x1)) = x1   
POL(U53(x1)) = x1   
POL(U54(x1)) = 2·x1   
POL(U55(x1)) = 2·x1   
POL(U56(x1)) = x1   
POL(U61(x1)) = x1   
POL(U62(x1)) = 2·x1   
POL(U63(x1)) = x1   
POL(U71(x1)) = 2·x1   
POL(U72(x1)) = x1   
POL(U73(x1)) = 2·x1   
POL(U74(x1)) = 2·x1   
POL(U81(x1)) = x1   
POL(U82(x1)) = 2·x1   
POL(U83(x1)) = x1   
POL(U91(x1)) = 2·x1   
POL(U92(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 0   
POL(isPal) = 0   
POL(isPalListKind) = 0   
POL(isQid) = 0   
POL(tt) = 0   




↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
  ↳ Zantema-Transformation

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

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPal → tt
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

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

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U63(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPal → tt
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

U63(tt) → tt
isPal → tt
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U12(x1)) = x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1)) = 2·x1   
POL(U22(x1)) = 2·x1   
POL(U23(x1)) = 2·x1   
POL(U24(x1)) = 2·x1   
POL(U25(x1)) = 2·x1   
POL(U26(x1)) = x1   
POL(U31(x1)) = x1   
POL(U32(x1)) = x1   
POL(U33(x1)) = x1   
POL(U41(x1)) = 2·x1   
POL(U42(x1)) = x1   
POL(U43(x1)) = x1   
POL(U44(x1)) = x1   
POL(U45(x1)) = 2·x1   
POL(U46(x1)) = x1   
POL(U51(x1)) = 2·x1   
POL(U52(x1)) = 2·x1   
POL(U53(x1)) = 2·x1   
POL(U54(x1)) = x1   
POL(U55(x1)) = 2·x1   
POL(U56(x1)) = x1   
POL(U61(x1)) = 2 + x1   
POL(U62(x1)) = 2 + 2·x1   
POL(U63(x1)) = 2 + x1   
POL(U71(x1)) = 2 + 2·x1   
POL(U72(x1)) = 2 + 2·x1   
POL(U73(x1)) = x1   
POL(U74(x1)) = 2·x1   
POL(U81(x1)) = 2 + 2·x1   
POL(U82(x1)) = 2 + x1   
POL(U83(x1)) = x1   
POL(U91(x1)) = 2·x1   
POL(U92(x1)) = 2·x1   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 2   
POL(isPal) = 2   
POL(isPalListKind) = 0   
POL(isQid) = 0   
POL(tt) = 0   




↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
  ↳ Zantema-Transformation

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

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

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

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

U61(tt) → U62(isPalListKind)
U62(tt) → U63(isQid)
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = 2·x1   
POL(U12(x1)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1)) = 2·x1   
POL(U22(x1)) = 2·x1   
POL(U23(x1)) = x1   
POL(U24(x1)) = 2·x1   
POL(U25(x1)) = x1   
POL(U26(x1)) = x1   
POL(U31(x1)) = 2·x1   
POL(U32(x1)) = 2·x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1)) = 2·x1   
POL(U42(x1)) = x1   
POL(U43(x1)) = 2·x1   
POL(U44(x1)) = 2·x1   
POL(U45(x1)) = 2·x1   
POL(U46(x1)) = x1   
POL(U51(x1)) = x1   
POL(U52(x1)) = 2·x1   
POL(U53(x1)) = x1   
POL(U54(x1)) = x1   
POL(U55(x1)) = x1   
POL(U56(x1)) = x1   
POL(U61(x1)) = 2 + x1   
POL(U62(x1)) = 1 + 2·x1   
POL(U63(x1)) = 2·x1   
POL(U71(x1)) = 2 + 2·x1   
POL(U72(x1)) = 2 + x1   
POL(U73(x1)) = x1   
POL(U74(x1)) = 2·x1   
POL(U81(x1)) = 2 + 2·x1   
POL(U82(x1)) = 2 + 2·x1   
POL(U83(x1)) = x1   
POL(U91(x1)) = x1   
POL(U92(x1)) = 2·x1   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 2   
POL(isPal) = 2   
POL(isPalListKind) = 0   
POL(isQid) = 0   
POL(tt) = 0   




↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
  ↳ Zantema-Transformation

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

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

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

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U61(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNePal → U61(isPalListKind)
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U12(x1)) = 2·x1   
POL(U13(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U22(x1)) = x1   
POL(U23(x1)) = 2·x1   
POL(U24(x1)) = 2·x1   
POL(U25(x1)) = 2·x1   
POL(U26(x1)) = 2·x1   
POL(U31(x1)) = 2·x1   
POL(U32(x1)) = x1   
POL(U33(x1)) = 2·x1   
POL(U41(x1)) = x1   
POL(U42(x1)) = 2·x1   
POL(U43(x1)) = x1   
POL(U44(x1)) = 2·x1   
POL(U45(x1)) = 2·x1   
POL(U46(x1)) = 2·x1   
POL(U51(x1)) = 2·x1   
POL(U52(x1)) = x1   
POL(U53(x1)) = x1   
POL(U54(x1)) = x1   
POL(U55(x1)) = 2·x1   
POL(U56(x1)) = 2·x1   
POL(U61(x1)) = x1   
POL(U71(x1)) = 1 + 2·x1   
POL(U72(x1)) = 1 + 2·x1   
POL(U73(x1)) = x1   
POL(U74(x1)) = 2·x1   
POL(U81(x1)) = 1 + 2·x1   
POL(U82(x1)) = 1 + 2·x1   
POL(U83(x1)) = x1   
POL(U91(x1)) = 2·x1   
POL(U92(x1)) = x1   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 1   
POL(isPal) = 1   
POL(isPalListKind) = 0   
POL(isQid) = 0   
POL(tt) = 0   




↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
  ↳ Zantema-Transformation

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

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

U731(tt) → ISPALLISTKIND
U431(tt) → ISPALLISTKIND
U311(tt) → ISPALLISTKIND
U311(tt) → U321(isPalListKind)
U251(tt) → U261(isList)
U731(tt) → U741(isPalListKind)
U321(tt) → U331(isQid)
ISNELIST → U411(isPalListKind)
U111(tt) → ISPALLISTKIND
U811(tt) → ISPALLISTKIND
U441(tt) → ISLIST
U821(tt) → U831(isNePal)
U221(tt) → ISPALLISTKIND
U241(tt) → U251(isList)
U451(tt) → ISNELIST
ISNEPAL → ISQID
U111(tt) → U121(isPalListKind)
ISPAL → U811(isPalListKind)
U211(tt) → U221(isPalListKind)
U251(tt) → ISLIST
U721(tt) → U731(isPal)
ISNELIST → U311(isPalListKind)
ISPAL → ISPALLISTKIND
U431(tt) → U441(isPalListKind)
U551(tt) → U561(isList)
U541(tt) → U551(isNeList)
U711(tt) → ISPALLISTKIND
U721(tt) → ISPAL
U441(tt) → U451(isList)
U531(tt) → ISPALLISTKIND
U211(tt) → ISPALLISTKIND
U411(tt) → ISPALLISTKIND
U511(tt) → U521(isPalListKind)
U521(tt) → U531(isPalListKind)
U711(tt) → U721(isPalListKind)
U541(tt) → ISNELIST
U811(tt) → U821(isPalListKind)
U511(tt) → ISPALLISTKIND
U121(tt) → U131(isNeList)
U421(tt) → ISPALLISTKIND
ISNEPAL → U711(isQid)
U531(tt) → U541(isPalListKind)
ISNELIST → U511(isPalListKind)
U241(tt) → ISLIST
U451(tt) → U461(isNeList)
ISLIST → ISPALLISTKIND
U421(tt) → U431(isPalListKind)
U821(tt) → ISNEPAL
U911(tt) → U921(isPalListKind)
U221(tt) → U231(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND
U231(tt) → ISPALLISTKIND
U321(tt) → ISQID
ISLIST → U111(isPalListKind)
ISLIST → U211(isPalListKind)
ISNELIST → ISPALLISTKIND
U521(tt) → ISPALLISTKIND
U121(tt) → ISNELIST
U911(tt) → ISPALLISTKIND
U231(tt) → U241(isPalListKind)
U551(tt) → ISLIST
U411(tt) → U421(isPalListKind)
ISPALLISTKIND → U911(isPalListKind)

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

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

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
  ↳ Zantema-Transformation

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

U731(tt) → ISPALLISTKIND
U431(tt) → ISPALLISTKIND
U311(tt) → ISPALLISTKIND
U311(tt) → U321(isPalListKind)
U251(tt) → U261(isList)
U731(tt) → U741(isPalListKind)
U321(tt) → U331(isQid)
ISNELIST → U411(isPalListKind)
U111(tt) → ISPALLISTKIND
U811(tt) → ISPALLISTKIND
U441(tt) → ISLIST
U821(tt) → U831(isNePal)
U221(tt) → ISPALLISTKIND
U241(tt) → U251(isList)
U451(tt) → ISNELIST
ISNEPAL → ISQID
U111(tt) → U121(isPalListKind)
ISPAL → U811(isPalListKind)
U211(tt) → U221(isPalListKind)
U251(tt) → ISLIST
U721(tt) → U731(isPal)
ISNELIST → U311(isPalListKind)
ISPAL → ISPALLISTKIND
U431(tt) → U441(isPalListKind)
U551(tt) → U561(isList)
U541(tt) → U551(isNeList)
U711(tt) → ISPALLISTKIND
U721(tt) → ISPAL
U441(tt) → U451(isList)
U531(tt) → ISPALLISTKIND
U211(tt) → ISPALLISTKIND
U411(tt) → ISPALLISTKIND
U511(tt) → U521(isPalListKind)
U521(tt) → U531(isPalListKind)
U711(tt) → U721(isPalListKind)
U541(tt) → ISNELIST
U811(tt) → U821(isPalListKind)
U511(tt) → ISPALLISTKIND
U121(tt) → U131(isNeList)
U421(tt) → ISPALLISTKIND
ISNEPAL → U711(isQid)
U531(tt) → U541(isPalListKind)
ISNELIST → U511(isPalListKind)
U241(tt) → ISLIST
U451(tt) → U461(isNeList)
ISLIST → ISPALLISTKIND
U421(tt) → U431(isPalListKind)
U821(tt) → ISNEPAL
U911(tt) → U921(isPalListKind)
U221(tt) → U231(isPalListKind)
ISPALLISTKIND → ISPALLISTKIND
U231(tt) → ISPALLISTKIND
U321(tt) → ISQID
ISLIST → U111(isPalListKind)
ISLIST → U211(isPalListKind)
ISNELIST → ISPALLISTKIND
U521(tt) → ISPALLISTKIND
U121(tt) → ISNELIST
U911(tt) → ISPALLISTKIND
U231(tt) → U241(isPalListKind)
U551(tt) → ISLIST
U411(tt) → U421(isPalListKind)
ISPALLISTKIND → U911(isPalListKind)

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 30 less nodes.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                  ↳ QDP
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U911(tt) → ISPALLISTKIND
ISPALLISTKIND → ISPALLISTKIND
ISPALLISTKIND → U911(isPalListKind)

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                  ↳ QDP
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U911(tt) → ISPALLISTKIND
ISPALLISTKIND → ISPALLISTKIND
ISPALLISTKIND → U911(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISPALLISTKIND → U911(isPalListKind) at position [0] we obtained the following new rules:

ISPALLISTKIND → U911(tt)
ISPALLISTKIND → U911(U91(isPalListKind))



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                          ↳ QDP
                                            ↳ NonTerminationProof
                                  ↳ QDP
                                  ↳ QDP
  ↳ Zantema-Transformation

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

ISPALLISTKIND → U911(tt)
U911(tt) → ISPALLISTKIND
ISPALLISTKIND → ISPALLISTKIND
ISPALLISTKIND → U911(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

ISPALLISTKIND → U911(tt)
U911(tt) → ISPALLISTKIND
ISPALLISTKIND → ISPALLISTKIND
ISPALLISTKIND → U911(U91(isPalListKind))

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt


s = ISPALLISTKIND evaluates to t =ISPALLISTKIND

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ISPALLISTKIND to ISPALLISTKIND.





↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U821(tt) → ISNEPAL
ISNEPAL → U711(isQid)
U711(tt) → U721(isPalListKind)
ISPAL → U811(isPalListKind)
U721(tt) → ISPAL
U811(tt) → U821(isPalListKind)

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U821(tt) → ISNEPAL
ISNEPAL → U711(isQid)
ISPAL → U811(isPalListKind)
U711(tt) → U721(isPalListKind)
U721(tt) → ISPAL
U811(tt) → U821(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNEPAL → U711(isQid) at position [0] we obtained the following new rules:

ISNEPAL → U711(tt)



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                          ↳ QDP
                                            ↳ UsableRulesProof
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U821(tt) → ISNEPAL
U711(tt) → U721(isPalListKind)
ISPAL → U811(isPalListKind)
ISNEPAL → U711(tt)
U721(tt) → ISPAL
U811(tt) → U821(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                          ↳ QDP
                                            ↳ UsableRulesProof
                                              ↳ QDP
                                                ↳ Narrowing
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U821(tt) → ISNEPAL
ISPAL → U811(isPalListKind)
U711(tt) → U721(isPalListKind)
ISNEPAL → U711(tt)
U721(tt) → ISPAL
U811(tt) → U821(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U711(tt) → U721(isPalListKind) at position [0] we obtained the following new rules:

U711(tt) → U721(U91(isPalListKind))
U711(tt) → U721(tt)



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                          ↳ QDP
                                            ↳ UsableRulesProof
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ Narrowing
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U821(tt) → ISNEPAL
U711(tt) → U721(U91(isPalListKind))
ISPAL → U811(isPalListKind)
ISNEPAL → U711(tt)
U711(tt) → U721(tt)
U721(tt) → ISPAL
U811(tt) → U821(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISPAL → U811(isPalListKind) at position [0] we obtained the following new rules:

ISPAL → U811(U91(isPalListKind))
ISPAL → U811(tt)



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                          ↳ QDP
                                            ↳ UsableRulesProof
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ Narrowing
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U821(tt) → ISNEPAL
ISPAL → U811(U91(isPalListKind))
ISPAL → U811(tt)
U711(tt) → U721(U91(isPalListKind))
ISNEPAL → U711(tt)
U721(tt) → ISPAL
U711(tt) → U721(tt)
U811(tt) → U821(isPalListKind)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U811(tt) → U821(isPalListKind) at position [0] we obtained the following new rules:

U811(tt) → U821(U91(isPalListKind))
U811(tt) → U821(tt)



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ Narrowing
                                          ↳ QDP
                                            ↳ UsableRulesProof
                                              ↳ QDP
                                                ↳ Narrowing
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ Narrowing
                                                          ↳ QDP
                                                            ↳ NonTerminationProof
                                  ↳ QDP
  ↳ Zantema-Transformation

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

U821(tt) → ISNEPAL
ISPAL → U811(U91(isPalListKind))
U711(tt) → U721(U91(isPalListKind))
ISPAL → U811(tt)
U811(tt) → U821(U91(isPalListKind))
ISNEPAL → U711(tt)
U711(tt) → U721(tt)
U721(tt) → ISPAL
U811(tt) → U821(tt)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U821(tt) → ISNEPAL
ISPAL → U811(U91(isPalListKind))
U711(tt) → U721(U91(isPalListKind))
ISPAL → U811(tt)
U811(tt) → U821(U91(isPalListKind))
ISNEPAL → U711(tt)
U711(tt) → U721(tt)
U721(tt) → ISPAL
U811(tt) → U821(tt)

The TRS R consists of the following rules:

isPalListKind → tt
isPalListKind → U91(isPalListKind)
U91(tt) → U92(isPalListKind)
U92(tt) → tt


s = ISNEPAL evaluates to t =ISNEPAL

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

ISNEPAL → U711(tt)
with rule ISNEPAL → U711(tt) at position [] and matcher [ ]

U711(tt) → U721(tt)
with rule U711(tt) → U721(tt) at position [] and matcher [ ]

U721(tt) → ISPAL
with rule U721(tt) → ISPAL at position [] and matcher [ ]

ISPAL → U811(tt)
with rule ISPAL → U811(tt) at position [] and matcher [ ]

U811(tt) → U821(tt)
with rule U811(tt) → U821(tt) at position [] and matcher [ ]

U821(tt) → ISNEPAL
with rule U821(tt) → ISNEPAL

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
  ↳ Zantema-Transformation

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

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

The TRS R consists of the following rules:

U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
U13(tt) → tt
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
U33(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U71(tt) → U72(isPalListKind)
U72(tt) → U73(isPal)
U73(tt) → U74(isPalListKind)
U74(tt) → tt
U81(tt) → U82(isPalListKind)
U82(tt) → U83(isNePal)
U83(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
isNePal → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ DependencyPairsProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
  ↳ Zantema-Transformation

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

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

The TRS R consists of the following rules:

isList → U11(isPalListKind)
isList → tt
isList → U21(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
U21(tt) → U22(isPalListKind)
U22(tt) → U23(isPalListKind)
U23(tt) → U24(isPalListKind)
U24(tt) → U25(isList)
U25(tt) → U26(isList)
U26(tt) → tt
U91(tt) → U92(isPalListKind)
U92(tt) → tt
U11(tt) → U12(isPalListKind)
U12(tt) → U13(isNeList)
isNeList → U31(isPalListKind)
isNeList → U41(isPalListKind)
isNeList → U51(isPalListKind)
U13(tt) → tt
U51(tt) → U52(isPalListKind)
U52(tt) → U53(isPalListKind)
U53(tt) → U54(isPalListKind)
U54(tt) → U55(isNeList)
U55(tt) → U56(isList)
U56(tt) → tt
U41(tt) → U42(isPalListKind)
U42(tt) → U43(isPalListKind)
U43(tt) → U44(isPalListKind)
U44(tt) → U45(isList)
U45(tt) → U46(isNeList)
U46(tt) → tt
U31(tt) → U32(isPalListKind)
U32(tt) → U33(isQid)
isQid → tt
U33(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Zantema [34] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof

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

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ISPAL(V) → A(V)
ISNEPAL(V) → A(V)
U721(tt, P) → U731(isPal(a(P)), a(P))
U431(tt, V1, V2) → A(V2)
A(aInact) → A
ISPALLISTKIND(__Inact(V1, V2)) → A(V2)
ISNEPAL(__Inact(I, __(P, I))) → ISQID(a(I))
A(__Inact(x1, x2)) → __1(x1, x2)
U711(tt, I, P) → A(P)
A(eInact) → E
ISNEPAL(__Inact(I, __(P, I))) → U711(isQid(a(I)), a(I), a(P))
U431(tt, V1, V2) → ISPALLISTKIND(a(V2))
U321(tt, V) → ISQID(a(V))
U811(tt, V) → A(V)
U311(tt, V) → A(V)
ISLIST(__Inact(V1, V2)) → A(V2)
U511(tt, V1, V2) → U521(isPalListKind(a(V1)), a(V1), a(V2))
U511(tt, V1, V2) → A(V2)
U551(tt, V2) → ISLIST(a(V2))
U421(tt, V1, V2) → U431(isPalListKind(a(V2)), a(V1), a(V2))
U221(tt, V1, V2) → ISPALLISTKIND(a(V2))
U731(tt, P) → U741(isPalListKind(a(P)))
ISNELIST(V) → U311(isPalListKind(a(V)), a(V))
U411(tt, V1, V2) → A(V1)
U551(tt, V2) → A(V2)
U611(tt, V) → ISPALLISTKIND(a(V))
ISPAL(V) → ISPALLISTKIND(a(V))
A(iInact) → I
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
U531(tt, V1, V2) → ISPALLISTKIND(a(V2))
U611(tt, V) → A(V)
U531(tt, V1, V2) → A(V2)
U411(tt, V1, V2) → ISPALLISTKIND(a(V1))
ISNEPAL(__Inact(I, __(P, I))) → A(I)
U621(tt, V) → A(V)
__1(__(X, Y), Z) → __1(Y, Z)
U441(tt, V1, V2) → A(V2)
U311(tt, V) → ISPALLISTKIND(a(V))
U621(tt, V) → U631(isQid(a(V)))
U421(tt, V1, V2) → ISPALLISTKIND(a(V2))
ISNELIST(__Inact(V1, V2)) → U411(isPalListKind(a(V1)), a(V1), a(V2))
U441(tt, V1, V2) → ISLIST(a(V1))
U431(tt, V1, V2) → A(V1)
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
ISLIST(__Inact(V1, V2)) → A(V1)
U121(tt, V) → U131(isNeList(a(V)))
ISPALLISTKIND(__Inact(V1, V2)) → U911(isPalListKind(a(V1)), a(V2))
ISNEPAL(__Inact(I, __(P, I))) → A(P)
U451(tt, V2) → ISNELIST(a(V2))
U111(tt, V) → A(V)
U441(tt, V1, V2) → U451(isList(a(V1)), a(V2))
U231(tt, V1, V2) → A(V1)
U521(tt, V1, V2) → A(V1)
U521(tt, V1, V2) → A(V2)
U551(tt, V2) → U561(isList(a(V2)))
ISNELIST(V) → ISPALLISTKIND(a(V))
A(uInact) → U
ISNELIST(__Inact(V1, V2)) → A(V1)
U711(tt, I, P) → ISPALLISTKIND(a(I))
U221(tt, V1, V2) → A(V2)
U731(tt, P) → ISPALLISTKIND(a(P))
U521(tt, V1, V2) → ISPALLISTKIND(a(V2))
U411(tt, V1, V2) → A(V2)
ISNELIST(V) → A(V)
U321(tt, V) → U331(isQid(a(V)))
U241(tt, V1, V2) → U251(isList(a(V1)), a(V2))
U231(tt, V1, V2) → ISPALLISTKIND(a(V2))
U241(tt, V1, V2) → A(V1)
U251(tt, V2) → A(V2)
U541(tt, V1, V2) → U551(isNeList(a(V1)), a(V2))
U541(tt, V1, V2) → A(V2)
U241(tt, V1, V2) → ISLIST(a(V1))
U241(tt, V1, V2) → A(V2)
U231(tt, V1, V2) → U241(isPalListKind(a(V2)), a(V1), a(V2))
U441(tt, V1, V2) → A(V1)
U431(tt, V1, V2) → U441(isPalListKind(a(V2)), a(V1), a(V2))
U821(tt, V) → A(V)
U121(tt, V) → A(V)
ISLIST(__Inact(V1, V2)) → U211(isPalListKind(a(V1)), a(V1), a(V2))
U541(tt, V1, V2) → A(V1)
ISLIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
ISNELIST(__Inact(V1, V2)) → A(V2)
U451(tt, V2) → U461(isNeList(a(V2)))
ISPALLISTKIND(__Inact(V1, V2)) → A(V1)
ISLIST(V) → ISPALLISTKIND(a(V))
U251(tt, V2) → U261(isList(a(V2)))
U711(tt, I, P) → A(I)
U121(tt, V) → ISNELIST(a(V))
U721(tt, P) → ISPAL(a(P))
ISNEPAL(V) → U611(isPalListKind(a(V)), a(V))
U731(tt, P) → A(P)
U411(tt, V1, V2) → U421(isPalListKind(a(V1)), a(V1), a(V2))
U521(tt, V1, V2) → U531(isPalListKind(a(V2)), a(V1), a(V2))
U511(tt, V1, V2) → ISPALLISTKIND(a(V1))
U451(tt, V2) → A(V2)
ISNEPAL(V) → ISPALLISTKIND(a(V))
U421(tt, V1, V2) → A(V2)
A(nilInact) → NIL
U211(tt, V1, V2) → A(V1)
A(oInact) → O
U811(tt, V) → U821(isPalListKind(a(V)), a(V))
U311(tt, V) → U321(isPalListKind(a(V)), a(V))
__1(__(X, Y), Z) → __1(X, __(Y, Z))
U211(tt, V1, V2) → U221(isPalListKind(a(V1)), a(V1), a(V2))
U531(tt, V1, V2) → A(V1)
U541(tt, V1, V2) → ISNELIST(a(V1))
ISPAL(V) → U811(isPalListKind(a(V)), a(V))
ISLIST(V) → A(V)
U711(tt, I, P) → U721(isPalListKind(a(I)), a(P))
U421(tt, V1, V2) → A(V1)
ISNELIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
U531(tt, V1, V2) → U541(isPalListKind(a(V2)), a(V1), a(V2))
U821(tt, V) → ISNEPAL(a(V))
U911(tt, V2) → U921(isPalListKind(a(V2)))
U911(tt, V2) → A(V2)
U221(tt, V1, V2) → A(V1)
U621(tt, V) → ISQID(a(V))
U251(tt, V2) → ISLIST(a(V2))
U611(tt, V) → U621(isPalListKind(a(V)), a(V))
ISNELIST(__Inact(V1, V2)) → U511(isPalListKind(a(V1)), a(V1), a(V2))
U221(tt, V1, V2) → U231(isPalListKind(a(V2)), a(V1), a(V2))
U111(tt, V) → U121(isPalListKind(a(V)), a(V))
U111(tt, V) → ISPALLISTKIND(a(V))
U511(tt, V1, V2) → A(V1)
U721(tt, P) → A(P)
U811(tt, V) → ISPALLISTKIND(a(V))
U211(tt, V1, V2) → ISPALLISTKIND(a(V1))
U231(tt, V1, V2) → A(V2)
U821(tt, V) → U831(isNePal(a(V)))
U321(tt, V) → A(V)
U211(tt, V1, V2) → A(V2)
U911(tt, V2) → ISPALLISTKIND(a(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(a(V)), a(V))
U12(tt, V) → U13(isNeList(a(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(a(V1)), a(V1), a(V2))
U22(tt, V1, V2) → U23(isPalListKind(a(V2)), a(V1), a(V2))
U23(tt, V1, V2) → U24(isPalListKind(a(V2)), a(V1), a(V2))
U24(tt, V1, V2) → U25(isList(a(V1)), a(V2))
U25(tt, V2) → U26(isList(a(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(a(V)), a(V))
U32(tt, V) → U33(isQid(a(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(a(V1)), a(V1), a(V2))
U42(tt, V1, V2) → U43(isPalListKind(a(V2)), a(V1), a(V2))
U43(tt, V1, V2) → U44(isPalListKind(a(V2)), a(V1), a(V2))
U44(tt, V1, V2) → U45(isList(a(V1)), a(V2))
U45(tt, V2) → U46(isNeList(a(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(a(V1)), a(V1), a(V2))
U52(tt, V1, V2) → U53(isPalListKind(a(V2)), a(V1), a(V2))
U53(tt, V1, V2) → U54(isPalListKind(a(V2)), a(V1), a(V2))
U54(tt, V1, V2) → U55(isNeList(a(V1)), a(V2))
U55(tt, V2) → U56(isList(a(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(a(V)), a(V))
U62(tt, V) → U63(isQid(a(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(a(I)), a(P))
U72(tt, P) → U73(isPal(a(P)), a(P))
U73(tt, P) → U74(isPalListKind(a(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(a(V)), a(V))
U82(tt, V) → U83(isNePal(a(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(a(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(isPalListKind(a(V1)), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(I), a(P))
isPal(V) → U81(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → U91(isPalListKind(a(V1)), a(V2))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
u → uInact
a(uInact) → u
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e

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

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof

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

ISPAL(V) → A(V)
ISNEPAL(V) → A(V)
U721(tt, P) → U731(isPal(a(P)), a(P))
U431(tt, V1, V2) → A(V2)
A(aInact) → A
ISPALLISTKIND(__Inact(V1, V2)) → A(V2)
ISNEPAL(__Inact(I, __(P, I))) → ISQID(a(I))
A(__Inact(x1, x2)) → __1(x1, x2)
U711(tt, I, P) → A(P)
A(eInact) → E
ISNEPAL(__Inact(I, __(P, I))) → U711(isQid(a(I)), a(I), a(P))
U431(tt, V1, V2) → ISPALLISTKIND(a(V2))
U321(tt, V) → ISQID(a(V))
U811(tt, V) → A(V)
U311(tt, V) → A(V)
ISLIST(__Inact(V1, V2)) → A(V2)
U511(tt, V1, V2) → U521(isPalListKind(a(V1)), a(V1), a(V2))
U511(tt, V1, V2) → A(V2)
U551(tt, V2) → ISLIST(a(V2))
U421(tt, V1, V2) → U431(isPalListKind(a(V2)), a(V1), a(V2))
U221(tt, V1, V2) → ISPALLISTKIND(a(V2))
U731(tt, P) → U741(isPalListKind(a(P)))
ISNELIST(V) → U311(isPalListKind(a(V)), a(V))
U411(tt, V1, V2) → A(V1)
U551(tt, V2) → A(V2)
U611(tt, V) → ISPALLISTKIND(a(V))
ISPAL(V) → ISPALLISTKIND(a(V))
A(iInact) → I
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
U531(tt, V1, V2) → ISPALLISTKIND(a(V2))
U611(tt, V) → A(V)
U531(tt, V1, V2) → A(V2)
U411(tt, V1, V2) → ISPALLISTKIND(a(V1))
ISNEPAL(__Inact(I, __(P, I))) → A(I)
U621(tt, V) → A(V)
__1(__(X, Y), Z) → __1(Y, Z)
U441(tt, V1, V2) → A(V2)
U311(tt, V) → ISPALLISTKIND(a(V))
U621(tt, V) → U631(isQid(a(V)))
U421(tt, V1, V2) → ISPALLISTKIND(a(V2))
ISNELIST(__Inact(V1, V2)) → U411(isPalListKind(a(V1)), a(V1), a(V2))
U441(tt, V1, V2) → ISLIST(a(V1))
U431(tt, V1, V2) → A(V1)
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
ISLIST(__Inact(V1, V2)) → A(V1)
U121(tt, V) → U131(isNeList(a(V)))
ISPALLISTKIND(__Inact(V1, V2)) → U911(isPalListKind(a(V1)), a(V2))
ISNEPAL(__Inact(I, __(P, I))) → A(P)
U451(tt, V2) → ISNELIST(a(V2))
U111(tt, V) → A(V)
U441(tt, V1, V2) → U451(isList(a(V1)), a(V2))
U231(tt, V1, V2) → A(V1)
U521(tt, V1, V2) → A(V1)
U521(tt, V1, V2) → A(V2)
U551(tt, V2) → U561(isList(a(V2)))
ISNELIST(V) → ISPALLISTKIND(a(V))
A(uInact) → U
ISNELIST(__Inact(V1, V2)) → A(V1)
U711(tt, I, P) → ISPALLISTKIND(a(I))
U221(tt, V1, V2) → A(V2)
U731(tt, P) → ISPALLISTKIND(a(P))
U521(tt, V1, V2) → ISPALLISTKIND(a(V2))
U411(tt, V1, V2) → A(V2)
ISNELIST(V) → A(V)
U321(tt, V) → U331(isQid(a(V)))
U241(tt, V1, V2) → U251(isList(a(V1)), a(V2))
U231(tt, V1, V2) → ISPALLISTKIND(a(V2))
U241(tt, V1, V2) → A(V1)
U251(tt, V2) → A(V2)
U541(tt, V1, V2) → U551(isNeList(a(V1)), a(V2))
U541(tt, V1, V2) → A(V2)
U241(tt, V1, V2) → ISLIST(a(V1))
U241(tt, V1, V2) → A(V2)
U231(tt, V1, V2) → U241(isPalListKind(a(V2)), a(V1), a(V2))
U441(tt, V1, V2) → A(V1)
U431(tt, V1, V2) → U441(isPalListKind(a(V2)), a(V1), a(V2))
U821(tt, V) → A(V)
U121(tt, V) → A(V)
ISLIST(__Inact(V1, V2)) → U211(isPalListKind(a(V1)), a(V1), a(V2))
U541(tt, V1, V2) → A(V1)
ISLIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
ISNELIST(__Inact(V1, V2)) → A(V2)
U451(tt, V2) → U461(isNeList(a(V2)))
ISPALLISTKIND(__Inact(V1, V2)) → A(V1)
ISLIST(V) → ISPALLISTKIND(a(V))
U251(tt, V2) → U261(isList(a(V2)))
U711(tt, I, P) → A(I)
U121(tt, V) → ISNELIST(a(V))
U721(tt, P) → ISPAL(a(P))
ISNEPAL(V) → U611(isPalListKind(a(V)), a(V))
U731(tt, P) → A(P)
U411(tt, V1, V2) → U421(isPalListKind(a(V1)), a(V1), a(V2))
U521(tt, V1, V2) → U531(isPalListKind(a(V2)), a(V1), a(V2))
U511(tt, V1, V2) → ISPALLISTKIND(a(V1))
U451(tt, V2) → A(V2)
ISNEPAL(V) → ISPALLISTKIND(a(V))
U421(tt, V1, V2) → A(V2)
A(nilInact) → NIL
U211(tt, V1, V2) → A(V1)
A(oInact) → O
U811(tt, V) → U821(isPalListKind(a(V)), a(V))
U311(tt, V) → U321(isPalListKind(a(V)), a(V))
__1(__(X, Y), Z) → __1(X, __(Y, Z))
U211(tt, V1, V2) → U221(isPalListKind(a(V1)), a(V1), a(V2))
U531(tt, V1, V2) → A(V1)
U541(tt, V1, V2) → ISNELIST(a(V1))
ISPAL(V) → U811(isPalListKind(a(V)), a(V))
ISLIST(V) → A(V)
U711(tt, I, P) → U721(isPalListKind(a(I)), a(P))
U421(tt, V1, V2) → A(V1)
ISNELIST(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
U531(tt, V1, V2) → U541(isPalListKind(a(V2)), a(V1), a(V2))
U821(tt, V) → ISNEPAL(a(V))
U911(tt, V2) → U921(isPalListKind(a(V2)))
U911(tt, V2) → A(V2)
U221(tt, V1, V2) → A(V1)
U621(tt, V) → ISQID(a(V))
U251(tt, V2) → ISLIST(a(V2))
U611(tt, V) → U621(isPalListKind(a(V)), a(V))
ISNELIST(__Inact(V1, V2)) → U511(isPalListKind(a(V1)), a(V1), a(V2))
U221(tt, V1, V2) → U231(isPalListKind(a(V2)), a(V1), a(V2))
U111(tt, V) → U121(isPalListKind(a(V)), a(V))
U111(tt, V) → ISPALLISTKIND(a(V))
U511(tt, V1, V2) → A(V1)
U721(tt, P) → A(P)
U811(tt, V) → ISPALLISTKIND(a(V))
U211(tt, V1, V2) → ISPALLISTKIND(a(V1))
U231(tt, V1, V2) → A(V2)
U821(tt, V) → U831(isNePal(a(V)))
U321(tt, V) → A(V)
U211(tt, V1, V2) → A(V2)
U911(tt, V2) → ISPALLISTKIND(a(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(a(V)), a(V))
U12(tt, V) → U13(isNeList(a(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(a(V1)), a(V1), a(V2))
U22(tt, V1, V2) → U23(isPalListKind(a(V2)), a(V1), a(V2))
U23(tt, V1, V2) → U24(isPalListKind(a(V2)), a(V1), a(V2))
U24(tt, V1, V2) → U25(isList(a(V1)), a(V2))
U25(tt, V2) → U26(isList(a(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(a(V)), a(V))
U32(tt, V) → U33(isQid(a(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(a(V1)), a(V1), a(V2))
U42(tt, V1, V2) → U43(isPalListKind(a(V2)), a(V1), a(V2))
U43(tt, V1, V2) → U44(isPalListKind(a(V2)), a(V1), a(V2))
U44(tt, V1, V2) → U45(isList(a(V1)), a(V2))
U45(tt, V2) → U46(isNeList(a(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(a(V1)), a(V1), a(V2))
U52(tt, V1, V2) → U53(isPalListKind(a(V2)), a(V1), a(V2))
U53(tt, V1, V2) → U54(isPalListKind(a(V2)), a(V1), a(V2))
U54(tt, V1, V2) → U55(isNeList(a(V1)), a(V2))
U55(tt, V2) → U56(isList(a(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(a(V)), a(V))
U62(tt, V) → U63(isQid(a(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(a(I)), a(P))
U72(tt, P) → U73(isPal(a(P)), a(P))
U73(tt, P) → U74(isPalListKind(a(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(a(V)), a(V))
U82(tt, V) → U83(isNePal(a(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(a(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(isPalListKind(a(V1)), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(I), a(P))
isPal(V) → U81(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → U91(isPalListKind(a(V1)), a(V2))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
u → uInact
a(uInact) → u
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 97 less nodes.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
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(a(V)), a(V))
U12(tt, V) → U13(isNeList(a(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(a(V1)), a(V1), a(V2))
U22(tt, V1, V2) → U23(isPalListKind(a(V2)), a(V1), a(V2))
U23(tt, V1, V2) → U24(isPalListKind(a(V2)), a(V1), a(V2))
U24(tt, V1, V2) → U25(isList(a(V1)), a(V2))
U25(tt, V2) → U26(isList(a(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(a(V)), a(V))
U32(tt, V) → U33(isQid(a(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(a(V1)), a(V1), a(V2))
U42(tt, V1, V2) → U43(isPalListKind(a(V2)), a(V1), a(V2))
U43(tt, V1, V2) → U44(isPalListKind(a(V2)), a(V1), a(V2))
U44(tt, V1, V2) → U45(isList(a(V1)), a(V2))
U45(tt, V2) → U46(isNeList(a(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(a(V1)), a(V1), a(V2))
U52(tt, V1, V2) → U53(isPalListKind(a(V2)), a(V1), a(V2))
U53(tt, V1, V2) → U54(isPalListKind(a(V2)), a(V1), a(V2))
U54(tt, V1, V2) → U55(isNeList(a(V1)), a(V2))
U55(tt, V2) → U56(isList(a(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(a(V)), a(V))
U62(tt, V) → U63(isQid(a(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(a(I)), a(P))
U72(tt, P) → U73(isPal(a(P)), a(P))
U73(tt, P) → U74(isPalListKind(a(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(a(V)), a(V))
U82(tt, V) → U83(isNePal(a(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(a(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(isPalListKind(a(V1)), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(I), a(P))
isPal(V) → U81(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → U91(isPalListKind(a(V1)), a(V2))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
u → uInact
a(uInact) → u
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
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
__(x1, x2) → __Inact(x1, x2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP

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

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
              ↳ QDP
              ↳ QDP

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

ISPALLISTKIND(__Inact(V1, V2)) → U911(isPalListKind(a(V1)), a(V2))
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))
U911(tt, V2) → ISPALLISTKIND(a(V2))

The TRS R consists of the following rules:

a(x) → x
a(aInact) → a
a(__Inact(x1, x2)) → __(x1, x2)
a(iInact) → i
a(uInact) → u
a(nilInact) → nil
a(oInact) → o
a(eInact) → e
e → eInact
o → oInact
nil → nilInact
u → uInact
i → iInact
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
__(x1, x2) → __Inact(x1, x2)
a → aInact
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → U91(isPalListKind(a(V1)), a(V2))
U91(tt, V2) → U92(isPalListKind(a(V2)))
U92(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISPALLISTKIND(__Inact(V1, V2)) → U911(isPalListKind(a(V1)), a(V2))
ISPALLISTKIND(__Inact(V1, V2)) → ISPALLISTKIND(a(V1))

Strictly oriented rules of the TRS R:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
isPalListKind(eInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
U91(tt, V2) → U92(isPalListKind(a(V2)))
U92(tt) → tt

Used ordering: POLO with Polynomial interpretation [25]:

POL(ISPALLISTKIND(x1)) = 2·x1   
POL(U91(x1, x2)) = 2 + x1 + 2·x2   
POL(U911(x1, x2)) = 2·x1 + 2·x2   
POL(U92(x1)) = 1 + x1   
POL(__(x1, x2)) = 1 + 2·x1 + x2   
POL(__Inact(x1, x2)) = 1 + 2·x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(e) = 2   
POL(eInact) = 2   
POL(i) = 0   
POL(iInact) = 0   
POL(isPalListKind(x1)) = 2·x1   
POL(nil) = 2   
POL(nilInact) = 2   
POL(o) = 1   
POL(oInact) = 1   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ RuleRemovalProof
                      ↳ QDP
                        ↳ DependencyGraphProof
              ↳ QDP
              ↳ QDP

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

U911(tt, V2) → ISPALLISTKIND(a(V2))

The TRS R consists of the following rules:

a(x) → x
a(aInact) → a
a(__Inact(x1, x2)) → __(x1, x2)
a(iInact) → i
a(uInact) → u
a(nilInact) → nil
a(oInact) → o
a(eInact) → e
e → eInact
o → oInact
nil → nilInact
u → uInact
i → iInact
__(x1, x2) → __Inact(x1, x2)
a → aInact
isPalListKind(aInact) → tt
isPalListKind(iInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → U91(isPalListKind(a(V1)), a(V2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP

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

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U711(tt, I, P) → U721(isPalListKind(a(I)), a(P))
The remaining pairs can at least be oriented weakly.

ISPAL(V) → U811(isPalListKind(a(V)), a(V))
U821(tt, V) → ISNEPAL(a(V))
U721(tt, P) → ISPAL(a(P))
U811(tt, V) → U821(isPalListKind(a(V)), a(V))
ISNEPAL(__Inact(I, __(P, I))) → U711(isQid(a(I)), a(I), a(P))
Used ordering: Polynomial interpretation [25]:

POL(ISNEPAL(x1)) = x1   
POL(ISPAL(x1)) = x1   
POL(U711(x1, x2, x3)) = 1 + x1 + x3   
POL(U721(x1, x2)) = x2   
POL(U811(x1, x2)) = x2   
POL(U821(x1, x2)) = x2   
POL(U91(x1, x2)) = 0   
POL(U92(x1)) = 0   
POL(__(x1, x2)) = 1 + x1 + x2   
POL(__Inact(x1, x2)) = 1 + x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(e) = 0   
POL(eInact) = 0   
POL(i) = 0   
POL(iInact) = 0   
POL(isPalListKind(x1)) = 0   
POL(isQid(x1)) = 1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   

The following usable rules [17] were oriented:

__(X, nil) → X
a(__Inact(x1, x2)) → __(x1, x2)
isQid(oInact) → tt
a(oInact) → o
nil → nilInact
isQid(eInact) → tt
a(iInact) → i
isQid(aInact) → tt
u → uInact
a(eInact) → e
e → eInact
a(uInact) → u
isQid(iInact) → tt
__(nil, X) → X
i → iInact
o → oInact
a → aInact
a(aInact) → a
__(__(X, Y), Z) → __(X, __(Y, Z))
a(nilInact) → nil
a(x) → x
__(x1, x2) → __Inact(x1, x2)
isQid(uInact) → tt



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ DependencyGraphProof
              ↳ QDP

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

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 5 less nodes.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof

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

U531(tt, V1, V2) → U541(isPalListKind(a(V2)), a(V1), a(V2))
U241(tt, V1, V2) → U251(isList(a(V1)), a(V2))
U211(tt, V1, V2) → U221(isPalListKind(a(V1)), a(V1), a(V2))
U511(tt, V1, V2) → U521(isPalListKind(a(V1)), a(V1), a(V2))
ISNELIST(__Inact(V1, V2)) → U411(isPalListKind(a(V1)), a(V1), a(V2))
U441(tt, V1, V2) → ISLIST(a(V1))
U121(tt, V) → ISNELIST(a(V))
U541(tt, V1, V2) → U551(isNeList(a(V1)), a(V2))
U251(tt, V2) → ISLIST(a(V2))
U551(tt, V2) → ISLIST(a(V2))
U411(tt, V1, V2) → U421(isPalListKind(a(V1)), a(V1), a(V2))
U421(tt, V1, V2) → U431(isPalListKind(a(V2)), a(V1), a(V2))
U221(tt, V1, V2) → U231(isPalListKind(a(V2)), a(V1), a(V2))
U111(tt, V) → U121(isPalListKind(a(V)), a(V))
ISNELIST(__Inact(V1, V2)) → U511(isPalListKind(a(V1)), a(V1), a(V2))
U541(tt, V1, V2) → ISNELIST(a(V1))
U241(tt, V1, V2) → ISLIST(a(V1))
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
U231(tt, V1, V2) → U241(isPalListKind(a(V2)), a(V1), a(V2))
U521(tt, V1, V2) → U531(isPalListKind(a(V2)), a(V1), a(V2))
U431(tt, V1, V2) → U441(isPalListKind(a(V2)), a(V1), a(V2))
ISLIST(__Inact(V1, V2)) → U211(isPalListKind(a(V1)), a(V1), a(V2))
U451(tt, V2) → ISNELIST(a(V2))
U441(tt, V1, V2) → U451(isList(a(V1)), a(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(a(V)), a(V))
U12(tt, V) → U13(isNeList(a(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(a(V1)), a(V1), a(V2))
U22(tt, V1, V2) → U23(isPalListKind(a(V2)), a(V1), a(V2))
U23(tt, V1, V2) → U24(isPalListKind(a(V2)), a(V1), a(V2))
U24(tt, V1, V2) → U25(isList(a(V1)), a(V2))
U25(tt, V2) → U26(isList(a(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(a(V)), a(V))
U32(tt, V) → U33(isQid(a(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(a(V1)), a(V1), a(V2))
U42(tt, V1, V2) → U43(isPalListKind(a(V2)), a(V1), a(V2))
U43(tt, V1, V2) → U44(isPalListKind(a(V2)), a(V1), a(V2))
U44(tt, V1, V2) → U45(isList(a(V1)), a(V2))
U45(tt, V2) → U46(isNeList(a(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(a(V1)), a(V1), a(V2))
U52(tt, V1, V2) → U53(isPalListKind(a(V2)), a(V1), a(V2))
U53(tt, V1, V2) → U54(isPalListKind(a(V2)), a(V1), a(V2))
U54(tt, V1, V2) → U55(isNeList(a(V1)), a(V2))
U55(tt, V2) → U56(isList(a(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(a(V)), a(V))
U62(tt, V) → U63(isQid(a(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(a(I)), a(P))
U72(tt, P) → U73(isPal(a(P)), a(P))
U73(tt, P) → U74(isPalListKind(a(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(a(V)), a(V))
U82(tt, V) → U83(isNePal(a(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(a(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(isPalListKind(a(V1)), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(I), a(P))
isPal(V) → U81(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → U91(isPalListKind(a(V1)), a(V2))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
u → uInact
a(uInact) → u
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U441(tt, V1, V2) → ISLIST(a(V1))
ISNELIST(__Inact(V1, V2)) → U511(isPalListKind(a(V1)), a(V1), a(V2))
ISLIST(__Inact(V1, V2)) → U211(isPalListKind(a(V1)), a(V1), a(V2))
U451(tt, V2) → ISNELIST(a(V2))
The remaining pairs can at least be oriented weakly.

U531(tt, V1, V2) → U541(isPalListKind(a(V2)), a(V1), a(V2))
U241(tt, V1, V2) → U251(isList(a(V1)), a(V2))
U211(tt, V1, V2) → U221(isPalListKind(a(V1)), a(V1), a(V2))
U511(tt, V1, V2) → U521(isPalListKind(a(V1)), a(V1), a(V2))
ISNELIST(__Inact(V1, V2)) → U411(isPalListKind(a(V1)), a(V1), a(V2))
U121(tt, V) → ISNELIST(a(V))
U541(tt, V1, V2) → U551(isNeList(a(V1)), a(V2))
U251(tt, V2) → ISLIST(a(V2))
U551(tt, V2) → ISLIST(a(V2))
U411(tt, V1, V2) → U421(isPalListKind(a(V1)), a(V1), a(V2))
U421(tt, V1, V2) → U431(isPalListKind(a(V2)), a(V1), a(V2))
U221(tt, V1, V2) → U231(isPalListKind(a(V2)), a(V1), a(V2))
U111(tt, V) → U121(isPalListKind(a(V)), a(V))
U541(tt, V1, V2) → ISNELIST(a(V1))
U241(tt, V1, V2) → ISLIST(a(V1))
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
U231(tt, V1, V2) → U241(isPalListKind(a(V2)), a(V1), a(V2))
U521(tt, V1, V2) → U531(isPalListKind(a(V2)), a(V1), a(V2))
U431(tt, V1, V2) → U441(isPalListKind(a(V2)), a(V1), a(V2))
U441(tt, V1, V2) → U451(isList(a(V1)), a(V2))
Used ordering: Polynomial interpretation [25]:

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

The following usable rules [17] were oriented:

a(oInact) → o
a(eInact) → e
e → eInact
a(uInact) → u
__(nil, X) → X
a(aInact) → a
__(__(X, Y), Z) → __(X, __(Y, Z))
__(x1, x2) → __Inact(x1, x2)
__(X, nil) → X
a(__Inact(x1, x2)) → __(x1, x2)
nil → nilInact
a(iInact) → i
u → uInact
i → iInact
o → oInact
a → aInact
a(nilInact) → nil
a(x) → x



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ DependencyGraphProof

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

U531(tt, V1, V2) → U541(isPalListKind(a(V2)), a(V1), a(V2))
U241(tt, V1, V2) → U251(isList(a(V1)), a(V2))
U211(tt, V1, V2) → U221(isPalListKind(a(V1)), a(V1), a(V2))
U511(tt, V1, V2) → U521(isPalListKind(a(V1)), a(V1), a(V2))
ISNELIST(__Inact(V1, V2)) → U411(isPalListKind(a(V1)), a(V1), a(V2))
U121(tt, V) → ISNELIST(a(V))
U541(tt, V1, V2) → U551(isNeList(a(V1)), a(V2))
U251(tt, V2) → ISLIST(a(V2))
U551(tt, V2) → ISLIST(a(V2))
U411(tt, V1, V2) → U421(isPalListKind(a(V1)), a(V1), a(V2))
U421(tt, V1, V2) → U431(isPalListKind(a(V2)), a(V1), a(V2))
U221(tt, V1, V2) → U231(isPalListKind(a(V2)), a(V1), a(V2))
U111(tt, V) → U121(isPalListKind(a(V)), a(V))
U241(tt, V1, V2) → ISLIST(a(V1))
U541(tt, V1, V2) → ISNELIST(a(V1))
ISLIST(V) → U111(isPalListKind(a(V)), a(V))
U521(tt, V1, V2) → U531(isPalListKind(a(V2)), a(V1), a(V2))
U231(tt, V1, V2) → U241(isPalListKind(a(V2)), a(V1), a(V2))
U431(tt, V1, V2) → U441(isPalListKind(a(V2)), a(V1), a(V2))
U441(tt, V1, V2) → U451(isList(a(V1)), a(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(a(V)), a(V))
U12(tt, V) → U13(isNeList(a(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(a(V1)), a(V1), a(V2))
U22(tt, V1, V2) → U23(isPalListKind(a(V2)), a(V1), a(V2))
U23(tt, V1, V2) → U24(isPalListKind(a(V2)), a(V1), a(V2))
U24(tt, V1, V2) → U25(isList(a(V1)), a(V2))
U25(tt, V2) → U26(isList(a(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(a(V)), a(V))
U32(tt, V) → U33(isQid(a(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(a(V1)), a(V1), a(V2))
U42(tt, V1, V2) → U43(isPalListKind(a(V2)), a(V1), a(V2))
U43(tt, V1, V2) → U44(isPalListKind(a(V2)), a(V1), a(V2))
U44(tt, V1, V2) → U45(isList(a(V1)), a(V2))
U45(tt, V2) → U46(isNeList(a(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(a(V1)), a(V1), a(V2))
U52(tt, V1, V2) → U53(isPalListKind(a(V2)), a(V1), a(V2))
U53(tt, V1, V2) → U54(isPalListKind(a(V2)), a(V1), a(V2))
U54(tt, V1, V2) → U55(isNeList(a(V1)), a(V2))
U55(tt, V2) → U56(isList(a(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(a(V)), a(V))
U62(tt, V) → U63(isQid(a(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(a(I)), a(P))
U72(tt, P) → U73(isPal(a(P)), a(P))
U73(tt, P) → U74(isPalListKind(a(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(a(V)), a(V))
U82(tt, V) → U83(isNePal(a(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(a(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(a(V)), a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(V) → U31(isPalListKind(a(V)), a(V))
isNeList(__Inact(V1, V2)) → U41(isPalListKind(a(V1)), a(V1), a(V2))
isNeList(__Inact(V1, V2)) → U51(isPalListKind(a(V1)), a(V1), a(V2))
isNePal(V) → U61(isPalListKind(a(V)), a(V))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(I), a(P))
isPal(V) → U81(isPalListKind(a(V)), a(V))
isPal(nilInact) → tt
isPalListKind(aInact) → tt
isPalListKind(eInact) → tt
isPalListKind(iInact) → tt
isPalListKind(nilInact) → tt
isPalListKind(oInact) → tt
isPalListKind(uInact) → tt
isPalListKind(__Inact(V1, V2)) → U91(isPalListKind(a(V1)), a(V2))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
u → uInact
a(uInact) → u
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 20 less nodes.