YES
The TRS could be proven terminating. The proof took 1351 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (83ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (1019ms).
| | – Problem 3 was processed with processor DependencyGraph (7ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4iUR (47ms).
| | | | – Problem 5 was processed with processor PolynomialLinearRange4iUR (30ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| u31#(dout(DX), X, Y) | → | din#(der(Y)) | | din#(der(times(X, Y))) | → | din#(der(X)) |
| u41#(dout(DX), X) | → | din#(der(DX)) | | din#(der(der(X))) | → | u41#(din(der(X)), X) |
| din#(der(plus(X, Y))) | → | u21#(din(der(X)), X, Y) | | u21#(dout(DX), X, Y) | → | din#(der(Y)) |
| u21#(dout(DX), X, Y) | → | u22#(din(der(Y)), X, Y, DX) | | u31#(dout(DX), X, Y) | → | u32#(din(der(Y)), X, Y, DX) |
| u41#(dout(DX), X) | → | u42#(din(der(DX)), X, DX) | | din#(der(plus(X, Y))) | → | din#(der(X)) |
| din#(der(times(X, Y))) | → | u31#(din(der(X)), X, Y) | | din#(der(der(X))) | → | din#(der(X)) |
Rewrite Rules
| din(der(plus(X, Y))) | → | u21(din(der(X)), X, Y) | | u21(dout(DX), X, Y) | → | u22(din(der(Y)), X, Y, DX) |
| u22(dout(DY), X, Y, DX) | → | dout(plus(DX, DY)) | | din(der(times(X, Y))) | → | u31(din(der(X)), X, Y) |
| u31(dout(DX), X, Y) | → | u32(din(der(Y)), X, Y, DX) | | u32(dout(DY), X, Y, DX) | → | dout(plus(times(X, DY), times(Y, DX))) |
| din(der(der(X))) | → | u41(din(der(X)), X) | | u41(dout(DX), X) | → | u42(din(der(DX)), X, DX) |
| u42(dout(DDX), X, DX) | → | dout(DDX) |
Original Signature
Termination of terms over the following signature is verified: din, plus, der, u22, u21, times, u41, u42, u31, u32, dout
Strategy
The following SCCs where found
| u31#(dout(DX), X, Y) → din#(der(Y)) | din#(der(times(X, Y))) → din#(der(X)) |
| u41#(dout(DX), X) → din#(der(DX)) | din#(der(der(X))) → u41#(din(der(X)), X) |
| din#(der(plus(X, Y))) → u21#(din(der(X)), X, Y) | u21#(dout(DX), X, Y) → din#(der(Y)) |
| din#(der(times(X, Y))) → u31#(din(der(X)), X, Y) | din#(der(plus(X, Y))) → din#(der(X)) |
| din#(der(der(X))) → din#(der(X)) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| u31#(dout(DX), X, Y) | → | din#(der(Y)) | | din#(der(times(X, Y))) | → | din#(der(X)) |
| u41#(dout(DX), X) | → | din#(der(DX)) | | din#(der(der(X))) | → | u41#(din(der(X)), X) |
| din#(der(plus(X, Y))) | → | u21#(din(der(X)), X, Y) | | u21#(dout(DX), X, Y) | → | din#(der(Y)) |
| din#(der(times(X, Y))) | → | u31#(din(der(X)), X, Y) | | din#(der(plus(X, Y))) | → | din#(der(X)) |
| din#(der(der(X))) | → | din#(der(X)) |
Rewrite Rules
| din(der(plus(X, Y))) | → | u21(din(der(X)), X, Y) | | u21(dout(DX), X, Y) | → | u22(din(der(Y)), X, Y, DX) |
| u22(dout(DY), X, Y, DX) | → | dout(plus(DX, DY)) | | din(der(times(X, Y))) | → | u31(din(der(X)), X, Y) |
| u31(dout(DX), X, Y) | → | u32(din(der(Y)), X, Y, DX) | | u32(dout(DY), X, Y, DX) | → | dout(plus(times(X, DY), times(Y, DX))) |
| din(der(der(X))) | → | u41(din(der(X)), X) | | u41(dout(DX), X) | → | u42(din(der(DX)), X, DX) |
| u42(dout(DDX), X, DX) | → | dout(DDX) |
Original Signature
Termination of terms over the following signature is verified: din, plus, der, u22, u21, times, u41, u42, u31, u32, dout
Strategy
Polynomial Interpretation
- der(x): 2
- din(x): 0
- din#(x): 1
- dout(x): x + 1
- plus(x,y): y
- times(x,y): 2
- u21(x,y,z): 0
- u21#(x,y,z): x
- u22(x1,x2,x3,x4): x1
- u31(x,y,z): 0
- u31#(x,y,z): x + 1
- u32(x1,x2,x3,x4): 3x1
- u41(x,y): x
- u41#(x,y): x
- u42(x,y,z): z + x
Improved Usable rules
| u21(dout(DX), X, Y) | → | u22(din(der(Y)), X, Y, DX) | | u41(dout(DX), X) | → | u42(din(der(DX)), X, DX) |
| u32(dout(DY), X, Y, DX) | → | dout(plus(times(X, DY), times(Y, DX))) | | u31(dout(DX), X, Y) | → | u32(din(der(Y)), X, Y, DX) |
| din(der(plus(X, Y))) | → | u21(din(der(X)), X, Y) | | din(der(der(X))) | → | u41(din(der(X)), X) |
| u22(dout(DY), X, Y, DX) | → | dout(plus(DX, DY)) | | din(der(times(X, Y))) | → | u31(din(der(X)), X, Y) |
| u42(dout(DDX), X, DX) | → | dout(DDX) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| u31#(dout(DX), X, Y) | → | din#(der(Y)) | | din#(der(der(X))) | → | u41#(din(der(X)), X) |
| din#(der(plus(X, Y))) | → | u21#(din(der(X)), X, Y) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| u41#(dout(DX), X) | → | din#(der(DX)) | | din#(der(times(X, Y))) | → | din#(der(X)) |
| u21#(dout(DX), X, Y) | → | din#(der(Y)) | | din#(der(plus(X, Y))) | → | din#(der(X)) |
| din#(der(times(X, Y))) | → | u31#(din(der(X)), X, Y) | | din#(der(der(X))) | → | din#(der(X)) |
Rewrite Rules
| din(der(plus(X, Y))) | → | u21(din(der(X)), X, Y) | | u21(dout(DX), X, Y) | → | u22(din(der(Y)), X, Y, DX) |
| u22(dout(DY), X, Y, DX) | → | dout(plus(DX, DY)) | | din(der(times(X, Y))) | → | u31(din(der(X)), X, Y) |
| u31(dout(DX), X, Y) | → | u32(din(der(Y)), X, Y, DX) | | u32(dout(DY), X, Y, DX) | → | dout(plus(times(X, DY), times(Y, DX))) |
| din(der(der(X))) | → | u41(din(der(X)), X) | | u41(dout(DX), X) | → | u42(din(der(DX)), X, DX) |
| u42(dout(DDX), X, DX) | → | dout(DDX) |
Original Signature
Termination of terms over the following signature is verified: der, plus, din, u22, u21, times, u41, u42, u31, u32, dout
Strategy
The following SCCs where found
| din#(der(times(X, Y))) → din#(der(X)) | din#(der(plus(X, Y))) → din#(der(X)) |
| din#(der(der(X))) → din#(der(X)) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| din#(der(times(X, Y))) | → | din#(der(X)) | | din#(der(plus(X, Y))) | → | din#(der(X)) |
| din#(der(der(X))) | → | din#(der(X)) |
Rewrite Rules
| din(der(plus(X, Y))) | → | u21(din(der(X)), X, Y) | | u21(dout(DX), X, Y) | → | u22(din(der(Y)), X, Y, DX) |
| u22(dout(DY), X, Y, DX) | → | dout(plus(DX, DY)) | | din(der(times(X, Y))) | → | u31(din(der(X)), X, Y) |
| u31(dout(DX), X, Y) | → | u32(din(der(Y)), X, Y, DX) | | u32(dout(DY), X, Y, DX) | → | dout(plus(times(X, DY), times(Y, DX))) |
| din(der(der(X))) | → | u41(din(der(X)), X) | | u41(dout(DX), X) | → | u42(din(der(DX)), X, DX) |
| u42(dout(DDX), X, DX) | → | dout(DDX) |
Original Signature
Termination of terms over the following signature is verified: der, plus, din, u22, u21, times, u41, u42, u31, u32, dout
Strategy
Polynomial Interpretation
- der(x): 2x + 1
- din(x): 0
- din#(x): x
- dout(x): 0
- plus(x,y): y + x + 1
- times(x,y): 2y + 2x
- u21(x,y,z): 0
- u22(x1,x2,x3,x4): 0
- u31(x,y,z): 0
- u32(x1,x2,x3,x4): 0
- u41(x,y): 0
- u42(x,y,z): 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:
| din#(der(plus(X, Y))) | → | din#(der(X)) | | din#(der(der(X))) | → | din#(der(X)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| din#(der(times(X, Y))) | → | din#(der(X)) |
Rewrite Rules
| din(der(plus(X, Y))) | → | u21(din(der(X)), X, Y) | | u21(dout(DX), X, Y) | → | u22(din(der(Y)), X, Y, DX) |
| u22(dout(DY), X, Y, DX) | → | dout(plus(DX, DY)) | | din(der(times(X, Y))) | → | u31(din(der(X)), X, Y) |
| u31(dout(DX), X, Y) | → | u32(din(der(Y)), X, Y, DX) | | u32(dout(DY), X, Y, DX) | → | dout(plus(times(X, DY), times(Y, DX))) |
| din(der(der(X))) | → | u41(din(der(X)), X) | | u41(dout(DX), X) | → | u42(din(der(DX)), X, DX) |
| u42(dout(DDX), X, DX) | → | dout(DDX) |
Original Signature
Termination of terms over the following signature is verified: din, plus, der, u22, u21, times, u41, u42, u31, u32, dout
Strategy
Polynomial Interpretation
- der(x): x + 1
- din(x): 0
- din#(x): x + 1
- dout(x): 0
- plus(x,y): 0
- times(x,y): x + 1
- u21(x,y,z): 0
- u22(x1,x2,x3,x4): 0
- u31(x,y,z): 0
- u32(x1,x2,x3,x4): 0
- u41(x,y): 0
- u42(x,y,z): 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:
| din#(der(times(X, Y))) | → | din#(der(X)) |