TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (534ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (348ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (3809ms), DependencyGraph (5ms), ReductionPairSAT (11632ms), DependencyGraph (3ms), SizeChangePrinciple (130ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| | – Problem 8 was processed with processor DependencyGraph (1ms).
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (4410ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (5ms), ReductionPairSAT (9267ms), DependencyGraph (4ms), SizeChangePrinciple (timeout)].
| – Problem 5 was processed with processor SubtermCriterion (5ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| | – Problem 9 was processed with processor DependencyGraph (1ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| averIter#(x, y, z) | → | ifIter#(ge(x, y), x, y, z) | | ifIter#(false, x, y, z) | → | averIter#(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, ge, if_low, ifquick, if, false, head, cons, averIter, app, append, plus, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Open Dependency Pair Problem 4
Dependency Pairs
| ifquick#(false, x) | → | quicksort#(low(head(x), tail(x))) | | ifquick#(false, x) | → | quicksort#(high(head(x), tail(x))) |
| quicksort#(x) | → | ifquick#(isempty(x), x) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, ge, if_low, ifquick, if, false, head, cons, averIter, app, append, plus, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| average#(x, y) | → | if#(ge(x, y), x, y) | | average#(x, y) | → | ge#(x, y) |
| averIter#(x, y, z) | → | ifIter#(ge(x, y), x, y, z) | | ifquick#(false, x) | → | high#(head(x), tail(x)) |
| ifquick#(false, x) | → | tail#(x) | | ifquick#(false, x) | → | head#(x) |
| ifquick#(false, x) | → | low#(head(x), tail(x)) | | if_low#(true, n, cons(m, x)) | → | low#(n, x) |
| plus#(s(x), y) | → | plus#(x, y) | | ifIter#(false, x, y, z) | → | plus#(x, s(s(s(0)))) |
| ifIter#(false, x, y, z) | → | plus#(z, s(0)) | | low#(n, cons(m, x)) | → | if_low#(ge(m, n), n, cons(m, x)) |
| if_low#(false, n, cons(m, x)) | → | low#(n, x) | | if_high#(true, n, cons(m, x)) | → | average#(m, m) |
| if#(true, x, y) | → | averIter#(y, x, y) | | ifquick#(false, x) | → | quicksort#(high(head(x), tail(x))) |
| high#(n, cons(m, x)) | → | ge#(m, n) | | quicksort#(x) | → | ifquick#(isempty(x), x) |
| ifIter#(false, x, y, z) | → | averIter#(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) | | if#(false, x, y) | → | averIter#(x, y, x) |
| averIter#(x, y, z) | → | ge#(x, y) | | ifquick#(false, x) | → | quicksort#(low(head(x), tail(x))) |
| if_high#(true, n, cons(m, x)) | → | high#(n, x) | | ifquick#(false, x) | → | append#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) |
| quicksort#(x) | → | isempty#(x) | | ge#(s(x), s(y)) | → | ge#(x, y) |
| high#(n, cons(m, x)) | → | if_high#(ge(m, n), n, cons(m, x)) | | if_high#(false, n, cons(m, x)) | → | high#(n, x) |
| ifIter#(false, x, y, z) | → | plus#(y, s(0)) | | low#(n, cons(m, x)) | → | ge#(m, n) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, if_low, ge, ifquick, if, false, head, cons, averIter, plus, append, app, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Strategy
The following SCCs where found
| if_high#(true, n, cons(m, x)) → high#(n, x) | high#(n, cons(m, x)) → if_high#(ge(m, n), n, cons(m, x)) |
| if_high#(false, n, cons(m, x)) → high#(n, x) |
| if_low#(true, n, cons(m, x)) → low#(n, x) | low#(n, cons(m, x)) → if_low#(ge(m, n), n, cons(m, x)) |
| if_low#(false, n, cons(m, x)) → low#(n, x) |
| averIter#(x, y, z) → ifIter#(ge(x, y), x, y, z) | ifIter#(false, x, y, z) → averIter#(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| plus#(s(x), y) → plus#(x, y) |
| ge#(s(x), s(y)) → ge#(x, y) |
| ifquick#(false, x) → quicksort#(low(head(x), tail(x))) | ifquick#(false, x) → quicksort#(high(head(x), tail(x))) |
| quicksort#(x) → ifquick#(isempty(x), x) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if_low#(true, n, cons(m, x)) | → | low#(n, x) | | low#(n, cons(m, x)) | → | if_low#(ge(m, n), n, cons(m, x)) |
| if_low#(false, n, cons(m, x)) | → | low#(n, x) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, if_low, ge, ifquick, if, false, head, cons, averIter, plus, append, app, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Strategy
Projection
The following projection was used:
- π (if_low#): 3
- π (low#): 2
Thus, the following dependency pairs are removed:
| if_low#(true, n, cons(m, x)) | → | low#(n, x) | | if_low#(false, n, cons(m, x)) | → | low#(n, x) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| low#(n, cons(m, x)) | → | if_low#(ge(m, n), n, cons(m, x)) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, ge, if_low, ifquick, if, false, head, cons, averIter, app, append, plus, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ge#(s(x), s(y)) | → | ge#(x, y) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, if_low, ge, ifquick, if, false, head, cons, averIter, plus, append, app, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ge#(s(x), s(y)) | → | ge#(x, y) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if_high#(true, n, cons(m, x)) | → | high#(n, x) | | high#(n, cons(m, x)) | → | if_high#(ge(m, n), n, cons(m, x)) |
| if_high#(false, n, cons(m, x)) | → | high#(n, x) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, if_low, ge, ifquick, if, false, head, cons, averIter, plus, append, app, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Strategy
Projection
The following projection was used:
- π (high#): 2
- π (if_high#): 3
Thus, the following dependency pairs are removed:
| if_high#(true, n, cons(m, x)) | → | high#(n, x) | | if_high#(false, n, cons(m, x)) | → | high#(n, x) |
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| high#(n, cons(m, x)) | → | if_high#(ge(m, n), n, cons(m, x)) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, ge, if_low, ifquick, if, false, head, cons, averIter, app, append, plus, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Strategy
There are no SCCs!
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) |
Rewrite Rules
| average(x, y) | → | if(ge(x, y), x, y) | | if(true, x, y) | → | averIter(y, x, y) |
| if(false, x, y) | → | averIter(x, y, x) | | averIter(x, y, z) | → | ifIter(ge(x, y), x, y, z) |
| ifIter(true, x, y, z) | → | z | | ifIter(false, x, y, z) | → | averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0))) |
| append(nil, y) | → | y | | append(cons(n, x), y) | → | cons(n, app(x, y)) |
| low(n, nil) | → | nil | | low(n, cons(m, x)) | → | if_low(ge(m, n), n, cons(m, x)) |
| if_low(false, n, cons(m, x)) | → | cons(m, low(n, x)) | | if_low(true, n, cons(m, x)) | → | low(n, x) |
| high(n, nil) | → | nil | | high(n, cons(m, x)) | → | if_high(ge(m, n), n, cons(m, x)) |
| if_high(false, n, cons(m, x)) | → | high(n, x) | | if_high(true, n, cons(m, x)) | → | cons(average(m, m), high(n, x)) |
| quicksort(x) | → | ifquick(isempty(x), x) | | ifquick(true, x) | → | nil |
| ifquick(false, x) | → | append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | isempty(nil) | → | true |
| isempty(cons(n, x)) | → | false | | head(nil) | → | error |
| head(cons(n, x)) | → | n | | tail(nil) | → | nil |
| tail(cons(n, x)) | → | x | | ge(x, 0) | → | true |
| ge(0, s(y)) | → | false | | ge(s(x), s(y)) | → | ge(x, y) |
| a | → | b | | a | → | c |
Original Signature
Termination of terms over the following signature is verified: ifIter, if_low, ge, ifquick, if, false, head, cons, averIter, plus, append, app, error, b, c, a, true, tail, 0, s, isempty, if_high, high, low, quicksort, average, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(s(x), y) | → | plus#(x, y) |