The rewrite relation of the following TRS is considered.
| min(x,0) | → | 0 | (1) |
| min(0,y) | → | 0 | (2) |
| min(s(x),s(y)) | → | s(min(x,y)) | (3) |
| max(x,0) | → | x | (4) |
| max(0,y) | → | y | (5) |
| max(s(x),s(y)) | → | s(max(x,y)) | (6) |
| -(x,0) | → | x | (7) |
| -(s(x),s(y)) | → | -(x,y) | (8) |
| gcd(s(x),s(y),z) | → | gcd(-(max(x,y),min(x,y)),s(min(x,y)),z) | (9) |
| gcd(x,s(y),s(z)) | → | gcd(x,-(max(y,z),min(y,z)),s(min(y,z))) | (10) |
| gcd(s(x),y,s(z)) | → | gcd(-(max(x,z),min(x,z)),y,s(min(x,z))) | (11) |
| gcd(x,0,0) | → | x | (12) |
| gcd(0,y,0) | → | y | (13) |
| gcd(0,0,z) | → | z | (14) |
| min#(s(x),s(y)) | → | min#(x,y) | (15) |
| max#(s(x),s(y)) | → | max#(x,y) | (16) |
| -#(s(x),s(y)) | → | -#(x,y) | (17) |
| gcd#(s(x),s(y),z) | → | gcd#(-(max(x,y),min(x,y)),s(min(x,y)),z) | (18) |
| gcd#(s(x),s(y),z) | → | -#(max(x,y),min(x,y)) | (19) |
| gcd#(s(x),s(y),z) | → | max#(x,y) | (20) |
| gcd#(s(x),s(y),z) | → | min#(x,y) | (21) |
| gcd#(x,s(y),s(z)) | → | gcd#(x,-(max(y,z),min(y,z)),s(min(y,z))) | (22) |
| gcd#(x,s(y),s(z)) | → | -#(max(y,z),min(y,z)) | (23) |
| gcd#(x,s(y),s(z)) | → | max#(y,z) | (24) |
| gcd#(x,s(y),s(z)) | → | min#(y,z) | (25) |
| gcd#(s(x),y,s(z)) | → | gcd#(-(max(x,z),min(x,z)),y,s(min(x,z))) | (26) |
| gcd#(s(x),y,s(z)) | → | -#(max(x,z),min(x,z)) | (27) |
| gcd#(s(x),y,s(z)) | → | max#(x,z) | (28) |
| gcd#(s(x),y,s(z)) | → | min#(x,z) | (29) |
The dependency pairs are split into 4 components.
| gcd#(x,s(y),s(z)) | → | gcd#(x,-(max(y,z),min(y,z)),s(min(y,z))) | (22) |
| gcd#(s(x),s(y),z) | → | gcd#(-(max(x,y),min(x,y)),s(min(x,y)),z) | (18) |
| gcd#(s(x),y,s(z)) | → | gcd#(-(max(x,z),min(x,z)),y,s(min(x,z))) | (26) |
| [gcd#(x1, x2, x3)] | = | 0 + 1 · x1 + 1 · x2 + 1/2 · x3 |
| [s(x1)] | = | 4 + 4 · x1 |
| [-(x1, x2)] | = | 0 + 1 · x1 + 0 · x2 |
| [max(x1, x2)] | = | 0 + 1 · x1 + 1 · x2 |
| [min(x1, x2)] | = | 0 + 1/2 · x1 + 1/2 · x2 |
| [0] | = | 0 |
| max(x,0) | → | x | (4) |
| max(0,y) | → | y | (5) |
| max(s(x),s(y)) | → | s(max(x,y)) | (6) |
| min(x,0) | → | 0 | (1) |
| min(0,y) | → | 0 | (2) |
| min(s(x),s(y)) | → | s(min(x,y)) | (3) |
| -(x,0) | → | x | (7) |
| -(s(x),s(y)) | → | -(x,y) | (8) |
| gcd#(x,s(y),s(z)) | → | gcd#(x,-(max(y,z),min(y,z)),s(min(y,z))) | (22) |
| gcd#(s(x),s(y),z) | → | gcd#(-(max(x,y),min(x,y)),s(min(x,y)),z) | (18) |
| gcd#(s(x),y,s(z)) | → | gcd#(-(max(x,z),min(x,z)),y,s(min(x,z))) | (26) |
There are no pairs anymore.
| min#(s(x),s(y)) | → | min#(x,y) | (15) |
| [s(x1)] | = | 1 · x1 |
| [min#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| min#(s(x),s(y)) | → | min#(x,y) | (15) |
| 1 | > | 1 | |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| max#(s(x),s(y)) | → | max#(x,y) | (16) |
| [s(x1)] | = | 1 · x1 |
| [max#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| max#(s(x),s(y)) | → | max#(x,y) | (16) |
| 1 | > | 1 | |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| -#(s(x),s(y)) | → | -#(x,y) | (17) |
| [s(x1)] | = | 1 · x1 |
| [-#(x1, x2)] | = | 1 · x1 + 1 · x2 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| -#(s(x),s(y)) | → | -#(x,y) | (17) |
| 1 | > | 1 | |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.