YES
The TRS could be proven terminating. The proof took 1079 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (121ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (648ms).
| – Problem 3 was processed with processor SubtermCriterion (7ms).
| – Problem 4 was processed with processor SubtermCriterion (22ms).
| – Problem 5 was processed with processor PolynomialLinearRange4iUR (60ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (16ms).
| – Problem 8 was processed with processor PolynomialLinearRange4iUR (129ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| avg#(xs) | → | hd#(sum(xs)) | | avg#(xs) | → | sum#(xs) |
| avg#(xs) | → | length#(xs) | | sum#(++(xs, :(x, :(y, ys)))) | → | ++#(xs, sum(:(x, :(y, ys)))) |
| sum#(:(x, :(y, xs))) | → | +#(x, y) | | quot#(s(x), s(y)) | → | -#(x, y) |
| +#(s(x), y) | → | +#(x, y) | | -#(s(x), s(y)) | → | -#(x, y) |
| length#(:(x, xs)) | → | length#(xs) | | sum#(++(xs, :(x, :(y, ys)))) | → | sum#(++(xs, sum(:(x, :(y, ys))))) |
| sum#(:(x, :(y, xs))) | → | sum#(:(+(x, y), xs)) | | sum#(++(xs, :(x, :(y, ys)))) | → | sum#(:(x, :(y, ys))) |
| quot#(s(x), s(y)) | → | quot#(-(x, y), s(y)) | | ++#(:(x, xs), ys) | → | ++#(xs, ys) |
| avg#(xs) | → | quot#(hd(sum(xs)), length(xs)) |
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
The following SCCs where found
| length#(:(x, xs)) → length#(xs) |
| sum#(++(xs, :(x, :(y, ys)))) → sum#(++(xs, sum(:(x, :(y, ys))))) |
| sum#(:(x, :(y, xs))) → sum#(:(+(x, y), xs)) |
| quot#(s(x), s(y)) → quot#(-(x, y), s(y)) |
| ++#(:(x, xs), ys) → ++#(xs, ys) |
| -#(s(x), s(y)) → -#(x, y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sum#(++(xs, :(x, :(y, ys)))) | → | sum#(++(xs, sum(:(x, :(y, ys))))) |
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
Polynomial Interpretation
- +(x,y): 2y
- ++(x,y): y + 2x
- -(x,y): 0
- 0: 3
- :(x,y): y + 1
- avg(x): 0
- hd(x): 0
- length(x): 0
- nil: 0
- quot(x,y): 0
- s(x): 0
- sum(x): 1
- sum#(x): x
Improved Usable rules
| sum(:(x, nil)) | → | :(x, nil) | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | ++(nil, ys) | → | ys |
| sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sum#(++(xs, :(x, :(y, ys)))) | → | sum#(++(xs, sum(:(x, :(y, ys))))) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(:(x, xs)) | → | length#(xs) |
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(:(x, xs)) | → | length#(xs) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| -#(s(x), s(y)) | → | -#(x, y) |
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| -#(s(x), s(y)) | → | -#(x, y) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sum#(:(x, :(y, xs))) | → | sum#(:(+(x, y), xs)) |
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
Polynomial Interpretation
- +(x,y): 0
- ++(x,y): 0
- -(x,y): 0
- 0: 3
- :(x,y): y + 1
- avg(x): 0
- hd(x): 0
- length(x): 0
- nil: 0
- quot(x,y): 0
- s(x): 0
- sum(x): 0
- sum#(x): x
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sum#(:(x, :(y, xs))) | → | sum#(:(+(x, y), xs)) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ++#(:(x, xs), ys) | → | ++#(xs, ys) |
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ++#(:(x, xs), ys) | → | ++#(xs, ys) |
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| quot#(s(x), s(y)) | → | quot#(-(x, y), s(y)) |
Rewrite Rules
| +(0, y) | → | y | | +(s(x), y) | → | s(+(x, y)) |
| ++(nil, ys) | → | ys | | ++(:(x, xs), ys) | → | :(x, ++(xs, ys)) |
| sum(:(x, nil)) | → | :(x, nil) | | sum(:(x, :(y, xs))) | → | sum(:(+(x, y), xs)) |
| sum(++(xs, :(x, :(y, ys)))) | → | sum(++(xs, sum(:(x, :(y, ys))))) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 | | -(s(x), s(y)) | → | -(x, y) |
| quot(0, s(y)) | → | 0 | | quot(s(x), s(y)) | → | s(quot(-(x, y), s(y))) |
| length(nil) | → | 0 | | length(:(x, xs)) | → | s(length(xs)) |
| hd(:(x, xs)) | → | x | | avg(xs) | → | quot(hd(sum(xs)), length(xs)) |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, +, :, sum, hd, ++, avg, quot, nil, -
Strategy
Polynomial Interpretation
- +(x,y): 0
- ++(x,y): 0
- -(x,y): x + 1
- 0: 1
- :(x,y): 0
- avg(x): 0
- hd(x): 0
- length(x): 0
- nil: 0
- quot(x,y): 0
- quot#(x,y): x + 1
- s(x): 2x + 2
- sum(x): 0
Improved Usable rules
| -(s(x), s(y)) | → | -(x, y) | | -(x, 0) | → | x |
| -(0, s(y)) | → | 0 |
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#(-(x, y), s(y)) |