YES
The TRS could be proven terminating. The proof took 741 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (11ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (190ms).
| | – Problem 4 was processed with processor PolynomialLinearRange4iUR (72ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (342ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| sum#(cons(s(n), x), cons(m, y)) | → | sum#(cons(n, x), cons(s(m), y)) | | sum#(cons(0, x), y) | → | sum#(x, y) |
| weight#(cons(n, cons(m, x))) | → | weight#(sum(cons(n, cons(m, x)), cons(0, x))) | | weight#(cons(n, cons(m, x))) | → | sum#(cons(n, cons(m, x)), cons(0, x)) |
Rewrite Rules
| sum(cons(s(n), x), cons(m, y)) | → | sum(cons(n, x), cons(s(m), y)) | | sum(cons(0, x), y) | → | sum(x, y) |
| sum(nil, y) | → | y | | weight(cons(n, cons(m, x))) | → | weight(sum(cons(n, cons(m, x)), cons(0, x))) |
| weight(cons(n, nil)) | → | n |
Original Signature
Termination of terms over the following signature is verified: 0, weight, s, sum, cons, nil
Strategy
The following SCCs where found
| weight#(cons(n, cons(m, x))) → weight#(sum(cons(n, cons(m, x)), cons(0, x))) |
| sum#(cons(s(n), x), cons(m, y)) → sum#(cons(n, x), cons(s(m), y)) | sum#(cons(0, x), y) → sum#(x, y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sum#(cons(s(n), x), cons(m, y)) | → | sum#(cons(n, x), cons(s(m), y)) | | sum#(cons(0, x), y) | → | sum#(x, y) |
Rewrite Rules
| sum(cons(s(n), x), cons(m, y)) | → | sum(cons(n, x), cons(s(m), y)) | | sum(cons(0, x), y) | → | sum(x, y) |
| sum(nil, y) | → | y | | weight(cons(n, cons(m, x))) | → | weight(sum(cons(n, cons(m, x)), cons(0, x))) |
| weight(cons(n, nil)) | → | n |
Original Signature
Termination of terms over the following signature is verified: 0, weight, s, sum, cons, nil
Strategy
Polynomial Interpretation
- 0: 1
- cons(x,y): y + x
- nil: 0
- s(x): x + 1
- sum(x,y): 0
- sum#(x,y): y + x
- weight(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sum#(cons(0, x), y) | → | sum#(x, y) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| sum#(cons(s(n), x), cons(m, y)) | → | sum#(cons(n, x), cons(s(m), y)) |
Rewrite Rules
| sum(cons(s(n), x), cons(m, y)) | → | sum(cons(n, x), cons(s(m), y)) | | sum(cons(0, x), y) | → | sum(x, y) |
| sum(nil, y) | → | y | | weight(cons(n, cons(m, x))) | → | weight(sum(cons(n, cons(m, x)), cons(0, x))) |
| weight(cons(n, nil)) | → | n |
Original Signature
Termination of terms over the following signature is verified: weight, 0, s, sum, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- cons(x,y): x
- nil: 0
- s(x): x + 1
- sum(x,y): 0
- sum#(x,y): 2x
- weight(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sum#(cons(s(n), x), cons(m, y)) | → | sum#(cons(n, x), cons(s(m), y)) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| weight#(cons(n, cons(m, x))) | → | weight#(sum(cons(n, cons(m, x)), cons(0, x))) |
Rewrite Rules
| sum(cons(s(n), x), cons(m, y)) | → | sum(cons(n, x), cons(s(m), y)) | | sum(cons(0, x), y) | → | sum(x, y) |
| sum(nil, y) | → | y | | weight(cons(n, cons(m, x))) | → | weight(sum(cons(n, cons(m, x)), cons(0, x))) |
| weight(cons(n, nil)) | → | n |
Original Signature
Termination of terms over the following signature is verified: 0, weight, s, sum, cons, nil
Strategy
Polynomial Interpretation
- 0: 2
- cons(x,y): y + 1
- nil: 1
- s(x): 2x + 2
- sum(x,y): y
- weight(x): 0
- weight#(x): x
Improved Usable rules
| sum(nil, y) | → | y | | sum(cons(0, x), y) | → | sum(x, y) |
| sum(cons(s(n), x), cons(m, y)) | → | sum(cons(n, x), cons(s(m), y)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| weight#(cons(n, cons(m, x))) | → | weight#(sum(cons(n, cons(m, x)), cons(0, x))) |