YES
The TRS could be proven terminating. The proof took 3193 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1138ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| | – Problem 16 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (0ms).
| – Problem 8 was processed with processor SubtermCriterion (0ms).
| – Problem 9 was processed with processor SubtermCriterion (0ms).
| – Problem 10 was processed with processor PolynomialLinearRange4iUR (412ms).
| | – Problem 17 was processed with processor PolynomialLinearRange4iUR (97ms).
| | | – Problem 21 was processed with processor PolynomialLinearRange4iUR (82ms).
| – Problem 11 was processed with processor PolynomialLinearRange4iUR (116ms).
| | – Problem 18 was processed with processor PolynomialLinearRange4iUR (10ms).
| – Problem 12 was processed with processor PolynomialLinearRange4iUR (337ms).
| | – Problem 19 was processed with processor PolynomialLinearRange4iUR (226ms).
| | | – Problem 22 was processed with processor PolynomialLinearRange4iUR (218ms).
| | | | – Problem 23 was processed with processor PolynomialLinearRange4iUR (148ms).
| | | | | – Problem 24 was processed with processor DependencyGraph (1ms).
| – Problem 13 was processed with processor PolynomialLinearRange4iUR (127ms).
| | – Problem 20 was processed with processor PolynomialLinearRange4iUR (79ms).
| – Problem 14 was processed with processor SubtermCriterion (0ms).
| – Problem 15 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| -#(1(x), 1(y)) | → | 0#(-(x, y)) | | +#(0(x), 0(y)) | → | +#(x, y) |
| -#(0(x), 1(y)) | → | -#(x, y) | | -#(0(x), 0(y)) | → | -#(x, y) |
| log'#(1(x)) | → | +#(log'(x), 1(#)) | | app#(cons(x, l1), l2) | → | app#(l1, l2) |
| inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) | | sum#(nil) | → | 0#(#) |
| mem#(x, cons(y, l)) | → | if#(eq(x, y), true, mem(x, l)) | | *#(x, +(y, z)) | → | *#(x, y) |
| prod#(app(l1, l2)) | → | prod#(l2) | | sum#(app(l1, l2)) | → | sum#(l2) |
| +#(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) |
| ge#(0(x), 1(y)) | → | ge#(y, x) | | *#(*(x, y), z) | → | *#(y, z) |
| sum#(cons(x, l)) | → | sum#(l) | | inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) |
| log'#(0(x)) | → | ge#(x, 1(#)) | | ge#(1(x), 0(y)) | → | ge#(x, y) |
| eq#(#, 0(y)) | → | eq#(#, y) | | *#(1(x), y) | → | *#(x, y) |
| log'#(1(x)) | → | log'#(x) | | *#(1(x), y) | → | 0#(*(x, y)) |
| inter#(app(l1, l2), l3) | → | inter#(l1, l3) | | log'#(0(x)) | → | log'#(x) |
| +#(1(x), 1(y)) | → | +#(x, y) | | ge#(#, 0(x)) | → | ge#(#, x) |
| ge#(0(x), 1(y)) | → | not#(ge(y, x)) | | -#(0(x), 0(y)) | → | 0#(-(x, y)) |
| eq#(0(x), 0(y)) | → | eq#(x, y) | | *#(*(x, y), z) | → | *#(x, *(y, z)) |
| log'#(0(x)) | → | +#(log'(x), 1(#)) | | +#(+(x, y), z) | → | +#(y, z) |
| *#(0(x), y) | → | 0#(*(x, y)) | | prod#(cons(x, l)) | → | *#(x, prod(l)) |
| sum#(cons(x, l)) | → | +#(x, sum(l)) | | +#(+(x, y), z) | → | +#(x, +(y, z)) |
| +#(0(x), 0(y)) | → | 0#(+(x, y)) | | inter#(app(l1, l2), l3) | → | app#(inter(l1, l3), inter(l2, l3)) |
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) | | inter#(cons(x, l1), l2) | → | mem#(x, l2) |
| *#(x, +(y, z)) | → | +#(*(x, y), *(x, z)) | | log#(x) | → | log'#(x) |
| eq#(1(x), 1(y)) | → | eq#(x, y) | | ifinter#(false, x, l1, l2) | → | inter#(l1, l2) |
| *#(0(x), y) | → | *#(x, y) | | -#(1(x), 1(y)) | → | -#(x, y) |
| sum#(app(l1, l2)) | → | +#(sum(l1), sum(l2)) | | +#(1(x), 1(y)) | → | 0#(+(+(x, y), 1(#))) |
| +#(0(x), 1(y)) | → | +#(x, y) | | -#(1(x), 0(y)) | → | -#(x, y) |
| inter#(app(l1, l2), l3) | → | inter#(l2, l3) | | -#(0(x), 1(y)) | → | -#(-(x, y), 1(#)) |
| +#(1(x), 1(y)) | → | +#(+(x, y), 1(#)) | | eq#(0(x), #) | → | eq#(x, #) |
| inter#(l1, app(l2, l3)) | → | app#(inter(l1, l2), inter(l1, l3)) | | *#(1(x), y) | → | +#(0(*(x, y)), y) |
| prod#(app(l1, l2)) | → | *#(prod(l1), prod(l2)) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l3) |
| *#(x, +(y, z)) | → | *#(x, z) | | prod#(cons(x, l)) | → | prod#(l) |
| inter#(l1, cons(x, l2)) | → | mem#(x, l1) | | mem#(x, cons(y, l)) | → | mem#(x, l) |
| sum#(app(l1, l2)) | → | sum#(l1) | | prod#(app(l1, l2)) | → | prod#(l1) |
| inter#(l1, app(l2, l3)) | → | inter#(l1, l2) | | ge#(0(x), 0(y)) | → | ge#(x, y) |
| mem#(x, cons(y, l)) | → | eq#(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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
The following SCCs where found
| log'#(1(x)) → log'#(x) | log'#(0(x)) → log'#(x) |
| sum#(app(l1, l2)) → sum#(l1) | sum#(cons(x, l)) → sum#(l) |
| sum#(app(l1, l2)) → sum#(l2) |
| eq#(0(x), 0(y)) → eq#(x, y) | eq#(1(x), 1(y)) → eq#(x, y) |
| inter#(l1, app(l2, l3)) → inter#(l1, l3) | inter#(l1, app(l2, l3)) → inter#(l1, l2) |
| ifinter#(true, x, l1, l2) → inter#(l1, l2) | inter#(app(l1, l2), l3) → inter#(l2, l3) |
| inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1) | ifinter#(false, x, l1, l2) → inter#(l1, l2) |
| inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2) | inter#(app(l1, l2), l3) → inter#(l1, l3) |
| +#(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)) |
| *#(x, +(y, z)) → *#(x, z) | *#(1(x), y) → *#(x, y) |
| *#(*(x, y), z) → *#(x, *(y, z)) | *#(*(x, y), z) → *#(y, z) |
| *#(x, +(y, z)) → *#(x, y) | *#(0(x), y) → *#(x, y) |
| -#(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) |
| app#(cons(x, l1), l2) → app#(l1, l2) |
| mem#(x, cons(y, l)) → mem#(x, l) |
| 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) |
| prod#(cons(x, l)) → prod#(l) | prod#(app(l1, l2)) → prod#(l1) |
| prod#(app(l1, l2)) → prod#(l2) |
Problem 2: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sum#(app(l1, l2)) | → | sum#(l1) | | sum#(cons(x, l)) | → | sum#(l) |
| sum#(app(l1, l2)) | → | sum#(l2) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sum#(app(l1, l2)) | → | sum#(l1) | | sum#(cons(x, l)) | → | sum#(l) |
| sum#(app(l1, l2)) | → | sum#(l2) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| mem#(x, cons(y, l)) | → | mem#(x, l) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| mem#(x, cons(y, l)) | → | mem#(x, l) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| *#(x, +(y, z)) | → | *#(x, z) | | *#(1(x), y) | → | *#(x, y) |
| *#(*(x, y), z) | → | *#(x, *(y, z)) | | *#(*(x, y), z) | → | *#(y, z) |
| *#(x, +(y, z)) | → | *#(x, y) | | *#(0(x), 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| *#(1(x), y) | → | *#(x, y) | | *#(*(x, y), z) | → | *#(y, z) |
| *#(*(x, y), z) | → | *#(x, *(y, z)) | | *#(0(x), y) | → | *#(x, y) |
Problem 16: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| *#(x, +(y, z)) | → | *#(x, z) | | *#(x, +(y, z)) | → | *#(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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| *#(x, +(y, z)) | → | *#(x, z) | | *#(x, +(y, z)) | → | *#(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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| log'#(1(x)) | → | log'#(x) | | log'#(0(x)) | → | log'#(x) |
Problem 7: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(0(x), 0(y)) | → | eq#(x, y) | | eq#(1(x), 1(y)) | → | eq#(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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(0(x), 0(y)) | → | eq#(x, y) | | eq#(1(x), 1(y)) | → | eq#(x, y) |
Problem 9: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 10: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): y + x
- +#(x,y): y + 2x
- -(x,y): 0
- 0(x): 2x
- 1(x): 2x + 1
- app(x,y): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- inter(x,y): 0
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 0
- not(x): 0
- prod(x): 0
- sum(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 17: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq
Strategy
Polynomial Interpretation
- #: 1
- *(x,y): 0
- +(x,y): 2y + x
- +#(x,y): x
- -(x,y): 0
- 0(x): x + 1
- 1(x): 0
- app(x,y): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- inter(x,y): 0
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 0
- not(x): 0
- prod(x): 0
- sum(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 21: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): 2y + x + 1
- +#(x,y): x
- -(x,y): 0
- 0(x): 0
- 1(x): 3x
- app(x,y): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- inter(x,y): 0
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 0
- not(x): 0
- prod(x): 0
- sum(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 11: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- 0(x): 2x
- 1(x): x + 1
- app(x,y): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- ge(x,y): 0
- ge#(x,y): 2y + x
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- inter(x,y): 0
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 0
- not(x): 0
- prod(x): 0
- sum(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 18: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- 0(x): 2x + 1
- 1(x): 0
- app(x,y): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- ge(x,y): 0
- ge#(x,y): y
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- inter(x,y): 0
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 0
- not(x): 0
- prod(x): 0
- sum(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 12: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l2) |
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) | | inter#(app(l1, l2), l3) | → | inter#(l2, l3) |
| inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) | | ifinter#(false, x, l1, l2) | → | inter#(l1, l2) |
| inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) | | inter#(app(l1, l2), l3) | → | inter#(l1, l3) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Polynomial Interpretation
- #: 1
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- 0(x): 3x + 3
- 1(x): 3x + 1
- app(x,y): 2y + x
- cons(x,y): 3y + x + 1
- eq(x,y): 0
- false: 1
- ge(x,y): 0
- if(x,y,z): z + y
- ifinter(x1,x2,x3,x4): 0
- ifinter#(x1,x2,x3,x4): 2x4 + 3x3 + 2x1
- inter(x,y): 0
- inter#(x,y): 2y + 2x
- log(x): 0
- log'(x): 0
- mem(x,y): 1
- nil: 3
- not(x): 0
- prod(x): 0
- sum(x): 0
- true: 0
Improved Usable rules
| if(false, x, y) | → | y | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | if(true, x, y) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ifinter#(false, x, l1, l2) | → | inter#(l1, l2) |
Problem 19: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l2) |
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) | | inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) |
| inter#(app(l1, l2), l3) | → | inter#(l2, l3) | | inter#(app(l1, l2), l3) | → | inter#(l1, l3) |
| inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- 0(x): 3x
- 1(x): 3
- app(x,y): y + x + 2
- cons(x,y): y + 3x + 2
- eq(x,y): 0
- false: 1
- ge(x,y): 0
- if(x,y,z): z + y
- ifinter(x1,x2,x3,x4): 0
- ifinter#(x1,x2,x3,x4): x4 + x3 + x2 + x1
- inter(x,y): 0
- inter#(x,y): y + x
- log(x): 0
- log'(x): 0
- mem(x,y): x + 2
- nil: 3
- not(x): 0
- prod(x): 0
- sum(x): 0
- true: 0
Improved Usable rules
| if(false, x, y) | → | y | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | if(true, x, y) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| inter#(l1, app(l2, l3)) | → | inter#(l1, l3) | | inter#(l1, app(l2, l3)) | → | inter#(l1, l2) |
| inter#(app(l1, l2), l3) | → | inter#(l2, l3) | | inter#(app(l1, l2), l3) | → | inter#(l1, l3) |
Problem 22: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) | | inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) |
| inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Polynomial Interpretation
- #: 3
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- 0(x): 3
- 1(x): 2
- app(x,y): 0
- cons(x,y): 3y + 3x + 1
- eq(x,y): y
- false: 1
- ge(x,y): 0
- if(x,y,z): z + y
- ifinter(x1,x2,x3,x4): 0
- ifinter#(x1,x2,x3,x4): 2x4 + 3x3 + 2x1
- inter(x,y): 0
- inter#(x,y): 2y + 3x
- log(x): 0
- log'(x): 0
- mem(x,y): 1
- nil: 3
- not(x): 0
- prod(x): 0
- sum(x): 0
- true: 0
Improved Usable rules
| if(false, x, y) | → | y | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | if(true, x, y) | → | x |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| inter#(cons(x, l1), l2) | → | ifinter#(mem(x, l2), x, l1, l2) |
Problem 23: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) | | inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- 0(x): 1
- 1(x): 1
- app(x,y): 0
- cons(x,y): y + 2
- eq(x,y): 2y
- false: 3
- ge(x,y): 0
- if(x,y,z): 3z + y
- ifinter(x1,x2,x3,x4): 0
- ifinter#(x1,x2,x3,x4): x4 + x3
- inter(x,y): 0
- inter#(x,y): y + x
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 3
- not(x): 0
- prod(x): 0
- sum(x): 0
- true: 1
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| inter#(l1, cons(x, l2)) | → | ifinter#(mem(x, l1), x, l2, l1) |
Problem 24: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ifinter#(true, x, l1, l2) | → | inter#(l1, l2) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
There are no SCCs!
Problem 13: 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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): 0
- -(x,y): 2y + x
- -#(x,y): 2y
- 0(x): 2x + 1
- 1(x): 2x
- app(x,y): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- inter(x,y): 0
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 0
- not(x): 0
- prod(x): 0
- sum(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:
| -#(1(x), 0(y)) | → | -#(x, y) | | -#(0(x), 0(y)) | → | -#(x, y) |
Problem 20: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(0(x), 1(y)) | → | -#(x, y) | | -#(0(x), 1(y)) | → | -#(-(x, y), 1(#)) |
| -#(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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq
Strategy
Polynomial Interpretation
- #: 0
- *(x,y): 0
- +(x,y): 0
- -(x,y): x
- -#(x,y): 2x + 1
- 0(x): 2x + 1
- 1(x): 2x + 1
- app(x,y): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- ge(x,y): 0
- if(x,y,z): 0
- ifinter(x1,x2,x3,x4): 0
- inter(x,y): 0
- log(x): 0
- log'(x): 0
- mem(x,y): 0
- nil: 0
- not(x): 0
- prod(x): 0
- sum(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:
| -#(0(x), 1(y)) | → | -#(x, y) | | -#(0(x), 1(y)) | → | -#(-(x, y), 1(#)) |
| -#(1(x), 1(y)) | → | -#(x, y) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| app#(cons(x, l1), l2) | → | app#(l1, l2) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| app#(cons(x, l1), l2) | → | app#(l1, l2) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| prod#(cons(x, l)) | → | prod#(l) | | prod#(app(l1, l2)) | → | prod#(l1) |
| prod#(app(l1, l2)) | → | prod#(l2) |
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 |
| eq(#, #) | → | true | | eq(#, 1(y)) | → | false |
| eq(1(x), #) | → | false | | eq(#, 0(y)) | → | eq(#, y) |
| eq(0(x), #) | → | eq(x, #) | | eq(1(x), 1(y)) | → | eq(x, y) |
| eq(0(x), 1(y)) | → | false | | eq(1(x), 0(y)) | → | false |
| eq(0(x), 0(y)) | → | eq(x, 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(#)), #) |
| *(#, x) | → | # | | *(0(x), y) | → | 0(*(x, y)) |
| *(1(x), y) | → | +(0(*(x, y)), y) | | *(*(x, y), z) | → | *(x, *(y, z)) |
| *(x, +(y, z)) | → | +(*(x, y), *(x, z)) | | app(nil, l) | → | l |
| app(cons(x, l1), l2) | → | cons(x, app(l1, l2)) | | sum(nil) | → | 0(#) |
| sum(cons(x, l)) | → | +(x, sum(l)) | | sum(app(l1, l2)) | → | +(sum(l1), sum(l2)) |
| prod(nil) | → | 1(#) | | prod(cons(x, l)) | → | *(x, prod(l)) |
| prod(app(l1, l2)) | → | *(prod(l1), prod(l2)) | | mem(x, nil) | → | false |
| mem(x, cons(y, l)) | → | if(eq(x, y), true, mem(x, l)) | | inter(x, nil) | → | nil |
| inter(nil, x) | → | nil | | inter(app(l1, l2), l3) | → | app(inter(l1, l3), inter(l2, l3)) |
| inter(l1, app(l2, l3)) | → | app(inter(l1, l2), inter(l1, l3)) | | inter(cons(x, l1), l2) | → | ifinter(mem(x, l2), x, l1, l2) |
| inter(l1, cons(x, l2)) | → | ifinter(mem(x, l1), x, l2, l1) | | ifinter(true, x, l1, l2) | → | cons(x, inter(l1, l2)) |
| ifinter(false, x, l1, l2) | → | inter(l1, l2) |
Original Signature
Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| prod#(cons(x, l)) | → | prod#(l) | | prod#(app(l1, l2)) | → | prod#(l1) |
| prod#(app(l1, l2)) | → | prod#(l2) |