The rewrite relation of the following TRS is considered.
| *(x,1) | → | x | (1) |
| *(1,y) | → | y | (2) |
| *(i(x),x) | → | 1 | (3) |
| *(x,i(x)) | → | 1 | (4) |
| *(x,*(y,z)) | → | *(*(x,y),z) | (5) |
| i(1) | → | 1 | (6) |
| *(*(x,y),i(y)) | → | x | (7) |
| *(*(x,i(y)),y) | → | x | (8) |
| i(i(x)) | → | x | (9) |
| i(*(x,y)) | → | *(i(y),i(x)) | (10) |
| k(x,1) | → | 1 | (11) |
| k(x,x) | → | 1 | (12) |
| *(k(x,y),k(y,x)) | → | 1 | (13) |
| *(*(i(x),k(y,z)),x) | → | k(*(*(i(x),y),x),*(*(i(x),z),x)) | (14) |
| k(*(x,i(y)),*(y,i(x))) | → | 1 | (15) |
| prec(*) | = | 1 | stat(*) | = | lex | |
| prec(1) | = | 0 | stat(1) | = | lex | |
| prec(i) | = | 2 | stat(i) | = | lex | |
| prec(k) | = | 0 | stat(k) | = | lex |
| π(*) | = | [2,1] |
| π(1) | = | [] |
| π(i) | = | [1] |
| π(k) | = | [1,2] |
| *(x,1) | → | x | (1) |
| *(1,y) | → | y | (2) |
| *(i(x),x) | → | 1 | (3) |
| *(x,i(x)) | → | 1 | (4) |
| *(x,*(y,z)) | → | *(*(x,y),z) | (5) |
| i(1) | → | 1 | (6) |
| *(*(x,y),i(y)) | → | x | (7) |
| *(*(x,i(y)),y) | → | x | (8) |
| i(i(x)) | → | x | (9) |
| i(*(x,y)) | → | *(i(y),i(x)) | (10) |
| k(x,1) | → | 1 | (11) |
| k(x,x) | → | 1 | (12) |
| *(k(x,y),k(y,x)) | → | 1 | (13) |
| *(*(i(x),k(y,z)),x) | → | k(*(*(i(x),y),x),*(*(i(x),z),x)) | (14) |
| k(*(x,i(y)),*(y,i(x))) | → | 1 | (15) |
There are no rules in the TRS. Hence, it is terminating.