YES
The TRS could be proven terminating. The proof took 321 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (19ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (265ms).
| | – Problem 3 was processed with processor DependencyGraph (4ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| =#(.(x, y), .(u, v)) | → | =#(y, v) | | f#(true, x, y, z) | → | del#(.(y, z)) |
| del#(.(x, .(y, z))) | → | =#(x, y) | | =#(.(x, y), .(u, v)) | → | =#(x, u) |
| del#(.(x, .(y, z))) | → | f#(=(x, y), x, y, z) | | f#(false, x, y, z) | → | del#(.(y, z)) |
Rewrite Rules
| del(.(x, .(y, z))) | → | f(=(x, y), x, y, z) | | f(true, x, y, z) | → | del(.(y, z)) |
| f(false, x, y, z) | → | .(x, del(.(y, z))) | | =(nil, nil) | → | true |
| =(.(x, y), nil) | → | false | | =(nil, .(y, z)) | → | false |
| =(.(x, y), .(u, v)) | → | and(=(x, u), =(y, v)) |
Original Signature
Termination of terms over the following signature is verified: f, v, u, true, false, del, ., =, nil, and
Strategy
The following SCCs where found
| f#(true, x, y, z) → del#(.(y, z)) | del#(.(x, .(y, z))) → f#(=(x, y), x, y, z) |
| f#(false, x, y, z) → del#(.(y, z)) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(true, x, y, z) | → | del#(.(y, z)) | | del#(.(x, .(y, z))) | → | f#(=(x, y), x, y, z) |
| f#(false, x, y, z) | → | del#(.(y, z)) |
Rewrite Rules
| del(.(x, .(y, z))) | → | f(=(x, y), x, y, z) | | f(true, x, y, z) | → | del(.(y, z)) |
| f(false, x, y, z) | → | .(x, del(.(y, z))) | | =(nil, nil) | → | true |
| =(.(x, y), nil) | → | false | | =(nil, .(y, z)) | → | false |
| =(.(x, y), .(u, v)) | → | and(=(x, u), =(y, v)) |
Original Signature
Termination of terms over the following signature is verified: f, v, u, true, false, del, ., =, nil, and
Strategy
Polynomial Interpretation
- .(x,y): 3y + 2x
- =(x,y): y + x + 1
- and(x,y): x
- del(x): 0
- del#(x): x + 1
- f(x1,x2,x3,x4): 0
- f#(x1,x2,x3,x4): 3x4 + 3x3 + x2 + x1
- false: 2
- nil: 1
- true: 3
- u: 0
- v: 0
Improved Usable rules
| =(nil, nil) | → | true | | =(nil, .(y, z)) | → | false |
| =(.(x, y), nil) | → | false | | =(.(x, y), .(u, v)) | → | and(=(x, u), =(y, v)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(true, x, y, z) | → | del#(.(y, z)) | | f#(false, x, y, z) | → | del#(.(y, z)) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| del#(.(x, .(y, z))) | → | f#(=(x, y), x, y, z) |
Rewrite Rules
| del(.(x, .(y, z))) | → | f(=(x, y), x, y, z) | | f(true, x, y, z) | → | del(.(y, z)) |
| f(false, x, y, z) | → | .(x, del(.(y, z))) | | =(nil, nil) | → | true |
| =(.(x, y), nil) | → | false | | =(nil, .(y, z)) | → | false |
| =(.(x, y), .(u, v)) | → | and(=(x, u), =(y, v)) |
Original Signature
Termination of terms over the following signature is verified: f, v, u, false, true, del, ., =, and, nil
Strategy
There are no SCCs!