YES
The TRS could be proven terminating. The proof took 631 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (8ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (189ms).
| | – Problem 4 was processed with processor PolynomialLinearRange4iUR (102ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (80ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (110ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(.(nil, y)) | → | f#(y) | | f#(.(.(x, y), z)) | → | f#(.(x, .(y, z))) |
| g#(.(x, nil)) | → | g#(x) | | g#(.(x, .(y, z))) | → | g#(.(.(x, y), z)) |
Rewrite Rules
| f(nil) | → | nil | | f(.(nil, y)) | → | .(nil, f(y)) |
| f(.(.(x, y), z)) | → | f(.(x, .(y, z))) | | g(nil) | → | nil |
| g(.(x, nil)) | → | .(g(x), nil) | | g(.(x, .(y, z))) | → | g(.(.(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: f, g, ., nil
Strategy
The following SCCs where found
| f#(.(nil, y)) → f#(y) | f#(.(.(x, y), z)) → f#(.(x, .(y, z))) |
| g#(.(x, nil)) → g#(x) | g#(.(x, .(y, z))) → g#(.(.(x, y), z)) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(.(nil, y)) | → | f#(y) | | f#(.(.(x, y), z)) | → | f#(.(x, .(y, z))) |
Rewrite Rules
| f(nil) | → | nil | | f(.(nil, y)) | → | .(nil, f(y)) |
| f(.(.(x, y), z)) | → | f(.(x, .(y, z))) | | g(nil) | → | nil |
| g(.(x, nil)) | → | .(g(x), nil) | | g(.(x, .(y, z))) | → | g(.(.(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: f, g, ., nil
Strategy
Polynomial Interpretation
- .(x,y): y + x
- f(x): 0
- f#(x): 2x
- g(x): 0
- nil: 1
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(.(.(x, y), z)) | → | f#(.(x, .(y, z))) |
Rewrite Rules
| f(nil) | → | nil | | f(.(nil, y)) | → | .(nil, f(y)) |
| f(.(.(x, y), z)) | → | f(.(x, .(y, z))) | | g(nil) | → | nil |
| g(.(x, nil)) | → | .(g(x), nil) | | g(.(x, .(y, z))) | → | g(.(.(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: f, g, ., nil
Strategy
Polynomial Interpretation
- .(x,y): x + 1
- f(x): 0
- f#(x): x + 1
- g(x): 0
- nil: 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:
| f#(.(.(x, y), z)) | → | f#(.(x, .(y, z))) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| g#(.(x, nil)) | → | g#(x) | | g#(.(x, .(y, z))) | → | g#(.(.(x, y), z)) |
Rewrite Rules
| f(nil) | → | nil | | f(.(nil, y)) | → | .(nil, f(y)) |
| f(.(.(x, y), z)) | → | f(.(x, .(y, z))) | | g(nil) | → | nil |
| g(.(x, nil)) | → | .(g(x), nil) | | g(.(x, .(y, z))) | → | g(.(.(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: f, g, ., nil
Strategy
Polynomial Interpretation
- .(x,y): y + x
- f(x): 0
- g(x): 0
- g#(x): 2x
- nil: 1
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| g#(.(x, .(y, z))) | → | g#(.(.(x, y), z)) |
Rewrite Rules
| f(nil) | → | nil | | f(.(nil, y)) | → | .(nil, f(y)) |
| f(.(.(x, y), z)) | → | f(.(x, .(y, z))) | | g(nil) | → | nil |
| g(.(x, nil)) | → | .(g(x), nil) | | g(.(x, .(y, z))) | → | g(.(.(x, y), z)) |
Original Signature
Termination of terms over the following signature is verified: f, g, ., nil
Strategy
Polynomial Interpretation
- .(x,y): y + 1
- f(x): 0
- g(x): 0
- g#(x): x + 1
- nil: 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:
| g#(.(x, .(y, z))) | → | g#(.(.(x, y), z)) |