YES
Confluence Proof
Confluence Proof
by ACP
Input
The rewrite relation of the following TRS is considered.
-
(
0
,
0
)
→
0
-
(
s
(
x
),
0
)
→
s
(
x
)
-
(
x
,
s
(
y
))
→
-
(
d
(
x
),
y
)
d
(
s
(
x
))
→
x
-
(
s
(
x
),
s
(
y
))
→
-
(
x
,
y
)
-
(
d
(
x
),
y
)
→
-
(
x
,
s
(
y
))
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