YES
The TRS could be proven terminating. The proof took 1877 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (563ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (345ms).
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (419ms).
| | – Problem 7 was processed with processor PolynomialLinearRange4iUR (93ms).
| | | – Problem 9 was processed with processor PolynomialLinearRange4iUR (89ms).
| – Problem 5 was processed with processor PolynomialLinearRange4iUR (58ms).
| | – Problem 8 was processed with processor PolynomialLinearRange4iUR (10ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ge#(0(x), 1(y)) | → | not#(ge(y, x)) | | -#(0(x), 0(y)) | → | 0#(-(x, y)) |
| -#(1(x), 1(y)) | → | 0#(-(x, y)) | | +#(0(x), 0(y)) | → | +#(x, y) |
| log'#(0(x)) | → | +#(log'(x), 1(#)) | | +#(+(x, y), z) | → | +#(y, z) |
| -#(0(x), 1(y)) | → | -#(x, y) | | -#(0(x), 0(y)) | → | -#(x, y) |
| +#(+(x, y), z) | → | +#(x, +(y, z)) | | +#(0(x), 0(y)) | → | 0#(+(x, y)) |
| log'#(1(x)) | → | +#(log'(x), 1(#)) | | log#(x) | → | log'#(x) |
| -#(1(x), 1(y)) | → | -#(x, y) | | +#(1(x), 0(y)) | → | +#(x, y) |
| log#(x) | → | -#(log'(x), 1(#)) | | log'#(0(x)) | → | if#(ge(x, 1(#)), +(log'(x), 1(#)), #) |
| ge#(1(x), 1(y)) | → | ge#(x, y) | | +#(1(x), 1(y)) | → | 0#(+(+(x, y), 1(#))) |
| +#(0(x), 1(y)) | → | +#(x, y) | | ge#(0(x), 1(y)) | → | ge#(y, x) |
| -#(1(x), 0(y)) | → | -#(x, y) | | -#(0(x), 1(y)) | → | -#(-(x, y), 1(#)) |
| +#(1(x), 1(y)) | → | +#(+(x, y), 1(#)) | | log'#(0(x)) | → | ge#(x, 1(#)) |
| ge#(1(x), 0(y)) | → | ge#(x, y) | | log'#(1(x)) | → | log'#(x) |
| ge#(0(x), 0(y)) | → | ge#(x, y) | | log'#(0(x)) | → | log'#(x) |
| ge#(#, 0(x)) | → | ge#(#, x) | | +#(1(x), 1(y)) | → | +#(x, y) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, +, false, true, ge, log, -
Strategy
The following SCCs where found
| log'#(1(x)) → log'#(x) | log'#(0(x)) → log'#(x) |
| ge#(1(x), 1(y)) → ge#(x, y) | ge#(0(x), 1(y)) → ge#(y, x) |
| ge#(0(x), 0(y)) → ge#(x, y) | ge#(1(x), 0(y)) → ge#(x, y) |
| +#(0(x), 1(y)) → +#(x, y) | +#(0(x), 0(y)) → +#(x, y) |
| +#(+(x, y), z) → +#(y, z) | +#(1(x), 1(y)) → +#(x, y) |
| +#(1(x), 1(y)) → +#(+(x, y), 1(#)) | +#(1(x), 0(y)) → +#(x, y) |
| +#(+(x, y), z) → +#(x, +(y, z)) |
| -#(1(x), 0(y)) → -#(x, y) | -#(0(x), 1(y)) → -#(x, y) |
| -#(0(x), 1(y)) → -#(-(x, y), 1(#)) | -#(1(x), 1(y)) → -#(x, y) |
| -#(0(x), 0(y)) → -#(x, y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(1(x), 0(y)) | → | -#(x, y) | | -#(0(x), 1(y)) | → | -#(x, y) |
| -#(0(x), 1(y)) | → | -#(-(x, y), 1(#)) | | -#(1(x), 1(y)) | → | -#(x, y) |
| -#(0(x), 0(y)) | → | -#(x, y) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, +, false, true, ge, log, -
Strategy
Polynomial Interpretation
- #: 1
- +(x,y): 0
- -(x,y): x
- -#(x,y): 2x
- 0(x): x + 1
- 1(x): x + 1
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- log(x): 0
- log'(x): 0
- not(x): 0
- true: 0
Improved Usable rules
| -(1(x), 1(y)) | → | 0(-(x, y)) | | 0(#) | → | # |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(1(x), 0(y)) | → | 1(-(x, y)) |
| -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) | | -(x, #) | → | x |
| -(#, x) | → | # |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| -#(1(x), 0(y)) | → | -#(x, y) | | -#(0(x), 1(y)) | → | -#(x, y) |
| -#(0(x), 1(y)) | → | -#(-(x, y), 1(#)) | | -#(1(x), 1(y)) | → | -#(x, y) |
| -#(0(x), 0(y)) | → | -#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, +, false, true, ge, log, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| +#(0(x), 1(y)) | → | +#(x, y) | | +#(0(x), 0(y)) | → | +#(x, y) |
| +#(+(x, y), z) | → | +#(y, z) | | +#(1(x), 1(y)) | → | +#(x, y) |
| +#(1(x), 1(y)) | → | +#(+(x, y), 1(#)) | | +#(1(x), 0(y)) | → | +#(x, y) |
| +#(+(x, y), z) | → | +#(x, +(y, z)) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, +, false, true, ge, log, -
Strategy
Polynomial Interpretation
- #: 0
- +(x,y): y + x
- +#(x,y): y + 2x
- -(x,y): 0
- 0(x): 2x
- 1(x): 2x + 1
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- log(x): 0
- log'(x): 0
- not(x): 0
- true: 0
Improved Usable rules
| +(+(x, y), z) | → | +(x, +(y, z)) | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(1(x), 0(y)) | → | 1(+(x, y)) | | 0(#) | → | # |
| +(x, #) | → | x | | +(0(x), 1(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(#, x) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| +#(0(x), 1(y)) | → | +#(x, y) | | +#(1(x), 1(y)) | → | +#(x, y) |
| +#(1(x), 1(y)) | → | +#(+(x, y), 1(#)) | | +#(1(x), 0(y)) | → | +#(x, y) |
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| +#(0(x), 0(y)) | → | +#(x, y) | | +#(+(x, y), z) | → | +#(y, z) |
| +#(+(x, y), z) | → | +#(x, +(y, z)) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, true, false, +, ge, log, -
Strategy
Polynomial Interpretation
- #: 1
- +(x,y): y + x
- +#(x,y): 2x
- -(x,y): 0
- 0(x): 2x + 1
- 1(x): 0
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- log(x): 0
- log'(x): 0
- not(x): 0
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| +#(0(x), 0(y)) | → | +#(x, y) |
Problem 9: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| +#(+(x, y), z) | → | +#(y, z) | | +#(+(x, y), z) | → | +#(x, +(y, z)) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, +, false, true, ge, log, -
Strategy
Polynomial Interpretation
- #: 1
- +(x,y): y + x + 1
- +#(x,y): x + 1
- -(x,y): 0
- 0(x): 0
- 1(x): 0
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- log(x): 0
- log'(x): 0
- not(x): 0
- true: 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| +#(+(x, y), z) | → | +#(y, z) | | +#(+(x, y), z) | → | +#(x, +(y, z)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ge#(1(x), 1(y)) | → | ge#(x, y) | | ge#(0(x), 1(y)) | → | ge#(y, x) |
| ge#(0(x), 0(y)) | → | ge#(x, y) | | ge#(1(x), 0(y)) | → | ge#(x, y) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, +, false, true, ge, log, -
Strategy
Polynomial Interpretation
- #: 0
- +(x,y): 0
- -(x,y): 0
- 0(x): x
- 1(x): 2x + 1
- false: 0
- ge(x,y): 0
- ge#(x,y): y + 2x
- if(x,y,z): 0
- log(x): 0
- log'(x): 0
- not(x): 0
- true: 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:
| ge#(1(x), 1(y)) | → | ge#(x, y) | | ge#(0(x), 1(y)) | → | ge#(y, x) |
| ge#(1(x), 0(y)) | → | ge#(x, y) |
Problem 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ge#(0(x), 0(y)) | → | ge#(x, y) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, true, false, +, ge, log, -
Strategy
Polynomial Interpretation
- #: 0
- +(x,y): 0
- -(x,y): 0
- 0(x): 2x + 1
- 1(x): 0
- false: 0
- ge(x,y): 0
- ge#(x,y): x + 1
- if(x,y,z): 0
- log(x): 0
- log'(x): 0
- not(x): 0
- true: 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:
| ge#(0(x), 0(y)) | → | ge#(x, y) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| log'#(1(x)) | → | log'#(x) | | log'#(0(x)) | → | log'#(x) |
Rewrite Rules
| 0(#) | → | # | | +(#, x) | → | x |
| +(x, #) | → | x | | +(0(x), 0(y)) | → | 0(+(x, y)) |
| +(0(x), 1(y)) | → | 1(+(x, y)) | | +(1(x), 0(y)) | → | 1(+(x, y)) |
| +(1(x), 1(y)) | → | 0(+(+(x, y), 1(#))) | | +(+(x, y), z) | → | +(x, +(y, z)) |
| -(#, x) | → | # | | -(x, #) | → | x |
| -(0(x), 0(y)) | → | 0(-(x, y)) | | -(0(x), 1(y)) | → | 1(-(-(x, y), 1(#))) |
| -(1(x), 0(y)) | → | 1(-(x, y)) | | -(1(x), 1(y)) | → | 0(-(x, y)) |
| not(true) | → | false | | not(false) | → | true |
| if(true, x, y) | → | x | | if(false, x, y) | → | y |
| ge(0(x), 0(y)) | → | ge(x, y) | | ge(0(x), 1(y)) | → | not(ge(y, x)) |
| ge(1(x), 0(y)) | → | ge(x, y) | | ge(1(x), 1(y)) | → | ge(x, y) |
| ge(x, #) | → | true | | ge(#, 0(x)) | → | ge(#, x) |
| ge(#, 1(x)) | → | false | | log(x) | → | -(log'(x), 1(#)) |
| log'(#) | → | # | | log'(1(x)) | → | +(log'(x), 1(#)) |
| log'(0(x)) | → | if(ge(x, 1(#)), +(log'(x), 1(#)), #) |
Original Signature
Termination of terms over the following signature is verified: not, #, 1, 0, log', if, +, false, true, ge, log, -
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| log'#(1(x)) | → | log'#(x) | | log'#(0(x)) | → | log'#(x) |