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

(0) Obligation:

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.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

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

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

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

(2) Obligation:

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.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

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

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNePal → U61(isPalListKind)
isPal → tt

(4) Obligation:

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 → U71(isQid)
isPal → U81(isPalListKind)
isPalListKind → tt
isPalListKind → U91(isPalListKind)
isQid → tt

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

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

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U62(tt) → U63(isQid)
U63(tt) → tt

(6) Obligation:

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)
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.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

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

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U61(tt) → U62(isPalListKind)

(8) Obligation:

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.

(9) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(10) Obligation:

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

U11¹(tt) → U12¹(isPalListKind)
U11¹(tt) → ISPALLISTKIND
U12¹(tt) → U13¹(isNeList)
U12¹(tt) → ISNELIST
U21¹(tt) → U22¹(isPalListKind)
U21¹(tt) → ISPALLISTKIND
U22¹(tt) → U23¹(isPalListKind)
U22¹(tt) → ISPALLISTKIND
U23¹(tt) → U24¹(isPalListKind)
U23¹(tt) → ISPALLISTKIND
U24¹(tt) → U25¹(isList)
U24¹(tt) → ISLIST
U25¹(tt) → U26¹(isList)
U25¹(tt) → ISLIST
U31¹(tt) → U32¹(isPalListKind)
U31¹(tt) → ISPALLISTKIND
U32¹(tt) → U33¹(isQid)
U32¹(tt) → ISQID
U41¹(tt) → U42¹(isPalListKind)
U41¹(tt) → ISPALLISTKIND
U42¹(tt) → U43¹(isPalListKind)
U42¹(tt) → ISPALLISTKIND
U43¹(tt) → U44¹(isPalListKind)
U43¹(tt) → ISPALLISTKIND
U44¹(tt) → U45¹(isList)
U44¹(tt) → ISLIST
U45¹(tt) → U46¹(isNeList)
U45¹(tt) → ISNELIST
U51¹(tt) → U52¹(isPalListKind)
U51¹(tt) → ISPALLISTKIND
U52¹(tt) → U53¹(isPalListKind)
U52¹(tt) → ISPALLISTKIND
U53¹(tt) → U54¹(isPalListKind)
U53¹(tt) → ISPALLISTKIND
U54¹(tt) → U55¹(isNeList)
U54¹(tt) → ISNELIST
U55¹(tt) → U56¹(isList)
U55¹(tt) → ISLIST
U71¹(tt) → U72¹(isPalListKind)
U71¹(tt) → ISPALLISTKIND
U72¹(tt) → U73¹(isPal)
U72¹(tt) → ISPAL
U73¹(tt) → U74¹(isPalListKind)
U73¹(tt) → ISPALLISTKIND
U81¹(tt) → U82¹(isPalListKind)
U81¹(tt) → ISPALLISTKIND
U82¹(tt) → U83¹(isNePal)
U82¹(tt) → ISNEPAL
U91¹(tt) → U92¹(isPalListKind)
U91¹(tt) → ISPALLISTKIND
ISLIST → U11¹(isPalListKind)
ISLIST → ISPALLISTKIND
ISLIST → U21¹(isPalListKind)
ISNELIST → U31¹(isPalListKind)
ISNELIST → ISPALLISTKIND
ISNELIST → U41¹(isPalListKind)
ISNELIST → U51¹(isPalListKind)
ISNEPAL → U71¹(isQid)
ISNEPAL → ISQID
ISPAL → U81¹(isPalListKind)
ISPAL → ISPALLISTKIND
ISPALLISTKIND → U91¹(isPalListKind)
ISPALLISTKIND → 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.

(11) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 30 less nodes.

(12) Complex Obligation (AND)

(13) Obligation:

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

U91¹(tt) → ISPALLISTKIND
ISPALLISTKIND → U91¹(isPalListKind)
ISPALLISTKIND → 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.

(14) NonLoopProof (EQUIVALENT transformation)

By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 0,
σ' = [ ], and μ' = [ ] on the rule
ISPALLISTKIND[ ]ⁿ[ ] → ISPALLISTKIND[ ]ⁿ[ ]
This rule is correct for the QDP as the following derivation shows:

ISPALLISTKIND[ ]ⁿ[ ] → ISPALLISTKIND[ ]ⁿ[ ]
    by OriginalRule from TRS P

(15) NO

(16) Obligation:

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

