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