YES
The TRS could be proven terminating. The proof took 1094 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (200ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (93ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (319ms).
| | – Problem 4 was processed with processor DependencyGraph (29ms).
| | | – Problem 5 was processed with processor PolynomialLinearRange4 (17ms).
| | | | – Problem 6 was processed with processor PolynomialLinearRange4 (34ms).
| | | | | – Problem 7 was processed with processor PolynomialLinearRange4 (12ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| and#(tt, X) | → | T(X) | | isNePal#(__(I, __(P, I))) | → | isQid#(I) |
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | isNeList#(__(V1, V2)) | → | isNeList#(V1) |
| isNeList#(__(V1, V2)) | → | and#(isNeList(V1), isList(V2)) | | isList#(__(V1, V2)) | → | isList#(V1) |
| T(isList(x_1)) | → | T(x_1) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
| isNeList#(__(V1, V2)) | → | isList#(V1) | | T(isNeList(x_1)) | → | T(x_1) |
| T(isNeList(V2)) | → | isNeList#(V2) | | isList#(__(V1, V2)) | → | and#(isList(V1), isList(V2)) |
| isList#(V) | → | isNeList#(V) | | isNePal#(__(I, __(P, I))) | → | and#(isQid(I), isPal(P)) |
| T(isPal(P)) | → | isPal#(P) | | isNeList#(V) | → | isQid#(V) |
| isPal#(V) | → | isNePal#(V) | | T(isPal(x_1)) | → | T(x_1) |
| isNePal#(V) | → | isQid#(V) | | T(isList(V2)) | → | isList#(V2) |
| isNeList#(__(V1, V2)) | → | and#(isList(V1), isNeList(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | X |
| isList(V) | → | isNeList(V) | | isList(nil) | → | tt |
| isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) | | isNeList(V) | → | isQid(V) |
| isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) | | isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) |
| isNePal(V) | → | isQid(V) | | isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) |
| isPal(V) | → | isNePal(V) | | isPal(nil) | → | tt |
| isQid(a) | → | tt | | isQid(e) | → | tt |
| isQid(i) | → | tt | | isQid(o) | → | tt |
| isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, __, o, isPal, and, i, u, tt, isNePal, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(e) = μ(isNePal#) = μ(a) = μ(isNeList) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isQid#) = μ(isList#) = μ(T) = μ(u) = μ(tt) = μ(isNePal) = μ(isQid) = μ(isNeList#) = μ(nil) = ∅
μ(and#) = μ(and) = {1}
μ(__) = μ(__#) = {1, 2}
The following SCCs where found
| and#(tt, X) → T(X) | isNeList#(__(V1, V2)) → isNeList#(V1) |
| isNeList#(__(V1, V2)) → and#(isNeList(V1), isList(V2)) | isList#(__(V1, V2)) → isList#(V1) |
| T(isList(x_1)) → T(x_1) | isNeList#(__(V1, V2)) → isList#(V1) |
| T(isNeList(x_1)) → T(x_1) | T(isNeList(V2)) → isNeList#(V2) |
| isList#(__(V1, V2)) → and#(isList(V1), isList(V2)) | isList#(V) → isNeList#(V) |
| isNePal#(__(I, __(P, I))) → and#(isQid(I), isPal(P)) | T(isPal(P)) → isPal#(P) |
| T(isPal(x_1)) → T(x_1) | isPal#(V) → isNePal#(V) |
| T(isList(V2)) → isList#(V2) | isNeList#(__(V1, V2)) → and#(isList(V1), isNeList(V2)) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
Problem 2: PolynomialLinearRange4
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) | → | X |
| isList(V) | → | isNeList(V) | | isList(nil) | → | tt |
| isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) | | isNeList(V) | → | isQid(V) |
| isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) | | isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) |
| isNePal(V) | → | isQid(V) | | isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) |
| isPal(V) | → | isNePal(V) | | isPal(nil) | → | tt |
| isQid(a) | → | tt | | isQid(e) | → | tt |
| isQid(i) | → | tt | | isQid(o) | → | tt |
| isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, __, o, isPal, and, i, u, tt, isNePal, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(e) = μ(isNePal#) = μ(a) = μ(isNeList) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(isQid#) = μ(T) = μ(u) = μ(tt) = μ(isNePal) = μ(isQid) = μ(isNeList#) = μ(nil) = ∅
μ(and#) = μ(and) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- __(x,y): y + x + 1
- __#(x,y): x
- a: 0
- and(x,y): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- nil: 2
- o: 0
- tt: 0
- u: 0
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| and#(tt, X) | → | T(X) | | isNeList#(__(V1, V2)) | → | isNeList#(V1) |
| isNeList#(__(V1, V2)) | → | and#(isNeList(V1), isList(V2)) | | isList#(__(V1, V2)) | → | isList#(V1) |
| T(isList(x_1)) | → | T(x_1) | | isNeList#(__(V1, V2)) | → | isList#(V1) |
| T(isNeList(x_1)) | → | T(x_1) | | T(isNeList(V2)) | → | isNeList#(V2) |
| isList#(__(V1, V2)) | → | and#(isList(V1), isList(V2)) | | isList#(V) | → | isNeList#(V) |
| isNePal#(__(I, __(P, I))) | → | and#(isQid(I), isPal(P)) | | T(isPal(P)) | → | isPal#(P) |
| T(isPal(x_1)) | → | T(x_1) | | isPal#(V) | → | isNePal#(V) |
| T(isList(V2)) | → | isList#(V2) | | isNeList#(__(V1, V2)) | → | and#(isList(V1), isNeList(V2)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | X |
| isList(V) | → | isNeList(V) | | isList(nil) | → | tt |
| isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) | | isNeList(V) | → | isQid(V) |
| isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) | | isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) |
| isNePal(V) | → | isQid(V) | | isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) |
| isPal(V) | → | isNePal(V) | | isPal(nil) | → | tt |
| isQid(a) | → | tt | | isQid(e) | → | tt |
| isQid(i) | → | tt | | isQid(o) | → | tt |
| isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, __, o, isPal, and, i, u, tt, isNePal, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(e) = μ(isNePal#) = μ(a) = μ(isNeList) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(isQid#) = μ(T) = μ(u) = μ(tt) = μ(isNePal) = μ(isQid) = μ(isNeList#) = μ(nil) = ∅
μ(and#) = μ(and) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- T(x): x
- __(x,y): y + 2x + 1
- a: 2
- and(x,y): y + 2x + 2
- and#(x,y): y
- e: 0
- i: 2
- isList(x): 2x
- isList#(x): 2x
- isNeList(x): 2x
- isNeList#(x): 2x
- isNePal(x): x
- isNePal#(x): x
- isPal(x): 2x
- isPal#(x): x
- isQid(x): x
- nil: 1
- o: 0
- tt: 0
- u: 0
Standard Usable rules
| isQid(i) | → | tt | | __(__(X, Y), Z) | → | __(X, __(Y, Z)) |
| isQid(e) | → | tt | | __(X, nil) | → | X |
| isQid(u) | → | tt | | isList(V) | → | isNeList(V) |
| isNeList(V) | → | isQid(V) | | isNePal(V) | → | isQid(V) |
| isPal(nil) | → | tt | | isList(nil) | → | tt |
| isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) | | isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) |
| isPal(V) | → | isNePal(V) | | isQid(a) | → | tt |
| and(tt, X) | → | X | | __(nil, X) | → | X |
| isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) | | isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) |
| isQid(o) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNeList#(__(V1, V2)) | → | isNeList#(V1) | | isNeList#(__(V1, V2)) | → | and#(isNeList(V1), isList(V2)) |
| isList#(__(V1, V2)) | → | isList#(V1) | | isNeList#(__(V1, V2)) | → | isList#(V1) |
| isList#(__(V1, V2)) | → | and#(isList(V1), isList(V2)) | | isNePal#(__(I, __(P, I))) | → | and#(isQid(I), isPal(P)) |
| isNeList#(__(V1, V2)) | → | and#(isList(V1), isNeList(V2)) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(V) | → | isNeList#(V) | | and#(tt, X) | → | T(X) |
| T(isPal(P)) | → | isPal#(P) | | isPal#(V) | → | isNePal#(V) |
| T(isPal(x_1)) | → | T(x_1) | | T(isList(x_1)) | → | T(x_1) |
| T(isList(V2)) | → | isList#(V2) | | T(isNeList(x_1)) | → | T(x_1) |
| T(isNeList(V2)) | → | isNeList#(V2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | X |
| isList(V) | → | isNeList(V) | | isList(nil) | → | tt |
| isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) | | isNeList(V) | → | isQid(V) |
| isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) | | isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) |
| isNePal(V) | → | isQid(V) | | isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) |
| isPal(V) | → | isNePal(V) | | isPal(nil) | → | tt |
| isQid(a) | → | tt | | isQid(e) | → | tt |
| isQid(i) | → | tt | | isQid(o) | → | tt |
| isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, __, o, isPal, and, i, u, tt, isNePal, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(e) = μ(isNePal#) = μ(a) = μ(isNeList) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isQid#) = μ(isList#) = μ(T) = μ(u) = μ(tt) = μ(isNePal) = μ(isQid) = μ(isNeList#) = μ(nil) = ∅
μ(and#) = μ(and) = {1}
μ(__) = μ(__#) = {1, 2}
The following SCCs where found
| T(isPal(x_1)) → T(x_1) | T(isList(x_1)) → T(x_1) |
| T(isNeList(x_1)) → T(x_1) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(isPal(x_1)) | → | T(x_1) | | T(isList(x_1)) | → | T(x_1) |
| T(isNeList(x_1)) | → | T(x_1) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | X |
| isList(V) | → | isNeList(V) | | isList(nil) | → | tt |
| isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) | | isNeList(V) | → | isQid(V) |
| isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) | | isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) |
| isNePal(V) | → | isQid(V) | | isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) |
| isPal(V) | → | isNePal(V) | | isPal(nil) | → | tt |
| isQid(a) | → | tt | | isQid(e) | → | tt |
| isQid(i) | → | tt | | isQid(o) | → | tt |
| isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, __, o, isPal, and, i, u, tt, isNePal, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(e) = μ(isNePal#) = μ(a) = μ(isNeList) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(isQid#) = μ(T) = μ(u) = μ(tt) = μ(isNePal) = μ(isQid) = μ(isNeList#) = μ(nil) = ∅
μ(and#) = μ(and) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- T(x): 2x
- __(x,y): 0
- a: 0
- and(x,y): 0
- e: 0
- i: 0
- isList(x): x + 1
- isNeList(x): x
- isNePal(x): 0
- isPal(x): 2x
- isQid(x): 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:
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(isPal(x_1)) | → | T(x_1) | | T(isNeList(x_1)) | → | T(x_1) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | X |
| isList(V) | → | isNeList(V) | | isList(nil) | → | tt |
| isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) | | isNeList(V) | → | isQid(V) |
| isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) | | isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) |
| isNePal(V) | → | isQid(V) | | isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) |
| isPal(V) | → | isNePal(V) | | isPal(nil) | → | tt |
| isQid(a) | → | tt | | isQid(e) | → | tt |
| isQid(i) | → | tt | | isQid(o) | → | tt |
| isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, __, o, isPal, and, i, u, tt, isNePal, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(e) = μ(isNePal#) = μ(a) = μ(isNeList) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isQid#) = μ(isList#) = μ(T) = μ(u) = μ(tt) = μ(isNePal) = μ(isQid) = μ(isNeList#) = μ(nil) = ∅
μ(and#) = μ(and) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- T(x): 2x
- __(x,y): 0
- a: 0
- and(x,y): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): x
- isNePal(x): 0
- isPal(x): x + 1
- isQid(x): 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:
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(isNeList(x_1)) | → | T(x_1) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | and(tt, X) | → | X |
| isList(V) | → | isNeList(V) | | isList(nil) | → | tt |
| isList(__(V1, V2)) | → | and(isList(V1), isList(V2)) | | isNeList(V) | → | isQid(V) |
| isNeList(__(V1, V2)) | → | and(isList(V1), isNeList(V2)) | | isNeList(__(V1, V2)) | → | and(isNeList(V1), isList(V2)) |
| isNePal(V) | → | isQid(V) | | isNePal(__(I, __(P, I))) | → | and(isQid(I), isPal(P)) |
| isPal(V) | → | isNePal(V) | | isPal(nil) | → | tt |
| isQid(a) | → | tt | | isQid(e) | → | tt |
| isQid(i) | → | tt | | isQid(o) | → | tt |
| isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, __, o, isPal, and, i, u, tt, isNePal, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(e) = μ(isNePal#) = μ(a) = μ(isNeList) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(isQid#) = μ(T) = μ(u) = μ(tt) = μ(isNePal) = μ(isQid) = μ(isNeList#) = μ(nil) = ∅
μ(and#) = μ(and) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- T(x): x
- __(x,y): 0
- a: 0
- and(x,y): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): x + 1
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 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:
| T(isNeList(x_1)) | → | T(x_1) |