We consider the TRS containing the following rules:
| f(x,x) | → | a | (1) |
| c | → | h(c,g(c)) | (2) |
| h(x,g(x)) | → | f(x,h(x,g(c))) | (3) |
The underlying signature is as follows:
{f/2, a/0, c/0, h/2, g/1}To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| f(x,x) | → | a | (1) |
| c | → | h(c,g(c)) | (2) |
| h(x,g(x)) | → | f(x,h(x,g(c))) | (3) |
| c | → | f(c,h(c,g(c))) | (4) |
| f(f(x,x),a) | → | a | (5) |
| f(a,f(x,x)) | → | a | (6) |
| f(c,h(c,g(c))) | → | a | (7) |
| f(h(c,g(c)),c) | → | a | (8) |
All redundant rules that were added or removed can be simulated in 3 steps .
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| f(x,x) | → | a | (1) |
| c | → | h(c,g(c)) | (2) |
| h(x,g(x)) | → | f(x,h(x,g(c))) | (3) |
| c | → | f(c,h(c,g(c))) | (4) |
| f(f(x,x),a) | → | a | (5) |
| f(a,f(x,x)) | → | a | (6) |
| f(c,h(c,g(c))) | → | a | (7) |
| f(h(c,g(c)),c) | → | a | (8) |
| h(c,g(c)) | → | a | (9) |
| c | → | a | (10) |
| f(c,c) | → | a | (11) |
All redundant rules that were added or removed can be simulated in 3 steps .
| t0 | = | h(c,g(c)) |
| → | h(a,g(c)) | |
| = | t1 |
| t0 | = | h(c,g(c)) |
| → | a | |
| = | t1 |
Automaton 1
final states:
{624}
transitions:
| g(624) | → | 17 |
| g(623) | → | 17 |
| g(16) | → | 17 |
| h(624,17) | → | 16 |
| h(623,17) | → | 624 |
| h(16,17) | → | 16 |
| a | → | 623 |
| f(16,624) | → | 16 |
| f(623,624) | → | 624 |
| f(16,623) | → | 16 |
| f(623,16) | → | 16 |
| f(624,624) | → | 16 |
| f(624,16) | → | 16 |
| f(623,623) | → | 16 |
| f(623,15) | → | 624 |
| f(624,623) | → | 16 |
| f(16,16) | → | 16 |
| c | → | 16 |
| 16 | » | 624 |
| 16 | » | 623 |
| 16 | » | 16 |
| 17 | » | 17 |
| 15 | » | 624 |
| 15 | » | 15 |
| 624 | » | 624 |
| 623 | » | 623 |
Automaton 2
final states:
{4}
transitions:
| a | → | 4 |
| 4 | » | 4 |