YES
The TRS could be proven terminating. The proof took 16475 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1128ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (531ms).
| | – Problem 6 was processed with processor DependencyGraph (19ms).
| | | – Problem 9 was processed with processor PolynomialLinearRange4 (329ms).
| | | | – Problem 11 was processed with processor DependencyGraph (5ms).
| | | | | – Problem 13 was processed with processor PolynomialLinearRange4 (265ms).
| | | | | | – Problem 15 was processed with processor DependencyGraph (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (89ms).
| | – Problem 7 was processed with processor DependencyGraph (1ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| – Problem 5 was processed with processor PolynomialLinearRange4 (194ms).
| | – Problem 8 was processed with processor DependencyGraph (4ms).
| | | – Problem 10 was processed with processor PolynomialLinearRange4 (56ms).
| | | | – Problem 12 was processed with processor DependencyGraph (25ms).
| | | | | – Problem 14 was processed with processor PolynomialLinearRange4 (50ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__isPalListKind(X)) | → | isPalListKind#(X) | | U51#(tt, V1, V2) | → | U52#(isNeList(activate(V1)), activate(V2)) |
| and#(tt, X) | → | activate#(X) | | isNeList#(n____(V1, V2)) | → | U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isList#(V) | → | isPalListKind#(activate(V)) | | U51#(tt, V1, V2) | → | activate#(V1) |
| activate#(n__o) | → | o# | | U21#(tt, V1, V2) | → | U22#(isList(activate(V1)), activate(V2)) |
| activate#(n__a) | → | a# | | isNePal#(n____(I, __(P, I))) | → | and#(isQid(activate(I)), n__isPalListKind(activate(I))) |
| isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) | | isNeList#(n____(V1, V2)) | → | and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) |
| isNeList#(n____(V1, V2)) | → | activate#(V1) | | isNeList#(V) | → | U31#(isPalListKind(activate(V)), activate(V)) |
| U71#(tt, V) | → | U72#(isNePal(activate(V))) | | U21#(tt, V1, V2) | → | activate#(V1) |
| U11#(tt, V) | → | activate#(V) | | isNeList#(V) | → | isPalListKind#(activate(V)) |
| U52#(tt, V2) | → | U53#(isList(activate(V2))) | | U31#(tt, V) | → | U32#(isQid(activate(V))) |
| isPalListKind#(n____(V1, V2)) | → | and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) | | isList#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
| U52#(tt, V2) | → | activate#(V2) | | isNePal#(V) | → | U61#(isPalListKind(activate(V)), activate(V)) |
| isNePal#(n____(I, __(P, I))) | → | activate#(P) | | isNePal#(V) | → | isPalListKind#(activate(V)) |
| activate#(n__u) | → | u# | | U41#(tt, V1, V2) | → | activate#(V1) |
| activate#(n____(X1, X2)) | → | __#(X1, X2) | | U21#(tt, V1, V2) | → | activate#(V2) |
| U21#(tt, V1, V2) | → | isList#(activate(V1)) | | isNeList#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
| isNeList#(n____(V1, V2)) | → | U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | activate#(n__e) | → | e# |
| isNePal#(n____(I, __(P, I))) | → | activate#(I) | | U42#(tt, V2) | → | U43#(isNeList(activate(V2))) |
| isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) | | U22#(tt, V2) | → | U23#(isList(activate(V2))) |
| activate#(n__i) | → | i# | | isNeList#(n____(V1, V2)) | → | activate#(V2) |
| U41#(tt, V1, V2) | → | isList#(activate(V1)) | | U41#(tt, V1, V2) | → | U42#(isList(activate(V1)), activate(V2)) |
| isList#(n____(V1, V2)) | → | and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) | | isPal#(V) | → | isPalListKind#(activate(V)) |
| isPal#(V) | → | activate#(V) | | isPal#(V) | → | U71#(isPalListKind(activate(V)), activate(V)) |
| U42#(tt, V2) | → | isNeList#(activate(V2)) | | U51#(tt, V1, V2) | → | activate#(V2) |
| U61#(tt, V) | → | U62#(isQid(activate(V))) | | isNePal#(n____(I, __(P, I))) | → | and#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) |
| __#(__(X, Y), Z) | → | __#(Y, Z) | | isNePal#(V) | → | activate#(V) |
| U22#(tt, V2) | → | activate#(V2) | | U11#(tt, V) | → | isNeList#(activate(V)) |
| isNePal#(n____(I, __(P, I))) | → | isPal#(activate(P)) | | isList#(n____(V1, V2)) | → | activate#(V1) |
| U71#(tt, V) | → | isNePal#(activate(V)) | | isList#(n____(V1, V2)) | → | activate#(V2) |
| isNeList#(V) | → | activate#(V) | | U71#(tt, V) | → | activate#(V) |
| U31#(tt, V) | → | activate#(V) | | U11#(tt, V) | → | U12#(isNeList(activate(V))) |
| isPalListKind#(n____(V1, V2)) | → | activate#(V1) | | U51#(tt, V1, V2) | → | isNeList#(activate(V1)) |
| U42#(tt, V2) | → | activate#(V2) | | U22#(tt, V2) | → | isList#(activate(V2)) |
| U61#(tt, V) | → | isQid#(activate(V)) | | U52#(tt, V2) | → | isList#(activate(V2)) |
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | U41#(tt, V1, V2) | → | activate#(V2) |
| isList#(n____(V1, V2)) | → | U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | U61#(tt, V) | → | activate#(V) |
| activate#(n__nil) | → | nil# | | isPalListKind#(n____(V1, V2)) | → | activate#(V2) |
| U31#(tt, V) | → | isQid#(activate(V)) | | isNePal#(n____(I, __(P, I))) | → | isQid#(activate(I)) |
| isList#(V) | → | activate#(V) | | activate#(n__and(X1, X2)) | → | and#(X1, X2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
The following SCCs where found
| activate#(n__isPalListKind(X)) → isPalListKind#(X) | isPalListKind#(n____(V1, V2)) → activate#(V2) |
| and#(tt, X) → activate#(X) | isPalListKind#(n____(V1, V2)) → activate#(V1) |
| isPalListKind#(n____(V1, V2)) → isPalListKind#(activate(V1)) | activate#(n__and(X1, X2)) → and#(X1, X2) |
| isPalListKind#(n____(V1, V2)) → and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
| isPal#(V) → U71#(isPalListKind(activate(V)), activate(V)) | U71#(tt, V) → isNePal#(activate(V)) |
| isNePal#(n____(I, __(P, I))) → isPal#(activate(P)) |
| U51#(tt, V1, V2) → U52#(isNeList(activate(V1)), activate(V2)) | U42#(tt, V2) → isNeList#(activate(V2)) |
| U52#(tt, V2) → isList#(activate(V2)) | isNeList#(n____(V1, V2)) → U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| U21#(tt, V1, V2) → U22#(isList(activate(V1)), activate(V2)) | U11#(tt, V) → isNeList#(activate(V)) |
| isList#(n____(V1, V2)) → U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | U21#(tt, V1, V2) → isList#(activate(V1)) |
| isNeList#(n____(V1, V2)) → U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | isList#(V) → U11#(isPalListKind(activate(V)), activate(V)) |
| U41#(tt, V1, V2) → isList#(activate(V1)) | U51#(tt, V1, V2) → isNeList#(activate(V1)) |
| U41#(tt, V1, V2) → U42#(isList(activate(V1)), activate(V2)) | U22#(tt, V2) → isList#(activate(V2)) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U42#(tt, V2) | → | isNeList#(activate(V2)) | | U51#(tt, V1, V2) | → | U52#(isNeList(activate(V1)), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | U52#(tt, V2) | → | isList#(activate(V2)) |
| U21#(tt, V1, V2) | → | U22#(isList(activate(V1)), activate(V2)) | | U11#(tt, V) | → | isNeList#(activate(V)) |
| isList#(n____(V1, V2)) | → | U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | U21#(tt, V1, V2) | → | isList#(activate(V1)) |
| isNeList#(n____(V1, V2)) | → | U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) |
| U41#(tt, V1, V2) | → | U42#(isList(activate(V1)), activate(V2)) | | U51#(tt, V1, V2) | → | isNeList#(activate(V1)) |
| U41#(tt, V1, V2) | → | isList#(activate(V1)) | | U22#(tt, V2) | → | isList#(activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
Polynomial Interpretation
- U11(x,y): y + 1
- U11#(x,y): 2y
- U12(x): 0
- U21(x,y,z): y + 2
- U21#(x,y,z): 2z + 2y + x
- U22(x,y): x
- U22#(x,y): 2y
- U23(x): 0
- U31(x,y): 1
- U32(x): 0
- U41(x,y,z): 1
- U41#(x,y,z): 2z + 2y + x
- U42(x,y): 0
- U42#(x,y): 2y
- U43(x): 0
- U51(x,y,z): 1
- U51#(x,y,z): 2z + 2y
- U52(x,y): 0
- U52#(x,y): 2y
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + x + 1
- a: 0
- activate(x): x
- and(x,y): y
- e: 0
- i: 2
- isList(x): x + 1
- isList#(x): 2x
- isNeList(x): 1
- isNeList#(x): 2x
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 2
- isQid(x): x
- n____(x,y): y + x + 1
- n__a: 0
- n__and(x,y): y
- n__e: 0
- n__i: 2
- n__isPalListKind(x): 2
- n__nil: 2
- n__o: 2
- n__u: 0
- nil: 2
- o: 2
- tt: 0
- u: 0
Standard Usable rules
| U11(tt, V) | → | U12(isNeList(activate(V))) | | U53(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) | | isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U22(tt, V2) | → | U23(isList(activate(V2))) |
| activate(n__a) | → | a | | isPalListKind(X) | → | n__isPalListKind(X) |
| U43(tt) | → | tt | | activate(n__i) | → | i |
| U12(tt) | → | tt | | isQid(n__i) | → | tt |
| and(tt, X) | → | activate(X) | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| activate(X) | → | X | | __(nil, X) | → | X |
| u | → | n__u | | i | → | n__i |
| activate(n__and(X1, X2)) | → | and(X1, X2) | | o | → | n__o |
| nil | → | n__nil | | isQid(n__o) | → | tt |
| isPalListKind(n__i) | → | tt | | __(__(X, Y), Z) | → | __(X, __(Y, Z)) |
| __(X, nil) | → | X | | isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) |
| a | → | n__a | | isPalListKind(n____(V1, V2)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) |
| activate(n__nil) | → | nil | | isPalListKind(n__nil) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isQid(n__u) | → | tt | | U32(tt) | → | tt |
| isPalListKind(n__a) | → | tt | | isPalListKind(n__e) | → | tt |
| isQid(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| e | → | n__e | | isPalListKind(n__o) | → | tt |
| U23(tt) | → | tt | | and(X1, X2) | → | n__and(X1, X2) |
| isList(n__nil) | → | tt | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isQid(n__a) | → | tt | | isPalListKind(n__u) | → | tt |
| activate(n____(X1, X2)) | → | __(X1, X2) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| activate(n__u) | → | u | | U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) |
| activate(n__o) | → | o | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNeList#(n____(V1, V2)) | → | U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U42#(tt, V2) | → | isNeList#(activate(V2)) | | U51#(tt, V1, V2) | → | U52#(isNeList(activate(V1)), activate(V2)) |
| U52#(tt, V2) | → | isList#(activate(V2)) | | U21#(tt, V1, V2) | → | U22#(isList(activate(V1)), activate(V2)) |
| U11#(tt, V) | → | isNeList#(activate(V)) | | isList#(n____(V1, V2)) | → | U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| U21#(tt, V1, V2) | → | isList#(activate(V1)) | | isNeList#(n____(V1, V2)) | → | U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) | | U41#(tt, V1, V2) | → | U42#(isList(activate(V1)), activate(V2)) |
| U51#(tt, V1, V2) | → | isNeList#(activate(V1)) | | U41#(tt, V1, V2) | → | isList#(activate(V1)) |
| U22#(tt, V2) | → | isList#(activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, n__u, U62, U43, U61, n__o, U42, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, i, and, U71, n__and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, n____, n__isPalListKind, nil
Strategy
The following SCCs where found
| isList#(n____(V1, V2)) → U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | U21#(tt, V1, V2) → isList#(activate(V1)) |
| U42#(tt, V2) → isNeList#(activate(V2)) | isNeList#(n____(V1, V2)) → U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isList#(V) → U11#(isPalListKind(activate(V)), activate(V)) | U41#(tt, V1, V2) → isList#(activate(V1)) |
| U41#(tt, V1, V2) → U42#(isList(activate(V1)), activate(V2)) | U21#(tt, V1, V2) → U22#(isList(activate(V1)), activate(V2)) |
| U22#(tt, V2) → isList#(activate(V2)) | U11#(tt, V) → isNeList#(activate(V)) |
Problem 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isList#(n____(V1, V2)) | → | U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | U21#(tt, V1, V2) | → | isList#(activate(V1)) |
| U42#(tt, V2) | → | isNeList#(activate(V2)) | | isNeList#(n____(V1, V2)) | → | U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) | | U41#(tt, V1, V2) | → | isList#(activate(V1)) |
| U41#(tt, V1, V2) | → | U42#(isList(activate(V1)), activate(V2)) | | U21#(tt, V1, V2) | → | U22#(isList(activate(V1)), activate(V2)) |
| U22#(tt, V2) | → | isList#(activate(V2)) | | U11#(tt, V) | → | isNeList#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, n__u, U62, U43, U61, n__o, U42, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, i, and, U71, n__and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, n____, n__isPalListKind, nil
Strategy
Polynomial Interpretation
- U11(x,y): 1
- U11#(x,y): 2y
- U12(x): 1
- U21(x,y,z): 0
- U21#(x,y,z): 2z + 2y + 1
- U22(x,y): 0
- U22#(x,y): 2y + 1
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 3y + 1
- U41#(x,y,z): 2z + 2y + 2
- U42(x,y): x
- U42#(x,y): 2y + 2x
- U43(x): 0
- U51(x,y,z): 3
- U52(x,y): 1
- U53(x): x
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + x + 1
- a: 1
- activate(x): x
- and(x,y): y
- e: 1
- i: 1
- isList(x): 1
- isList#(x): 2x + 1
- isNeList(x): 3x
- isNeList#(x): 2x
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 2x
- isQid(x): 1
- n____(x,y): y + x + 1
- n__a: 1
- n__and(x,y): y
- n__e: 1
- n__i: 1
- n__isPalListKind(x): 2x
- n__nil: 0
- n__o: 1
- n__u: 1
- nil: 0
- o: 1
- tt: 0
- u: 1
Standard Usable rules
| U11(tt, V) | → | U12(isNeList(activate(V))) | | U53(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) | | isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U22(tt, V2) | → | U23(isList(activate(V2))) |
| activate(n__a) | → | a | | isPalListKind(X) | → | n__isPalListKind(X) |
| U43(tt) | → | tt | | activate(n__i) | → | i |
| U12(tt) | → | tt | | isQid(n__i) | → | tt |
| and(tt, X) | → | activate(X) | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| activate(X) | → | X | | __(nil, X) | → | X |
| i | → | n__i | | u | → | n__u |
| activate(n__and(X1, X2)) | → | and(X1, X2) | | nil | → | n__nil |
| o | → | n__o | | isQid(n__o) | → | 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)) | | isPalListKind(n____(V1, V2)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) |
| activate(n__nil) | → | nil | | isPalListKind(n__nil) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isQid(n__u) | → | tt | | U32(tt) | → | tt |
| isPalListKind(n__a) | → | tt | | isPalListKind(n__e) | → | tt |
| isQid(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| e | → | n__e | | isPalListKind(n__o) | → | tt |
| U23(tt) | → | tt | | isList(n__nil) | → | tt |
| and(X1, X2) | → | n__and(X1, X2) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isQid(n__a) | → | tt | | isPalListKind(n__u) | → | tt |
| activate(n____(X1, X2)) | → | __(X1, X2) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| activate(n__u) | → | u | | U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) |
| activate(n__o) | → | o | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isList#(n____(V1, V2)) | → | U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isList#(V) | → | U11#(isPalListKind(activate(V)), activate(V)) |
| U41#(tt, V1, V2) | → | isList#(activate(V1)) |
Problem 11: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U42#(tt, V2) | → | isNeList#(activate(V2)) | | U21#(tt, V1, V2) | → | isList#(activate(V1)) |
| isNeList#(n____(V1, V2)) | → | U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | U41#(tt, V1, V2) | → | U42#(isList(activate(V1)), activate(V2)) |
| U21#(tt, V1, V2) | → | U22#(isList(activate(V1)), activate(V2)) | | U22#(tt, V2) | → | isList#(activate(V2)) |
| U11#(tt, V) | → | isNeList#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
The following SCCs where found
| U42#(tt, V2) → isNeList#(activate(V2)) | isNeList#(n____(V1, V2)) → U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| U41#(tt, V1, V2) → U42#(isList(activate(V1)), activate(V2)) |
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U42#(tt, V2) | → | isNeList#(activate(V2)) | | isNeList#(n____(V1, V2)) | → | U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| U41#(tt, V1, V2) | → | U42#(isList(activate(V1)), activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
Polynomial Interpretation
- U11(x,y): x
- U12(x): 1
- U21(x,y,z): y + x
- U22(x,y): x + 1
- U23(x): 2
- U31(x,y): 2
- U32(x): x
- U41(x,y,z): 2
- U41#(x,y,z): 2z + y
- U42(x,y): 1
- U42#(x,y): 2y + x
- U43(x): 1
- U51(x,y,z): 1
- U52(x,y): 1
- U53(x): 1
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + x
- a: 1
- activate(x): x
- and(x,y): y
- e: 1
- i: 2
- isList(x): x
- isNeList(x): 2
- isNeList#(x): 2x + 1
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): x
- isQid(x): 1
- n____(x,y): y + x
- n__a: 1
- n__and(x,y): y
- n__e: 1
- n__i: 2
- n__isPalListKind(x): x
- n__nil: 2
- n__o: 1
- n__u: 1
- nil: 2
- o: 1
- tt: 1
- u: 1
Standard Usable rules
| U11(tt, V) | → | U12(isNeList(activate(V))) | | U53(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) | | isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U22(tt, V2) | → | U23(isList(activate(V2))) |
| activate(n__a) | → | a | | isPalListKind(X) | → | n__isPalListKind(X) |
| U43(tt) | → | tt | | activate(n__i) | → | i |
| U12(tt) | → | tt | | isQid(n__i) | → | tt |
| and(tt, X) | → | activate(X) | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| activate(X) | → | X | | __(nil, X) | → | X |
| i | → | n__i | | u | → | n__u |
| activate(n__and(X1, X2)) | → | and(X1, X2) | | nil | → | n__nil |
| o | → | n__o | | isQid(n__o) | → | 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)) | | isPalListKind(n____(V1, V2)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) |
| activate(n__nil) | → | nil | | isPalListKind(n__nil) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isQid(n__u) | → | tt | | U32(tt) | → | tt |
| isPalListKind(n__a) | → | tt | | isPalListKind(n__e) | → | tt |
| isQid(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| e | → | n__e | | isPalListKind(n__o) | → | tt |
| U23(tt) | → | tt | | isList(n__nil) | → | tt |
| and(X1, X2) | → | n__and(X1, X2) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isQid(n__a) | → | tt | | isPalListKind(n__u) | → | tt |
| activate(n____(X1, X2)) | → | __(X1, X2) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| activate(n__u) | → | u | | U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) |
| activate(n__o) | → | o | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNeList#(n____(V1, V2)) | → | U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
Problem 15: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U42#(tt, V2) | → | isNeList#(activate(V2)) | | U41#(tt, V1, V2) | → | U42#(isList(activate(V1)), activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, n__u, U62, U43, U61, n__o, U42, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, i, and, U71, n__and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, n____, n__isPalListKind, nil
Strategy
There are no SCCs!
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isPal#(V) | → | U71#(isPalListKind(activate(V)), activate(V)) | | U71#(tt, V) | → | isNePal#(activate(V)) |
| isNePal#(n____(I, __(P, I))) | → | isPal#(activate(P)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
Polynomial Interpretation
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U71#(x,y): y + x
- U72(x): 0
- __(x,y): y + 2x + 1
- a: 1
- activate(x): x
- and(x,y): y + 1
- e: 1
- i: 2
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isNePal#(x): x + 1
- isPal(x): 0
- isPal#(x): 2x
- isPalListKind(x): x
- isQid(x): 0
- n____(x,y): y + 2x + 1
- n__a: 1
- n__and(x,y): y + 1
- n__e: 1
- n__i: 2
- n__isPalListKind(x): x
- n__nil: 1
- n__o: 1
- n__u: 3
- nil: 1
- o: 1
- tt: 1
- u: 3
Standard Usable rules
| isPalListKind(n__i) | → | tt | | __(__(X, Y), Z) | → | __(X, __(Y, Z)) |
| __(X, nil) | → | X | | a | → | n__a |
| isPalListKind(n____(V1, V2)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) | | activate(n__nil) | → | nil |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| activate(n__a) | → | a | | isPalListKind(X) | → | n__isPalListKind(X) |
| e | → | n__e | | activate(n__i) | → | i |
| isPalListKind(n__o) | → | tt | | and(X1, X2) | → | n__and(X1, X2) |
| isPalListKind(n__u) | → | tt | | activate(n____(X1, X2)) | → | __(X1, X2) |
| and(tt, X) | → | activate(X) | | activate(n__isPalListKind(X)) | → | isPalListKind(X) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__and(X1, X2)) | → | and(X1, X2) |
| activate(n__o) | → | o | | nil | → | n__nil |
| o | → | n__o | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNePal#(n____(I, __(P, I))) | → | isPal#(activate(P)) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isPal#(V) | → | U71#(isPalListKind(activate(V)), activate(V)) | | U71#(tt, V) | → | isNePal#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, n__u, U62, U43, U61, n__o, U42, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, i, and, U71, n__and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, n____, n__isPalListKind, nil
Strategy
There are no SCCs!
Problem 4: 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(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
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 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| activate#(n__isPalListKind(X)) | → | isPalListKind#(X) | | isPalListKind#(n____(V1, V2)) | → | activate#(V2) |
| and#(tt, X) | → | activate#(X) | | isPalListKind#(n____(V1, V2)) | → | activate#(V1) |
| isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) | | activate#(n__and(X1, X2)) | → | and#(X1, X2) |
| isPalListKind#(n____(V1, V2)) | → | and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
Polynomial Interpretation
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + 3x
- a: 1
- activate(x): x
- activate#(x): x
- and(x,y): y + 3x
- and#(x,y): y + 2x
- 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__and(x,y): y + 3x
- n__e: 1
- n__i: 1
- n__isPalListKind(x): 2x
- n__nil: 1
- n__o: 1
- n__u: 1
- nil: 1
- o: 1
- tt: 1
- u: 1
Standard Usable rules
| isPalListKind(n__i) | → | tt | | __(__(X, Y), Z) | → | __(X, __(Y, Z)) |
| __(X, nil) | → | X | | a | → | n__a |
| isPalListKind(n____(V1, V2)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) | | activate(n__nil) | → | nil |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| activate(n__a) | → | a | | isPalListKind(X) | → | n__isPalListKind(X) |
| e | → | n__e | | activate(n__i) | → | i |
| isPalListKind(n__o) | → | tt | | and(X1, X2) | → | n__and(X1, X2) |
| isPalListKind(n__u) | → | tt | | activate(n____(X1, X2)) | → | __(X1, X2) |
| and(tt, X) | → | activate(X) | | activate(n__isPalListKind(X)) | → | isPalListKind(X) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__and(X1, X2)) | → | and(X1, X2) |
| activate(n__o) | → | o | | nil | → | n__nil |
| o | → | n__o | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| and#(tt, X) | → | activate#(X) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| activate#(n__isPalListKind(X)) | → | isPalListKind#(X) | | isPalListKind#(n____(V1, V2)) | → | activate#(V2) |
| isPalListKind#(n____(V1, V2)) | → | activate#(V1) | | isPalListKind#(n____(V1, V2)) | → | isPalListKind#(activate(V1)) |
| activate#(n__and(X1, X2)) | → | and#(X1, X2) | | isPalListKind#(n____(V1, V2)) | → | and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, n__u, U62, U43, U61, n__o, U42, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, i, and, U71, n__and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, n____, n__isPalListKind, nil
Strategy
The following SCCs where found
| activate#(n__isPalListKind(X)) → isPalListKind#(X) | isPalListKind#(n____(V1, V2)) → activate#(V2) |
| isPalListKind#(n____(V1, V2)) → activate#(V1) | isPalListKind#(n____(V1, V2)) → isPalListKind#(activate(V1)) |
Problem 10: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| activate#(n__isPalListKind(X)) | → | isPalListKind#(X) | | isPalListKind#(n____(V1, V2)) | → | activate#(V2) |
| isPalListKind#(n____(V1, V2)) | → | activate#(V1) | | 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(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, n__u, U62, U43, U61, n__o, U42, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, i, and, U71, n__and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, n____, n__isPalListKind, nil
Strategy
Polynomial Interpretation
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + 2x
- a: 0
- activate(x): x
- activate#(x): 2x
- and(x,y): y
- e: 0
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): x + 1
- isPalListKind#(x): 2x
- isQid(x): 0
- n____(x,y): y + 2x
- n__a: 0
- n__and(x,y): y
- n__e: 0
- n__i: 1
- n__isPalListKind(x): x + 1
- n__nil: 0
- n__o: 2
- n__u: 0
- nil: 0
- o: 2
- tt: 1
- u: 0
Standard Usable rules
| isPalListKind(n__i) | → | tt | | __(__(X, Y), Z) | → | __(X, __(Y, Z)) |
| __(X, nil) | → | X | | a | → | n__a |
| isPalListKind(n____(V1, V2)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) | | activate(n__nil) | → | nil |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| isPalListKind(X) | → | n__isPalListKind(X) | | activate(n__a) | → | a |
| e | → | n__e | | activate(n__i) | → | i |
| isPalListKind(n__o) | → | tt | | and(X1, X2) | → | n__and(X1, X2) |
| isPalListKind(n__u) | → | tt | | activate(n____(X1, X2)) | → | __(X1, X2) |
| and(tt, X) | → | activate(X) | | activate(n__isPalListKind(X)) | → | isPalListKind(X) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| activate(n__and(X1, X2)) | → | and(X1, X2) | | nil | → | n__nil |
| o | → | n__o | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__isPalListKind(X)) | → | isPalListKind#(X) |
Problem 12: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isPalListKind#(n____(V1, V2)) | → | activate#(V2) | | isPalListKind#(n____(V1, V2)) | → | activate#(V1) |
| 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(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
The following SCCs where found
| isPalListKind#(n____(V1, V2)) → isPalListKind#(activate(V1)) |
Problem 14: 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(isNeList(activate(V))) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(activate(V1)), activate(V2)) |
| U22(tt, V2) | → | U23(isList(activate(V2))) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(activate(V))) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(activate(V1)), activate(V2)) | | U42(tt, V2) | → | U43(isNeList(activate(V2))) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(activate(V1)), activate(V2)) |
| U52(tt, V2) | → | U53(isList(activate(V2))) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(activate(V))) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(activate(V))) | | U72(tt) | → | tt |
| and(tt, X) | → | activate(X) | | isList(V) | → | U11(isPalListKind(activate(V)), activate(V)) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(V) | → | U31(isPalListKind(activate(V)), activate(V)) | | isNeList(n____(V1, V2)) | → | U41(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)) | | isNePal(V) | → | U61(isPalListKind(activate(V)), activate(V)) |
| isNePal(n____(I, __(P, I))) | → | and(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))) | | isPal(V) | → | U71(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)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(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) | | isPalListKind(X) | → | n__isPalListKind(X) |
| and(X1, X2) | → | n__and(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)) | → | __(X1, X2) |
| activate(n__isPalListKind(X)) | → | isPalListKind(X) | | activate(n__and(X1, X2)) | → | and(X1, 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: isList, isNeList, __, activate, U62, n__u, U61, U43, U42, n__o, U41, isNePal, n__nil, U23, U21, U22, n__e, e, isPalListKind, n__a, a, o, isPal, n__i, U71, and, i, U72, n__and, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, n____, nil, n__isPalListKind
Strategy
Polynomial Interpretation
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + 2x + 1
- a: 2
- activate(x): 2x
- and(x,y): 2y
- e: 1
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 0
- isPalListKind#(x): x + 1
- isQid(x): 0
- n____(x,y): y + 2x + 1
- n__a: 1
- n__and(x,y): y
- n__e: 1
- n__i: 0
- n__isPalListKind(x): 0
- n__nil: 0
- n__o: 1
- n__u: 0
- nil: 0
- o: 2
- tt: 0
- u: 0
Standard Usable rules
| isPalListKind(n__i) | → | tt | | __(__(X, Y), Z) | → | __(X, __(Y, Z)) |
| __(X, nil) | → | X | | a | → | n__a |
| isPalListKind(n____(V1, V2)) | → | and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))) | | activate(n__nil) | → | nil |
| isPalListKind(n__nil) | → | tt | | isPalListKind(n__a) | → | tt |
| isPalListKind(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| isPalListKind(X) | → | n__isPalListKind(X) | | activate(n__a) | → | a |
| e | → | n__e | | activate(n__i) | → | i |
| isPalListKind(n__o) | → | tt | | and(X1, X2) | → | n__and(X1, X2) |
| isPalListKind(n__u) | → | tt | | activate(n____(X1, X2)) | → | __(X1, X2) |
| and(tt, X) | → | activate(X) | | activate(n__isPalListKind(X)) | → | isPalListKind(X) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| activate(n__and(X1, X2)) | → | and(X1, X2) | | nil | → | n__nil |
| o | → | n__o | | 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)) |