Certification Problem
Input (COPS 92)
We consider the TRS containing the following rules:
|
W(B(x)) |
→ |
W(x) |
(1) |
|
B(I(x)) |
→ |
J(x) |
(2) |
|
W(I(x)) |
→ |
W(J(x)) |
(3) |
The underlying signature is as follows:
{W/1, B/1, I/1, J/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).