We consider the TRS containing the following rules:
| f(u(O),u(y)) | → | A | (1) |
| f(v(x),v(O)) | → | B | (2) |
| O | → | u(O) | (3) |
| O | → | v(O) | (4) |
| u(x) | → | x | (5) |
| v(x) | → | x | (6) |
| f(x,y) | → | f(x,u(y)) | (7) |
| f(x,y) | → | f(v(x),y) | (8) |
The underlying signature is as follows:
{f/2, u/1, O/0, A/0, v/1, B/0}To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| f(u(O),u(y)) | → | A | (1) |
| f(v(x),v(O)) | → | B | (2) |
| O | → | u(O) | (3) |
| O | → | v(O) | (4) |
| u(x) | → | x | (5) |
| v(x) | → | x | (6) |
| f(x,y) | → | f(x,u(y)) | (7) |
| f(x,y) | → | f(v(x),y) | (8) |
| O | → | u(u(O)) | (9) |
| O | → | u(v(O)) | (10) |
| O | → | O | (11) |
| O | → | v(u(O)) | (12) |
| O | → | v(v(O)) | (13) |
| u(f(u(O),u(y))) | → | A | (14) |
| u(f(v(x),v(O))) | → | B | (15) |
| u(O) | → | u(O) | (16) |
| u(O) | → | v(O) | (17) |
| u(u(x)) | → | x | (18) |
| u(v(x)) | → | x | (19) |
| v(f(u(O),u(y))) | → | A | (20) |
| v(f(v(x),v(O))) | → | B | (21) |
| v(O) | → | u(O) | (22) |
| v(O) | → | v(O) | (23) |
| v(u(x)) | → | x | (24) |
| v(v(x)) | → | x | (25) |
| f(u(O),y) | → | A | (26) |
| f(x146,x) | → | f(x146,x) | (27) |
| f(x,v(O)) | → | B | (28) |
| f(x,x149) | → | f(x,x149) | (29) |
| f(O,u(x134)) | → | A | (30) |
| f(u(O),O) | → | A | (31) |
| f(u(O),u(O)) | → | A | (32) |
| u(f(u(O),u(x134))) | → | A | (33) |
| f(u(u(O)),u(x134)) | → | A | (34) |
| f(u(O),u(u(x134))) | → | A | (35) |
| f(u(O),u(u(x))) | → | A | (36) |
| v(f(u(O),u(x134))) | → | A | (37) |
| f(v(u(O)),u(x134)) | → | A | (38) |
| f(u(v(O)),u(x134)) | → | A | (39) |
| f(u(O),v(u(x134))) | → | A | (40) |
| f(u(O),u(v(x))) | → | A | (41) |
| f(v(O),v(O)) | → | B | (42) |
| f(O,v(O)) | → | B | (43) |
| f(v(x135),O) | → | B | (44) |
| u(f(v(x135),v(O))) | → | B | (45) |
| f(u(v(x135)),v(O)) | → | B | (46) |
| f(v(u(x)),v(O)) | → | B | (47) |
| f(v(x135),u(v(O))) | → | B | (48) |
| f(v(x135),v(u(O))) | → | B | (49) |
| v(f(v(x135),v(O))) | → | B | (50) |
| f(v(v(x135)),v(O)) | → | B | (51) |
| f(v(v(x)),v(O)) | → | B | (52) |
| f(v(x135),v(v(O))) | → | B | (53) |
| u(u(x136)) | → | x136 | (54) |
| v(u(x136)) | → | x136 | (55) |
| u(v(x137)) | → | x137 | (56) |
| v(v(x137)) | → | x137 | (57) |
All redundant rules that were added or removed can be simulated in 3 steps .
| t0 | = | f(u(O),v(O)) |
| → | A | |
| = | t1 |
| t0 | = | f(u(O),v(O)) |
| → | B | |
| = | t1 |