YES
The TRS could be proven terminating. The proof took 645 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (91ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (293ms).
| | – Problem 6 was processed with processor DependencyGraph (34ms).
| – Problem 4 was processed with processor SubtermCriterion (7ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| split#(N, add(M, Y)) | → | f_1#(split(N, Y), N, M, Y) | | qsort#(add(N, X)) | → | split#(N, X) |
| f_3#(pair(Y, Z), N, X) | → | qsort#(Z) | | append#(add(N, X), Y) | → | append#(X, Y) |
| f_1#(pair(X, Z), N, M, Y) | → | lt#(N, M) | | f_3#(pair(Y, Z), N, X) | → | append#(qsort(Y), add(X, qsort(Z))) |
| f_3#(pair(Y, Z), N, X) | → | qsort#(Y) | | split#(N, add(M, Y)) | → | split#(N, Y) |
| qsort#(add(N, X)) | → | f_3#(split(N, X), N, X) | | lt#(s(X), s(Y)) | → | lt#(X, Y) |
| f_1#(pair(X, Z), N, M, Y) | → | f_2#(lt(N, M), N, M, Y, X, Z) |
Rewrite Rules
| lt(0, s(X)) | → | true | | lt(s(X), 0) | → | false |
| lt(s(X), s(Y)) | → | lt(X, Y) | | append(nil, Y) | → | Y |
| append(add(N, X), Y) | → | add(N, append(X, Y)) | | split(N, nil) | → | pair(nil, nil) |
| split(N, add(M, Y)) | → | f_1(split(N, Y), N, M, Y) | | f_1(pair(X, Z), N, M, Y) | → | f_2(lt(N, M), N, M, Y, X, Z) |
| f_2(true, N, M, Y, X, Z) | → | pair(X, add(M, Z)) | | f_2(false, N, M, Y, X, Z) | → | pair(add(M, X), Z) |
| qsort(nil) | → | nil | | qsort(add(N, X)) | → | f_3(split(N, X), N, X) |
| f_3(pair(Y, Z), N, X) | → | append(qsort(Y), add(X, qsort(Z))) |
Original Signature
Termination of terms over the following signature is verified: append, pair, true, lt, add, 0, s, false, split, qsort, f_2, f_1, nil, f_3
Strategy
The following SCCs where found
| append#(add(N, X), Y) → append#(X, Y) |
| f_3#(pair(Y, Z), N, X) → qsort#(Z) | f_3#(pair(Y, Z), N, X) → qsort#(Y) |
| qsort#(add(N, X)) → f_3#(split(N, X), N, X) |
| split#(N, add(M, Y)) → split#(N, Y) |
| lt#(s(X), s(Y)) → lt#(X, Y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| lt#(s(X), s(Y)) | → | lt#(X, Y) |
Rewrite Rules
| lt(0, s(X)) | → | true | | lt(s(X), 0) | → | false |
| lt(s(X), s(Y)) | → | lt(X, Y) | | append(nil, Y) | → | Y |
| append(add(N, X), Y) | → | add(N, append(X, Y)) | | split(N, nil) | → | pair(nil, nil) |
| split(N, add(M, Y)) | → | f_1(split(N, Y), N, M, Y) | | f_1(pair(X, Z), N, M, Y) | → | f_2(lt(N, M), N, M, Y, X, Z) |
| f_2(true, N, M, Y, X, Z) | → | pair(X, add(M, Z)) | | f_2(false, N, M, Y, X, Z) | → | pair(add(M, X), Z) |
| qsort(nil) | → | nil | | qsort(add(N, X)) | → | f_3(split(N, X), N, X) |
| f_3(pair(Y, Z), N, X) | → | append(qsort(Y), add(X, qsort(Z))) |
Original Signature
Termination of terms over the following signature is verified: append, pair, true, lt, add, 0, s, false, split, qsort, f_2, f_1, nil, f_3
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| lt#(s(X), s(Y)) | → | lt#(X, Y) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f_3#(pair(Y, Z), N, X) | → | qsort#(Z) | | f_3#(pair(Y, Z), N, X) | → | qsort#(Y) |
| qsort#(add(N, X)) | → | f_3#(split(N, X), N, X) |
Rewrite Rules
| lt(0, s(X)) | → | true | | lt(s(X), 0) | → | false |
| lt(s(X), s(Y)) | → | lt(X, Y) | | append(nil, Y) | → | Y |
| append(add(N, X), Y) | → | add(N, append(X, Y)) | | split(N, nil) | → | pair(nil, nil) |
| split(N, add(M, Y)) | → | f_1(split(N, Y), N, M, Y) | | f_1(pair(X, Z), N, M, Y) | → | f_2(lt(N, M), N, M, Y, X, Z) |
| f_2(true, N, M, Y, X, Z) | → | pair(X, add(M, Z)) | | f_2(false, N, M, Y, X, Z) | → | pair(add(M, X), Z) |
| qsort(nil) | → | nil | | qsort(add(N, X)) | → | f_3(split(N, X), N, X) |
| f_3(pair(Y, Z), N, X) | → | append(qsort(Y), add(X, qsort(Z))) |
Original Signature
Termination of terms over the following signature is verified: append, pair, true, lt, add, 0, s, false, split, qsort, f_2, f_1, nil, f_3
Strategy
Polynomial Interpretation
- 0: 1
- add(x,y): 2y + 2
- append(x,y): 0
- f_1(x1,x2,x3,x4): 2x1 + 2
- f_2(x1,x2,x3,x4,x5,x6): 2x6 + 2x5 + 2
- f_3(x,y,z): 0
- f_3#(x,y,z): x
- false: 1
- lt(x,y): 0
- nil: 0
- pair(x,y): y + x
- qsort(x): 0
- qsort#(x): x
- s(x): 0
- split(x,y): y
- true: 1
Improved Usable rules
| f_2(true, N, M, Y, X, Z) | → | pair(X, add(M, Z)) | | split(N, add(M, Y)) | → | f_1(split(N, Y), N, M, Y) |
| f_1(pair(X, Z), N, M, Y) | → | f_2(lt(N, M), N, M, Y, X, Z) | | split(N, nil) | → | pair(nil, nil) |
| f_2(false, N, M, Y, X, Z) | → | pair(add(M, X), Z) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| qsort#(add(N, X)) | → | f_3#(split(N, X), N, X) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f_3#(pair(Y, Z), N, X) | → | qsort#(Z) | | f_3#(pair(Y, Z), N, X) | → | qsort#(Y) |
Rewrite Rules
| lt(0, s(X)) | → | true | | lt(s(X), 0) | → | false |
| lt(s(X), s(Y)) | → | lt(X, Y) | | append(nil, Y) | → | Y |
| append(add(N, X), Y) | → | add(N, append(X, Y)) | | split(N, nil) | → | pair(nil, nil) |
| split(N, add(M, Y)) | → | f_1(split(N, Y), N, M, Y) | | f_1(pair(X, Z), N, M, Y) | → | f_2(lt(N, M), N, M, Y, X, Z) |
| f_2(true, N, M, Y, X, Z) | → | pair(X, add(M, Z)) | | f_2(false, N, M, Y, X, Z) | → | pair(add(M, X), Z) |
| qsort(nil) | → | nil | | qsort(add(N, X)) | → | f_3(split(N, X), N, X) |
| f_3(pair(Y, Z), N, X) | → | append(qsort(Y), add(X, qsort(Z))) |
Original Signature
Termination of terms over the following signature is verified: append, pair, true, lt, add, 0, s, false, split, qsort, f_2, f_1, f_3, nil
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| split#(N, add(M, Y)) | → | split#(N, Y) |
Rewrite Rules
| lt(0, s(X)) | → | true | | lt(s(X), 0) | → | false |
| lt(s(X), s(Y)) | → | lt(X, Y) | | append(nil, Y) | → | Y |
| append(add(N, X), Y) | → | add(N, append(X, Y)) | | split(N, nil) | → | pair(nil, nil) |
| split(N, add(M, Y)) | → | f_1(split(N, Y), N, M, Y) | | f_1(pair(X, Z), N, M, Y) | → | f_2(lt(N, M), N, M, Y, X, Z) |
| f_2(true, N, M, Y, X, Z) | → | pair(X, add(M, Z)) | | f_2(false, N, M, Y, X, Z) | → | pair(add(M, X), Z) |
| qsort(nil) | → | nil | | qsort(add(N, X)) | → | f_3(split(N, X), N, X) |
| f_3(pair(Y, Z), N, X) | → | append(qsort(Y), add(X, qsort(Z))) |
Original Signature
Termination of terms over the following signature is verified: append, pair, true, lt, add, 0, s, false, split, qsort, f_2, f_1, nil, f_3
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| split#(N, add(M, Y)) | → | split#(N, Y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| append#(add(N, X), Y) | → | append#(X, Y) |
Rewrite Rules
| lt(0, s(X)) | → | true | | lt(s(X), 0) | → | false |
| lt(s(X), s(Y)) | → | lt(X, Y) | | append(nil, Y) | → | Y |
| append(add(N, X), Y) | → | add(N, append(X, Y)) | | split(N, nil) | → | pair(nil, nil) |
| split(N, add(M, Y)) | → | f_1(split(N, Y), N, M, Y) | | f_1(pair(X, Z), N, M, Y) | → | f_2(lt(N, M), N, M, Y, X, Z) |
| f_2(true, N, M, Y, X, Z) | → | pair(X, add(M, Z)) | | f_2(false, N, M, Y, X, Z) | → | pair(add(M, X), Z) |
| qsort(nil) | → | nil | | qsort(add(N, X)) | → | f_3(split(N, X), N, X) |
| f_3(pair(Y, Z), N, X) | → | append(qsort(Y), add(X, qsort(Z))) |
Original Signature
Termination of terms over the following signature is verified: append, pair, true, lt, add, 0, s, false, split, qsort, f_2, f_1, nil, f_3
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| append#(add(N, X), Y) | → | append#(X, Y) |