YES
The TRS could be proven terminating. The proof took 1118 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (124ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (668ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor PolynomialLinearRange4iUR (163ms).
| | – Problem 8 was processed with processor DependencyGraph (16ms).
| – Problem 6 was processed with processor SubtermCriterion (3ms).
| | – Problem 7 was processed with processor DependencyGraph (17ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| sort#(cons(n, x)) | → | min#(cons(n, x)) | | sort#(cons(n, x)) | → | sort#(replace(min(cons(n, x)), n, x)) |
| min#(cons(n, cons(m, x))) | → | le#(n, m) | | if_min#(true, cons(n, cons(m, x))) | → | min#(cons(n, x)) |
| if_min#(false, cons(n, cons(m, x))) | → | min#(cons(m, x)) | | replace#(n, m, cons(k, x)) | → | if_replace#(eq(n, k), n, m, cons(k, x)) |
| sort#(cons(n, x)) | → | replace#(min(cons(n, x)), n, x) | | le#(s(n), s(m)) | → | le#(n, m) |
| replace#(n, m, cons(k, x)) | → | eq#(n, k) | | min#(cons(n, cons(m, x))) | → | if_min#(le(n, m), cons(n, cons(m, x))) |
| if_replace#(false, n, m, cons(k, x)) | → | replace#(n, m, x) | | eq#(s(n), s(m)) | → | eq#(n, m) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
The following SCCs where found
| sort#(cons(n, x)) → sort#(replace(min(cons(n, x)), n, x)) |
| replace#(n, m, cons(k, x)) → if_replace#(eq(n, k), n, m, cons(k, x)) | if_replace#(false, n, m, cons(k, x)) → replace#(n, m, x) |
| le#(s(n), s(m)) → le#(n, m) |
| if_min#(false, cons(n, cons(m, x))) → min#(cons(m, x)) | if_min#(true, cons(n, cons(m, x))) → min#(cons(n, x)) |
| min#(cons(n, cons(m, x))) → if_min#(le(n, m), cons(n, cons(m, x))) |
| eq#(s(n), s(m)) → eq#(n, m) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sort#(cons(n, x)) | → | sort#(replace(min(cons(n, x)), n, x)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
Polynomial Interpretation
- 0: 1
- cons(x,y): 2y + 1
- eq(x,y): 0
- false: 3
- if_min(x,y): 0
- if_replace(x1,x2,x3,x4): x4
- le(x,y): 0
- min(x): x
- nil: 0
- replace(x,y,z): z
- s(x): 1
- sort(x): 0
- sort#(x): 2x
- true: 0
Improved Usable rules
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sort#(cons(n, x)) | → | sort#(replace(min(cons(n, x)), n, x)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(n), s(m)) | → | eq#(n, m) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(n), s(m)) | → | eq#(n, m) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(n), s(m)) | → | le#(n, m) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(n), s(m)) | → | le#(n, m) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| if_min#(false, cons(n, cons(m, x))) | → | min#(cons(m, x)) | | if_min#(true, cons(n, cons(m, x))) | → | min#(cons(n, x)) |
| min#(cons(n, cons(m, x))) | → | if_min#(le(n, m), cons(n, cons(m, x))) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- cons(x,y): 2y + 1
- eq(x,y): 0
- false: 0
- if_min(x,y): 0
- if_min#(x,y): y
- if_replace(x1,x2,x3,x4): 0
- le(x,y): x
- min(x): 0
- min#(x): x
- nil: 0
- replace(x,y,z): 0
- s(x): 2x + 1
- sort(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:
| if_min#(true, cons(n, cons(m, x))) | → | min#(cons(n, x)) | | if_min#(false, cons(n, cons(m, x))) | → | min#(cons(m, x)) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| min#(cons(n, cons(m, x))) | → | if_min#(le(n, m), cons(n, cons(m, x))) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
There are no SCCs!
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| replace#(n, m, cons(k, x)) | → | if_replace#(eq(n, k), n, m, cons(k, x)) | | if_replace#(false, n, m, cons(k, x)) | → | replace#(n, m, x) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
Projection
The following projection was used:
- π (replace#): 3
- π (if_replace#): 4
Thus, the following dependency pairs are removed:
| if_replace#(false, n, m, cons(k, x)) | → | replace#(n, m, x) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| replace#(n, m, cons(k, x)) | → | if_replace#(eq(n, k), n, m, cons(k, x)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(m)) | → | false |
| eq(s(n), 0) | → | false | | eq(s(n), s(m)) | → | eq(n, m) |
| le(0, m) | → | true | | le(s(n), 0) | → | false |
| le(s(n), s(m)) | → | le(n, m) | | min(cons(0, nil)) | → | 0 |
| min(cons(s(n), nil)) | → | s(n) | | min(cons(n, cons(m, x))) | → | if_min(le(n, m), cons(n, cons(m, x))) |
| if_min(true, cons(n, cons(m, x))) | → | min(cons(n, x)) | | if_min(false, cons(n, cons(m, x))) | → | min(cons(m, x)) |
| replace(n, m, nil) | → | nil | | replace(n, m, cons(k, x)) | → | if_replace(eq(n, k), n, m, cons(k, x)) |
| if_replace(true, n, m, cons(k, x)) | → | cons(m, x) | | if_replace(false, n, m, cons(k, x)) | → | cons(k, replace(n, m, x)) |
| sort(nil) | → | nil | | sort(cons(n, x)) | → | cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) |
Original Signature
Termination of terms over the following signature is verified: min, sort, true, if_replace, replace, if_min, 0, s, le, false, eq, nil, cons
Strategy
There are no SCCs!