YES
Confluence Proof
Confluence Proof
by ACP
Input
The rewrite relation of the following TRS is considered.
a
→
c
b
→
c
f
(
a
,
b
)
→
d
f
(
x
,
c
)
→
f
(
c
,
c
)
f
(
c
,
x
)
→
f
(
c
,
c
)
d
→
f
(
a
,
c
)
d
→
f
(
c
,
b
)
Proof
1 Strongly closed
Confluence is proven since the TRS is strongly closed. The joins can be performed within 3 step(s).
Tool configuration
ACP
version: 0.72