TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60011 ms.
The following DP Processors were used
Problem 1 was processed with processor ForwardNarrowing (11ms).
| – Problem 2 was processed with processor ForwardNarrowing (3ms).
| | – Problem 3 was processed with processor ForwardNarrowing (3ms).
| | | – Problem 4 was processed with processor ForwardNarrowing (4ms).
| | | | – Problem 5 was processed with processor ForwardNarrowing (4ms).
| | | | | – Problem 6 was processed with processor ForwardNarrowing (3ms).
| | | | | | – Problem 7 was processed with processor ForwardNarrowing (5ms).
| | | | | | | – Problem 8 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | – Problem 9 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | – Problem 10 was processed with processor ForwardNarrowing (45ms).
| | | | | | | | | | – Problem 11 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | – Problem 12 was processed with processor ForwardNarrowing (5ms).
| | | | | | | | | | | | – Problem 13 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | | | – Problem 14 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | – Problem 15 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | | – Problem 16 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | | | | | – Problem 17 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | | | | | | | – Problem 18 was processed with processor ForwardNarrowing (9ms).
| | | | | | | | | | | | | | | | | | – Problem 19 was processed with processor ForwardInstantiation (36ms).
| | | | | | | | | | | | | | | | | | | – Problem 20 was processed with processor Propagation (60ms).
| | | | | | | | | | | | | | | | | | | | – Problem 21 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | | | | | | | | | | | – Problem 22 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | | | | | | | | | | | – Problem 23 was processed with processor ForwardNarrowing (37ms).
| | | | | | | | | | | | | | | | | | | | | | | – Problem 24 was processed with processor ForwardNarrowing (12ms).
| | | | | | | | | | | | | | | | | | | | | | | | – Problem 25 remains open; application of the following processors failed [ForwardNarrowing (40ms), BackwardInstantiation (24ms), ForwardInstantiation (19ms), Propagation (26ms), ForwardNarrowing (6ms), BackwardInstantiation (17ms), ForwardInstantiation (16ms), Propagation (27ms)].
The following open problems remain:
Open Dependency Pair Problem 1
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| *#(+(y, z), x) | → | *#(x, y) | | +#(.(x, y), z) | → | .#(x, +(y, z)) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| *#(2, min) | → | .#(min, 2) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | .#(x, min) | → | .#(+(min, x), 3) |
| +#(3, x) | → | +#(min, x) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| *#(3, x) | → | *#(min, x) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, y), z) | → | +#(y, z) | | *#(3, x) | → | .#(x, *(min, x)) |
| +#(3, x) | → | .#(1, +(min, x)) | | *#(.(x, y), z) | → | *#(y, z) |
| *#(+(y, z), x) | → | *#(x, z) | | *#(2, 2) | → | .#(1, 0) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Problem 1: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| *#(+(y, z), x) | → | *#(x, y) | | +#(.(x, y), z) | → | .#(x, +(y, z)) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| *#(2, min) | → | .#(min, 2) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | .#(x, min) | → | .#(+(min, x), 3) |
| +#(3, x) | → | +#(min, x) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| *#(3, x) | → | *#(min, x) | | +#(.(x, y), z) | → | +#(y, z) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(3, x) | → | .#(x, *(min, x)) | | *#(.(x, y), z) | → | *#(y, z) |
| *#(+(y, z), x) | → | *#(x, z) | | *#(2, 2) | → | .#(1, 0) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(.(
x,
y),
z) → .
#(
x, +(
y,
z)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| .#(x, .(_x33, +(_x32, _x31))) | |
| .#(x, .(1, +(min, _x31))) | |
| .#(x, 0) | |
| .#(x, *(2, _x31)) | |
| .#(x, _x31) | |
| .#(x, *(3, _x31)) | |
| .#(x, 1) | |
| .#(x, 3) | |
Thus, the rule +
#(.(
x,
y),
z) → .
#(
x, +(
y,
z)) is replaced by the following rules:
| +#(.(x, .(_x33, _x32)), _x31) → .#(x, .(_x33, +(_x32, _x31))) | +#(.(x, 3), _x31) → .#(x, .(1, +(min, _x31))) |
| +#(.(x, _x31), _x31) → .#(x, *(2, _x31)) | +#(.(x, *(min, _x31)), _x31) → .#(x, 0) |
| +#(.(x, 1), 2) → .#(x, 3) | +#(.(x, *(2, _x31)), *(min, _x31)) → .#(x, _x31) |
| +#(.(x, *(2, _x31)), _x31) → .#(x, *(3, _x31)) | +#(.(x, 0), _x31) → .#(x, _x31) |
| +#(.(x, 1), min) → .#(x, 0) | +#(.(x, 2), min) → .#(x, 1) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, *(2, _x31)), _x31) | → | .#(x, *(3, _x31)) | | +#(.(x, 0), _x31) | → | .#(x, _x31) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(3, x) | → | +#(min, x) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| *#(3, x) | → | *#(min, x) | | +#(.(x, y), z) | → | +#(y, z) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(3, x) | → | .#(x, *(min, x)) |
| *#(.(x, y), z) | → | *#(y, z) | | +#(.(x, 1), min) | → | .#(x, 0) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| +#(.(x, *(min, _x31)), _x31) | → | .#(x, 0) | | +#(.(x, 1), 2) | → | .#(x, 3) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| *#(2, min) | → | .#(min, 2) | | .#(x, min) | → | .#(+(min, x), 3) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(+(y, z), x) | → | *#(x, z) | | *#(2, 2) | → | .#(1, 0) |
| +#(.(x, 2), min) | → | .#(x, 1) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(.(
x, *(2,
_x31)),
_x31) → .
#(
x, *(3,
_x31)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| .#(x, .(_x41, *(min, _x41))) | |
Thus, the rule +
#(.(
x, *(2,
_x31)),
_x31) → .
#(
x, *(3,
_x31)) is replaced by the following rules:
| +#(.(x, *(2, _x41)), _x41) → .#(x, .(_x41, *(min, _x41))) |
Problem 3: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(3, x) | → | +#(min, x) |
| *#(3, x) | → | *#(min, x) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| +#(.(x, y), z) | → | +#(y, z) | | *#(3, x) | → | .#(x, *(min, x)) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(.(x, y), z) | → | *#(y, z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | +#(.(x, 1), min) | → | .#(x, 0) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| +#(.(x, *(min, _x31)), _x31) | → | .#(x, 0) | | +#(.(x, 1), 2) | → | .#(x, 3) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| *#(2, min) | → | .#(min, 2) | | .#(x, min) | → | .#(+(min, x), 3) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, 2), min) | → | .#(x, 1) |
| *#(2, 2) | → | .#(1, 0) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule *
#(3,
x) → *
#(min,
x) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(3,
x) → *
#(min,
x) is deleted.
Problem 4: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(3, x) | → | .#(x, *(min, x)) |
| *#(.(x, y), z) | → | *#(y, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| +#(.(x, 1), min) | → | .#(x, 0) | | *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) |
| +#(x, x) | → | *#(2, x) | | +#(.(x, *(min, _x31)), _x31) | → | .#(x, 0) |
| +#(.(x, 1), 2) | → | .#(x, 3) | | *#(.(x, y), z) | → | *#(x, z) |
| .#(x, min) | → | +#(min, x) | | *#(2, min) | → | .#(min, 2) |
| .#(x, min) | → | .#(+(min, x), 3) | | +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) |
| +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(3, x) | → | .#(1, +(min, x)) | | *#(+(y, z), x) | → | *#(x, z) |
| *#(2, 2) | → | .#(1, 0) | | +#(.(x, 2), min) | → | .#(x, 1) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(.(
x, 1), min) → .
#(
x, 0) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule +
#(.(
x, 1), min) → .
#(
x, 0) is deleted.
Problem 5: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| *#(3, x) | → | .#(x, *(min, x)) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(.(x, y), z) | → | *#(y, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| +#(.(x, *(min, _x31)), _x31) | → | .#(x, 0) | | +#(.(x, 1), 2) | → | .#(x, 3) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| *#(2, min) | → | .#(min, 2) | | .#(x, min) | → | .#(+(min, x), 3) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, 2), min) | → | .#(x, 1) |
| *#(2, 2) | → | .#(1, 0) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(.(
x, *(min,
_x31)),
_x31) → .
#(
x, 0) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule +
#(.(
x, *(min,
_x31)),
_x31) → .
#(
x, 0) is deleted.
Problem 6: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(3, x) | → | .#(x, *(min, x)) |
| *#(.(x, y), z) | → | *#(y, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| +#(.(x, 1), 2) | → | .#(x, 3) | | *#(.(x, y), z) | → | *#(x, z) |
| .#(x, min) | → | +#(min, x) | | *#(2, min) | → | .#(min, 2) |
| .#(x, min) | → | .#(+(min, x), 3) | | +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) |
| +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(3, x) | → | .#(1, +(min, x)) | | *#(+(y, z), x) | → | *#(x, z) |
| *#(2, 2) | → | .#(1, 0) | | +#(.(x, 2), min) | → | .#(x, 1) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(.(
x, 1), 2) → .
#(
x, 3) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule +
#(.(
x, 1), 2) → .
#(
x, 3) is deleted.
Problem 7: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| *#(3, x) | → | .#(x, *(min, x)) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(.(x, y), z) | → | *#(y, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| *#(2, min) | → | .#(min, 2) | | .#(x, min) | → | .#(+(min, x), 3) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(+(y, z), x) | → | *#(x, z) | | *#(2, 2) | → | .#(1, 0) |
| +#(.(x, 2), min) | → | .#(x, 1) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule *
#(2, min) → .
#(min, 2) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(2, min) → .
#(min, 2) is deleted.
Problem 8: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) |
| +#(x, x) | → | *#(2, x) | | *#(+(y, z), x) | → | *#(x, y) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) |
| .#(x, min) | → | .#(+(min, x), 3) | | +#(3, x) | → | +#(min, x) |
| +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(.(x, y), z) | → | +#(y, z) |
| +#(3, x) | → | .#(1, +(min, x)) | | *#(3, x) | → | .#(x, *(min, x)) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(.(x, y), z) | → | *#(y, z) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| +#(.(x, 2), min) | → | .#(x, 1) | | *#(2, 2) | → | .#(1, 0) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule .
#(
x, min) → .
#(+(min,
x), 3) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| .#(*(2, min), 3) | |
Thus, the rule .
#(
x, min) → .
#(+(min,
x), 3) is replaced by the following rules:
| .#(min, min) → .#(*(2, min), 3) |
Problem 9: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) |
| +#(x, x) | → | *#(2, x) | | *#(+(y, z), x) | → | *#(x, y) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) |
| +#(3, x) | → | +#(min, x) | | +#(.(x, _x31), _x31) | → | .#(x, *(2, _x31)) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(3, x) | → | .#(x, *(min, x)) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(.(x, y), z) | → | *#(y, z) | | *#(+(y, z), x) | → | *#(x, z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | *#(2, 2) | → | .#(1, 0) |
| +#(.(x, 2), min) | → | .#(x, 1) | | .#(min, min) | → | .#(*(2, min), 3) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(.(
x,
_x31),
_x31) → .
#(
x, *(2,
_x31)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| .#(x, .(1, 0)) | |
| .#(x, .(min, 2)) | |
Thus, the rule +
#(.(
x,
_x31),
_x31) → .
#(
x, *(2,
_x31)) is replaced by the following rules:
| +#(.(x, 2), 2) → .#(x, .(1, 0)) | +#(.(x, min), min) → .#(x, .(min, 2)) |
Problem 10: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, min), min) | → | .#(x, .(min, 2)) | | +#(.(x, 0), _x31) | → | .#(x, _x31) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(3, x) | → | +#(min, x) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| +#(.(x, y), z) | → | +#(y, z) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(3, x) | → | .#(x, *(min, x)) | | *#(.(x, y), z) | → | *#(y, z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | .#(min, min) | → | .#(*(2, min), 3) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, 2), min) | → | .#(x, 1) |
| *#(2, 2) | → | .#(1, 0) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule .
#(min, min) → .
#(*(2, min), 3) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| .#(.(min, 2), 3) | |
Thus, the rule .
#(min, min) → .
#(*(2, min), 3) is replaced by the following rules:
| .#(min, min) → .#(.(min, 2), 3) |
Problem 11: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(+(y, z), x) | → | *#(x, y) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(3, x) | → | +#(min, x) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| +#(.(x, y), z) | → | +#(y, z) | | *#(3, x) | → | .#(x, *(min, x)) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(.(x, y), z) | → | *#(y, z) |
| .#(min, min) | → | .#(.(min, 2), 3) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(x, x) | → | *#(2, x) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | +#(3, x) | → | .#(1, +(min, x)) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, 2), min) | → | .#(x, 1) |
| *#(2, 2) | → | .#(1, 0) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule .
#(min, min) → .
#(.(min, 2), 3) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule .
#(min, min) → .
#(.(min, 2), 3) is deleted.
Problem 12: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| +#(x, x) | → | *#(2, x) | | *#(+(y, z), x) | → | *#(x, y) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, y), z) | → | +#(y, z) | | +#(.(x, 2), 2) | → | .#(x, .(1, 0)) |
| +#(3, x) | → | .#(1, +(min, x)) | | *#(3, x) | → | .#(x, *(min, x)) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(.(x, y), z) | → | *#(y, z) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(2, 2) | → | .#(1, 0) | | +#(.(x, 2), min) | → | .#(x, 1) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(3,
x) → .
#(1, +(min,
x)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| .#(1, *(2, min)) | |
Thus, the rule +
#(3,
x) → .
#(1, +(min,
x)) is replaced by the following rules:
| +#(3, min) → .#(1, *(2, min)) |
Problem 13: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| +#(x, x) | → | *#(2, x) | | *#(+(y, z), x) | → | *#(x, y) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(.(x, 2), 2) | → | .#(x, .(1, 0)) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(3, x) | → | .#(x, *(min, x)) |
| *#(.(x, y), z) | → | *#(y, z) | | *#(+(y, z), x) | → | *#(x, z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | +#(.(x, 2), min) | → | .#(x, 1) |
| *#(2, 2) | → | .#(1, 0) | | +#(3, min) | → | .#(1, *(2, min)) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule *
#(2, 2) → .
#(1, 0) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(2, 2) → .
#(1, 0) is deleted.
Problem 14: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| +#(x, x) | → | *#(2, x) | | *#(+(y, z), x) | → | *#(x, y) |
| *#(.(x, y), z) | → | *#(x, z) | | .#(x, min) | → | +#(min, x) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, y), z) | → | +#(y, z) | | +#(.(x, 2), 2) | → | .#(x, .(1, 0)) |
| *#(3, x) | → | .#(x, *(min, x)) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(.(x, y), z) | → | *#(y, z) | | *#(+(y, z), x) | → | *#(x, z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | +#(.(x, 2), min) | → | .#(x, 1) |
| +#(3, min) | → | .#(1, *(2, min)) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(
x,
x) → *
#(2,
x) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule +
#(
x,
x) → *
#(2,
x) is deleted.
Problem 15: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| *#(+(y, z), x) | → | *#(x, y) | | *#(.(x, y), z) | → | *#(x, z) |
| .#(x, min) | → | +#(min, x) | | +#(.(x, 0), _x31) | → | .#(x, _x31) |
| +#(.(x, min), min) | → | .#(x, .(min, 2)) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) |
| +#(3, x) | → | +#(min, x) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| +#(.(x, y), z) | → | +#(y, z) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(3, x) | → | .#(x, *(min, x)) | | *#(.(x, y), z) | → | *#(y, z) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| +#(.(x, 2), min) | → | .#(x, 1) | | +#(3, min) | → | .#(1, *(2, min)) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule .
#(
x, min) → +
#(min,
x) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule .
#(
x, min) → +
#(min,
x) is deleted.
Problem 16: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| *#(+(y, z), x) | → | *#(x, y) | | *#(.(x, y), z) | → | *#(x, z) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(3, x) | → | +#(min, x) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(.(x, 2), 2) | → | .#(x, .(1, 0)) |
| *#(3, x) | → | .#(x, *(min, x)) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(.(x, y), z) | → | *#(y, z) | | *#(+(y, z), x) | → | *#(x, z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | +#(.(x, 2), min) | → | .#(x, 1) |
| +#(3, min) | → | .#(1, *(2, min)) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(3,
x) → +
#(min,
x) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule +
#(3,
x) → +
#(min,
x) is deleted.
Problem 17: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| *#(+(y, z), x) | → | *#(x, y) | | *#(.(x, y), z) | → | *#(x, z) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| +#(.(x, y), z) | → | +#(y, z) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) |
| *#(3, x) | → | .#(x, *(min, x)) | | *#(.(x, y), z) | → | *#(y, z) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| +#(.(x, 2), min) | → | .#(x, 1) | | +#(3, min) | → | .#(1, *(2, min)) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(.(
x, 2), min) → .
#(
x, 1) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule +
#(.(
x, 2), min) → .
#(
x, 1) is deleted.
Problem 18: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| *#(+(y, z), x) | → | *#(x, y) | | *#(.(x, y), z) | → | *#(x, z) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(*(2, x), x) | → | *#(3, x) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| +#(.(x, y), z) | → | +#(y, z) | | .#(x, .(y, z)) | → | +#(x, y) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | *#(3, x) | → | .#(x, *(min, x)) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(.(x, y), z) | → | *#(y, z) |
| *#(+(y, z), x) | → | *#(x, z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| +#(3, min) | → | .#(1, *(2, min)) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule +
#(3, min) → .
#(1, *(2, min)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| .#(1, .(min, 2)) | |
Thus, the rule +
#(3, min) → .
#(1, *(2, min)) is replaced by the following rules:
| +#(3, min) → .#(1, .(min, 2)) |
Problem 19: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) |
| *#(+(y, z), x) | → | *#(x, y) | | *#(.(x, y), z) | → | *#(x, z) |
| +#(.(x, 0), _x31) | → | .#(x, _x31) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| +#(3, min) | → | .#(1, .(min, 2)) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(*(2, x), x) | → | *#(3, x) | | +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | +#(.(x, y), z) | → | +#(y, z) |
| .#(x, .(y, z)) | → | +#(x, y) | | +#(.(x, 2), 2) | → | .#(x, .(1, 0)) |
| +#(.(x, *(2, _x31)), *(min, _x31)) | → | .#(x, _x31) | | *#(3, x) | → | .#(x, *(min, x)) |
| *#(.(x, y), z) | → | *#(y, z) | | *#(+(y, z), x) | → | *#(x, z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
Instantiation
For all potential successors l → r of the rule *
#(+(
y,
z),
x) → *
#(
x,
y) on dependency pair chains it holds that:
- *#(x, y) matches l,
- all variables of *#(x, y) are embedded in constructor contexts, i.e., each subterm of *#(x, y) containing a variable is rooted by a constructor symbol.
Thus, *
#(+(
y,
z),
x) → *
#(
x,
y) is replaced by instances determined through the above matching. These instances are:
| *#(+(y, z), .(_x, _y)) → *#(.(_x, _y), y) | *#(+(y, z), +(_y, _z)) → *#(+(_y, _z), y) |
| *#(+(y, z), 3) → *#(3, y) |
Instantiation
For all potential successors l → r of the rule *
#(.(
x,
y),
z) → *
#(
x,
z) on dependency pair chains it holds that:
- *#(x, z) matches l,
- all variables of *#(x, z) are embedded in constructor contexts, i.e., each subterm of *#(x, z) containing a variable is rooted by a constructor symbol.
Thus, *
#(.(
x,
y),
z) → *
#(
x,
z) is replaced by instances determined through the above matching. These instances are:
| *#(.(.(_x, _y), y), z) → *#(.(_x, _y), z) | *#(.(+(_y, _z), y), z) → *#(+(_y, _z), z) |
| *#(.(3, y), z) → *#(3, z) |
Instantiation
For all potential successors l → r of the rule +
#(.(
x, 0),
_x31) → .
#(
x,
_x31) on dependency pair chains it holds that:
- .#(x, _x31) matches l,
- all variables of .#(x, _x31) are embedded in constructor contexts, i.e., each subterm of .#(x, _x31) containing a variable is rooted by a constructor symbol.
Thus, +
#(.(
x, 0),
_x31) → .
#(
x,
_x31) is replaced by instances determined through the above matching. These instances are:
| +#(.(x, 0), .(_y, _z)) → .#(x, .(_y, _z)) |
Instantiation
For all potential successors l → r of the rule +
#(.(
x,
y),
z) → +
#(
y,
z) on dependency pair chains it holds that:
- +#(y, z) matches l,
- all variables of +#(y, z) are embedded in constructor contexts, i.e., each subterm of +#(y, z) containing a variable is rooted by a constructor symbol.
Thus, +
#(.(
x,
y),
z) → +
#(
y,
z) is replaced by instances determined through the above matching. These instances are:
| +#(.(x, 3), min) → +#(3, min) | +#(.(x, .(_x, _y)), z) → +#(.(_x, _y), z) |
| +#(.(x, .(x, 3)), z) → +#(.(x, 3), z) | +#(.(x, .(x, *(2, _x31))), *(min, _x31)) → +#(.(x, *(2, _x31)), *(min, _x31)) |
| +#(.(x, .(x, 2)), 2) → +#(.(x, 2), 2) | +#(.(x, .(x, min)), min) → +#(.(x, min), min) |
| +#(.(x, .(x, *(2, z))), z) → +#(.(x, *(2, z)), z) | +#(.(x, .(x, 0)), z) → +#(.(x, 0), z) |
| +#(.(x, .(x, .(_x33, _x32))), z) → +#(.(x, .(_x33, _x32)), z) | +#(.(z, *(2, z)), z) → +#(*(2, z), z) |
Instantiation
For all potential successors l → r of the rule .
#(
x, .(
y,
z)) → +
#(
x,
y) on dependency pair chains it holds that:
- +#(x, y) matches l,
- all variables of +#(x, y) are embedded in constructor contexts, i.e., each subterm of +#(x, y) containing a variable is rooted by a constructor symbol.
Thus, .
#(
x, .(
y,
z)) → +
#(
x,
y) is replaced by instances determined through the above matching. These instances are:
| .#(.(_x, *(2, __x31)), .(*(min, __x31), z)) → +#(.(_x, *(2, __x31)), *(min, __x31)) | .#(.(_x, _y), .(y, z)) → +#(.(_x, _y), y) |
| .#(3, .(min, z)) → +#(3, min) | .#(.(_x, .(__x33, __x32)), .(y, z)) → +#(.(_x, .(__x33, __x32)), y) |
| .#(*(2, y), .(y, z)) → +#(*(2, y), y) | .#(.(_x, 0), .(y, z)) → +#(.(_x, 0), y) |
| .#(.(_x, *(2, y)), .(y, z)) → +#(.(_x, *(2, y)), y) | .#(.(_x, 3), .(y, z)) → +#(.(_x, 3), y) |
| .#(.(_x, min), .(min, z)) → +#(.(_x, min), min) | .#(.(_x, 2), .(2, z)) → +#(.(_x, 2), 2) |
Instantiation
For all potential successors l → r of the rule +
#(.(
x, *(2,
_x31)), *(min,
_x31)) → .
#(
x,
_x31) on dependency pair chains it holds that:
- .#(x, _x31) matches l,
- all variables of .#(x, _x31) are embedded in constructor contexts, i.e., each subterm of .#(x, _x31) containing a variable is rooted by a constructor symbol.
Thus, +
#(.(
x, *(2,
_x31)), *(min,
_x31)) → .
#(
x,
_x31) is replaced by instances determined through the above matching. These instances are:
| +#(.(x, *(2, .(_y, _z))), *(min, .(_y, _z))) → .#(x, .(_y, _z)) |
Instantiation
For all potential successors l → r of the rule *
#(.(
x,
y),
z) → *
#(
y,
z) on dependency pair chains it holds that:
- *#(y, z) matches l,
- all variables of *#(y, z) are embedded in constructor contexts, i.e., each subterm of *#(y, z) containing a variable is rooted by a constructor symbol.
Thus, *
#(.(
x,
y),
z) → *
#(
y,
z) is replaced by instances determined through the above matching. These instances are:
| *#(.(x, .(_x, _y)), z) → *#(.(_x, _y), z) | *#(.(x, +(_y, _z)), z) → *#(+(_y, _z), z) |
| *#(.(z, 3), z) → *#(3, z) |
Instantiation
For all potential successors l → r of the rule *
#(+(
y,
z),
x) → *
#(
x,
z) on dependency pair chains it holds that:
- *#(x, z) matches l,
- all variables of *#(x, z) are embedded in constructor contexts, i.e., each subterm of *#(x, z) containing a variable is rooted by a constructor symbol.
Thus, *
#(+(
y,
z),
x) → *
#(
x,
z) is replaced by instances determined through the above matching. These instances are:
| *#(+(y, z), 3) → *#(3, z) | *#(+(y, z), +(_y, _z)) → *#(+(_y, _z), z) |
| *#(+(y, z), .(_x, _y)) → *#(.(_x, _y), z) |
Problem 20: Propagation
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(.(z, 3), z) | → | *#(3, z) |
| .#(.(_x, 0), .(y, z)) | → | +#(.(_x, 0), y) | | +#(.(x, .(x, 3)), z) | → | +#(.(x, 3), z) |
| +#(.(x, 0), .(_y, _z)) | → | .#(x, .(_y, _z)) | | *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), z) |
| +#(.(x, .(x, 2)), 2) | → | +#(.(x, 2), 2) | | .#(.(_x, min), .(min, z)) | → | +#(.(_x, min), min) |
| +#(.(x, min), min) | → | .#(x, .(min, 2)) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(.(z, *(2, z)), z) | → | +#(*(2, z), z) | | +#(*(2, x), x) | → | *#(3, x) |
| .#(.(_x, _y), .(y, z)) | → | +#(.(_x, _y), y) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| *#(.(x, +(_y, _z)), z) | → | *#(+(_y, _z), z) | | .#(*(2, y), .(y, z)) | → | +#(*(2, y), y) |
| +#(.(x, .(_x, _y)), z) | → | +#(.(_x, _y), z) | | *#(3, x) | → | .#(x, *(min, x)) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | *#(.(+(_y, _z), y), z) | → | *#(+(_y, _z), z) |
| +#(.(x, *(2, .(_y, _z))), *(min, .(_y, _z))) | → | .#(x, .(_y, _z)) | | +#(.(x, .(x, *(2, z))), z) | → | +#(.(x, *(2, z)), z) |
| *#(.(3, y), z) | → | *#(3, z) | | *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) |
| .#(.(_x, *(2, __x31)), .(*(min, __x31), z)) | → | +#(.(_x, *(2, __x31)), *(min, __x31)) | | .#(.(_x, .(__x33, __x32)), .(y, z)) | → | +#(.(_x, .(__x33, __x32)), y) |
| .#(.(_x, *(2, y)), .(y, z)) | → | +#(.(_x, *(2, y)), y) | | *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), y) |
| +#(.(x, .(x, min)), min) | → | +#(.(x, min), min) | | .#(.(_x, 2), .(2, z)) | → | +#(.(_x, 2), 2) |
| *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), z) | | +#(3, min) | → | .#(1, .(min, 2)) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | *#(.(x, .(_x, _y)), z) | → | *#(.(_x, _y), z) |
| *#(+(y, z), 3) | → | *#(3, z) | | *#(.(.(_x, _y), y), z) | → | *#(.(_x, _y), z) |
| +#(.(x, 3), min) | → | +#(3, min) | | .#(3, .(min, z)) | → | +#(3, min) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | +#(.(x, .(x, *(2, _x31))), *(min, _x31)) | → | +#(.(x, *(2, _x31)), *(min, _x31)) |
| .#(.(_x, 3), .(y, z)) | → | +#(.(_x, 3), y) | | +#(.(x, .(x, .(_x33, _x32))), z) | → | +#(.(x, .(_x33, _x32)), z) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), y) | | *#(+(y, z), 3) | → | *#(3, y) |
| +#(.(x, .(x, 0)), z) | → | +#(.(x, 0), z) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The dependency pairs +
#(*(2,
x),
x) → *
#(3,
x) and *
#(3,
x) → .
#(
x, *(min,
x)) are consolidated into the rule +
#(*(2,
x),
x) → .
#(
x, *(min,
x)) .
This is possible as
- all subterms of *#(3, x) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in *#(3, x), but non-replacing in both +#(*(2, x), x) and .#(x, *(min, x))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| *#(3, x) → .#(x, *(min, x)) | +#(*(2, x), x) → .#(x, *(min, x)) |
| +#(*(2, x), x) → *#(3, x) | |
Problem 21: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | *#(.(z, 3), z) | → | *#(3, z) |
| +#(.(x, .(x, 3)), z) | → | +#(.(x, 3), z) | | .#(.(_x, 0), .(y, z)) | → | +#(.(_x, 0), y) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), z) | | +#(.(x, 0), .(_y, _z)) | → | .#(x, .(_y, _z)) |
| +#(.(x, .(x, 2)), 2) | → | +#(.(x, 2), 2) | | .#(.(_x, min), .(min, z)) | → | +#(.(_x, min), min) |
| +#(.(x, min), min) | → | .#(x, .(min, 2)) | | *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) |
| +#(.(z, *(2, z)), z) | → | +#(*(2, z), z) | | .#(.(_x, _y), .(y, z)) | → | +#(.(_x, _y), y) |
| .#(x, .(y, z)) | → | .#(+(x, y), z) | | *#(.(x, +(_y, _z)), z) | → | *#(+(_y, _z), z) |
| .#(*(2, y), .(y, z)) | → | +#(*(2, y), y) | | +#(.(x, .(_x, _y)), z) | → | +#(.(_x, _y), z) |
| +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) | | *#(.(+(_y, _z), y), z) | → | *#(+(_y, _z), z) |
| +#(.(x, *(2, .(_y, _z))), *(min, .(_y, _z))) | → | .#(x, .(_y, _z)) | | +#(.(x, .(x, *(2, z))), z) | → | +#(.(x, *(2, z)), z) |
| *#(.(3, y), z) | → | *#(3, z) | | *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) |
| .#(.(_x, *(2, __x31)), .(*(min, __x31), z)) | → | +#(.(_x, *(2, __x31)), *(min, __x31)) | | .#(.(_x, .(__x33, __x32)), .(y, z)) | → | +#(.(_x, .(__x33, __x32)), y) |
| .#(.(_x, *(2, y)), .(y, z)) | → | +#(.(_x, *(2, y)), y) | | +#(*(2, x), x) | → | .#(x, *(min, x)) |
| *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), y) | | .#(.(_x, 2), .(2, z)) | → | +#(.(_x, 2), 2) |
| +#(.(x, .(x, min)), min) | → | +#(.(x, min), min) | | *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), z) |
| +#(3, min) | → | .#(1, .(min, 2)) | | *#(.(x, .(_x, _y)), z) | → | *#(.(_x, _y), z) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(.(x, 3), min) | → | +#(3, min) |
| *#(.(.(_x, _y), y), z) | → | *#(.(_x, _y), z) | | *#(+(y, z), 3) | → | *#(3, z) |
| .#(3, .(min, z)) | → | +#(3, min) | | +#(.(x, 2), 2) | → | .#(x, .(1, 0)) |
| +#(.(x, .(x, *(2, _x31))), *(min, _x31)) | → | +#(.(x, *(2, _x31)), *(min, _x31)) | | .#(.(_x, 3), .(y, z)) | → | +#(.(_x, 3), y) |
| +#(.(x, .(x, 0)), z) | → | +#(.(x, 0), z) | | *#(+(y, z), 3) | → | *#(3, y) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), y) | | +#(.(x, .(x, .(_x33, _x32))), z) | → | +#(.(x, .(_x33, _x32)), z) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule *
#(.(
z, 3),
z) → *
#(3,
z) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(.(
z, 3),
z) → *
#(3,
z) is deleted.
Problem 22: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | .#(.(_x, 0), .(y, z)) | → | +#(.(_x, 0), y) |
| +#(.(x, .(x, 3)), z) | → | +#(.(x, 3), z) | | +#(.(x, 0), .(_y, _z)) | → | .#(x, .(_y, _z)) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), z) | | +#(.(x, .(x, 2)), 2) | → | +#(.(x, 2), 2) |
| .#(.(_x, min), .(min, z)) | → | +#(.(_x, min), min) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(.(z, *(2, z)), z) | → | +#(*(2, z), z) |
| .#(.(_x, _y), .(y, z)) | → | +#(.(_x, _y), y) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| *#(.(x, +(_y, _z)), z) | → | *#(+(_y, _z), z) | | .#(*(2, y), .(y, z)) | → | +#(*(2, y), y) |
| +#(.(x, .(_x, _y)), z) | → | +#(.(_x, _y), z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(.(+(_y, _z), y), z) | → | *#(+(_y, _z), z) | | +#(.(x, *(2, .(_y, _z))), *(min, .(_y, _z))) | → | .#(x, .(_y, _z)) |
| +#(.(x, .(x, *(2, z))), z) | → | +#(.(x, *(2, z)), z) | | *#(.(3, y), z) | → | *#(3, z) |
| *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) | | .#(.(_x, *(2, __x31)), .(*(min, __x31), z)) | → | +#(.(_x, *(2, __x31)), *(min, __x31)) |
| .#(.(_x, .(__x33, __x32)), .(y, z)) | → | +#(.(_x, .(__x33, __x32)), y) | | .#(.(_x, *(2, y)), .(y, z)) | → | +#(.(_x, *(2, y)), y) |
| +#(*(2, x), x) | → | .#(x, *(min, x)) | | *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), y) |
| +#(.(x, .(x, min)), min) | → | +#(.(x, min), min) | | .#(.(_x, 2), .(2, z)) | → | +#(.(_x, 2), 2) |
| *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), z) | | +#(3, min) | → | .#(1, .(min, 2)) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | *#(.(x, .(_x, _y)), z) | → | *#(.(_x, _y), z) |
| *#(+(y, z), 3) | → | *#(3, z) | | *#(.(.(_x, _y), y), z) | → | *#(.(_x, _y), z) |
| +#(.(x, 3), min) | → | +#(3, min) | | .#(3, .(min, z)) | → | +#(3, min) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | +#(.(x, .(x, *(2, _x31))), *(min, _x31)) | → | +#(.(x, *(2, _x31)), *(min, _x31)) |
| .#(.(_x, 3), .(y, z)) | → | +#(.(_x, 3), y) | | +#(.(x, .(x, .(_x33, _x32))), z) | → | +#(.(x, .(_x33, _x32)), z) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), y) | | *#(+(y, z), 3) | → | *#(3, y) |
| +#(.(x, .(x, 0)), z) | → | +#(.(x, 0), z) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule *
#(.(3,
y),
z) → *
#(3,
z) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(.(3,
y),
z) → *
#(3,
z) is deleted.
Problem 23: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | +#(.(x, .(x, 3)), z) | → | +#(.(x, 3), z) |
| .#(.(_x, 0), .(y, z)) | → | +#(.(_x, 0), y) | | *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), z) |
| +#(.(x, 0), .(_y, _z)) | → | .#(x, .(_y, _z)) | | +#(.(x, .(x, 2)), 2) | → | +#(.(x, 2), 2) |
| .#(.(_x, min), .(min, z)) | → | +#(.(_x, min), min) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(.(z, *(2, z)), z) | → | +#(*(2, z), z) |
| .#(.(_x, _y), .(y, z)) | → | +#(.(_x, _y), y) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| *#(.(x, +(_y, _z)), z) | → | *#(+(_y, _z), z) | | .#(*(2, y), .(y, z)) | → | +#(*(2, y), y) |
| +#(.(x, .(_x, _y)), z) | → | +#(.(_x, _y), z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(.(+(_y, _z), y), z) | → | *#(+(_y, _z), z) | | +#(.(x, *(2, .(_y, _z))), *(min, .(_y, _z))) | → | .#(x, .(_y, _z)) |
| +#(.(x, .(x, *(2, z))), z) | → | +#(.(x, *(2, z)), z) | | *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) |
| .#(.(_x, *(2, __x31)), .(*(min, __x31), z)) | → | +#(.(_x, *(2, __x31)), *(min, __x31)) | | .#(.(_x, .(__x33, __x32)), .(y, z)) | → | +#(.(_x, .(__x33, __x32)), y) |
| .#(.(_x, *(2, y)), .(y, z)) | → | +#(.(_x, *(2, y)), y) | | +#(*(2, x), x) | → | .#(x, *(min, x)) |
| *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), y) | | .#(.(_x, 2), .(2, z)) | → | +#(.(_x, 2), 2) |
| +#(.(x, .(x, min)), min) | → | +#(.(x, min), min) | | *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), z) |
| +#(3, min) | → | .#(1, .(min, 2)) | | *#(.(x, .(_x, _y)), z) | → | *#(.(_x, _y), z) |
| +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) | | +#(.(x, 3), min) | → | +#(3, min) |
| *#(.(.(_x, _y), y), z) | → | *#(.(_x, _y), z) | | *#(+(y, z), 3) | → | *#(3, z) |
| .#(3, .(min, z)) | → | +#(3, min) | | +#(.(x, 2), 2) | → | .#(x, .(1, 0)) |
| +#(.(x, .(x, *(2, _x31))), *(min, _x31)) | → | +#(.(x, *(2, _x31)), *(min, _x31)) | | .#(.(_x, 3), .(y, z)) | → | +#(.(_x, 3), y) |
| +#(.(x, .(x, 0)), z) | → | +#(.(x, 0), z) | | *#(+(y, z), 3) | → | *#(3, y) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), y) | | +#(.(x, .(x, .(_x33, _x32))), z) | → | +#(.(x, .(_x33, _x32)), z) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: min, 3, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule *
#(+(
y,
z), 3) → *
#(3,
z) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(+(
y,
z), 3) → *
#(3,
z) is deleted.
Problem 24: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| +#(.(x, 3), _x31) | → | .#(x, .(1, +(min, _x31))) | | .#(.(_x, 0), .(y, z)) | → | +#(.(_x, 0), y) |
| +#(.(x, .(x, 3)), z) | → | +#(.(x, 3), z) | | +#(.(x, 0), .(_y, _z)) | → | .#(x, .(_y, _z)) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), z) | | +#(.(x, .(x, 2)), 2) | → | +#(.(x, 2), 2) |
| .#(.(_x, min), .(min, z)) | → | +#(.(_x, min), min) | | +#(.(x, min), min) | → | .#(x, .(min, 2)) |
| *#(+(y, z), x) | → | +#(*(x, y), *(x, z)) | | +#(.(z, *(2, z)), z) | → | +#(*(2, z), z) |
| .#(.(_x, _y), .(y, z)) | → | +#(.(_x, _y), y) | | .#(x, .(y, z)) | → | .#(+(x, y), z) |
| *#(.(x, +(_y, _z)), z) | → | *#(+(_y, _z), z) | | .#(*(2, y), .(y, z)) | → | +#(*(2, y), y) |
| +#(.(x, .(_x, _y)), z) | → | +#(.(_x, _y), z) | | +#(.(x, *(2, _x41)), _x41) | → | .#(x, .(_x41, *(min, _x41))) |
| *#(.(+(_y, _z), y), z) | → | *#(+(_y, _z), z) | | +#(.(x, *(2, .(_y, _z))), *(min, .(_y, _z))) | → | .#(x, .(_y, _z)) |
| +#(.(x, .(x, *(2, z))), z) | → | +#(.(x, *(2, z)), z) | | *#(.(x, y), z) | → | .#(*(x, z), *(y, z)) |
| .#(.(_x, *(2, __x31)), .(*(min, __x31), z)) | → | +#(.(_x, *(2, __x31)), *(min, __x31)) | | .#(.(_x, .(__x33, __x32)), .(y, z)) | → | +#(.(_x, .(__x33, __x32)), y) |
| .#(.(_x, *(2, y)), .(y, z)) | → | +#(.(_x, *(2, y)), y) | | +#(*(2, x), x) | → | .#(x, *(min, x)) |
| *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), y) | | +#(.(x, .(x, min)), min) | → | +#(.(x, min), min) |
| .#(.(_x, 2), .(2, z)) | → | +#(.(_x, 2), 2) | | *#(+(y, z), .(_x, _y)) | → | *#(.(_x, _y), z) |
| +#(3, min) | → | .#(1, .(min, 2)) | | +#(.(x, .(_x33, _x32)), _x31) | → | .#(x, .(_x33, +(_x32, _x31))) |
| *#(.(x, .(_x, _y)), z) | → | *#(.(_x, _y), z) | | *#(.(.(_x, _y), y), z) | → | *#(.(_x, _y), z) |
| +#(.(x, 3), min) | → | +#(3, min) | | .#(3, .(min, z)) | → | +#(3, min) |
| +#(.(x, 2), 2) | → | .#(x, .(1, 0)) | | +#(.(x, .(x, *(2, _x31))), *(min, _x31)) | → | +#(.(x, *(2, _x31)), *(min, _x31)) |
| .#(.(_x, 3), .(y, z)) | → | +#(.(_x, 3), y) | | +#(.(x, .(x, .(_x33, _x32))), z) | → | +#(.(x, .(_x33, _x32)), z) |
| *#(+(y, z), +(_y, _z)) | → | *#(+(_y, _z), y) | | *#(+(y, z), 3) | → | *#(3, y) |
| +#(.(x, .(x, 0)), z) | → | +#(.(x, 0), z) |
Rewrite Rules
| *(0, x) | → | 0 | | *(1, x) | → | x |
| *(2, 2) | → | .(1, 0) | | *(3, x) | → | .(x, *(min, x)) |
| *(min, min) | → | 1 | | *(2, min) | → | .(min, 2) |
| *(.(x, y), z) | → | .(*(x, z), *(y, z)) | | *(+(y, z), x) | → | +(*(x, y), *(x, z)) |
| +(0, x) | → | x | | +(x, x) | → | *(2, x) |
| +(1, 2) | → | 3 | | +(1, min) | → | 0 |
| +(2, min) | → | 1 | | +(3, x) | → | .(1, +(min, x)) |
| +(.(x, y), z) | → | .(x, +(y, z)) | | +(*(2, x), x) | → | *(3, x) |
| +(*(min, x), x) | → | 0 | | +(*(2, v), *(min, v)) | → | v |
| .(min, 3) | → | min | | .(x, min) | → | .(+(min, x), 3) |
| .(0, x) | → | x | | .(x, .(y, z)) | → | .(+(x, y), z) |
Original Signature
Termination of terms over the following signature is verified: 3, min, 2, 1, 0, *, +, .
Strategy
The right-hand side of the rule *
#(+(
y,
z), 3) → *
#(3,
y) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule *
#(+(
y,
z), 3) → *
#(3,
y) is deleted.