YES
The TRS could be proven terminating. The proof took 3240 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (998ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (127ms).
| | – Problem 6 was processed with processor PolynomialLinearRange4 (21ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (780ms).
| | – Problem 7 was processed with processor DependencyGraph (80ms).
| | | – Problem 10 was processed with processor PolynomialLinearRange4 (291ms).
| | | | – Problem 11 was processed with processor DependencyGraph (35ms).
| | | | | – Problem 12 was processed with processor PolynomialLinearRange4 (190ms).
| | | | | | – Problem 14 was processed with processor DependencyGraph (3ms).
| | | | | – Problem 13 was processed with processor PolynomialLinearRange4 (179ms).
| | | | | | – Problem 15 was processed with processor DependencyGraph (5ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (99ms).
| | – Problem 8 was processed with processor DependencyGraph (3ms).
| – Problem 5 was processed with processor PolynomialLinearRange4 (47ms).
| | – Problem 9 was processed with processor DependencyGraph (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U91#(tt, V2) | → | isPalListKind#(V2) | | U53#(tt, V1, V2) | → | isPalListKind#(V2) |
| U61#(tt, V) | → | U62#(isPalListKind(V), V) | | U55#(tt, V2) | → | isList#(V2) |
| U52#(tt, V1, V2) | → | isPalListKind#(V2) | | isList#(V) | → | isPalListKind#(V) |
| U44#(tt, V1, V2) | → | isList#(V1) | | U51#(tt, V1, V2) | → | U52#(isPalListKind(V1), V1, V2) |
| U72#(tt, P) | → | U73#(isPal(P), P) | | U71#(tt, I, P) | → | isPalListKind#(I) |
| U81#(tt, V) | → | U82#(isPalListKind(V), V) | | U31#(tt, V) | → | U32#(isPalListKind(V), V) |
| U24#(tt, V1, V2) | → | isList#(V1) | | U54#(tt, V1, V2) | → | isNeList#(V1) |
| U62#(tt, V) | → | U63#(isQid(V)) | | U62#(tt, V) | → | isQid#(V) |
| U31#(tt, V) | → | isPalListKind#(V) | | U22#(tt, V1, V2) | → | isPalListKind#(V2) |
| U55#(tt, V2) | → | U56#(isList(V2)) | | U91#(tt, V2) | → | U92#(isPalListKind(V2)) |
| isList#(__(V1, V2)) | → | U21#(isPalListKind(V1), V1, V2) | | isNeList#(V) | → | isPalListKind#(V) |
| isNeList#(V) | → | U31#(isPalListKind(V), V) | | isNePal#(__(I, __(P, I))) | → | isQid#(I) |
| U12#(tt, V) | → | U13#(isNeList(V)) | | U52#(tt, V1, V2) | → | U53#(isPalListKind(V2), V1, V2) |
| isPal#(V) | → | U81#(isPalListKind(V), V) | | U25#(tt, V2) | → | U26#(isList(V2)) |
| U73#(tt, P) | → | U74#(isPalListKind(P)) | | isList#(V) | → | U11#(isPalListKind(V), V) |
| U43#(tt, V1, V2) | → | isPalListKind#(V2) | | U43#(tt, V1, V2) | → | U44#(isPalListKind(V2), V1, V2) |
| U11#(tt, V) | → | isPalListKind#(V) | | U45#(tt, V2) | → | isNeList#(V2) |
| U23#(tt, V1, V2) | → | isPalListKind#(V2) | | U42#(tt, V1, V2) | → | isPalListKind#(V2) |
| U32#(tt, V) | → | isQid#(V) | | isPal#(V) | → | isPalListKind#(V) |
| isNeList#(__(V1, V2)) | → | U41#(isPalListKind(V1), V1, V2) | | isNePal#(V) | → | U61#(isPalListKind(V), V) |
| U23#(tt, V1, V2) | → | U24#(isPalListKind(V2), V1, V2) | | isPalListKind#(__(V1, V2)) | → | isPalListKind#(V1) |
| U22#(tt, V1, V2) | → | U23#(isPalListKind(V2), V1, V2) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(V1), V1, V2) | | U53#(tt, V1, V2) | → | U54#(isPalListKind(V2), V1, V2) |
| U24#(tt, V1, V2) | → | U25#(isList(V1), V2) | | U71#(tt, I, P) | → | U72#(isPalListKind(I), P) |
| isNePal#(__(I, __(P, I))) | → | U71#(isQid(I), I, P) | | U32#(tt, V) | → | U33#(isQid(V)) |
| U82#(tt, V) | → | isNePal#(V) | | U44#(tt, V1, V2) | → | U45#(isList(V1), V2) |
| isNePal#(V) | → | isPalListKind#(V) | | U45#(tt, V2) | → | U46#(isNeList(V2)) |
| U73#(tt, P) | → | isPalListKind#(P) | | isNeList#(__(V1, V2)) | → | U51#(isPalListKind(V1), V1, V2) |
| U12#(tt, V) | → | isNeList#(V) | | __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
| U72#(tt, P) | → | isPal#(P) | | isList#(__(V1, V2)) | → | isPalListKind#(V1) |
| U41#(tt, V1, V2) | → | isPalListKind#(V1) | | U81#(tt, V) | → | isPalListKind#(V) |
| U25#(tt, V2) | → | isList#(V2) | | U54#(tt, V1, V2) | → | U55#(isNeList(V1), V2) |
| U11#(tt, V) | → | U12#(isPalListKind(V), V) | | U21#(tt, V1, V2) | → | isPalListKind#(V1) |
| U21#(tt, V1, V2) | → | U22#(isPalListKind(V1), V1, V2) | | U82#(tt, V) | → | U83#(isNePal(V)) |
| U61#(tt, V) | → | isPalListKind#(V) | | U42#(tt, V1, V2) | → | U43#(isPalListKind(V2), V1, V2) |
| isNeList#(__(V1, V2)) | → | isPalListKind#(V1) | | isPalListKind#(__(V1, V2)) | → | U91#(isPalListKind(V1), V2) |
| U51#(tt, V1, V2) | → | isPalListKind#(V1) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
The following SCCs where found
| U91#(tt, V2) → isPalListKind#(V2) | isPalListKind#(__(V1, V2)) → isPalListKind#(V1) |
| isPalListKind#(__(V1, V2)) → U91#(isPalListKind(V1), V2) |
| isNePal#(__(I, __(P, I))) → U71#(isQid(I), I, P) | U82#(tt, V) → isNePal#(V) |
| U72#(tt, P) → isPal#(P) | U81#(tt, V) → U82#(isPalListKind(V), V) |
| isPal#(V) → U81#(isPalListKind(V), V) | U71#(tt, I, P) → U72#(isPalListKind(I), P) |
| U23#(tt, V1, V2) → U24#(isPalListKind(V2), V1, V2) | isList#(__(V1, V2)) → U21#(isPalListKind(V1), V1, V2) |
| U55#(tt, V2) → isList#(V2) | U22#(tt, V1, V2) → U23#(isPalListKind(V2), V1, V2) |
| U52#(tt, V1, V2) → U53#(isPalListKind(V2), V1, V2) | U44#(tt, V1, V2) → isList#(V1) |
| U53#(tt, V1, V2) → U54#(isPalListKind(V2), V1, V2) | U41#(tt, V1, V2) → U42#(isPalListKind(V1), V1, V2) |
| U51#(tt, V1, V2) → U52#(isPalListKind(V1), V1, V2) | U24#(tt, V1, V2) → U25#(isList(V1), V2) |
| isList#(V) → U11#(isPalListKind(V), V) | U43#(tt, V1, V2) → U44#(isPalListKind(V2), V1, V2) |
| U25#(tt, V2) → isList#(V2) | U45#(tt, V2) → isNeList#(V2) |
| U11#(tt, V) → U12#(isPalListKind(V), V) | U54#(tt, V1, V2) → U55#(isNeList(V1), V2) |
| U21#(tt, V1, V2) → U22#(isPalListKind(V1), V1, V2) | U54#(tt, V1, V2) → isNeList#(V1) |
| U24#(tt, V1, V2) → isList#(V1) | U44#(tt, V1, V2) → U45#(isList(V1), V2) |
| U42#(tt, V1, V2) → U43#(isPalListKind(V2), V1, V2) | isNeList#(__(V1, V2)) → U51#(isPalListKind(V1), V1, V2) |
| U12#(tt, V) → isNeList#(V) | isNeList#(__(V1, V2)) → U41#(isPalListKind(V1), V1, V2) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U26#) = μ(U61#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U46) = μ(U74#) = μ(U45) = μ(U44) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U92) = μ(U91) = μ(U54#) = μ(U33#) = μ(U63#) = μ(U92#) = μ(U83) = μ(U24#) = μ(U53#) = μ(U82#) = μ(U55) = μ(U54) = μ(U44#) = μ(U73#) = μ(U56) = μ(U51) = μ(U53) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U12(x,y): 0
- U13(x): 0
- U21(x,y,z): 0
- U22(x,y,z): 0
- U23(x,y,z): 0
- U24(x,y,z): 0
- U25(x,y): 0
- U26(x): 0
- U31(x,y): 0
- U32(x,y): 0
- U33(x): 0
- U41(x,y,z): 0
- U42(x,y,z): 0
- U43(x,y,z): 0
- U44(x,y,z): 0
- U45(x,y): 0
- U46(x): 0
- U51(x,y,z): 0
- U52(x,y,z): 0
- U53(x,y,z): 0
- U54(x,y,z): 0
- U55(x,y): 0
- U56(x): 0
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U82(x,y): 0
- U83(x): 0
- U91(x,y): 0
- U92(x): 0
- __(x,y): y + x + 1
- __#(x,y): y + x
- a: 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 0
- isQid(x): 0
- nil: 0
- o: 0
- tt: 0
- u: 0
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| __#(__(X, Y), Z) | → | __#(Y, Z) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, isQid, U31, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U12(x,y): 0
- U13(x): 0
- U21(x,y,z): 0
- U22(x,y,z): 0
- U23(x,y,z): 0
- U24(x,y,z): 0
- U25(x,y): 0
- U26(x): 0
- U31(x,y): 0
- U32(x,y): 0
- U33(x): 0
- U41(x,y,z): 0
- U42(x,y,z): 0
- U43(x,y,z): 0
- U44(x,y,z): 0
- U45(x,y): 0
- U46(x): 0
- U51(x,y,z): 0
- U52(x,y,z): 0
- U53(x,y,z): 0
- U54(x,y,z): 0
- U55(x,y): 0
- U56(x): 0
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U82(x,y): 0
- U83(x): 0
- U91(x,y): 0
- U92(x): 0
- __(x,y): y + x + 1
- __#(x,y): x
- a: 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 0
- isQid(x): 0
- nil: 2
- o: 0
- tt: 0
- u: 0
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isList#(__(V1, V2)) | → | U21#(isPalListKind(V1), V1, V2) | | U23#(tt, V1, V2) | → | U24#(isPalListKind(V2), V1, V2) |
| U22#(tt, V1, V2) | → | U23#(isPalListKind(V2), V1, V2) | | U55#(tt, V2) | → | isList#(V2) |
| U52#(tt, V1, V2) | → | U53#(isPalListKind(V2), V1, V2) | | U44#(tt, V1, V2) | → | isList#(V1) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(V1), V1, V2) | | U53#(tt, V1, V2) | → | U54#(isPalListKind(V2), V1, V2) |
| U24#(tt, V1, V2) | → | U25#(isList(V1), V2) | | U51#(tt, V1, V2) | → | U52#(isPalListKind(V1), V1, V2) |
| isList#(V) | → | U11#(isPalListKind(V), V) | | U43#(tt, V1, V2) | → | U44#(isPalListKind(V2), V1, V2) |
| U25#(tt, V2) | → | isList#(V2) | | U45#(tt, V2) | → | isNeList#(V2) |
| U11#(tt, V) | → | U12#(isPalListKind(V), V) | | U54#(tt, V1, V2) | → | U55#(isNeList(V1), V2) |
| U21#(tt, V1, V2) | → | U22#(isPalListKind(V1), V1, V2) | | U44#(tt, V1, V2) | → | U45#(isList(V1), V2) |
| U24#(tt, V1, V2) | → | isList#(V1) | | U54#(tt, V1, V2) | → | isNeList#(V1) |
| U42#(tt, V1, V2) | → | U43#(isPalListKind(V2), V1, V2) | | isNeList#(__(V1, V2)) | → | U51#(isPalListKind(V1), V1, V2) |
| U12#(tt, V) | → | isNeList#(V) | | isNeList#(__(V1, V2)) | → | U41#(isPalListKind(V1), V1, V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U26#) = μ(U61#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U46) = μ(U74#) = μ(U45) = μ(U44) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U92) = μ(U91) = μ(U54#) = μ(U33#) = μ(U63#) = μ(U92#) = μ(U83) = μ(U24#) = μ(U53#) = μ(U82#) = μ(U55) = μ(U54) = μ(U44#) = μ(U73#) = μ(U56) = μ(U51) = μ(U53) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U11#(x,y): 2y
- U12(x,y): 0
- U12#(x,y): 2y
- U13(x): 0
- U21(x,y,z): 0
- U21#(x,y,z): 2z + 2y + 2x
- U22(x,y,z): 0
- U22#(x,y,z): 2z + 2y
- U23(x,y,z): 0
- U23#(x,y,z): 2z + 2y
- U24(x,y,z): 0
- U24#(x,y,z): 2z + 2y
- U25(x,y): 0
- U25#(x,y): 2y
- U26(x): 0
- U31(x,y): x + 1
- U32(x,y): 0
- U33(x): 0
- U41(x,y,z): 2
- U41#(x,y,z): 3z + 2y + 2x
- U42(x,y,z): 2
- U42#(x,y,z): 2z + 2y
- U43(x,y,z): 1
- U43#(x,y,z): 2z + 2y
- U44(x,y,z): 1
- U44#(x,y,z): 2z + 2y
- U45(x,y): 1
- U45#(x,y): 2y
- U46(x): 0
- U51(x,y,z): 2
- U51#(x,y,z): 3z + 2y + 1
- U52(x,y,z): 0
- U52#(x,y,z): 3z + 2y + 1
- U53(x,y,z): 0
- U53#(x,y,z): 2z + 2y + 1
- U54(x,y,z): 0
- U54#(x,y,z): 2z + 2y
- U55(x,y): 0
- U55#(x,y): 2y
- U56(x): 0
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U82(x,y): 0
- U83(x): 0
- U91(x,y): 0
- U92(x): 0
- __(x,y): 2y + x + 1
- a: 3
- e: 0
- i: 3
- isList(x): 0
- isList#(x): 2x
- isNeList(x): 2
- isNeList#(x): 2x
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 1
- isQid(x): 1
- nil: 0
- o: 1
- tt: 0
- u: 0
Standard Usable rules
| U42(tt, V1, V2) | → | U43(isPalListKind(V2), V1, V2) | | U52(tt, V1, V2) | → | U53(isPalListKind(V2), V1, V2) |
| U54(tt, V1, V2) | → | U55(isNeList(V1), V2) | | isQid(u) | → | tt |
| U12(tt, V) | → | U13(isNeList(V)) | | U31(tt, V) | → | U32(isPalListKind(V), V) |
| isPalListKind(e) | → | tt | | U43(tt, V1, V2) | → | U44(isPalListKind(V2), V1, V2) |
| U92(tt) | → | tt | | isPalListKind(a) | → | tt |
| isList(__(V1, V2)) | → | U21(isPalListKind(V1), V1, V2) | | U32(tt, V) | → | U33(isQid(V)) |
| U33(tt) | → | tt | | U13(tt) | → | tt |
| U25(tt, V2) | → | U26(isList(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(V2), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(isPalListKind(V1), V1, V2) | | isNeList(V) | → | U31(isPalListKind(V), V) |
| U56(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(V2)) |
| isQid(o) | → | tt | | isQid(i) | → | tt |
| isQid(e) | → | tt | | U44(tt, V1, V2) | → | U45(isList(V1), V2) |
| U45(tt, V2) | → | U46(isNeList(V2)) | | U41(tt, V1, V2) | → | U42(isPalListKind(V1), V1, V2) |
| isPalListKind(nil) | → | tt | | U53(tt, V1, V2) | → | U54(isPalListKind(V2), V1, V2) |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| isList(nil) | → | tt | | U55(tt, V2) | → | U56(isList(V2)) |
| U24(tt, V1, V2) | → | U25(isList(V1), V2) | | isPalListKind(i) | → | tt |
| U23(tt, V1, V2) | → | U24(isPalListKind(V2), V1, V2) | | isPalListKind(__(V1, V2)) | → | U91(isPalListKind(V1), V2) |
| isQid(a) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(V1), V1, V2) |
| isNeList(__(V1, V2)) | → | U41(isPalListKind(V1), V1, V2) | | isList(V) | → | U11(isPalListKind(V), V) |
| U11(tt, V) | → | U12(isPalListKind(V), V) | | U26(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(V1), V1, V2) | | U46(tt) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U53#(tt, V1, V2) | → | U54#(isPalListKind(V2), V1, V2) | | isNeList#(__(V1, V2)) | → | U51#(isPalListKind(V1), V1, V2) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(__(V1, V2)) | → | U21#(isPalListKind(V1), V1, V2) | | U23#(tt, V1, V2) | → | U24#(isPalListKind(V2), V1, V2) |
| U22#(tt, V1, V2) | → | U23#(isPalListKind(V2), V1, V2) | | U55#(tt, V2) | → | isList#(V2) |
| U52#(tt, V1, V2) | → | U53#(isPalListKind(V2), V1, V2) | | U44#(tt, V1, V2) | → | isList#(V1) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(V1), V1, V2) | | U24#(tt, V1, V2) | → | U25#(isList(V1), V2) |
| U51#(tt, V1, V2) | → | U52#(isPalListKind(V1), V1, V2) | | isList#(V) | → | U11#(isPalListKind(V), V) |
| U43#(tt, V1, V2) | → | U44#(isPalListKind(V2), V1, V2) | | U25#(tt, V2) | → | isList#(V2) |
| U45#(tt, V2) | → | isNeList#(V2) | | U54#(tt, V1, V2) | → | U55#(isNeList(V1), V2) |
| U11#(tt, V) | → | U12#(isPalListKind(V), V) | | U21#(tt, V1, V2) | → | U22#(isPalListKind(V1), V1, V2) |
| U54#(tt, V1, V2) | → | isNeList#(V1) | | U24#(tt, V1, V2) | → | isList#(V1) |
| U44#(tt, V1, V2) | → | U45#(isList(V1), V2) | | U42#(tt, V1, V2) | → | U43#(isPalListKind(V2), V1, V2) |
| U12#(tt, V) | → | isNeList#(V) | | isNeList#(__(V1, V2)) | → | U41#(isPalListKind(V1), V1, V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, isQid, U31, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
The following SCCs where found
| U23#(tt, V1, V2) → U24#(isPalListKind(V2), V1, V2) | isList#(__(V1, V2)) → U21#(isPalListKind(V1), V1, V2) |
| U22#(tt, V1, V2) → U23#(isPalListKind(V2), V1, V2) | U44#(tt, V1, V2) → isList#(V1) |
| U41#(tt, V1, V2) → U42#(isPalListKind(V1), V1, V2) | U24#(tt, V1, V2) → U25#(isList(V1), V2) |
| isList#(V) → U11#(isPalListKind(V), V) | U43#(tt, V1, V2) → U44#(isPalListKind(V2), V1, V2) |
| U25#(tt, V2) → isList#(V2) | U45#(tt, V2) → isNeList#(V2) |
| U11#(tt, V) → U12#(isPalListKind(V), V) | U21#(tt, V1, V2) → U22#(isPalListKind(V1), V1, V2) |
| U24#(tt, V1, V2) → isList#(V1) | U44#(tt, V1, V2) → U45#(isList(V1), V2) |
| U42#(tt, V1, V2) → U43#(isPalListKind(V2), V1, V2) | U12#(tt, V) → isNeList#(V) |
| isNeList#(__(V1, V2)) → U41#(isPalListKind(V1), V1, V2) |
Problem 10: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isList#(__(V1, V2)) | → | U21#(isPalListKind(V1), V1, V2) | | U23#(tt, V1, V2) | → | U24#(isPalListKind(V2), V1, V2) |
| U22#(tt, V1, V2) | → | U23#(isPalListKind(V2), V1, V2) | | U44#(tt, V1, V2) | → | isList#(V1) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(V1), V1, V2) | | U24#(tt, V1, V2) | → | U25#(isList(V1), V2) |
| isList#(V) | → | U11#(isPalListKind(V), V) | | U43#(tt, V1, V2) | → | U44#(isPalListKind(V2), V1, V2) |
| U25#(tt, V2) | → | isList#(V2) | | U45#(tt, V2) | → | isNeList#(V2) |
| U11#(tt, V) | → | U12#(isPalListKind(V), V) | | U21#(tt, V1, V2) | → | U22#(isPalListKind(V1), V1, V2) |
| U24#(tt, V1, V2) | → | isList#(V1) | | U44#(tt, V1, V2) | → | U45#(isList(V1), V2) |
| U42#(tt, V1, V2) | → | U43#(isPalListKind(V2), V1, V2) | | U12#(tt, V) | → | isNeList#(V) |
| isNeList#(__(V1, V2)) | → | U41#(isPalListKind(V1), V1, V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, isQid, U31, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U26#) = μ(U61#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U46) = μ(U74#) = μ(U45) = μ(U44) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U92) = μ(U91) = μ(U54#) = μ(U33#) = μ(U63#) = μ(U92#) = μ(U83) = μ(U24#) = μ(U53#) = μ(U82#) = μ(U55) = μ(U54) = μ(U44#) = μ(U73#) = μ(U56) = μ(U51) = μ(U53) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 2
- U11#(x,y): y + 2x
- U12(x,y): 2
- U12#(x,y): y
- U13(x): x
- U21(x,y,z): z + 1
- U21#(x,y,z): 3z + 3y
- U22(x,y,z): z
- U22#(x,y,z): 3z + 3y
- U23(x,y,z): x
- U23#(x,y,z): 3z + 3y
- U24(x,y,z): 1
- U24#(x,y,z): 3z + 3y
- U25(x,y): 1
- U25#(x,y): 3y
- U26(x): 1
- U31(x,y): 1
- U32(x,y): 1
- U33(x): 1
- U41(x,y,z): 1
- U41#(x,y,z): z + 3y
- U42(x,y,z): 1
- U42#(x,y,z): z + 3y
- U43(x,y,z): 1
- U43#(x,y,z): z + 3y
- U44(x,y,z): 1
- U44#(x,y,z): z + 3y
- U45(x,y): 1
- U45#(x,y): y
- U46(x): 1
- U51(x,y,z): 1
- U52(x,y,z): 1
- U53(x,y,z): 1
- U54(x,y,z): 1
- U55(x,y): 1
- U56(x): 1
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U82(x,y): 0
- U83(x): 0
- U91(x,y): y + 2x
- U92(x): x + 1
- __(x,y): y + 3x
- a: 2
- e: 2
- i: 2
- isList(x): x + 2
- isList#(x): 3x
- isNeList(x): 2
- isNeList#(x): x
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): x
- isQid(x): 1
- nil: 1
- o: 1
- tt: 1
- u: 2
Standard Usable rules
| U42(tt, V1, V2) | → | U43(isPalListKind(V2), V1, V2) | | U52(tt, V1, V2) | → | U53(isPalListKind(V2), V1, V2) |
| U54(tt, V1, V2) | → | U55(isNeList(V1), V2) | | isQid(u) | → | tt |
| U12(tt, V) | → | U13(isNeList(V)) | | U31(tt, V) | → | U32(isPalListKind(V), V) |
| isPalListKind(e) | → | tt | | U92(tt) | → | tt |
| U43(tt, V1, V2) | → | U44(isPalListKind(V2), V1, V2) | | isPalListKind(a) | → | tt |
| isList(__(V1, V2)) | → | U21(isPalListKind(V1), V1, V2) | | U32(tt, V) | → | U33(isQid(V)) |
| U33(tt) | → | tt | | U13(tt) | → | tt |
| U25(tt, V2) | → | U26(isList(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(V2), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(isPalListKind(V1), V1, V2) | | isNeList(V) | → | U31(isPalListKind(V), V) |
| U56(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(V2)) |
| isQid(o) | → | tt | | isQid(i) | → | tt |
| isQid(e) | → | tt | | U44(tt, V1, V2) | → | U45(isList(V1), V2) |
| U45(tt, V2) | → | U46(isNeList(V2)) | | U41(tt, V1, V2) | → | U42(isPalListKind(V1), V1, V2) |
| isPalListKind(nil) | → | tt | | U53(tt, V1, V2) | → | U54(isPalListKind(V2), V1, V2) |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| isList(nil) | → | tt | | U55(tt, V2) | → | U56(isList(V2)) |
| U24(tt, V1, V2) | → | U25(isList(V1), V2) | | isPalListKind(i) | → | tt |
| U23(tt, V1, V2) | → | U24(isPalListKind(V2), V1, V2) | | isPalListKind(__(V1, V2)) | → | U91(isPalListKind(V1), V2) |
| isQid(a) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(V1), V1, V2) |
| isNeList(__(V1, V2)) | → | U41(isPalListKind(V1), V1, V2) | | isList(V) | → | U11(isPalListKind(V), V) |
| U11(tt, V) | → | U12(isPalListKind(V), V) | | U26(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(V1), V1, V2) | | U46(tt) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U11#(tt, V) | → | U12#(isPalListKind(V), V) |
Problem 11: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(__(V1, V2)) | → | U21#(isPalListKind(V1), V1, V2) | | U23#(tt, V1, V2) | → | U24#(isPalListKind(V2), V1, V2) |
| U22#(tt, V1, V2) | → | U23#(isPalListKind(V2), V1, V2) | | U44#(tt, V1, V2) | → | isList#(V1) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(V1), V1, V2) | | U24#(tt, V1, V2) | → | U25#(isList(V1), V2) |
| isList#(V) | → | U11#(isPalListKind(V), V) | | U43#(tt, V1, V2) | → | U44#(isPalListKind(V2), V1, V2) |
| U25#(tt, V2) | → | isList#(V2) | | U45#(tt, V2) | → | isNeList#(V2) |
| U21#(tt, V1, V2) | → | U22#(isPalListKind(V1), V1, V2) | | U24#(tt, V1, V2) | → | isList#(V1) |
| U44#(tt, V1, V2) | → | U45#(isList(V1), V2) | | U42#(tt, V1, V2) | → | U43#(isPalListKind(V2), V1, V2) |
| U12#(tt, V) | → | isNeList#(V) | | isNeList#(__(V1, V2)) | → | U41#(isPalListKind(V1), V1, V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
The following SCCs where found
| U23#(tt, V1, V2) → U24#(isPalListKind(V2), V1, V2) | U25#(tt, V2) → isList#(V2) |
| isList#(__(V1, V2)) → U21#(isPalListKind(V1), V1, V2) | U21#(tt, V1, V2) → U22#(isPalListKind(V1), V1, V2) |
| U24#(tt, V1, V2) → isList#(V1) | U22#(tt, V1, V2) → U23#(isPalListKind(V2), V1, V2) |
| U24#(tt, V1, V2) → U25#(isList(V1), V2) |
| U43#(tt, V1, V2) → U44#(isPalListKind(V2), V1, V2) | U45#(tt, V2) → isNeList#(V2) |
| U44#(tt, V1, V2) → U45#(isList(V1), V2) | U42#(tt, V1, V2) → U43#(isPalListKind(V2), V1, V2) |
| U41#(tt, V1, V2) → U42#(isPalListKind(V1), V1, V2) | isNeList#(__(V1, V2)) → U41#(isPalListKind(V1), V1, V2) |
Problem 12: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U43#(tt, V1, V2) | → | U44#(isPalListKind(V2), V1, V2) | | U45#(tt, V2) | → | isNeList#(V2) |
| U44#(tt, V1, V2) | → | U45#(isList(V1), V2) | | U42#(tt, V1, V2) | → | U43#(isPalListKind(V2), V1, V2) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(V1), V1, V2) | | isNeList#(__(V1, V2)) | → | U41#(isPalListKind(V1), V1, V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U26#) = μ(U61#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U46) = μ(U74#) = μ(U45) = μ(U44) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U92) = μ(U91) = μ(U54#) = μ(U33#) = μ(U63#) = μ(U92#) = μ(U83) = μ(U24#) = μ(U53#) = μ(U82#) = μ(U55) = μ(U54) = μ(U44#) = μ(U73#) = μ(U56) = μ(U51) = μ(U53) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): y
- U12(x,y): y
- U13(x): 0
- U21(x,y,z): 3z + 2
- U22(x,y,z): 2z + 2
- U23(x,y,z): 2
- U24(x,y,z): 2
- U25(x,y): 2
- U26(x): 2
- U31(x,y): 2
- U32(x,y): x + 1
- U33(x): 1
- U41(x,y,z): 0
- U41#(x,y,z): 3z + 2
- U42(x,y,z): 0
- U42#(x,y,z): 3z + 2
- U43(x,y,z): 0
- U43#(x,y,z): 2z + x + 1
- U44(x,y,z): 0
- U44#(x,y,z): z
- U45(x,y): 0
- U45#(x,y): y
- U46(x): 0
- U51(x,y,z): 2
- U52(x,y,z): 2
- U53(x,y,z): 2
- U54(x,y,z): 2
- U55(x,y): 0
- U56(x): 0
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U82(x,y): 0
- U83(x): 0
- U91(x,y): 1
- U92(x): 0
- __(x,y): 3y + 2
- a: 3
- e: 1
- i: 3
- isList(x): x
- isNeList(x): 2
- isNeList#(x): x
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 1
- isQid(x): 1
- nil: 0
- o: 3
- tt: 0
- u: 1
Standard Usable rules
| U42(tt, V1, V2) | → | U43(isPalListKind(V2), V1, V2) | | U52(tt, V1, V2) | → | U53(isPalListKind(V2), V1, V2) |
| U54(tt, V1, V2) | → | U55(isNeList(V1), V2) | | isQid(u) | → | tt |
| U12(tt, V) | → | U13(isNeList(V)) | | U31(tt, V) | → | U32(isPalListKind(V), V) |
| isPalListKind(e) | → | tt | | U92(tt) | → | tt |
| U43(tt, V1, V2) | → | U44(isPalListKind(V2), V1, V2) | | isPalListKind(a) | → | tt |
| isList(__(V1, V2)) | → | U21(isPalListKind(V1), V1, V2) | | U32(tt, V) | → | U33(isQid(V)) |
| U33(tt) | → | tt | | U13(tt) | → | tt |
| U25(tt, V2) | → | U26(isList(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(V2), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(isPalListKind(V1), V1, V2) | | isNeList(V) | → | U31(isPalListKind(V), V) |
| U56(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(V2)) |
| isQid(o) | → | tt | | isQid(i) | → | tt |
| isQid(e) | → | tt | | U44(tt, V1, V2) | → | U45(isList(V1), V2) |
| U45(tt, V2) | → | U46(isNeList(V2)) | | U41(tt, V1, V2) | → | U42(isPalListKind(V1), V1, V2) |
| isPalListKind(nil) | → | tt | | U53(tt, V1, V2) | → | U54(isPalListKind(V2), V1, V2) |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| isList(nil) | → | tt | | U55(tt, V2) | → | U56(isList(V2)) |
| U24(tt, V1, V2) | → | U25(isList(V1), V2) | | isPalListKind(i) | → | tt |
| U23(tt, V1, V2) | → | U24(isPalListKind(V2), V1, V2) | | isPalListKind(__(V1, V2)) | → | U91(isPalListKind(V1), V2) |
| isQid(a) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(V1), V1, V2) |
| isNeList(__(V1, V2)) | → | U41(isPalListKind(V1), V1, V2) | | isList(V) | → | U11(isPalListKind(V), V) |
| U11(tt, V) | → | U12(isPalListKind(V), V) | | U26(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(V1), V1, V2) | | U46(tt) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U43#(tt, V1, V2) | → | U44#(isPalListKind(V2), V1, V2) |
Problem 14: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U45#(tt, V2) | → | isNeList#(V2) | | U44#(tt, V1, V2) | → | U45#(isList(V1), V2) |
| U42#(tt, V1, V2) | → | U43#(isPalListKind(V2), V1, V2) | | U41#(tt, V1, V2) | → | U42#(isPalListKind(V1), V1, V2) |
| isNeList#(__(V1, V2)) | → | U41#(isPalListKind(V1), V1, V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, isQid, U31, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
There are no SCCs!
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U23#(tt, V1, V2) | → | U24#(isPalListKind(V2), V1, V2) | | U25#(tt, V2) | → | isList#(V2) |
| isList#(__(V1, V2)) | → | U21#(isPalListKind(V1), V1, V2) | | U21#(tt, V1, V2) | → | U22#(isPalListKind(V1), V1, V2) |
| U24#(tt, V1, V2) | → | isList#(V1) | | U22#(tt, V1, V2) | → | U23#(isPalListKind(V2), V1, V2) |
| U24#(tt, V1, V2) | → | U25#(isList(V1), V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U26#) = μ(U61#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U46) = μ(U74#) = μ(U45) = μ(U44) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U92) = μ(U91) = μ(U54#) = μ(U33#) = μ(U63#) = μ(U92#) = μ(U83) = μ(U24#) = μ(U53#) = μ(U82#) = μ(U55) = μ(U54) = μ(U44#) = μ(U73#) = μ(U56) = μ(U51) = μ(U53) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): y + 1
- U12(x,y): y + 1
- U13(x): x
- U21(x,y,z): 2y + 2
- U21#(x,y,z): z + 2y + x + 1
- U22(x,y,z): 2y + 2x
- U22#(x,y,z): z + 2y
- U23(x,y,z): y
- U23#(x,y,z): z + 2y
- U24(x,y,z): 0
- U24#(x,y,z): z + 2y
- U25(x,y): 0
- U25#(x,y): y
- U26(x): 0
- U31(x,y): 0
- U32(x,y): 0
- U33(x): 0
- U41(x,y,z): 2z + 2
- U42(x,y,z): z
- U43(x,y,z): 0
- U44(x,y,z): 0
- U45(x,y): 0
- U46(x): 0
- U51(x,y,z): 2y + 3
- U52(x,y,z): 3
- U53(x,y,z): 2x + 1
- U54(x,y,z): 1
- U55(x,y): 0
- U56(x): 0
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U82(x,y): 0
- U83(x): 0
- U91(x,y): x
- U92(x): 0
- __(x,y): 2y + 2x + 2
- a: 3
- e: 3
- i: 3
- isList(x): x + 1
- isList#(x): x
- isNeList(x): x + 1
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 1
- isQid(x): 0
- nil: 1
- o: 0
- tt: 0
- u: 3
Standard Usable rules
| U42(tt, V1, V2) | → | U43(isPalListKind(V2), V1, V2) | | U52(tt, V1, V2) | → | U53(isPalListKind(V2), V1, V2) |
| U54(tt, V1, V2) | → | U55(isNeList(V1), V2) | | isQid(u) | → | tt |
| U12(tt, V) | → | U13(isNeList(V)) | | U31(tt, V) | → | U32(isPalListKind(V), V) |
| isPalListKind(e) | → | tt | | U92(tt) | → | tt |
| U43(tt, V1, V2) | → | U44(isPalListKind(V2), V1, V2) | | isPalListKind(a) | → | tt |
| isList(__(V1, V2)) | → | U21(isPalListKind(V1), V1, V2) | | U32(tt, V) | → | U33(isQid(V)) |
| U33(tt) | → | tt | | U13(tt) | → | tt |
| U25(tt, V2) | → | U26(isList(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(V2), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(isPalListKind(V1), V1, V2) | | isNeList(V) | → | U31(isPalListKind(V), V) |
| U56(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(V2)) |
| isQid(o) | → | tt | | isQid(i) | → | tt |
| isQid(e) | → | tt | | U44(tt, V1, V2) | → | U45(isList(V1), V2) |
| U45(tt, V2) | → | U46(isNeList(V2)) | | U41(tt, V1, V2) | → | U42(isPalListKind(V1), V1, V2) |
| isPalListKind(nil) | → | tt | | U53(tt, V1, V2) | → | U54(isPalListKind(V2), V1, V2) |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| isList(nil) | → | tt | | U55(tt, V2) | → | U56(isList(V2)) |
| U24(tt, V1, V2) | → | U25(isList(V1), V2) | | isPalListKind(i) | → | tt |
| U23(tt, V1, V2) | → | U24(isPalListKind(V2), V1, V2) | | isPalListKind(__(V1, V2)) | → | U91(isPalListKind(V1), V2) |
| isQid(a) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(V1), V1, V2) |
| isNeList(__(V1, V2)) | → | U41(isPalListKind(V1), V1, V2) | | isList(V) | → | U11(isPalListKind(V), V) |
| U11(tt, V) | → | U12(isPalListKind(V), V) | | U26(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(V1), V1, V2) | | U46(tt) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U21#(tt, V1, V2) | → | U22#(isPalListKind(V1), V1, V2) |
Problem 15: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(__(V1, V2)) | → | U21#(isPalListKind(V1), V1, V2) | | U25#(tt, V2) | → | isList#(V2) |
| U23#(tt, V1, V2) | → | U24#(isPalListKind(V2), V1, V2) | | U24#(tt, V1, V2) | → | isList#(V1) |
| U22#(tt, V1, V2) | → | U23#(isPalListKind(V2), V1, V2) | | U24#(tt, V1, V2) | → | U25#(isList(V1), V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, isQid, U31, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
There are no SCCs!
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNePal#(__(I, __(P, I))) | → | U71#(isQid(I), I, P) | | U82#(tt, V) | → | isNePal#(V) |
| U72#(tt, P) | → | isPal#(P) | | U81#(tt, V) | → | U82#(isPalListKind(V), V) |
| isPal#(V) | → | U81#(isPalListKind(V), V) | | U71#(tt, I, P) | → | U72#(isPalListKind(I), P) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U26#) = μ(U61#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U46) = μ(U74#) = μ(U45) = μ(U44) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U92) = μ(U91) = μ(U54#) = μ(U33#) = μ(U63#) = μ(U92#) = μ(U83) = μ(U24#) = μ(U53#) = μ(U82#) = μ(U55) = μ(U54) = μ(U44#) = μ(U73#) = μ(U56) = μ(U51) = μ(U53) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U12(x,y): 0
- U13(x): 0
- U21(x,y,z): 0
- U22(x,y,z): 0
- U23(x,y,z): 0
- U24(x,y,z): 0
- U25(x,y): 0
- U26(x): 0
- U31(x,y): 0
- U32(x,y): 0
- U33(x): 0
- U41(x,y,z): 0
- U42(x,y,z): 0
- U43(x,y,z): 0
- U44(x,y,z): 0
- U45(x,y): 0
- U46(x): 0
- U51(x,y,z): 0
- U52(x,y,z): 0
- U53(x,y,z): 0
- U54(x,y,z): 0
- U55(x,y): 0
- U56(x): 0
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U71#(x,y,z): z + x + 1
- U72(x,y): 0
- U72#(x,y): y
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U81#(x,y): y
- U82(x,y): 0
- U82#(x,y): y
- U83(x): 0
- U91(x,y): y + 1
- U92(x): 1
- __(x,y): 2y + 2x + 1
- a: 2
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isNePal#(x): x
- isPal(x): 0
- isPal#(x): x
- isPalListKind(x): x
- isQid(x): 2
- nil: 2
- o: 0
- tt: 0
- u: 3
Standard Usable rules
| isQid(i) | → | tt | | isQid(e) | → | tt |
| isQid(u) | → | tt | | isPalListKind(nil) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| U92(tt) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(__(V1, V2)) | → | U91(isPalListKind(V1), V2) | | isQid(a) | → | tt |
| U91(tt, V2) | → | U92(isPalListKind(V2)) | | isQid(o) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U71#(tt, I, P) | → | U72#(isPalListKind(I), P) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNePal#(__(I, __(P, I))) | → | U71#(isQid(I), I, P) | | U82#(tt, V) | → | isNePal#(V) |
| U72#(tt, P) | → | isPal#(P) | | U81#(tt, V) | → | U82#(isPalListKind(V), V) |
| isPal#(V) | → | U81#(isPalListKind(V), V) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, isQid, U31, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
There are no SCCs!
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U91#(tt, V2) | → | isPalListKind#(V2) | | isPalListKind#(__(V1, V2)) | → | isPalListKind#(V1) |
| isPalListKind#(__(V1, V2)) | → | U91#(isPalListKind(V1), V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, U31, isQid, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U26#) = μ(U61#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U46) = μ(U74#) = μ(U45) = μ(U44) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U92) = μ(U91) = μ(U54#) = μ(U33#) = μ(U63#) = μ(U92#) = μ(U83) = μ(U24#) = μ(U53#) = μ(U82#) = μ(U55) = μ(U54) = μ(U44#) = μ(U73#) = μ(U56) = μ(U51) = μ(U53) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U12(x,y): 0
- U13(x): 0
- U21(x,y,z): 0
- U22(x,y,z): 0
- U23(x,y,z): 0
- U24(x,y,z): 0
- U25(x,y): 0
- U26(x): 0
- U31(x,y): 0
- U32(x,y): 0
- U33(x): 0
- U41(x,y,z): 0
- U42(x,y,z): 0
- U43(x,y,z): 0
- U44(x,y,z): 0
- U45(x,y): 0
- U46(x): 0
- U51(x,y,z): 0
- U52(x,y,z): 0
- U53(x,y,z): 0
- U54(x,y,z): 0
- U55(x,y): 0
- U56(x): 0
- U61(x,y): 0
- U62(x,y): 0
- U63(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U82(x,y): 0
- U83(x): 0
- U91(x,y): 0
- U91#(x,y): y
- U92(x): 0
- __(x,y): y + 2x + 3
- a: 3
- e: 3
- i: 3
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 0
- isPalListKind#(x): x
- isQid(x): 0
- nil: 3
- o: 3
- tt: 0
- u: 3
Standard Usable rules
| U92(tt) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(a) | → | tt | | isPalListKind(__(V1, V2)) | → | U91(isPalListKind(V1), V2) |
| isPalListKind(nil) | → | tt | | isPalListKind(u) | → | tt |
| isPalListKind(o) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(V2)) |
| isPalListKind(e) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isPalListKind#(__(V1, V2)) | → | isPalListKind#(V1) | | isPalListKind#(__(V1, V2)) | → | U91#(isPalListKind(V1), V2) |
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U91#(tt, V2) | → | isPalListKind#(V2) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: U63, U25, U62, U26, U61, U23, U24, U21, U22, isPal, U71, U73, U72, U74, isQid, U31, U32, U33, isList, isNeList, __, U46, U45, U44, U43, U42, U41, U92, isNePal, U91, e, isPalListKind, a, U83, o, i, U55, U54, u, U56, U51, tt, U53, U82, U52, U81, U11, U12, U13, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U56#) = μ(U25#) = μ(U52#) = μ(U63) = μ(U41#) = μ(U25) = μ(U62) = μ(U26) = μ(U61) = μ(U45#) = μ(U72#) = μ(U23) = μ(U24) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U26#) = μ(U55#) = μ(U51#) = μ(U71) = μ(U73) = μ(U42#) = μ(U72) = μ(U71#) = μ(U74) = μ(U46#) = μ(U32#) = μ(U31) = μ(U32) = μ(U33) = μ(U13#) = μ(U91#) = μ(U81#) = μ(U23#) = μ(U74#) = μ(U46) = μ(U45) = μ(U43#) = μ(U44) = μ(U43) = μ(U42) = μ(U92) = μ(U41) = μ(U54#) = μ(U91) = μ(U33#) = μ(U92#) = μ(U63#) = μ(U83) = μ(U82#) = μ(U53#) = μ(U24#) = μ(U55) = μ(U73#) = μ(U44#) = μ(U54) = μ(U56) = μ(U51) = μ(U82) = μ(U53) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(U13) = μ(U83#) = {1}
μ(__#) = μ(__) = {1, 2}
There are no SCCs!