YES
The TRS could be proven terminating. The proof took 2517 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (110ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (982ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (720ms).
| | | – Problem 6 was processed with processor PolynomialLinearRange4iUR (319ms).
| | | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (275ms).
| | | | | – Problem 8 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(minus(x, y)) | → | minus_active#(x, y) | | mark#(if(x, y, z)) | → | if_active#(mark(x), y, z) |
| div_active#(s(x), s(y)) | → | ge_active#(x, y) | | div_active#(s(x), s(y)) | → | if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0) |
| if_active#(false, x, y) | → | mark#(y) | | if_active#(true, x, y) | → | mark#(x) |
| mark#(s(x)) | → | mark#(x) | | mark#(div(x, y)) | → | mark#(x) |
| mark#(div(x, y)) | → | div_active#(mark(x), y) | | mark#(ge(x, y)) | → | ge_active#(x, y) |
| mark#(if(x, y, z)) | → | mark#(x) | | minus_active#(s(x), s(y)) | → | minus_active#(x, y) |
| ge_active#(s(x), s(y)) | → | ge_active#(x, y) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
The following SCCs where found
| mark#(div(x, y)) → mark#(x) | mark#(if(x, y, z)) → if_active#(mark(x), y, z) |
| mark#(div(x, y)) → div_active#(mark(x), y) | div_active#(s(x), s(y)) → if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0) |
| if_active#(false, x, y) → mark#(y) | mark#(if(x, y, z)) → mark#(x) |
| if_active#(true, x, y) → mark#(x) | mark#(s(x)) → mark#(x) |
| minus_active#(s(x), s(y)) → minus_active#(x, y) |
| ge_active#(s(x), s(y)) → ge_active#(x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ge_active#(s(x), s(y)) | → | ge_active#(x, y) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ge_active#(s(x), s(y)) | → | ge_active#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| minus_active#(s(x), s(y)) | → | minus_active#(x, y) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| minus_active#(s(x), s(y)) | → | minus_active#(x, y) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(div(x, y)) | → | mark#(x) | | mark#(if(x, y, z)) | → | if_active#(mark(x), y, z) |
| mark#(div(x, y)) | → | div_active#(mark(x), y) | | div_active#(s(x), s(y)) | → | if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0) |
| if_active#(false, x, y) | → | mark#(y) | | mark#(if(x, y, z)) | → | mark#(x) |
| if_active#(true, x, y) | → | mark#(x) | | mark#(s(x)) | → | mark#(x) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
Polynomial Interpretation
- 0: 0
- div(x,y): 2x + 1
- div_active(x,y): 2
- div_active#(x,y): 2
- false: 0
- ge(x,y): 1
- ge_active(x,y): 0
- if(x,y,z): z + 2y + x
- if_active(x,y,z): 2y
- if_active#(x,y,z): 2z + 2y
- mark(x): 2x
- mark#(x): 2x
- minus(x,y): 0
- minus_active(x,y): 1
- s(x): x
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(div(x, y)) | → | mark#(x) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(if(x, y, z)) | → | if_active#(mark(x), y, z) | | mark#(div(x, y)) | → | div_active#(mark(x), y) |
| div_active#(s(x), s(y)) | → | if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | mark#(if(x, y, z)) | → | mark#(x) |
| if_active#(false, x, y) | → | mark#(y) | | if_active#(true, x, y) | → | mark#(x) |
| mark#(s(x)) | → | mark#(x) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
Polynomial Interpretation
- 0: 0
- div(x,y): y + 1
- div_active(x,y): 0
- div_active#(x,y): 2y + 2
- false: 0
- ge(x,y): 2y + 2x + 1
- ge_active(x,y): 0
- if(x,y,z): 2z + y + x + 1
- if_active(x,y,z): 1
- if_active#(x,y,z): 2z + 2y
- mark(x): 0
- mark#(x): 2x
- minus(x,y): 3y + 2x
- minus_active(x,y): 0
- s(x): x
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(if(x, y, z)) | → | if_active#(mark(x), y, z) | | mark#(if(x, y, z)) | → | mark#(x) |
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(div(x, y)) | → | div_active#(mark(x), y) | | div_active#(s(x), s(y)) | → | if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0) |
| if_active#(false, x, y) | → | mark#(y) | | if_active#(true, x, y) | → | mark#(x) |
| mark#(s(x)) | → | mark#(x) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
Polynomial Interpretation
- 0: 0
- div(x,y): 2x
- div_active(x,y): 2x
- div_active#(x,y): 2x
- false: 0
- ge(x,y): 2y
- ge_active(x,y): 2y
- if(x,y,z): z + 2y
- if_active(x,y,z): 2z + 2y
- if_active#(x,y,z): 2z + 2y
- mark(x): 2x
- mark#(x): 2x
- minus(x,y): 0
- minus_active(x,y): 0
- s(x): x + 1
- true: 0
Improved Usable rules
| mark(ge(x, y)) | → | ge_active(x, y) | | if_active(true, x, y) | → | mark(x) |
| mark(0) | → | 0 | | ge_active(x, y) | → | ge(x, y) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | if_active(x, y, z) | → | if(x, y, z) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | ge_active(x, 0) | → | true |
| mark(s(x)) | → | s(mark(x)) | | div_active(0, s(y)) | → | 0 |
| minus_active(0, y) | → | 0 | | minus_active(s(x), s(y)) | → | minus_active(x, y) |
| div_active(x, y) | → | div(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(div(x, y)) | → | div_active#(mark(x), y) | | div_active#(s(x), s(y)) | → | if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0) |
| if_active#(false, x, y) | → | mark#(y) | | if_active#(true, x, y) | → | mark#(x) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
Polynomial Interpretation
- 0: 0
- div(x,y): y + x + 1
- div_active(x,y): 1
- div_active#(x,y): 2y + 1
- false: 0
- ge(x,y): 0
- ge_active(x,y): 0
- if(x,y,z): z + y + 1
- if_active(x,y,z): z + x + 1
- if_active#(x,y,z): 2z + 2y
- mark(x): 2x
- mark#(x): 2x
- minus(x,y): 1
- minus_active(x,y): y + x + 1
- s(x): 1
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(div(x, y)) | → | div_active#(mark(x), y) | | div_active#(s(x), s(y)) | → | if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if_active#(false, x, y) | → | mark#(y) | | if_active#(true, x, y) | → | mark#(x) |
Rewrite Rules
| minus_active(0, y) | → | 0 | | mark(0) | → | 0 |
| minus_active(s(x), s(y)) | → | minus_active(x, y) | | mark(s(x)) | → | s(mark(x)) |
| ge_active(x, 0) | → | true | | mark(minus(x, y)) | → | minus_active(x, y) |
| ge_active(0, s(y)) | → | false | | mark(ge(x, y)) | → | ge_active(x, y) |
| ge_active(s(x), s(y)) | → | ge_active(x, y) | | mark(div(x, y)) | → | div_active(mark(x), y) |
| div_active(0, s(y)) | → | 0 | | mark(if(x, y, z)) | → | if_active(mark(x), y, z) |
| div_active(s(x), s(y)) | → | if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0) | | if_active(true, x, y) | → | mark(x) |
| minus_active(x, y) | → | minus(x, y) | | if_active(false, x, y) | → | mark(y) |
| ge_active(x, y) | → | ge(x, y) | | if_active(x, y, z) | → | if(x, y, z) |
| div_active(x, y) | → | div(x, y) |
Original Signature
Termination of terms over the following signature is verified: minus, minus_active, div, true, mark, ge, ge_active, 0, div_active, s, if, false, if_active
Strategy
There are no SCCs!