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