We consider the TRS containing the following rules:
| s(p(x)) | → | x | (1) |
| p(s(x)) | → | x | (2) |
| +(x,0) | → | x | (3) |
| +(x,s(y)) | → | s(+(x,y)) | (4) |
| +(x,p(y)) | → | p(+(x,y)) | (5) |
| +(0,y) | → | y | (6) |
| +(p(x),y) | → | p(+(x,y)) | (7) |
| +(s(x),y) | → | s(+(x,y)) | (8) |
The underlying signature is as follows:
{s/1, p/1, +/2, 0/0}To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| +(s(x),y) | → | s(+(x,y)) | (8) |
| +(p(x),y) | → | p(+(x,y)) | (7) |
| +(0,y) | → | y | (6) |
| +(x,p(y)) | → | p(+(x,y)) | (5) |
| +(x,s(y)) | → | s(+(x,y)) | (4) |
| +(x,0) | → | x | (3) |
| p(s(x)) | → | x | (2) |
| s(p(x)) | → | x | (1) |
All redundant rules that were added or removed can be simulated in 2 steps .
Confluence is proven using the following terminating critical-pair-closing-system R:
| +(x,p(y)) | → | p(+(x,y)) | (5) |
| s(p(x)) | → | x | (1) |
| +(s(x),y) | → | s(+(x,y)) | (8) |
| p(s(x)) | → | x | (2) |
| +(x,s(y)) | → | s(+(x,y)) | (4) |
| +(x,0) | → | x | (3) |
| +(p(x),y) | → | p(+(x,y)) | (7) |
| +(0,y) | → | y | (6) |
| [+(x1, x2)] | = | 5 · x1 + 2 · x2 + 4 |
| [0] | = | 0 |
| [s(x1)] | = | 1 · x1 + 5 |
| [p(x1)] | = | 1 · x1 + 2 |
| +(x,p(y)) | → | p(+(x,y)) | (5) |
| s(p(x)) | → | x | (1) |
| +(s(x),y) | → | s(+(x,y)) | (8) |
| p(s(x)) | → | x | (2) |
| +(x,s(y)) | → | s(+(x,y)) | (4) |
| +(x,0) | → | x | (3) |
| +(p(x),y) | → | p(+(x,y)) | (7) |
| +(0,y) | → | y | (6) |
There are no rules in the TRS. Hence, it is terminating.