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