by Hakusan
The rewrite relation of the following TRS is considered.
| inv(0) | → | 0 |
| inv(s(x)) | → | p(inv(x)) |
| inv(p(x)) | → | s(inv(x)) |
| minus(x,0) | → | x |
| minus(x,p(y)) | → | s(minus(x,y)) |
| minus(x,s(y)) | → | p(minus(x,y)) |
| minus(0,x) | → | inv(x) |
| minus(s(x),s(y)) | → | minus(x,y) |
| minus(p(x),p(y)) | → | minus(x,y) |
| inv(x) | → | minus(0,x) |
| s(p(x)) | → | x |
| p(s(x)) | → | x |
| t0 | = | minus(p(x1),p(y2)) |
| →ε | minus(x1,y2) | |
| = | t1 |
| t0 | = | minus(p(x1),p(y2)) |
| →ε | s(minus(p(x1),y2)) | |
| = | t1 |
Hakusan