YES
The TRS could be proven terminating. The proof took 23535 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (3141ms).
| – Problem 2 was processed with processor SubtermCriterion (3ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (1362ms).
| | – Problem 7 was processed with processor DependencyGraph (0ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4 (166ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (1202ms).
| | – Problem 9 was processed with processor DependencyGraph (86ms).
| – Problem 5 was processed with processor SubtermCriterion (3ms).
| – Problem 6 was processed with processor PolynomialLinearRange4 (160ms).
| | – Problem 10 was processed with processor DependencyGraph (26ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U62#(tt, V) | → | U63#(isQid(activate(V))) | | U53#(tt, V1, V2) | → | isPalListKind#(activate(V2)) |
| U52#(tt, V1, V2) | → | U53#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | activate#(n____(X1, X2)) | → | activate#(X2) |
| U53#(tt, V1, V2) | → | activate#(V2) | | U23#(tt, V1, V2) | → | activate#(V2) |
| U55#(tt, V2) | → | activate#(V2) | | U45#(tt, V2) | → | isNeList#(activate(V2)) |
| U24#(tt, V1, V2) | → | U25#(isList(activate(V1)), activate(V2)) | | U23#(tt, V1, V2) | → | U24#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| isNePal#(n____(I, n____(P, I))) | → | U71#(isQid(activate(I)), activate(I), activate(P)) | | U81#(tt, V) | → | isPalListKind#(activate(V)) |
| U24#(tt, V1, V2) | → | activate#(V2) | | U91#(tt, V2) | → | U92#(isPalListKind(activate(V2))) |
| U12#(tt, V) | → | isNeList#(activate(V)) | | U72#(tt, P) | → | U73#(isPal(activate(P)), activate(P)) |
| U24#(tt, V1, V2) | → | activate#(V1) | | isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) |
| U42#(tt, V1, V2) | → | U43#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U54#(tt, V1, V2) | → | U55#(isNeList(activate(V1)), activate(V2)) |
| isNeList#(V) | → | U31#(isPalListKind(activate(V)), activate(V)) | | U71#(tt, I, P) | → | isPalListKind#(activate(I)) |
| U71#(tt, I, P) | → | activate#(P) | | U61#(tt, V) | → | U62#(isPalListKind(activate(V)), activate(V)) |
| isList#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) | | U22#(tt, V1, V2) | → | U23#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| isNePal#(V) | → | isPalListKind#(activate(V)) | | U71#(tt, I, P) | → | U72#(isPalListKind(activate(I)), activate(P)) |
| U25#(tt, V2) | → | activate#(V2) | | U32#(tt, V) | → | U33#(isQid(activate(V))) |
| U12#(tt, V) | → | U13#(isNeList(activate(V))) | | isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
| isPal#(V) | → | isPalListKind#(activate(V)) | | isPal#(V) | → | activate#(V) |
| U91#(tt, V2) | → | activate#(V2) | | U31#(tt, V) | → | U32#(isPalListKind(activate(V)), activate(V)) |
| U23#(tt, V1, V2) | → | isPalListKind#(activate(V2)) | | U11#(tt, V) | → | U12#(isPalListKind(activate(V)), activate(V)) |
| U61#(tt, V) | → | isPalListKind#(activate(V)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
| isNePal#(V) | → | activate#(V) | | U25#(tt, V2) | → | U26#(isList(activate(V2))) |
| U71#(tt, I, P) | → | activate#(I) | | U51#(tt, V1, V2) | → | U52#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U22#(tt, V1, V2) | → | activate#(V2) | | isList#(n____(V1, V2)) | → | activate#(V1) |
| U62#(tt, V) | → | isQid#(activate(V)) | | isNeList#(V) | → | activate#(V) |
| U31#(tt, V) | → | activate#(V) | | U82#(tt, V) | → | activate#(V) |
| U12#(tt, V) | → | activate#(V) | | U31#(tt, V) | → | isPalListKind#(activate(V)) |
| U73#(tt, P) | → | isPalListKind#(activate(P)) | | __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
| U32#(tt, V) | → | activate#(V) | | U41#(tt, V1, V2) | → | activate#(V2) |
| U52#(tt, V1, V2) | → | activate#(V2) | | U55#(tt, V2) | → | U56#(isList(activate(V2))) |
| U72#(tt, P) | → | isPal#(activate(P)) | | U43#(tt, V1, V2) | → | activate#(V2) |
| isPalListKind#(n____(V1, V2)) | → | activate#(V2) | | U25#(tt, V2) | → | isList#(activate(V2)) |
| U21#(tt, V1, V2) | → | isPalListKind#(activate(V1)) | | U41#(tt, V1, V2) | → | isPalListKind#(activate(V1)) |
| U82#(tt, V) | → | U83#(isNePal(activate(V))) | | isNeList#(n____(V1, V2)) | → | U51#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U44#(tt, V1, V2) | → | activate#(V2) | | U21#(tt, V1, V2) | → | U22#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U43#(tt, V1, V2) | → | U44#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | isList#(V) | → | activate#(V) |
| isList#(V) | → | isPalListKind#(activate(V)) | | U22#(tt, V1, V2) | → | isPalListKind#(activate(V2)) |
| U51#(tt, V1, V2) | → | activate#(V1) | | activate#(n__o) | → | o# |
| isNePal#(n____(I, n____(P, I))) | → | activate#(I) | | isPal#(V) | → | U81#(isPalListKind(activate(V)), activate(V)) |
| U43#(tt, V1, V2) | → | isPalListKind#(activate(V2)) | | U45#(tt, V2) | → | activate#(V2) |
| U81#(tt, V) | → | U82#(isPalListKind(activate(V)), activate(V)) | | activate#(n__a) | → | a# |
| isNePal#(n____(I, n____(P, I))) | → | isQid#(activate(I)) | | U44#(tt, V1, V2) | → | activate#(V1) |
| U22#(tt, V1, V2) | → | activate#(V1) | | U53#(tt, V1, V2) | → | activate#(V1) |
| isNeList#(n____(V1, V2)) | → | activate#(V1) | | U21#(tt, V1, V2) | → | activate#(V1) |
| U11#(tt, V) | → | activate#(V) | | U62#(tt, V) | → | activate#(V) |
| isNeList#(V) | → | isPalListKind#(activate(V)) | | isNePal#(V) | → | U61#(isPalListKind(activate(V)), activate(V)) |
| U42#(tt, V1, V2) | → | activate#(V1) | | isPalListKind#(n____(V1, V2)) | → | U91#(isPalListKind(activate(V1)), activate(V2)) |
| U52#(tt, V1, V2) | → | activate#(V1) | | U54#(tt, V1, V2) | → | activate#(V1) |
| U73#(tt, P) | → | U74#(isPalListKind(activate(P))) | | U72#(tt, P) | → | activate#(P) |
| U41#(tt, V1, V2) | → | activate#(V1) | | activate#(n__u) | → | u# |
| U21#(tt, V1, V2) | → | activate#(V2) | | isNeList#(n____(V1, V2)) | → | U41#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42#(tt, V1, V2) | → | activate#(V2) | | isNeList#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
| activate#(n__e) | → | e# | | U54#(tt, V1, V2) | → | isNeList#(activate(V1)) |
| U32#(tt, V) | → | isQid#(activate(V)) | | isNeList#(n____(V1, V2)) | → | activate#(V2) |
| activate#(n__i) | → | i# | | U45#(tt, V2) | → | U46#(isNeList(activate(V2))) |
| U81#(tt, V) | → | activate#(V) | | U24#(tt, V1, V2) | → | isList#(activate(V1)) |
| U23#(tt, V1, V2) | → | activate#(V1) | | isNePal#(n____(I, n____(P, I))) | → | activate#(P) |
| U51#(tt, V1, V2) | → | activate#(V2) | | U53#(tt, V1, V2) | → | U54#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54#(tt, V1, V2) | → | activate#(V2) | | activate#(n____(X1, X2)) | → | __#(activate(X1), activate(X2)) |
| isList#(n____(V1, V2)) | → | activate#(V2) | | isList#(n____(V1, V2)) | → | U21#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| activate#(n____(X1, X2)) | → | activate#(X1) | | isPalListKind#(n____(V1, V2)) | → | activate#(V1) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U82#(tt, V) | → | isNePal#(activate(V)) |
| U52#(tt, V1, V2) | → | isPalListKind#(activate(V2)) | | U51#(tt, V1, V2) | → | isPalListKind#(activate(V1)) |
| U11#(tt, V) | → | isPalListKind#(activate(V)) | | U43#(tt, V1, V2) | → | activate#(V1) |
| U44#(tt, V1, V2) | → | isList#(activate(V1)) | | U61#(tt, V) | → | activate#(V) |
| activate#(n__nil) | → | nil# | | U42#(tt, V1, V2) | → | isPalListKind#(activate(V2)) |
| U55#(tt, V2) | → | isList#(activate(V2)) | | U91#(tt, V2) | → | isPalListKind#(activate(V2)) |
| U44#(tt, V1, V2) | → | U45#(isList(activate(V1)), activate(V2)) | | U73#(tt, P) | → | activate#(P) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, U82, U53, U81, U52, U11, U12, U13, n____, nil
Strategy
The following SCCs where found
| activate#(n____(X1, X2)) → activate#(X1) | activate#(n____(X1, X2)) → activate#(X2) |
| U71#(tt, I, P) → U72#(isPalListKind(activate(I)), activate(P)) | isNePal#(n____(I, n____(P, I))) → U71#(isQid(activate(I)), activate(I), activate(P)) |
| U82#(tt, V) → isNePal#(activate(V)) | isPal#(V) → U81#(isPalListKind(activate(V)), activate(V)) |
| U72#(tt, P) → isPal#(activate(P)) | U81#(tt, V) → U82#(isPalListKind(activate(V)), activate(V)) |
| U24#(tt, V1, V2) → isList#(activate(V1)) | U11#(tt, V) → U12#(isPalListKind(activate(V)), activate(V)) |
| U52#(tt, V1, V2) → U53#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | U22#(tt, V1, V2) → U23#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U53#(tt, V1, V2) → U54#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | U45#(tt, V2) → isNeList#(activate(V2)) |
| U24#(tt, V1, V2) → U25#(isList(activate(V1)), activate(V2)) | U51#(tt, V1, V2) → U52#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U44#(tt, V1, V2) → isList#(activate(V1)) | U23#(tt, V1, V2) → U24#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| isNeList#(n____(V1, V2)) → U41#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | U25#(tt, V2) → isList#(activate(V2)) |
| U55#(tt, V2) → isList#(activate(V2)) | isList#(n____(V1, V2)) → U21#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U12#(tt, V) → isNeList#(activate(V)) | U44#(tt, V1, V2) → U45#(isList(activate(V1)), activate(V2)) |
| U54#(tt, V1, V2) → isNeList#(activate(V1)) | isList#(V) → U11#(isPalListKind(activate(V)), activate(V)) |
| isNeList#(n____(V1, V2)) → U51#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | U21#(tt, V1, V2) → U22#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U41#(tt, V1, V2) → U42#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | U42#(tt, V1, V2) → U43#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54#(tt, V1, V2) → U55#(isNeList(activate(V1)), activate(V2)) | U43#(tt, V1, V2) → U44#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
| U91#(tt, V2) → isPalListKind#(activate(V2)) | isPalListKind#(n____(V1, V2)) → isPalListKind#(activate(V1)) |
| isPalListKind#(n____(V1, V2)) → U91#(isPalListKind(activate(V1)), activate(V2)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| activate#(n____(X1, X2)) | → | activate#(X1) | | activate#(n____(X1, X2)) | → | activate#(X2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, U82, U53, U81, U52, U11, U12, U13, n____, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| activate#(n____(X1, X2)) | → | activate#(X1) | | activate#(n____(X1, X2)) | → | activate#(X2) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| U91#(tt, V2) | → | isPalListKind#(activate(V2)) | | isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
| isPalListKind#(n____(V1, V2)) | → | U91#(isPalListKind(activate(V1)), activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, U82, U53, U81, U52, U11, U12, U13, n____, nil
Strategy
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): y + 2x
- U91#(x,y): 2y + 2x
- U92(x): 1
- __(x,y): y + 3x
- a: 1
- activate(x): x
- e: 1
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 2x
- isPalListKind#(x): 2x
- isQid(x): 0
- n____(x,y): y + 3x
- n__a: 1
- n__e: 1
- n__i: 1
- n__nil: 1
- n__o: 1
- n__u: 1
- nil: 1
- o: 1
- tt: 1
- u: 1
Improved Usable rules
| isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) | | isPalListKind(n__i) | → | tt |
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| a | → | n__a | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) | | isPalListKind(n__nil) | → | tt |
| U92(tt) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| activate(n__a) | → | a | | e | → | n__e |
| activate(n__i) | → | i | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | u | → | n__u |
| i | → | n__i | | activate(n__o) | → | o |
| o | → | n__o | | nil | → | n__nil |
| activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U91#(tt, V2) | → | isPalListKind#(activate(V2)) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) | | isPalListKind#(n____(V1, V2)) | → | U91#(isPalListKind(activate(V1)), activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, n____, nil
Strategy
The following SCCs where found
| isPalListKind#(n____(V1, V2)) → isPalListKind#(activate(V1)) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, n____, nil
Strategy
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
- a: 1
- activate(x): x
- e: 1
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 0
- isPalListKind#(x): x
- isQid(x): 0
- n____(x,y): y + x + 1
- n__a: 1
- n__e: 1
- n__i: 1
- n__nil: 0
- n__o: 1
- n__u: 1
- nil: 0
- o: 1
- tt: 0
- u: 1
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | e | → | n__e |
| __(X, nil) | → | X | | activate(n__i) | → | i |
| a | → | n__a | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) | | activate(X) | → | X |
| activate(n__u) | → | u | | __(nil, X) | → | X |
| i | → | n__i | | u | → | n__u |
| __(X1, X2) | → | n____(X1, X2) | | activate(n__o) | → | o |
| nil | → | n__nil | | o | → | n__o |
| activate(n__a) | → | a | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U24#(tt, V1, V2) | → | isList#(activate(V1)) | | U52#(tt, V1, V2) | → | U53#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U11#(tt, V) | → | U12#(isPalListKind(activate(V)), activate(V)) | | U22#(tt, V1, V2) | → | U23#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U53#(tt, V1, V2) | → | U54#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U45#(tt, V2) | → | isNeList#(activate(V2)) |
| U51#(tt, V1, V2) | → | U52#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U24#(tt, V1, V2) | → | U25#(isList(activate(V1)), activate(V2)) |
| U44#(tt, V1, V2) | → | isList#(activate(V1)) | | U23#(tt, V1, V2) | → | U24#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | U41#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U25#(tt, V2) | → | isList#(activate(V2)) |
| U55#(tt, V2) | → | isList#(activate(V2)) | | isList#(n____(V1, V2)) | → | U21#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U44#(tt, V1, V2) | → | U45#(isList(activate(V1)), activate(V2)) | | U12#(tt, V) | → | isNeList#(activate(V)) |
| U54#(tt, V1, V2) | → | isNeList#(activate(V1)) | | isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) |
| isNeList#(n____(V1, V2)) | → | U51#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U21#(tt, V1, V2) | → | U22#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U41#(tt, V1, V2) | → | U42#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U54#(tt, V1, V2) | → | U55#(isNeList(activate(V1)), activate(V2)) |
| U42#(tt, V1, V2) | → | U43#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43#(tt, V1, V2) | → | U44#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, U82, U53, U81, U52, U11, U12, U13, n____, nil
Strategy
Polynomial Interpretation
- U11(x,y): y
- U11#(x,y): 2y
- U12(x,y): y
- U12#(x,y): 2y
- U13(x): 0
- U21(x,y,z): y
- U21#(x,y,z): 2z + 2y
- U22(x,y,z): y
- 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 + 2x
- U26(x): 0
- U31(x,y): 0
- U32(x,y): 0
- U33(x): 0
- U41(x,y,z): 0
- U41#(x,y,z): 2z + 2y
- U42(x,y,z): 0
- U42#(x,y,z): 2z + 2y
- U43(x,y,z): 0
- U43#(x,y,z): 2z + 2y
- U44(x,y,z): 0
- U44#(x,y,z): 2z + 2y
- U45(x,y): 0
- U45#(x,y): 2y
- U46(x): 0
- U51(x,y,z): 0
- U51#(x,y,z): 2z + 2y + 2
- U52(x,y,z): 0
- U52#(x,y,z): 2z + 2y
- U53(x,y,z): 0
- U53#(x,y,z): 2z + 2y
- 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): y + x + 1
- a: 2
- activate(x): x
- e: 0
- i: 0
- isList(x): x
- isList#(x): 2x
- isNeList(x): 0
- isNeList#(x): 2x
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 0
- isQid(x): x
- n____(x,y): y + x + 1
- n__a: 2
- n__e: 0
- n__i: 0
- n__nil: 2
- n__o: 0
- n__u: 2
- nil: 2
- o: 0
- tt: 0
- u: 2
Standard Usable rules
| isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U92(tt) | → | tt | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U13(tt) | → | tt | | U12(tt, V) | → | U13(isNeList(activate(V))) |
| U56(tt) | → | tt | | activate(n__a) | → | a |
| U32(tt, V) | → | U33(isQid(activate(V))) | | activate(n__i) | → | i |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | isQid(n__i) | → | tt |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| activate(X) | → | X | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| __(nil, X) | → | X | | u | → | n__u |
| i | → | n__i | | o | → | n__o |
| nil | → | n__nil | | isQid(n__o) | → | tt |
| U46(tt) | → | tt | | __(__(X, Y), Z) | → | __(X, __(Y, Z)) |
| isPalListKind(n__i) | → | tt | | __(X, nil) | → | X |
| a | → | n__a | | isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| isPalListKind(n__nil) | → | tt | | U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) | | U33(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isQid(n__u) | → | tt |
| isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isQid(n__e) | → | tt |
| __(X1, X2) | → | n____(X1, X2) | | U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| e | → | n__e | | U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| isPalListKind(n__o) | → | tt | | isList(n__nil) | → | tt |
| isQid(n__a) | → | tt | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isPalListKind(n__u) | → | tt |
| U55(tt, V2) | → | U56(isList(activate(V2))) | | isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| activate(n__u) | → | u | | U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) |
| activate(n__o) | → | o | | U26(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U51#(tt, V1, V2) | → | U52#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isList#(n____(V1, V2)) | → | U21#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | U41#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U24#(tt, V1, V2) | → | isList#(activate(V1)) | | U52#(tt, V1, V2) | → | U53#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U11#(tt, V) | → | U12#(isPalListKind(activate(V)), activate(V)) | | U22#(tt, V1, V2) | → | U23#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U53#(tt, V1, V2) | → | U54#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U45#(tt, V2) | → | isNeList#(activate(V2)) |
| U24#(tt, V1, V2) | → | U25#(isList(activate(V1)), activate(V2)) | | U44#(tt, V1, V2) | → | isList#(activate(V1)) |
| U23#(tt, V1, V2) | → | U24#(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U25#(tt, V2) | → | isList#(activate(V2)) |
| U55#(tt, V2) | → | isList#(activate(V2)) | | U44#(tt, V1, V2) | → | U45#(isList(activate(V1)), activate(V2)) |
| U12#(tt, V) | → | isNeList#(activate(V)) | | isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) |
| U54#(tt, V1, V2) | → | isNeList#(activate(V1)) | | U21#(tt, V1, V2) | → | U22#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | U51#(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U42#(tt, V1, V2) | → | U43#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54#(tt, V1, V2) | → | U55#(isNeList(activate(V1)), activate(V2)) | | U41#(tt, V1, V2) | → | U42#(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U43#(tt, V1, V2) | → | U44#(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, n____, nil
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
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(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, U82, U53, U81, U52, U11, U12, U13, n____, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U71#(tt, I, P) | → | U72#(isPalListKind(activate(I)), activate(P)) | | isNePal#(n____(I, n____(P, I))) | → | U71#(isQid(activate(I)), activate(I), activate(P)) |
| U82#(tt, V) | → | isNePal#(activate(V)) | | isPal#(V) | → | U81#(isPalListKind(activate(V)), activate(V)) |
| U72#(tt, P) | → | isPal#(activate(P)) | | U81#(tt, V) | → | U82#(isPalListKind(activate(V)), activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, U82, U53, U81, U52, U11, U12, U13, n____, nil
Strategy
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): 2z + 2y + 2
- U72(x,y): 0
- U72#(x,y): 2y + x + 2
- U73(x,y): 0
- U74(x): 0
- U81(x,y): 0
- U81#(x,y): 2y + 2
- U82(x,y): 0
- U82#(x,y): y + 2
- U83(x): 0
- U91(x,y): y + 2x
- U92(x): 1
- __(x,y): y + 2x
- a: 1
- activate(x): x
- e: 1
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isNePal#(x): x + 2
- isPal(x): 0
- isPal#(x): 2x + 2
- isPalListKind(x): 2x
- isQid(x): 2x
- n____(x,y): y + 2x
- n__a: 1
- n__e: 1
- n__i: 1
- n__nil: 1
- n__o: 1
- n__u: 1
- nil: 1
- o: 1
- tt: 1
- u: 1
Standard Usable rules
| isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) | | isPalListKind(n__i) | → | tt |
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| a | → | n__a | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) | | isPalListKind(n__nil) | → | tt |
| U92(tt) | → | tt | | isQid(n__u) | → | tt |
| isPalListKind(n__a) | → | tt | | isQid(n__e) | → | tt |
| isPalListKind(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| activate(n__a) | → | a | | e | → | n__e |
| activate(n__i) | → | i | | isPalListKind(n__o) | → | tt |
| isQid(n__a) | → | tt | | isPalListKind(n__u) | → | tt |
| isQid(n__i) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| nil | → | n__nil | | o | → | n__o |
| isQid(n__o) | → | tt | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U72#(tt, P) | → | isPal#(activate(P)) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNePal#(n____(I, n____(P, I))) | → | U71#(isQid(activate(I)), activate(I), activate(P)) | | U71#(tt, I, P) | → | U72#(isPalListKind(activate(I)), activate(P)) |
| U82#(tt, V) | → | isNePal#(activate(V)) | | isPal#(V) | → | U81#(isPalListKind(activate(V)), activate(V)) |
| U81#(tt, V) | → | U82#(isPalListKind(activate(V)), activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isPalListKind(activate(V)), activate(V)) |
| U12(tt, V) | → | U13(isNeList(activate(V))) | | U13(tt) | → | tt |
| U21(tt, V1, V2) | → | U22(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | U22(tt, V1, V2) | → | U23(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U23(tt, V1, V2) | → | U24(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U24(tt, V1, V2) | → | U25(isList(activate(V1)), activate(V2)) |
| U25(tt, V2) | → | U26(isList(activate(V2))) | | U26(tt) | → | tt |
| U31(tt, V) | → | U32(isPalListKind(activate(V)), activate(V)) | | U32(tt, V) | → | U33(isQid(activate(V))) |
| U33(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U42(tt, V1, V2) | → | U43(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U43(tt, V1, V2) | → | U44(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U44(tt, V1, V2) | → | U45(isList(activate(V1)), activate(V2)) | | U45(tt, V2) | → | U46(isNeList(activate(V2))) |
| U46(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| U52(tt, V1, V2) | → | U53(isPalListKind(activate(V2)), activate(V1), activate(V2)) | | U53(tt, V1, V2) | → | U54(isPalListKind(activate(V2)), activate(V1), activate(V2)) |
| U54(tt, V1, V2) | → | U55(isNeList(activate(V1)), activate(V2)) | | U55(tt, V2) | → | U56(isList(activate(V2))) |
| U56(tt) | → | tt | | U61(tt, V) | → | U62(isPalListKind(activate(V)), activate(V)) |
| U62(tt, V) | → | U63(isQid(activate(V))) | | U63(tt) | → | tt |
| U71(tt, I, P) | → | U72(isPalListKind(activate(I)), activate(P)) | | U72(tt, P) | → | U73(isPal(activate(P)), activate(P)) |
| U73(tt, P) | → | U74(isPalListKind(activate(P))) | | U74(tt) | → | tt |
| U81(tt, V) | → | U82(isPalListKind(activate(V)), activate(V)) | | U82(tt, V) | → | U83(isNePal(activate(V))) |
| U83(tt) | → | tt | | U91(tt, V2) | → | U92(isPalListKind(activate(V2))) |
| U92(tt) | → | tt | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(isPalListKind(activate(V1)), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isPalListKind(activate(V1)), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, n____(P, I))) | → | U71(isQid(activate(I)), activate(I), activate(P)) | | isPal(V) | → | U81(isPalListKind(activate(V)), activate(V)) |
| isPal(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | isPalListKind(n__i) | → | tt |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__o) | → | tt |
| isPalListKind(n__u) | → | tt | | isPalListKind(n____(V1, V2)) | → | U91(isPalListKind(activate(V1)), activate(V2)) |
| isQid(n__a) | → | tt | | isQid(n__e) | → | tt |
| isQid(n__i) | → | tt | | isQid(n__o) | → | tt |
| isQid(n__u) | → | tt | | nil | → | n__nil |
| __(X1, X2) | → | n____(X1, X2) | | a | → | n__a |
| e | → | n__e | | i | → | n__i |
| o | → | n__o | | u | → | n__u |
| activate(n__nil) | → | nil | | activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) |
| activate(n__a) | → | a | | activate(n__e) | → | e |
| activate(n__i) | → | i | | activate(n__o) | → | o |
| activate(n__u) | → | u | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: activate, U63, n__u, U25, U62, U26, U61, n__o, n__nil, U23, U24, U21, U22, n__e, n__a, isPal, n__i, 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, n____, nil
Strategy
There are no SCCs!