YES
The TRS could be proven terminating. The proof took 904 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (192ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (370ms).
| – Problem 3 was processed with processor SubtermCriterion (3ms).
| | – Problem 9 was processed with processor DependencyGraph (0ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| | – Problem 10 was processed with processor DependencyGraph (9ms).
| – Problem 5 was processed with processor SubtermCriterion (3ms).
| – Problem 6 was processed with processor SubtermCriterion (2ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor PolynomialLinearRange4iUR (175ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| high#(n, add(m, x)) | → | le#(m, n) | | if_low#(true, n, add(m, x)) | → | low#(n, x) |
| quicksort#(add(n, x)) | → | high#(n, x) | | app#(add(n, x), y) | → | app#(x, y) |
| if_high#(true, n, add(m, x)) | → | high#(n, x) | | if_high#(false, n, add(m, x)) | → | high#(n, x) |
| quicksort#(add(n, x)) | → | app#(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) | | if_low#(false, n, add(m, x)) | → | low#(n, x) |
| quicksort#(add(n, x)) | → | quicksort#(low(n, x)) | | quot#(s(x), s(y)) | → | minus#(x, y) |
| quicksort#(add(n, x)) | → | low#(n, x) | | low#(n, add(m, x)) | → | if_low#(le(m, n), n, add(m, x)) |
| high#(n, add(m, x)) | → | if_high#(le(m, n), n, add(m, x)) | | le#(s(x), s(y)) | → | le#(x, y) |
| quot#(s(x), s(y)) | → | quot#(minus(x, y), s(y)) | | minus#(s(x), s(y)) | → | minus#(x, y) |
| low#(n, add(m, x)) | → | le#(m, n) | | quicksort#(add(n, x)) | → | quicksort#(high(n, x)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
The following SCCs where found
| le#(s(x), s(y)) → le#(x, y) |
| quot#(s(x), s(y)) → quot#(minus(x, y), s(y)) |
| app#(add(n, x), y) → app#(x, y) |
| minus#(s(x), s(y)) → minus#(x, y) |
| low#(n, add(m, x)) → if_low#(le(m, n), n, add(m, x)) | if_low#(true, n, add(m, x)) → low#(n, x) |
| if_low#(false, n, add(m, x)) → low#(n, x) |
| quicksort#(add(n, x)) → quicksort#(low(n, x)) | quicksort#(add(n, x)) → quicksort#(high(n, x)) |
| high#(n, add(m, x)) → if_high#(le(m, n), n, add(m, x)) | if_high#(true, n, add(m, x)) → high#(n, x) |
| if_high#(false, n, add(m, x)) → high#(n, x) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| quicksort#(add(n, x)) | → | quicksort#(low(n, x)) | | quicksort#(add(n, x)) | → | quicksort#(high(n, x)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
Polynomial Interpretation
- 0: 0
- add(x,y): 2y + 1
- app(x,y): 0
- false: 0
- high(x,y): 2y
- if_high(x,y,z): 2z
- if_low(x,y,z): z
- le(x,y): 0
- low(x,y): y
- minus(x,y): 0
- nil: 1
- quicksort(x): 0
- quicksort#(x): 2x
- quot(x,y): 0
- s(x): x + 3
- true: 0
Improved Usable rules
| low(n, nil) | → | nil | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | if_high(false, n, add(m, x)) | → | add(m, high(n, x)) |
| high(n, nil) | → | nil | | if_high(true, n, add(m, x)) | → | high(n, x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| quicksort#(add(n, x)) | → | quicksort#(low(n, x)) | | quicksort#(add(n, x)) | → | quicksort#(high(n, x)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| high#(n, add(m, x)) | → | if_high#(le(m, n), n, add(m, x)) | | if_high#(true, n, add(m, x)) | → | high#(n, x) |
| if_high#(false, n, add(m, x)) | → | high#(n, x) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
Projection
The following projection was used:
- π (high#): 2
- π (if_high#): 3
Thus, the following dependency pairs are removed:
| if_high#(true, n, add(m, x)) | → | high#(n, x) | | if_high#(false, n, add(m, x)) | → | high#(n, x) |
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| high#(n, add(m, x)) | → | if_high#(le(m, n), n, add(m, x)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quicksort, quot, nil
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| low#(n, add(m, x)) | → | if_low#(le(m, n), n, add(m, x)) | | if_low#(true, n, add(m, x)) | → | low#(n, x) |
| if_low#(false, n, add(m, x)) | → | low#(n, x) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
Projection
The following projection was used:
- π (if_low#): 3
- π (low#): 2
Thus, the following dependency pairs are removed:
| if_low#(true, n, add(m, x)) | → | low#(n, x) | | if_low#(false, n, add(m, x)) | → | low#(n, x) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| low#(n, add(m, x)) | → | if_low#(le(m, n), n, add(m, x)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quicksort, quot, nil
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| minus#(s(x), s(y)) | → | minus#(x, y) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus#(s(x), s(y)) | → | minus#(x, y) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(x), s(y)) | → | le#(x, y) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(x), s(y)) | → | le#(x, y) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| app#(add(n, x), y) | → | app#(x, y) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| app#(add(n, x), y) | → | app#(x, y) |
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| quot#(s(x), s(y)) | → | quot#(minus(x, y), s(y)) |
Rewrite Rules
| minus(x, 0) | → | x | | minus(s(x), s(y)) | → | minus(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(minus(x, y), s(y))) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | low(n, nil) | → | nil |
| low(n, add(m, x)) | → | if_low(le(m, n), n, add(m, x)) | | if_low(true, n, add(m, x)) | → | add(m, low(n, x)) |
| if_low(false, n, add(m, x)) | → | low(n, x) | | high(n, nil) | → | nil |
| high(n, add(m, x)) | → | if_high(le(m, n), n, add(m, x)) | | if_high(true, n, add(m, x)) | → | high(n, x) |
| if_high(false, n, add(m, x)) | → | add(m, high(n, x)) | | quicksort(nil) | → | nil |
| quicksort(add(n, x)) | → | app(quicksort(low(n, x)), add(n, quicksort(high(n, x)))) |
Original Signature
Termination of terms over the following signature is verified: app, minus, true, if_low, add, 0, s, le, false, if_high, high, low, quot, quicksort, nil
Strategy
Polynomial Interpretation
- 0: 2
- add(x,y): 0
- app(x,y): 0
- false: 0
- high(x,y): 0
- if_high(x,y,z): 0
- if_low(x,y,z): 0
- le(x,y): 0
- low(x,y): 0
- minus(x,y): 2x
- nil: 0
- quicksort(x): 0
- quot(x,y): 0
- quot#(x,y): 2x + 1
- s(x): 2x + 1
- true: 0
Improved Usable rules
| minus(s(x), s(y)) | → | minus(x, y) | | minus(x, 0) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| quot#(s(x), s(y)) | → | quot#(minus(x, y), s(y)) |