We consider the TRS containing the following rules:
| a1 | → | b1 | (1) |
| a1 | → | c1 | (2) |
| b1 | → | b2 | (3) |
| c1 | → | c2 | (4) |
| a2 | → | b2 | (5) |
| a2 | → | c2 | (6) |
| b2 | → | b3 | (7) |
| c2 | → | c3 | (8) |
| a3 | → | b3 | (9) |
| a3 | → | c3 | (10) |
| b3 | → | b4 | (11) |
| c3 | → | c4 | (12) |
| a4 | → | b4 | (13) |
| a4 | → | c4 | (14) |
| b4 | → | b5 | (15) |
| c4 | → | c5 | (16) |
| a5 | → | b5 | (17) |
| a5 | → | c5 | (18) |
| b5 | → | b6 | (19) |
| c5 | → | c6 | (20) |
| a6 | → | b6 | (21) |
| a6 | → | c6 | (22) |
| b6 | → | b7 | (23) |
| c6 | → | b7 | (24) |
| b7 | → | b1 | (25) |
| b7 | → | c1 | (26) |
The underlying signature is as follows:
{a1/0, b1/0, c1/0, b2/0, c2/0, a2/0, b3/0, c3/0, a3/0, b4/0, c4/0, a4/0, b5/0, c5/0, a5/0, b6/0, c6/0, a6/0, b7/0}To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| b7 | → | c1 | (26) |
| b7 | → | b1 | (25) |
| c6 | → | b7 | (24) |
| b6 | → | b7 | (23) |
| a6 | → | c6 | (22) |
| a6 | → | b6 | (21) |
| c5 | → | c6 | (20) |
| b5 | → | b6 | (19) |
| a5 | → | c5 | (18) |
| a5 | → | b5 | (17) |
| c4 | → | c5 | (16) |
| b4 | → | b5 | (15) |
| a4 | → | c4 | (14) |
| a4 | → | b4 | (13) |
| c3 | → | c4 | (12) |
| b3 | → | b4 | (11) |
| a3 | → | c3 | (10) |
| a3 | → | b3 | (9) |
| c2 | → | c3 | (8) |
| b2 | → | b3 | (7) |
| a2 | → | c2 | (6) |
| a2 | → | b2 | (5) |
| c1 | → | c2 | (4) |
| b1 | → | b2 | (3) |
| a1 | → | c1 | (2) |
| a1 | → | b1 | (1) |
| b1 | → | b7 | (27) |
| c1 | → | b7 | (28) |
| b2 | → | b7 | (29) |
| c2 | → | b7 | (30) |
| b3 | → | b7 | (31) |
| c3 | → | b7 | (32) |
| b4 | → | b7 | (33) |
| c4 | → | b7 | (34) |
| b5 | → | b7 | (35) |
| c5 | → | b7 | (36) |
All redundant rules that were added or removed can be simulated in 6 steps .