U72¹(tt) → ISPAL
ISPAL → U81¹(isPalListKind)
U81¹(tt) → U82¹(isPalListKind)
U82¹(tt) → ISNEPAL
ISNEPAL → U71¹(isQid)
U71¹(tt) → U72¹(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.

(17) NonLoopProof (EQUIVALENT transformation)

By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 0,
σ' = [ ], and μ' = [ ] on the rule
U72¹(tt)[ ]ⁿ[ ] → U72¹(tt)[ ]ⁿ[ ]
This rule is correct for the QDP as the following derivation shows:

U72¹(tt)[ ]ⁿ[ ] → U72¹(tt)[ ]ⁿ[ ]
    by Narrowing at position: [0]
        U72¹(tt)[ ]ⁿ[ ] → U72¹(isPalListKind)[ ]ⁿ[ ]
            by Narrowing at position: []
                U72¹(tt)[ ]ⁿ[ ] → U71¹(tt)[ ]ⁿ[ ]
                    by Narrowing at position: [0]
                        U72¹(tt)[ ]ⁿ[ ] → U71¹(isQid)[ ]ⁿ[ ]
                            by Narrowing at position: []
                                U72¹(tt)[ ]ⁿ[ ] → ISNEPAL[ ]ⁿ[ ]
                                    by Narrowing at position: []
                                        U72¹(tt)[ ]ⁿ[ ] → U82¹(tt)[ ]ⁿ[ ]
                                            by Narrowing at position: [0]
                                                U72¹(tt)[ ]ⁿ[ ] → U82¹(isPalListKind)[ ]ⁿ[ ]
                                                    by Narrowing at position: []
                                                        U72¹(tt)[ ]ⁿ[ ] → U81¹(tt)[ ]ⁿ[ ]
                                                            by Narrowing at position: [0]
                                                                U72¹(tt)[ ]ⁿ[ ] → U81¹(isPalListKind)[ ]ⁿ[ ]
                                                                    by Narrowing at position: []
                                                                        U72¹(tt)[ ]ⁿ[ ] → ISPAL[ ]ⁿ[ ]
                                                                            by OriginalRule from TRS P

                                                                        ISPAL[ ]ⁿ[ ] → U81¹(isPalListKind)[ ]ⁿ[ ]
                                                                            by OriginalRule from TRS P

                                                                isPalListKind[ ]ⁿ[ ] → tt[ ]ⁿ[ ]
                                                                    by OriginalRule from TRS R

                                                        U81¹(tt)[ ]ⁿ[ ] → U82¹(isPalListKind)[ ]ⁿ[ ]
                                                            by OriginalRule from TRS P

                                                isPalListKind[ ]ⁿ[ ] → tt[ ]ⁿ[ ]
                                                    by OriginalRule from TRS R

                                        U82¹(tt)[ ]ⁿ[ ] → ISNEPAL[ ]ⁿ[ ]
                                            by OriginalRule from TRS P

                                ISNEPAL[ ]ⁿ[ ] → U71¹(isQid)[ ]ⁿ[ ]
                                    by OriginalRule from TRS P

                        isQid[ ]ⁿ[ ] → tt[ ]ⁿ[ ]
                            by OriginalRule from TRS R

                U71¹(tt)[ ]ⁿ[ ] → U72¹(isPalListKind)[ ]ⁿ[ ]
                    by OriginalRule from TRS P

        isPalListKind[ ]ⁿ[ ] → tt[ ]ⁿ[ ]
            by OriginalRule from TRS R

(18) NO

(19) Obligation:

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

U12¹(tt) → ISNELIST
ISNELIST → U41¹(isPalListKind)
U41¹(tt) → U42¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST

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.

(20) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(21) Obligation:

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

U12¹(tt) → ISNELIST
ISNELIST → U41¹(isPalListKind)
U41¹(tt) → U42¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(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.

(22) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNELIST → U41¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))

(23) Obligation:

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

U12¹(tt) → ISNELIST
U41¹(tt) → U42¹(isPalListKind)
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))

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.

(24) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U41¹(tt) → U42¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))

(25) Obligation:

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

U12¹(tt) → ISNELIST
U42¹(tt) → U43¹(isPalListKind)
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))

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.

(26) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U42¹(tt) → U43¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))

(27) Obligation:

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

U12¹(tt) → ISNELIST
U43¹(tt) → U44¹(isPalListKind)
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))

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.

(28) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U43¹(tt) → U44¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))

(29) Obligation:

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

U12¹(tt) → ISNELIST
U44¹(tt) → U45¹(isList)
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))

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.

(30) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U44¹(tt) → U45¹(isList) at position [0] we obtained the following new rules [LPAR04]:

U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))

(31) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
ISNELIST → U51¹(isPalListKind)
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))

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.

(32) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNELIST → U51¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))

(33) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U51¹(tt) → U52¹(isPalListKind)
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))

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.

