YES
The TRS could be proven terminating. The proof took 22058 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (602ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (191ms).
| | – Problem 5 was processed with processor DependencyGraph (8ms).
| | | – Problem 7 was processed with processor PolynomialLinearRange4 (131ms).
| | | | – Problem 8 was processed with processor DependencyGraph (4ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (71ms).
| | – Problem 6 was processed with processor DependencyGraph (0ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isPal#(V) | → | U81#(isNePal(activate(V))) | | isNeList#(n____(V1, V2)) | → | U41#(isList(activate(V1)), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | U51#(isNeList(activate(V1)), activate(V2)) | | activate#(n__o) | → | o# |
| isList#(V) | → | U11#(isNeList(activate(V))) | | isNePal#(V) | → | isQid#(activate(V)) |
| __#(__(X, Y), Z) | → | __#(Y, Z) | | isNePal#(V) | → | activate#(V) |
| isList#(n____(V1, V2)) | → | activate#(V1) | | U41#(tt, V2) | → | isNeList#(activate(V2)) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isList#(n____(V1, V2)) | → | U21#(isList(activate(V1)), activate(V2)) |
| activate#(n__a) | → | a# | | isList#(n____(V1, V2)) | → | activate#(V2) |
| U41#(tt, V2) | → | activate#(V2) | | U21#(tt, V2) | → | activate#(V2) |
| isNeList#(V) | → | activate#(V) | | isNePal#(V) | → | U61#(isQid(activate(V))) |
| U21#(tt, V2) | → | isList#(activate(V2)) | | U21#(tt, V2) | → | U22#(isList(activate(V2))) |
| isNeList#(n____(V1, V2)) | → | activate#(V1) | | isNePal#(n____(I, __(P, I))) | → | U71#(isQid(activate(I)), activate(P)) |
| U71#(tt, P) | → | U72#(isPal(activate(P))) | | U51#(tt, V2) | → | activate#(V2) |
| U71#(tt, P) | → | isPal#(activate(P)) | | __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
| isNeList#(V) | → | isQid#(activate(V)) | | U71#(tt, P) | → | activate#(P) |
| U41#(tt, V2) | → | U42#(isNeList(activate(V2))) | | isNePal#(n____(I, __(P, I))) | → | activate#(P) |
| isPal#(V) | → | isNePal#(activate(V)) | | activate#(n__u) | → | u# |
| activate#(n__nil) | → | nil# | | activate#(n____(X1, X2)) | → | __#(X1, X2) |
| isNePal#(n____(I, __(P, I))) | → | activate#(I) | | activate#(n__e) | → | e# |
| isNeList#(V) | → | U31#(isQid(activate(V))) | | U51#(tt, V2) | → | isList#(activate(V2)) |
| isNePal#(n____(I, __(P, I))) | → | isQid#(activate(I)) | | isNeList#(n____(V1, V2)) | → | activate#(V2) |
| activate#(n__i) | → | i# | | isList#(V) | → | activate#(V) |
| U51#(tt, V2) | → | U52#(isList(activate(V2))) | | 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 | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, U42, n__o, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U81, U52, U11, isQid, U31, n____, nil
Strategy
The following SCCs where found
| U71#(tt, P) → isPal#(activate(P)) | isPal#(V) → isNePal#(activate(V)) |
| isNePal#(n____(I, __(P, I))) → U71#(isQid(activate(I)), activate(P)) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
| isList#(n____(V1, V2)) → U21#(isList(activate(V1)), activate(V2)) | isNeList#(n____(V1, V2)) → U41#(isList(activate(V1)), activate(V2)) |
| isNeList#(n____(V1, V2)) → U51#(isNeList(activate(V1)), activate(V2)) | U21#(tt, V2) → isList#(activate(V2)) |
| U51#(tt, V2) → isList#(activate(V2)) | isNeList#(n____(V1, V2)) → isNeList#(activate(V1)) |
| U41#(tt, V2) → isNeList#(activate(V2)) | isNeList#(n____(V1, V2)) → isList#(activate(V1)) |
| isList#(n____(V1, V2)) → isList#(activate(V1)) | isList#(V) → isNeList#(activate(V)) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isList#(n____(V1, V2)) | → | U21#(isList(activate(V1)), activate(V2)) | | isNeList#(n____(V1, V2)) | → | U41#(isList(activate(V1)), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | U51#(isNeList(activate(V1)), activate(V2)) | | U21#(tt, V2) | → | isList#(activate(V2)) |
| U51#(tt, V2) | → | isList#(activate(V2)) | | isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) |
| U41#(tt, V2) | → | isNeList#(activate(V2)) | | 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 | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, U42, n__o, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U81, U52, U11, isQid, U31, n____, nil
Strategy
Polynomial Interpretation
- U11(x): 2x
- U21(x,y): 2y + 2x
- U21#(x,y): 2y + 2x
- U22(x): 1
- U31(x): x
- U41(x,y): x
- U41#(x,y): 2y
- U42(x): 1
- U51(x,y): 3x
- U51#(x,y): 2y
- U52(x): 1
- U61(x): 0
- U71(x,y): 0
- U72(x): 0
- U81(x): 0
- __(x,y): y + 3x
- a: 2
- activate(x): x
- e: 1
- i: 2
- isList(x): 2x
- isList#(x): 2x
- isNeList(x): x
- isNeList#(x): 2x
- isNePal(x): 0
- isPal(x): 0
- isQid(x): x
- n____(x,y): y + 3x
- n__a: 2
- n__e: 1
- n__i: 2
- n__nil: 1
- n__o: 2
- n__u: 2
- nil: 1
- o: 2
- tt: 1
- u: 2
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| __(X, nil) | → | X | | a | → | n__a |
| U31(tt) | → | tt | | activate(n__nil) | → | nil |
| isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) | | isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) |
| isQid(n__u) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isQid(n__e) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| isList(V) | → | U11(isNeList(activate(V))) | | __(X1, X2) | → | n____(X1, X2) |
| U22(tt) | → | tt | | activate(n__a) | → | a |
| U11(tt) | → | tt | | e | → | n__e |
| activate(n__i) | → | i | | isList(n__nil) | → | tt |
| isQid(n__a) | → | tt | | isQid(n__i) | → | tt |
| activate(n____(X1, X2)) | → | __(X1, X2) | | U42(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | isNeList(V) | → | U31(isQid(activate(V))) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| nil | → | n__nil | | o | → | n__o |
| isQid(n__o) | → | tt | | U52(tt) | → | tt |
| activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U21#(tt, V2) | → | isList#(activate(V2)) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(n____(V1, V2)) | → | U21#(isList(activate(V1)), activate(V2)) | | isNeList#(n____(V1, V2)) | → | U41#(isList(activate(V1)), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | U51#(isNeList(activate(V1)), activate(V2)) | | U51#(tt, V2) | → | isList#(activate(V2)) |
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isList#(V) | → | isNeList#(activate(V)) |
| isList#(n____(V1, V2)) | → | isList#(activate(V1)) | | isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) |
| U41#(tt, V2) | → | isNeList#(activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, n__o, U42, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U52, U81, U11, U31, isQid, n____, nil
Strategy
The following SCCs where found
| isNeList#(n____(V1, V2)) → U41#(isList(activate(V1)), activate(V2)) | isNeList#(n____(V1, V2)) → U51#(isNeList(activate(V1)), activate(V2)) |
| U51#(tt, V2) → isList#(activate(V2)) | isNeList#(n____(V1, V2)) → isNeList#(activate(V1)) |
| U41#(tt, V2) → isNeList#(activate(V2)) | isNeList#(n____(V1, V2)) → isList#(activate(V1)) |
| isList#(n____(V1, V2)) → isList#(activate(V1)) | isList#(V) → isNeList#(activate(V)) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNeList#(n____(V1, V2)) | → | U41#(isList(activate(V1)), activate(V2)) | | isNeList#(n____(V1, V2)) | → | U51#(isNeList(activate(V1)), activate(V2)) |
| U51#(tt, V2) | → | isList#(activate(V2)) | | isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) |
| U41#(tt, V2) | → | isNeList#(activate(V2)) | | 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 | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, n__o, U42, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U52, U81, U11, U31, isQid, n____, nil
Strategy
Polynomial Interpretation
- U11(x): 1
- U21(x,y): 1
- U22(x): 1
- U31(x): 2x
- U41(x,y): 2y + 1
- U41#(x,y): y
- U42(x): 1
- U51(x,y): y + 2
- U51#(x,y): y
- U52(x): 2x
- U61(x): 0
- U71(x,y): 0
- U72(x): 0
- U81(x): 0
- __(x,y): y + x + 1
- a: 1
- activate(x): x
- e: 1
- i: 1
- isList(x): 1
- isList#(x): x
- isNeList(x): 2x
- isNeList#(x): x
- isNePal(x): 0
- isPal(x): 0
- isQid(x): x
- n____(x,y): y + x + 1
- n__a: 1
- n__e: 1
- n__i: 1
- n__nil: 2
- n__o: 1
- n__u: 2
- nil: 2
- o: 1
- tt: 1
- u: 2
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| __(X, nil) | → | X | | a | → | n__a |
| U31(tt) | → | tt | | activate(n__nil) | → | nil |
| isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) | | isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) |
| isQid(n__u) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isQid(n__e) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| isList(V) | → | U11(isNeList(activate(V))) | | __(X1, X2) | → | n____(X1, X2) |
| U22(tt) | → | tt | | activate(n__a) | → | a |
| U11(tt) | → | tt | | e | → | n__e |
| activate(n__i) | → | i | | isList(n__nil) | → | tt |
| isQid(n__a) | → | tt | | isQid(n__i) | → | tt |
| activate(n____(X1, X2)) | → | __(X1, X2) | | U42(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | isNeList(V) | → | U31(isQid(activate(V))) |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | i | → | n__i |
| u | → | n__u | | activate(n__o) | → | o |
| nil | → | n__nil | | o | → | n__o |
| isQid(n__o) | → | tt | | U52(tt) | → | 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)) | → | U41#(isList(activate(V1)), activate(V2)) | | isNeList#(n____(V1, V2)) | → | U51#(isNeList(activate(V1)), activate(V2)) |
| isNeList#(n____(V1, V2)) | → | isNeList#(activate(V1)) | | isList#(n____(V1, V2)) | → | isList#(activate(V1)) |
| isNeList#(n____(V1, V2)) | → | isList#(activate(V1)) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U51#(tt, V2) | → | isList#(activate(V2)) | | isList#(V) | → | isNeList#(activate(V)) |
| U41#(tt, V2) | → | isNeList#(activate(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, U42, n__o, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U81, U52, U11, isQid, U31, n____, nil
Strategy
There are no SCCs!
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| U71#(tt, P) | → | isPal#(activate(P)) | | isPal#(V) | → | isNePal#(activate(V)) |
| isNePal#(n____(I, __(P, I))) | → | U71#(isQid(activate(I)), activate(P)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, U42, n__o, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U81, U52, U11, isQid, U31, n____, nil
Strategy
Polynomial Interpretation
- U11(x): 0
- U21(x,y): 0
- U22(x): 0
- U31(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x): 0
- U71(x,y): 0
- U71#(x,y): 2y + x
- U72(x): 0
- U81(x): 0
- __(x,y): y + x
- a: 2
- activate(x): x
- e: 1
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isNePal#(x): 2x + 1
- isPal(x): 0
- isPal#(x): 2x + 1
- isQid(x): x
- n____(x,y): y + x
- n__a: 2
- n__e: 1
- n__i: 1
- n__nil: 0
- n__o: 1
- n__u: 2
- nil: 0
- o: 1
- tt: 1
- u: 2
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| e | → | n__e | | activate(n__i) | → | i |
| a | → | n__a | | isQid(n__a) | → | tt |
| activate(n__nil) | → | nil | | isQid(n__i) | → | tt |
| activate(n____(X1, X2)) | → | __(X1, X2) | | isQid(n__u) | → | tt |
| activate(X) | → | X | | activate(n__u) | → | u |
| __(nil, X) | → | X | | isQid(n__e) | → | tt |
| i | → | n__i | | u | → | n__u |
| __(X1, X2) | → | n____(X1, X2) | | activate(n__o) | → | o |
| nil | → | n__nil | | o | → | n__o |
| isQid(n__o) | → | tt | | activate(n__a) | → | a |
| activate(n__e) | → | e |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNePal#(n____(I, __(P, I))) | → | U71#(isQid(activate(I)), activate(P)) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U71#(tt, P) | → | isPal#(activate(P)) | | isPal#(V) | → | isNePal#(activate(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, n__o, U42, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U52, U81, U11, U31, isQid, n____, nil
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(activate(V2))) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(activate(V2))) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(activate(V2))) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(activate(P))) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(activate(V))) |
| isList(n__nil) | → | tt | | isList(n____(V1, V2)) | → | U21(isList(activate(V1)), activate(V2)) |
| isNeList(V) | → | U31(isQid(activate(V))) | | isNeList(n____(V1, V2)) | → | U41(isList(activate(V1)), activate(V2)) |
| isNeList(n____(V1, V2)) | → | U51(isNeList(activate(V1)), activate(V2)) | | isNePal(V) | → | U61(isQid(activate(V))) |
| isNePal(n____(I, __(P, I))) | → | U71(isQid(activate(I)), activate(P)) | | isPal(V) | → | U81(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) |
| a | → | n__a | | e | → | n__e |
| i | → | n__i | | o | → | n__o |
| u | → | n__u | | activate(n__nil) | → | nil |
| activate(n____(X1, X2)) | → | __(X1, X2) | | activate(n__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, U61, U42, n__o, U41, isNePal, n__nil, U21, U22, n__e, e, n__a, a, o, isPal, n__i, i, U71, U72, u, U51, tt, U81, U52, U11, isQid, U31, n____, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |