We consider the TRS containing the following rules:
| if(true,x,y) | → | x | (1) |
| if(false,x,y) | → | y | (2) |
| -(s(x),s(y)) | → | -(x,y) | (3) |
| -(x,0) | → | x | (4) |
| -(0,x) | → | 0 | (5) |
| <(s(x),s(y)) | → | <(x,y) | (6) |
| <(0,s(x)) | → | true | (7) |
| <(x,0) | → | false | (8) |
| mod(0,y) | → | 0 | (9) |
| mod(x,s(y)) | → | if(<(x,s(y)),x,mod(-(x,s(y)),s(y))) | (10) |
| mod(x,0) | → | x | (11) |
| gcd(x,y) | → | gcd(y,mod(x,y)) | (12) |
| gcd(x,0) | → | x | (13) |
| gcd(0,x) | → | x | (14) |
The underlying signature is as follows:
{if/3, true/0, false/0, -/2, s/1, 0/0, </2, mod/2, gcd/2}Confluence is proven using the following terminating critical-pair-closing-system R:
| <(0,s(x)) | → | true | (7) |
| if(true,x,y) | → | x | (1) |
| gcd(0,x) | → | x | (14) |
| mod(x,0) | → | x | (11) |
| mod(0,y) | → | 0 | (9) |
| gcd(x,0) | → | x | (13) |
| [gcd(x1, x2)] | = | 1 · x1 + 5 · x2 + 0 |
| [mod(x1, x2)] | = | 4 · x1 + 2 · x2 + 4 |
| [<(x1, x2)] | = | 1 · x1 + 4 · x2 + 0 |
| [0] | = | 1 |
| [s(x1)] | = | 4 · x1 + 4 |
| [if(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 + 2 |
| [true] | = | 6 |
| <(0,s(x)) | → | true | (7) |
| if(true,x,y) | → | x | (1) |
| gcd(0,x) | → | x | (14) |
| mod(x,0) | → | x | (11) |
| mod(0,y) | → | 0 | (9) |
| gcd(x,0) | → | x | (13) |
There are no rules in the TRS. Hence, it is terminating.