YES
The TRS could be proven terminating. The proof took 710 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (134ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (351ms).
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| | – Problem 7 was processed with processor DependencyGraph (12ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| | – Problem 8 was processed with processor DependencyGraph (25ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| high#(N, cons(M, L)) | → | ifhigh#(le(M, N), N, cons(M, L)) | | quicksort#(cons(N, L)) | → | quicksort#(high(N, L)) |
| quicksort#(cons(N, L)) | → | low#(N, L) | | le#(s(X), s(Y)) | → | le#(X, Y) |
| quicksort#(cons(N, L)) | → | app#(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) | | ifhigh#(true, N, cons(M, L)) | → | high#(N, L) |
| quicksort#(cons(N, L)) | → | quicksort#(low(N, L)) | | low#(N, cons(M, L)) | → | le#(M, N) |
| iflow#(false, N, cons(M, L)) | → | low#(N, L) | | low#(N, cons(M, L)) | → | iflow#(le(M, N), N, cons(M, L)) |
| iflow#(true, N, cons(M, L)) | → | low#(N, L) | | quicksort#(cons(N, L)) | → | high#(N, L) |
| app#(cons(N, L), Y) | → | app#(L, Y) | | ifhigh#(false, N, cons(M, L)) | → | high#(N, L) |
| high#(N, cons(M, L)) | → | le#(M, N) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
The following SCCs where found
| ifhigh#(true, N, cons(M, L)) → high#(N, L) | high#(N, cons(M, L)) → ifhigh#(le(M, N), N, cons(M, L)) |
| ifhigh#(false, N, cons(M, L)) → high#(N, L) |
| iflow#(false, N, cons(M, L)) → low#(N, L) | iflow#(true, N, cons(M, L)) → low#(N, L) |
| low#(N, cons(M, L)) → iflow#(le(M, N), N, cons(M, L)) |
| quicksort#(cons(N, L)) → quicksort#(low(N, L)) | quicksort#(cons(N, L)) → quicksort#(high(N, L)) |
| app#(cons(N, L), Y) → app#(L, Y) |
| le#(s(X), s(Y)) → le#(X, Y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| quicksort#(cons(N, L)) | → | quicksort#(low(N, L)) | | quicksort#(cons(N, L)) | → | quicksort#(high(N, L)) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- app(x,y): 0
- cons(x,y): 2y + 1
- false: 0
- high(x,y): 2y
- ifhigh(x,y,z): 2z
- iflow(x,y,z): 2z
- le(x,y): 1
- low(x,y): 2y
- nil: 0
- quicksort(x): 0
- quicksort#(x): 2x
- s(x): 3
- true: 0
Improved Usable rules
| ifhigh(true, N, cons(M, L)) | → | high(N, L) | | iflow(false, N, cons(M, L)) | → | low(N, L) |
| high(N, nil) | → | nil | | high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) |
| low(N, nil) | → | nil | | ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) |
| iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) | | low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| quicksort#(cons(N, L)) | → | quicksort#(low(N, L)) | | quicksort#(cons(N, L)) | → | quicksort#(high(N, L)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ifhigh#(true, N, cons(M, L)) | → | high#(N, L) | | high#(N, cons(M, L)) | → | ifhigh#(le(M, N), N, cons(M, L)) |
| ifhigh#(false, N, cons(M, L)) | → | high#(N, L) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
Projection
The following projection was used:
- π (high#): 2
- π (ifhigh#): 3
Thus, the following dependency pairs are removed:
| ifhigh#(true, N, cons(M, L)) | → | high#(N, L) | | ifhigh#(false, N, cons(M, L)) | → | high#(N, L) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| high#(N, cons(M, L)) | → | ifhigh#(le(M, N), N, cons(M, L)) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| iflow#(false, N, cons(M, L)) | → | low#(N, L) | | iflow#(true, N, cons(M, L)) | → | low#(N, L) |
| low#(N, cons(M, L)) | → | iflow#(le(M, N), N, cons(M, L)) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
Projection
The following projection was used:
- π (iflow#): 3
- π (low#): 2
Thus, the following dependency pairs are removed:
| iflow#(false, N, cons(M, L)) | → | low#(N, L) | | iflow#(true, N, cons(M, L)) | → | low#(N, L) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| low#(N, cons(M, L)) | → | iflow#(le(M, N), N, cons(M, L)) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| app#(cons(N, L), Y) | → | app#(L, Y) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| app#(cons(N, L), Y) | → | app#(L, Y) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(X), s(Y)) | → | le#(X, Y) |
Rewrite Rules
| le(0, Y) | → | true | | le(s(X), 0) | → | false |
| le(s(X), s(Y)) | → | le(X, Y) | | app(nil, Y) | → | Y |
| app(cons(N, L), Y) | → | cons(N, app(L, Y)) | | low(N, nil) | → | nil |
| low(N, cons(M, L)) | → | iflow(le(M, N), N, cons(M, L)) | | iflow(true, N, cons(M, L)) | → | cons(M, low(N, L)) |
| iflow(false, N, cons(M, L)) | → | low(N, L) | | high(N, nil) | → | nil |
| high(N, cons(M, L)) | → | ifhigh(le(M, N), N, cons(M, L)) | | ifhigh(true, N, cons(M, L)) | → | high(N, L) |
| ifhigh(false, N, cons(M, L)) | → | cons(M, high(N, L)) | | quicksort(nil) | → | nil |
| quicksort(cons(N, L)) | → | app(quicksort(low(N, L)), cons(N, quicksort(high(N, L)))) |
Original Signature
Termination of terms over the following signature is verified: app, ifhigh, iflow, true, 0, le, s, false, high, low, quicksort, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(X), s(Y)) | → | le#(X, Y) |