YES
The TRS could be proven terminating. The proof took 1775 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (35ms).
| – Problem 2 was processed with processor PolynomialOrderingProcessor (810ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (88ms).
| – Problem 4 was processed with processor SubtermCriterion (5ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| bubble#(.(x, .(y, z))) | → | bubble#(.(y, z)) | | bsort#(.(x, y)) | → | butlast#(bubble(.(x, y))) |
| last#(.(x, .(y, z))) | → | last#(.(y, z)) | | bsort#(.(x, y)) | → | last#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) |
| bubble#(.(x, .(y, z))) | → | bubble#(.(x, z)) | | butlast#(.(x, .(y, z))) | → | butlast#(.(y, z)) |
| bsort#(.(x, y)) | → | bsort#(butlast(bubble(.(x, y)))) | | bsort#(.(x, y)) | → | bubble#(.(x, y)) |
Rewrite Rules
| bsort(nil) | → | nil | | bsort(.(x, y)) | → | last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) |
| bubble(nil) | → | nil | | bubble(.(x, nil)) | → | .(x, nil) |
| bubble(.(x, .(y, z))) | → | if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) | | last(nil) | → | 0 |
| last(.(x, nil)) | → | x | | last(.(x, .(y, z))) | → | last(.(y, z)) |
| butlast(nil) | → | nil | | butlast(.(x, nil)) | → | nil |
| butlast(.(x, .(y, z))) | → | .(x, butlast(.(y, z))) |
Original Signature
Termination of terms over the following signature is verified: bsort, bubble, 0, last, if, <=, ., butlast, nil
Strategy
The following SCCs where found
| last#(.(x, .(y, z))) → last#(.(y, z)) |
| butlast#(.(x, .(y, z))) → butlast#(.(y, z)) |
| bsort#(.(x, y)) → bsort#(butlast(bubble(.(x, y)))) |
| bubble#(.(x, .(y, z))) → bubble#(.(y, z)) | bubble#(.(x, .(y, z))) → bubble#(.(x, z)) |
Problem 2: PolynomialOrderingProcessor
Dependency Pair Problem
Dependency Pairs
| bsort#(.(x, y)) | → | bsort#(butlast(bubble(.(x, y)))) |
Rewrite Rules
| bsort(nil) | → | nil | | bsort(.(x, y)) | → | last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) |
| bubble(nil) | → | nil | | bubble(.(x, nil)) | → | .(x, nil) |
| bubble(.(x, .(y, z))) | → | if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) | | last(nil) | → | 0 |
| last(.(x, nil)) | → | x | | last(.(x, .(y, z))) | → | last(.(y, z)) |
| butlast(nil) | → | nil | | butlast(.(x, nil)) | → | nil |
| butlast(.(x, .(y, z))) | → | .(x, butlast(.(y, z))) |
Original Signature
Termination of terms over the following signature is verified: bsort, bubble, 0, last, if, <=, ., butlast, nil
Strategy
Polynomial Interpretation
- .(x,y): y + 1
- 0: -2
- <=(x,y): -1
- bsort(x): -2
- bsort#(x): 4x - 1
- bubble(x): 1
- butlast(x): 2x - 2
- if(x,y,z): -2
- last(x): -2
- nil: -2
Improved Usable rules
| butlast(.(x, .(y, z))) | → | .(x, butlast(.(y, z))) | | bubble(.(x, nil)) | → | .(x, nil) |
| butlast(.(x, nil)) | → | nil | | butlast(nil) | → | nil |
| bubble(.(x, .(y, z))) | → | if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) | | bubble(nil) | → | nil |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| bsort#(.(x, y)) | → | bsort#(butlast(bubble(.(x, y)))) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| bubble#(.(x, .(y, z))) | → | bubble#(.(y, z)) | | bubble#(.(x, .(y, z))) | → | bubble#(.(x, z)) |
Rewrite Rules
| bsort(nil) | → | nil | | bsort(.(x, y)) | → | last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) |
| bubble(nil) | → | nil | | bubble(.(x, nil)) | → | .(x, nil) |
| bubble(.(x, .(y, z))) | → | if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) | | last(nil) | → | 0 |
| last(.(x, nil)) | → | x | | last(.(x, .(y, z))) | → | last(.(y, z)) |
| butlast(nil) | → | nil | | butlast(.(x, nil)) | → | nil |
| butlast(.(x, .(y, z))) | → | .(x, butlast(.(y, z))) |
Original Signature
Termination of terms over the following signature is verified: bsort, bubble, 0, last, if, <=, ., butlast, nil
Strategy
Polynomial Interpretation
- .(x,y): y + 1
- 0: 0
- <=(x,y): 0
- bsort(x): 0
- bubble(x): 0
- bubble#(x): x
- butlast(x): 0
- if(x,y,z): 0
- last(x): 0
- nil: 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:
| bubble#(.(x, .(y, z))) | → | bubble#(.(y, z)) | | bubble#(.(x, .(y, z))) | → | bubble#(.(x, z)) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| butlast#(.(x, .(y, z))) | → | butlast#(.(y, z)) |
Rewrite Rules
| bsort(nil) | → | nil | | bsort(.(x, y)) | → | last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) |
| bubble(nil) | → | nil | | bubble(.(x, nil)) | → | .(x, nil) |
| bubble(.(x, .(y, z))) | → | if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) | | last(nil) | → | 0 |
| last(.(x, nil)) | → | x | | last(.(x, .(y, z))) | → | last(.(y, z)) |
| butlast(nil) | → | nil | | butlast(.(x, nil)) | → | nil |
| butlast(.(x, .(y, z))) | → | .(x, butlast(.(y, z))) |
Original Signature
Termination of terms over the following signature is verified: bsort, bubble, 0, last, if, <=, ., butlast, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| butlast#(.(x, .(y, z))) | → | butlast#(.(y, z)) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| last#(.(x, .(y, z))) | → | last#(.(y, z)) |
Rewrite Rules
| bsort(nil) | → | nil | | bsort(.(x, y)) | → | last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))) |
| bubble(nil) | → | nil | | bubble(.(x, nil)) | → | .(x, nil) |
| bubble(.(x, .(y, z))) | → | if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z)))) | | last(nil) | → | 0 |
| last(.(x, nil)) | → | x | | last(.(x, .(y, z))) | → | last(.(y, z)) |
| butlast(nil) | → | nil | | butlast(.(x, nil)) | → | nil |
| butlast(.(x, .(y, z))) | → | .(x, butlast(.(y, z))) |
Original Signature
Termination of terms over the following signature is verified: bsort, bubble, 0, last, if, <=, ., butlast, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| last#(.(x, .(y, z))) | → | last#(.(y, z)) |