YES
The TRS could be proven terminating. The proof took 2439 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (207ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (1080ms).
| | – Problem 8 was processed with processor PolynomialLinearRange4iUR (850ms).
| | | – Problem 10 was processed with processor DependencyGraph (7ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (95ms).
| | – Problem 9 was processed with processor DependencyGraph (1ms).
| – Problem 4 was processed with processor SubtermCriterion (9ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| | – Problem 7 was processed with processor DependencyGraph (0ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| replace#(N, M, cons(K, L)) | → | eq#(N, K) | | replace#(N, M, cons(K, L)) | → | ifrepl#(eq(N, K), N, M, cons(K, L)) |
| ifselsort#(false, cons(N, L)) | → | replace#(min(cons(N, L)), N, L) | | selsort#(cons(N, L)) | → | min#(cons(N, L)) |
| ifselsort#(false, cons(N, L)) | → | selsort#(replace(min(cons(N, L)), N, L)) | | selsort#(cons(N, L)) | → | ifselsort#(eq(N, min(cons(N, L))), cons(N, L)) |
| min#(cons(N, cons(M, L))) | → | ifmin#(le(N, M), cons(N, cons(M, L))) | | ifselsort#(true, cons(N, L)) | → | selsort#(L) |
| ifmin#(true, cons(N, cons(M, L))) | → | min#(cons(N, L)) | | le#(s(X), s(Y)) | → | le#(X, Y) |
| ifselsort#(false, cons(N, L)) | → | min#(cons(N, L)) | | eq#(s(X), s(Y)) | → | eq#(X, Y) |
| selsort#(cons(N, L)) | → | eq#(N, min(cons(N, L))) | | ifmin#(false, cons(N, cons(M, L))) | → | min#(cons(M, L)) |
| ifrepl#(false, N, M, cons(K, L)) | → | replace#(N, M, L) | | min#(cons(N, cons(M, L))) | → | le#(N, M) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, cons, eq, nil
Strategy
The following SCCs where found
| eq#(s(X), s(Y)) → eq#(X, Y) |
| ifselsort#(false, cons(N, L)) → selsort#(replace(min(cons(N, L)), N, L)) | selsort#(cons(N, L)) → ifselsort#(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort#(true, cons(N, L)) → selsort#(L) |
| replace#(N, M, cons(K, L)) → ifrepl#(eq(N, K), N, M, cons(K, L)) | ifrepl#(false, N, M, cons(K, L)) → replace#(N, M, L) |
| min#(cons(N, cons(M, L))) → ifmin#(le(N, M), cons(N, cons(M, L))) | ifmin#(false, cons(N, cons(M, L))) → min#(cons(M, L)) |
| ifmin#(true, cons(N, cons(M, L))) → min#(cons(N, L)) |
| le#(s(X), s(Y)) → le#(X, Y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ifselsort#(false, cons(N, L)) | → | selsort#(replace(min(cons(N, L)), N, L)) | | selsort#(cons(N, L)) | → | ifselsort#(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort#(true, cons(N, L)) | → | selsort#(L) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, cons, eq, nil
Strategy
Polynomial Interpretation
- 0: 1
- cons(x,y): y + x + 1
- eq(x,y): 1
- false: 0
- ifmin(x,y): 0
- ifrepl(x1,x2,x3,x4): x4 + x3 + 1
- ifselsort(x,y): 0
- ifselsort#(x,y): 2y
- le(x,y): 0
- min(x): 0
- nil: 0
- replace(x,y,z): z + y + 1
- s(x): 0
- selsort(x): 0
- selsort#(x): 2x
- true: 0
Improved Usable rules
| replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) | | replace(N, M, nil) | → | nil |
| ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) | | ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ifselsort#(true, cons(N, L)) | → | selsort#(L) |
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ifselsort#(false, cons(N, L)) | → | selsort#(replace(min(cons(N, L)), N, L)) | | selsort#(cons(N, L)) | → | ifselsort#(eq(N, min(cons(N, L))), cons(N, L)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, nil, cons, eq
Strategy
Polynomial Interpretation
- 0: 2
- cons(x,y): 2y + 1
- eq(x,y): y
- false: 0
- ifmin(x,y): y
- ifrepl(x1,x2,x3,x4): 2x4
- ifselsort(x,y): 0
- ifselsort#(x,y): 2y
- le(x,y): 2
- min(x): 2
- nil: 0
- replace(x,y,z): 2z
- s(x): 0
- selsort(x): 0
- selsort#(x): 2x
- true: 0
Improved Usable rules
| replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) | | replace(N, M, nil) | → | nil |
| ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) | | ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ifselsort#(false, cons(N, L)) | → | selsort#(replace(min(cons(N, L)), N, L)) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| selsort#(cons(N, L)) | → | ifselsort#(eq(N, min(cons(N, L))), cons(N, L)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, eq, nil, cons
Strategy
There are no SCCs!
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| min#(cons(N, cons(M, L))) | → | ifmin#(le(N, M), cons(N, cons(M, L))) | | ifmin#(false, cons(N, cons(M, L))) | → | min#(cons(M, L)) |
| ifmin#(true, cons(N, cons(M, L))) | → | min#(cons(N, L)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, cons, eq, nil
Strategy
Polynomial Interpretation
- 0: 2
- cons(x,y): y + 1
- eq(x,y): 0
- false: 0
- ifmin(x,y): 0
- ifmin#(x,y): y
- ifrepl(x1,x2,x3,x4): 0
- ifselsort(x,y): 0
- le(x,y): 0
- min(x): 0
- min#(x): x + 1
- nil: 0
- replace(x,y,z): 0
- s(x): 3x
- selsort(x): 0
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| min#(cons(N, cons(M, L))) | → | ifmin#(le(N, M), cons(N, cons(M, L))) |
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ifmin#(false, cons(N, cons(M, L))) | → | min#(cons(M, L)) | | ifmin#(true, cons(N, cons(M, L))) | → | min#(cons(N, L)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, nil, cons, eq
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(X), s(Y)) | → | eq#(X, Y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, cons, eq, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(X), s(Y)) | → | eq#(X, Y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| replace#(N, M, cons(K, L)) | → | ifrepl#(eq(N, K), N, M, cons(K, L)) | | ifrepl#(false, N, M, cons(K, L)) | → | replace#(N, M, L) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, cons, eq, nil
Strategy
Projection
The following projection was used:
- π (replace#): 3
- π (ifrepl#): 4
Thus, the following dependency pairs are removed:
| ifrepl#(false, N, M, cons(K, L)) | → | replace#(N, M, L) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| replace#(N, M, cons(K, L)) | → | ifrepl#(eq(N, K), N, M, cons(K, L)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, nil, cons, eq
Strategy
There are no SCCs!
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(X), s(Y)) | → | le#(X, Y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(Y)) | → | false |
| eq(s(X), 0) | → | false | | eq(s(X), s(Y)) | → | eq(X, Y) |
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(N), nil)) | → | s(N) | | min(cons(N, cons(M, L))) | → | ifmin(le(N, M), cons(N, cons(M, L))) |
| ifmin(true, cons(N, cons(M, L))) | → | min(cons(N, L)) | | ifmin(false, cons(N, cons(M, L))) | → | min(cons(M, L)) |
| replace(N, M, nil) | → | nil | | replace(N, M, cons(K, L)) | → | ifrepl(eq(N, K), N, M, cons(K, L)) |
| ifrepl(true, N, M, cons(K, L)) | → | cons(M, L) | | ifrepl(false, N, M, cons(K, L)) | → | cons(K, replace(N, M, L)) |
| selsort(nil) | → | nil | | selsort(cons(N, L)) | → | ifselsort(eq(N, min(cons(N, L))), cons(N, L)) |
| ifselsort(true, cons(N, L)) | → | cons(N, selsort(L)) | | ifselsort(false, cons(N, L)) | → | cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) |
Original Signature
Termination of terms over the following signature is verified: min, ifselsort, true, ifmin, replace, ifrepl, 0, s, le, selsort, false, cons, eq, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(X), s(Y)) | → | le#(X, Y) |