We consider the TRS containing the following rules:
F(x,y) | → | c(y) | (1) |
G(x) | → | x | (2) |
f(x) | → | g(x) | (3) |
g(x) | → | c(x) | (4) |
The underlying signature is as follows:
{F/2, c/1, G/1, f/1, g/1}F | : | 2 ⨯ 3 → 0 |
c | : | 3 → 0 |
G | : | 1 → 1 |
f | : | 3 → 0 |
g | : | 3 → 0 |
F(x,y) | → | c(y) | (1) |
f(x) | → | g(x) | (3) |
g(x) | → | c(x) | (4) |
G(x) | → | x | (2) |
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
g(x) | → | c(x) | (4) |
f(x) | → | g(x) | (3) |
F(x,y) | → | c(y) | (1) |
f(x) | → | c(x) | (5) |
All redundant rules that were added or removed can be simulated in 2 steps .
Confluence is proven using the following terminating critical-pair-closing-system R:
g(x) | → | c(x) | (4) |
[g(x1)] | = | 4 · x1 + 1 |
[c(x1)] | = | 4 · x1 + 0 |
g(x) | → | c(x) | (4) |
There are no rules in the TRS. Hence, it is terminating.
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
G(x) | → | x | (2) |
All redundant rules that were added or removed can be simulated in 2 steps .
Confluence is proven using the following terminating critical-pair-closing-system R:
There are no rules.
There are no rules in the TRS. Hence, it is terminating.