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