Certification Problem
Input (COPS 50)
We consider the TRS containing the following rules:
|
F(G(x,A,B)) |
→ |
x |
(1) |
|
G(F(H(C,D)),x,y) |
→ |
H(K1(x),K2(y)) |
(2) |
|
K1(A) |
→ |
C |
(3) |
|
K2(B) |
→ |
D |
(4) |
The underlying signature is as follows:
{F/1, G/3, A/0, B/0, H/2, C/0, D/0, K1/1, K2/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by ACP @ CoCo 2023)
1 Development Closed
Confluence is proven since the TRS is development closed.
The joins can be performed using
1 development
step(s).