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 2023)
1 Development Closed
Confluence is proven since the TRS is development closed. The joins can be performed using 1 development step(s).