We consider the TRS containing the following rules:
| c(a(x)) | → | b(c(x)) | (1) |
| c(b(x)) | → | b(b(x)) | (2) |
| c(c(x)) | → | a(c(x)) | (3) |
| a(c(x)) | → | c(b(x)) | (4) |
| b(a(x)) | → | c(b(x)) | (5) |
| b(b(x)) | → | a(c(x)) | (6) |
| c(c(x)) | → | c(b(x)) | (7) |
The underlying signature is as follows:
{c/1, a/1, b/1}To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| c(a(x)) | → | b(c(x)) | (1) |
| c(b(x)) | → | b(b(x)) | (2) |
| c(c(x)) | → | a(c(x)) | (3) |
| a(c(x)) | → | c(b(x)) | (4) |
| b(a(x)) | → | c(b(x)) | (5) |
| b(b(x)) | → | a(c(x)) | (6) |
| c(c(x)) | → | c(b(x)) | (7) |
| c(b(x)) | → | a(c(x)) | (8) |
| a(c(x)) | → | b(b(x)) | (9) |
| b(a(x)) | → | b(b(x)) | (10) |
| b(b(x)) | → | c(b(x)) | (11) |
| c(c(x)) | → | b(b(x)) | (12) |
All redundant rules that were added or removed can be simulated in 3 steps .
| t0 | = | a(c(a(f205))) |
| → | a(b(c(f205))) | |
| = | t1 |
| t0 | = | a(c(a(f205))) |
| → | b(b(a(f205))) | |
| → | b(c(b(f205))) | |
| = | t2 |
Automaton 1
final states:
{1482}
transitions:
| f205 | → | 1483 |
| b(1484) | → | 1485 |
| c(1483) | → | 1484 |
| a(1485) | → | 1482 |
Automaton 2
final states:
{1490}
transitions:
| f205 | → | 1491 |
| b(1492) | → | 1493 |
| b(1493) | → | 1490 |
| b(1491) | → | 1492 |
| b(19949) | → | 33296 |
| b(33296) | → | 1490 |
| c(33296) | → | 1490 |
| c(19949) | → | 1493 |
| c(1492) | → | 1493 |
| c(1493) | → | 1490 |
| c(1491) | → | 19949 |
| a(19949) | → | 1493 |
| a(1493) | → | 1490 |