Certification Problem
Input (COPS 93)
We consider the TRS containing the following rules:
|
F(H(x),y) |
→ |
G(H(x)) |
(1) |
|
H(I(x)) |
→ |
I(x) |
(2) |
|
F(I(x),y) |
→ |
G(I(x)) |
(3) |
The underlying signature is as follows:
{F/2, H/1, G/1, I/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by ACP @ CoCo 2020)
1 Strongly closed
Confluence is proven since the TRS is strongly closed.
The joins can be performed using
2
step(s).