YES
The TRS could be proven terminating. The proof took 60003 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (469ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (300ms).
| | – Problem 4 was processed with processor PolynomialLinearRange4 (203ms).
| | | – Problem 5 was processed with processor DependencyGraph (79ms).
| | | | – Problem 6 was processed with processor PolynomialLinearRange4 (310ms).
| | | | | – Problem 7 was processed with processor DependencyGraph (11ms).
| | | | | | – Problem 8 was processed with processor PolynomialLinearRange4 (124ms).
| | | | | | | – Problem 9 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNePal#(n____(I, n____(P, I))) | → | activate#(P) | | and#(tt, X) | → | activate#(X) |
| isNeList#(n____(V1, V2)) | → | and#(isNeList(activate(V1)), n__isList(activate(V2))) | | activate#(n__o) | → | o# |
| isNePal#(n____(I, n____(P, I))) | → | activate#(I) | | activate#(n____(X1, X2)) | → | activate#(X2) |
| isNeList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isNeList(activate(V2))) | | isList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isList(activate(V2))) |
| isNePal#(V) | → | isQid#(activate(V)) | | isNePal#(V) | → | activate#(V) |
| __#(__(X, Y), Z) | → | __#(Y, Z) | | activate#(n____(X1, X2)) | → | __#(activate(X1), activate(X2)) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isList#(n____(V1, V2)) | → | activate#(V1) |
| activate#(n__a) | → | a# | | isNePal#(n____(I, n____(P, I))) | → | and#(isQid(activate(I)), n__isPal(activate(P))) |
| isList#(n____(V1, V2)) | → | activate#(V2) | | isNePal#(n____(I, n____(P, I))) | → | isQid#(activate(I)) |
| activate#(n____(X1, X2)) | → | activate#(X1) | | isNeList#(V) | → | activate#(V) |
| isNeList#(n____(V1, V2)) | → | activate#(V1) | | __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
| activate#(n__isList(X)) | → | isList#(X) | | isNeList#(V) | → | isQid#(activate(V)) |
| activate#(n__isNeList(X)) | → | isNeList#(X) | | isPal#(V) | → | isNePal#(activate(V)) |
| activate#(n__u) | → | u# | | activate#(n__nil) | → | nil# |
| activate#(n__e) | → | e# | | isNeList#(n____(V1, V2)) | → | activate#(V2) |
| activate#(n__i) | → | i# | | activate#(n__isPal(X)) | → | isPal#(X) |
| isPal#(V) | → | activate#(V) | | isList#(V) | → | activate#(V) |
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isList#(V) | → | isNeList#(activate(V)) |
| isList#(n____(V1, V2)) | → | isList#(activate(V1)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
The following SCCs where found
| isNePal#(n____(I, n____(P, I))) → activate#(P) | and#(tt, X) → activate#(X) |
| isNeList#(n____(V1, V2)) → and#(isNeList(activate(V1)), n__isList(activate(V2))) | isNePal#(n____(I, n____(P, I))) → activate#(I) |
| activate#(n____(X1, X2)) → activate#(X2) | isNeList#(n____(V1, V2)) → and#(isList(activate(V1)), n__isNeList(activate(V2))) |
| isList#(n____(V1, V2)) → and#(isList(activate(V1)), n__isList(activate(V2))) | isNePal#(V) → activate#(V) |
| isNeList#(n____(V1, V2)) → isList#(activate(V1)) | isList#(n____(V1, V2)) → activate#(V1) |
| isNePal#(n____(I, n____(P, I))) → and#(isQid(activate(I)), n__isPal(activate(P))) | isList#(n____(V1, V2)) → activate#(V2) |
| isNeList#(V) → activate#(V) | activate#(n____(X1, X2)) → activate#(X1) |
| isNeList#(n____(V1, V2)) → activate#(V1) | activate#(n__isList(X)) → isList#(X) |
| activate#(n__isNeList(X)) → isNeList#(X) | isPal#(V) → isNePal#(activate(V)) |
| isNeList#(n____(V1, V2)) → activate#(V2) | activate#(n__isPal(X)) → isPal#(X) |
| isList#(V) → activate#(V) | isPal#(V) → activate#(V) |
| isNeList#(n____(V1, V2)) → isNeList#(activate(V1)) | isList#(V) → isNeList#(activate(V)) |
| isList#(n____(V1, V2)) → isList#(activate(V1)) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
Problem 2: 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 | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, 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 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNePal#(n____(I, n____(P, I))) | → | activate#(P) | | and#(tt, X) | → | activate#(X) |
| isNeList#(n____(V1, V2)) | → | and#(isNeList(activate(V1)), n__isList(activate(V2))) | | isNePal#(n____(I, n____(P, I))) | → | activate#(I) |
| activate#(n____(X1, X2)) | → | activate#(X2) | | isNeList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isNeList(activate(V2))) |
| isList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isList(activate(V2))) | | isNePal#(V) | → | activate#(V) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isList#(n____(V1, V2)) | → | activate#(V1) |
| isNePal#(n____(I, n____(P, I))) | → | and#(isQid(activate(I)), n__isPal(activate(P))) | | isList#(n____(V1, V2)) | → | activate#(V2) |
| activate#(n____(X1, X2)) | → | activate#(X1) | | isNeList#(V) | → | activate#(V) |
| isNeList#(n____(V1, V2)) | → | activate#(V1) | | activate#(n__isList(X)) | → | isList#(X) |
| activate#(n__isNeList(X)) | → | isNeList#(X) | | isPal#(V) | → | isNePal#(activate(V)) |
| isNeList#(n____(V1, V2)) | → | activate#(V2) | | activate#(n__isPal(X)) | → | isPal#(X) |
| isPal#(V) | → | activate#(V) | | isList#(V) | → | activate#(V) |
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isList#(n____(V1, V2)) | → | isList#(activate(V1)) |
| isList#(V) | → | isNeList#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
Polynomial Interpretation
- __(x,y): y + x
- a: 1
- activate(x): x
- activate#(x): x
- and(x,y): y
- and#(x,y): y
- e: 3
- i: 2
- isList(x): 2x + 1
- isList#(x): 2x + 1
- isNeList(x): 2x + 1
- isNeList#(x): 2x + 1
- isNePal(x): x
- isNePal#(x): x
- isPal(x): x
- isPal#(x): x
- isQid(x): 0
- n____(x,y): y + x
- n__a: 1
- n__e: 3
- n__i: 2
- n__isList(x): 2x + 1
- n__isNeList(x): 2x + 1
- n__isPal(x): x
- n__nil: 1
- n__o: 1
- n__u: 3
- nil: 1
- o: 1
- tt: 0
- u: 3
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| a | → | n__a | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) | | isPal(n__nil) | → | tt |
| isPal(X) | → | n__isPal(X) | | isQid(n__u) | → | tt |
| isQid(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| isNePal(V) | → | isQid(activate(V)) | | activate(n__isPal(X)) | → | isPal(X) |
| isNeList(X) | → | n__isNeList(X) | | isList(V) | → | isNeList(activate(V)) |
| activate(n__a) | → | a | | e | → | n__e |
| activate(n__i) | → | i | | isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isList(n__nil) | → | tt | | isQid(n__a) | → | tt |
| isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) | | activate(n__isList(X)) | → | isList(X) |
| isQid(n__i) | → | tt | | and(tt, X) | → | activate(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | activate(X) | → | X |
| isList(X) | → | n__isList(X) | | isPal(V) | → | isNePal(activate(V)) |
| activate(n__u) | → | u | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| o | → | n__o | | nil | → | n__nil |
| isQid(n__o) | → | tt | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isList#(n____(V1, V2)) | → | activate#(V1) | | isList#(n____(V1, V2)) | → | activate#(V2) |
| isNeList#(V) | → | activate#(V) | | isNeList#(n____(V1, V2)) | → | activate#(V1) |
| isNeList#(n____(V1, V2)) | → | activate#(V2) | | isList#(V) | → | activate#(V) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNePal#(n____(I, n____(P, I))) | → | activate#(P) | | and#(tt, X) | → | activate#(X) |
| isNeList#(n____(V1, V2)) | → | and#(isNeList(activate(V1)), n__isList(activate(V2))) | | isNePal#(n____(I, n____(P, I))) | → | activate#(I) |
| activate#(n__isList(X)) | → | isList#(X) | | activate#(n____(X1, X2)) | → | activate#(X2) |
| isNeList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isNeList(activate(V2))) | | isList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isList(activate(V2))) |
| activate#(n__isNeList(X)) | → | isNeList#(X) | | isPal#(V) | → | isNePal#(activate(V)) |
| isNePal#(V) | → | activate#(V) | | isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) |
| isNePal#(n____(I, n____(P, I))) | → | and#(isQid(activate(I)), n__isPal(activate(P))) | | activate#(n____(X1, X2)) | → | activate#(X1) |
| activate#(n__isPal(X)) | → | isPal#(X) | | isPal#(V) | → | activate#(V) |
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isList#(V) | → | isNeList#(activate(V)) |
| isList#(n____(V1, V2)) | → | isList#(activate(V1)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
Polynomial Interpretation
- __(x,y): y + 2x + 1
- a: 3
- activate(x): x
- activate#(x): x
- and(x,y): y
- and#(x,y): 2y
- e: 0
- i: 1
- isList(x): 0
- isList#(x): 0
- isNeList(x): 0
- isNeList#(x): 0
- isNePal(x): x
- isNePal#(x): x
- isPal(x): x + 1
- isPal#(x): x
- isQid(x): 0
- n____(x,y): y + 2x + 1
- n__a: 3
- n__e: 0
- n__i: 1
- n__isList(x): 0
- n__isNeList(x): 0
- n__isPal(x): x + 1
- n__nil: 0
- n__o: 2
- n__u: 0
- nil: 0
- o: 2
- tt: 0
- u: 0
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| a | → | n__a | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) | | isPal(n__nil) | → | tt |
| isPal(X) | → | n__isPal(X) | | isQid(n__u) | → | tt |
| isQid(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| isNePal(V) | → | isQid(activate(V)) | | activate(n__isPal(X)) | → | isPal(X) |
| isNeList(X) | → | n__isNeList(X) | | isList(V) | → | isNeList(activate(V)) |
| activate(n__a) | → | a | | e | → | n__e |
| activate(n__i) | → | i | | isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isList(n__nil) | → | tt | | isQid(n__a) | → | tt |
| isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) | | activate(n__isList(X)) | → | isList(X) |
| isQid(n__i) | → | tt | | and(tt, X) | → | activate(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | activate(X) | → | X |
| isList(X) | → | n__isList(X) | | isPal(V) | → | isNePal(activate(V)) |
| activate(n__u) | → | u | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| o | → | n__o | | nil | → | n__nil |
| isQid(n__o) | → | tt | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNePal#(n____(I, n____(P, I))) | → | activate#(P) | | isNePal#(n____(I, n____(P, I))) | → | activate#(I) |
| activate#(n____(X1, X2)) | → | activate#(X2) | | activate#(n____(X1, X2)) | → | activate#(X1) |
| activate#(n__isPal(X)) | → | isPal#(X) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| and#(tt, X) | → | activate#(X) | | isNeList#(n____(V1, V2)) | → | and#(isNeList(activate(V1)), n__isList(activate(V2))) |
| activate#(n__isList(X)) | → | isList#(X) | | isNeList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isNeList(activate(V2))) |
| isList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isList(activate(V2))) | | activate#(n__isNeList(X)) | → | isNeList#(X) |
| isPal#(V) | → | isNePal#(activate(V)) | | isNePal#(V) | → | activate#(V) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isNePal#(n____(I, n____(P, I))) | → | and#(isQid(activate(I)), n__isPal(activate(P))) |
| isPal#(V) | → | activate#(V) | | isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) |
| isList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isList#(V) | → | isNeList#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
The following SCCs where found
| and#(tt, X) → activate#(X) | isNeList#(n____(V1, V2)) → and#(isNeList(activate(V1)), n__isList(activate(V2))) |
| activate#(n__isList(X)) → isList#(X) | isNeList#(n____(V1, V2)) → and#(isList(activate(V1)), n__isNeList(activate(V2))) |
| isList#(n____(V1, V2)) → and#(isList(activate(V1)), n__isList(activate(V2))) | activate#(n__isNeList(X)) → isNeList#(X) |
| isNeList#(n____(V1, V2)) → isNeList#(activate(V1)) | isList#(V) → isNeList#(activate(V)) |
| isNeList#(n____(V1, V2)) → isList#(activate(V1)) | isList#(n____(V1, V2)) → isList#(activate(V1)) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| and#(tt, X) | → | activate#(X) | | isNeList#(n____(V1, V2)) | → | and#(isNeList(activate(V1)), n__isList(activate(V2))) |
| activate#(n__isList(X)) | → | isList#(X) | | isNeList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isNeList(activate(V2))) |
| isList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isList(activate(V2))) | | activate#(n__isNeList(X)) | → | isNeList#(X) |
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isList#(V) | → | isNeList#(activate(V)) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isList#(n____(V1, V2)) | → | isList#(activate(V1)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
Polynomial Interpretation
- __(x,y): y + x
- a: 1
- activate(x): x
- activate#(x): 2x + 2
- and(x,y): y + x
- and#(x,y): 2y + 2x
- e: 1
- i: 1
- isList(x): x
- isList#(x): 2x
- isNeList(x): x
- isNeList#(x): 2x
- isNePal(x): x + 1
- isPal(x): x + 1
- isQid(x): x
- n____(x,y): y + x
- n__a: 1
- n__e: 1
- n__i: 1
- n__isList(x): x
- n__isNeList(x): x
- n__isPal(x): x + 1
- n__nil: 1
- n__o: 1
- n__u: 1
- nil: 1
- o: 1
- tt: 1
- u: 1
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| a | → | n__a | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) | | isPal(n__nil) | → | tt |
| isQid(n__u) | → | tt | | isPal(X) | → | n__isPal(X) |
| isQid(n__e) | → | tt | | __(X1, X2) | → | n____(X1, X2) |
| isNePal(V) | → | isQid(activate(V)) | | activate(n__isPal(X)) | → | isPal(X) |
| isNeList(X) | → | n__isNeList(X) | | isList(V) | → | isNeList(activate(V)) |
| activate(n__a) | → | a | | e | → | n__e |
| activate(n__i) | → | i | | isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isList(n__nil) | → | tt | | isQid(n__a) | → | tt |
| activate(n__isList(X)) | → | isList(X) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isQid(n__i) | → | tt | | and(tt, X) | → | activate(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | activate(X) | → | X |
| isList(X) | → | n__isList(X) | | isPal(V) | → | isNePal(activate(V)) |
| activate(n__u) | → | u | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| nil | → | n__nil | | o | → | n__o |
| isQid(n__o) | → | tt | | activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| activate#(n__isList(X)) | → | isList#(X) | | activate#(n__isNeList(X)) | → | isNeList#(X) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| and#(tt, X) | → | activate#(X) | | isNeList#(n____(V1, V2)) | → | and#(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNeList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isNeList(activate(V2))) | | isList#(n____(V1, V2)) | → | and#(isList(activate(V1)), n__isList(activate(V2))) |
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isList#(n____(V1, V2)) | → | isList#(activate(V1)) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isList#(V) | → | isNeList#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
The following SCCs where found
| isNeList#(n____(V1, V2)) → isNeList#(activate(V1)) | isNeList#(n____(V1, V2)) → isList#(activate(V1)) |
| isList#(n____(V1, V2)) → isList#(activate(V1)) | isList#(V) → isNeList#(activate(V)) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) |
| isList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isList#(V) | → | isNeList#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
Polynomial Interpretation
- __(x,y): y + 2x + 1
- a: 0
- activate(x): x
- and(x,y): y
- e: 0
- i: 0
- isList(x): 2x + 1
- isList#(x): x
- isNeList(x): 2x
- isNeList#(x): x
- isNePal(x): x
- isPal(x): x + 2
- isQid(x): x
- n____(x,y): y + 2x + 1
- n__a: 0
- n__e: 0
- n__i: 0
- n__isList(x): 2x + 1
- n__isNeList(x): 2x
- n__isPal(x): x + 2
- n__nil: 1
- n__o: 0
- n__u: 0
- nil: 1
- o: 0
- tt: 0
- u: 0
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| a | → | n__a | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(activate(X1), activate(X2)) | | isPal(n__nil) | → | tt |
| isPal(X) | → | n__isPal(X) | | isQid(n__u) | → | tt |
| isQid(n__e) | → | tt | | activate(n__isPal(X)) | → | isPal(X) |
| isNePal(V) | → | isQid(activate(V)) | | __(X1, X2) | → | n____(X1, X2) |
| isNeList(X) | → | n__isNeList(X) | | activate(n__a) | → | a |
| isList(V) | → | isNeList(activate(V)) | | e | → | n__e |
| activate(n__i) | → | i | | isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) |
| isList(n__nil) | → | tt | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isQid(n__a) | → | tt |
| isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) | | activate(n__isList(X)) | → | isList(X) |
| isQid(n__i) | → | tt | | and(tt, X) | → | activate(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | activate(X) | → | X |
| isList(X) | → | n__isList(X) | | isPal(V) | → | isNePal(activate(V)) |
| activate(n__u) | → | u | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| __(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__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)) | → | isNeList#(activate(V1)) | | isList#(n____(V1, V2)) | → | isList#(activate(V1)) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) |
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(V) | → | isNeList#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | activate(X) |
| isList(V) | → | isNeList(activate(V)) | | isList(n__nil) | → | tt |
| isList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isList(activate(V2))) | | isNeList(V) | → | isQid(activate(V)) |
| isNeList(n____(V1, V2)) | → | and(isList(activate(V1)), n__isNeList(activate(V2))) | | isNeList(n____(V1, V2)) | → | and(isNeList(activate(V1)), n__isList(activate(V2))) |
| isNePal(V) | → | isQid(activate(V)) | | isNePal(n____(I, n____(P, I))) | → | and(isQid(activate(I)), n__isPal(activate(P))) |
| isPal(V) | → | isNePal(activate(V)) | | isPal(n__nil) | → | tt |
| 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) | | isList(X) | → | n__isList(X) |
| isNeList(X) | → | n__isNeList(X) | | 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__isList(X)) | → | isList(X) |
| activate(n__isNeList(X)) | → | isNeList(X) | | 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, n__o, isNePal, n__nil, n__e, e, n__a, a, o, isPal, n__i, and, i, u, tt, isQid, n____, n__isNeList, n__isList, nil, n__isPal
Strategy
There are no SCCs!