The rewrite relation of the following TRS is considered.
| le(0,y) | → | true | (1) |
| le(s(x),0) | → | false | (2) |
| le(s(x),s(y)) | → | le(x,y) | (3) |
| minus(x,0) | → | x | (4) |
| minus(s(x),s(y)) | → | minus(x,y) | (5) |
| gcd(0,y) | → | y | (6) |
| gcd(s(x),0) | → | s(x) | (7) |
| gcd(s(x),s(y)) | → | if_gcd(le(y,x),s(x),s(y)) | (8) |
| if_gcd(true,s(x),s(y)) | → | gcd(minus(x,y),s(y)) | (9) |
| if_gcd(false,s(x),s(y)) | → | gcd(minus(y,x),s(x)) | (10) |
| le#(s(x),s(y)) | → | le#(x,y) | (11) |
| minus#(s(x),s(y)) | → | minus#(x,y) | (12) |
| gcd#(s(x),s(y)) | → | le#(y,x) | (13) |
| gcd#(s(x),s(y)) | → | if_gcd#(le(y,x),s(x),s(y)) | (14) |
| if_gcd#(true,s(x),s(y)) | → | minus#(x,y) | (15) |
| if_gcd#(true,s(x),s(y)) | → | gcd#(minus(x,y),s(y)) | (16) |
| if_gcd#(false,s(x),s(y)) | → | minus#(y,x) | (17) |
| if_gcd#(false,s(x),s(y)) | → | gcd#(minus(y,x),s(x)) | (18) |
The dependency pairs are split into 3 components.
| if_gcd#(false,s(x),s(y)) | → | gcd#(minus(y,x),s(x)) | (18) |
| gcd#(s(x),s(y)) | → | if_gcd#(le(y,x),s(x),s(y)) | (14) |
| if_gcd#(true,s(x),s(y)) | → | gcd#(minus(x,y),s(y)) | (16) |
| π(if_gcd#) | = | { 2, 2, 3 } |
| π(gcd#) | = | { 1, 1, 1, 2 } |
| π(if_gcd) | = | { 2, 2, 2, 3, 3 } |
| π(gcd) | = | { 1, 1, 1, 2, 2 } |
| π(minus) | = | { 1, 1 } |
| if_gcd#(false,s(x),s(y)) | → | gcd#(minus(y,x),s(x)) | (18) |
| gcd#(s(x),s(y)) | → | if_gcd#(le(y,x),s(x),s(y)) | (14) |
| if_gcd#(true,s(x),s(y)) | → | gcd#(minus(x,y),s(y)) | (16) |
There are no pairs anymore.
| minus#(s(x),s(y)) | → | minus#(x,y) | (12) |
| π(minus#) | = | 1 |
| minus#(s(x),s(y)) | → | minus#(x,y) | (12) |
There are no pairs anymore.
| le#(s(x),s(y)) | → | le#(x,y) | (11) |
| π(le#) | = | 1 |
| le#(s(x),s(y)) | → | le#(x,y) | (11) |
There are no pairs anymore.