(34) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U51¹(tt) → U52¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))

(35) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U52¹(tt) → U53¹(isPalListKind)
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))

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.

(36) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U52¹(tt) → U53¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))

(37) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U53¹(tt) → U54¹(isPalListKind)
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))

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.

(38) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U53¹(tt) → U54¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))

(39) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U54¹(tt) → U55¹(isNeList)
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))

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.

(40) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U54¹(tt) → U55¹(isNeList) at position [0] we obtained the following new rules [LPAR04]:

U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))

(41) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
ISLIST → U11¹(isPalListKind)
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))

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.

(42) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISLIST → U11¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))

(43) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U11¹(tt) → U12¹(isPalListKind)
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))

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.

(44) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U11¹(tt) → U12¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))

(45) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
ISLIST → U21¹(isPalListKind)
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))

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.

(46) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISLIST → U21¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))

(47) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U21¹(tt) → U22¹(isPalListKind)
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))

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.

(48) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U21¹(tt) → U22¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))

(49) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U22¹(tt) → U23¹(isPalListKind)
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))

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.

(50) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U22¹(tt) → U23¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))

(51) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U23¹(tt) → U24¹(isPalListKind)
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))

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.

(52) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U23¹(tt) → U24¹(isPalListKind) at position [0] we obtained the following new rules [LPAR04]:

U23¹(tt) → U24¹(tt)
U23¹(tt) → U24¹(U91(isPalListKind))

(53) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U24¹(tt) → U25¹(isList)
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U23¹(tt) → U24¹(U91(isPalListKind))

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.

(54) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U24¹(tt) → U25¹(isList) at position [0] we obtained the following new rules [LPAR04]:

U24¹(tt) → U25¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))

(55) Obligation:

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

U12¹(tt) → ISNELIST
U45¹(tt) → ISNELIST
U55¹(tt) → ISLIST
U25¹(tt) → ISLIST
U24¹(tt) → ISLIST
U54¹(tt) → ISNELIST
U44¹(tt) → ISLIST
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U91(isPalListKind))
U41¹(tt) → U42¹(tt)
U41¹(tt) → U42¹(U91(isPalListKind))
U42¹(tt) → U43¹(tt)
U42¹(tt) → U43¹(U91(isPalListKind))
U43¹(tt) → U44¹(tt)
U43¹(tt) → U44¹(U91(isPalListKind))
U44¹(tt) → U45¹(U11(isPalListKind))
U44¹(tt) → U45¹(tt)
U44¹(tt) → U45¹(U21(isPalListKind))
ISNELIST → U51¹(tt)
ISNELIST → U51¹(U91(isPalListKind))
U51¹(tt) → U52¹(tt)
U51¹(tt) → U52¹(U91(isPalListKind))
U52¹(tt) → U53¹(tt)
U52¹(tt) → U53¹(U91(isPalListKind))
U53¹(tt) → U54¹(tt)
U53¹(tt) → U54¹(U91(isPalListKind))
U54¹(tt) → U55¹(U31(isPalListKind))
U54¹(tt) → U55¹(U41(isPalListKind))
U54¹(tt) → U55¹(U51(isPalListKind))
ISLIST → U11¹(tt)
ISLIST → U11¹(U91(isPalListKind))
U11¹(tt) → U12¹(tt)
U11¹(tt) → U12¹(U91(isPalListKind))
ISLIST → U21¹(tt)
ISLIST → U21¹(U91(isPalListKind))
U21¹(tt) → U22¹(tt)
U21¹(tt) → U22¹(U91(isPalListKind))
U22¹(tt) → U23¹(tt)
U22¹(tt) → U23¹(U91(isPalListKind))
U23¹(tt) → U24¹(tt)
U23¹(tt) → U24¹(U91(isPalListKind))
U24¹(tt) → U25¹(U11(isPalListKind))
U24¹(tt) → U25¹(tt)
U24¹(tt) → U25¹(U21(isPalListKind))

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.

(56) NonTerminationLoopProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ISLIST evaluates to t =ISLIST

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

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

ISLIST → U21¹(tt)
with rule ISLIST → U21¹(tt) at position [] and matcher [ ]

U21¹(tt) → U22¹(tt)
with rule U21¹(tt) → U22¹(tt) at position [] and matcher [ ]

U22¹(tt) → U23¹(tt)
with rule U22¹(tt) → U23¹(tt) at position [] and matcher [ ]

U23¹(tt) → U24¹(tt)
with rule U23¹(tt) → U24¹(tt) at position [] and matcher [ ]

U24¹(tt) → ISLIST
with rule U24¹(tt) → ISLIST

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.

(57) NO