Certification Problem
Input (COPS 681)
We consider the TRS containing the following rules:
h
(
f
(
f
(
f
(
h
(
c
,
h
(
b
,
c
))))),
h
(
f
(
f
(
b
)),
b
))
→
f
(
h
(
b
,
f
(
a
)))
(1)
f
(
c
)
→
b
(2)
The underlying signature is as follows:
{
h
/2,
f
/1,
c
/0,
b
/0,
a
/0}
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 0 step(s).