YES
Confluence Proof
Confluence Proof
by ACP
Input
The rewrite relation of the following TRS is considered.
W
(
W
(
x
))
→
W
(
x
)
B
(
I
(
x
))
→
W
(
x
)
W
(
B
(
x
))
→
B
(
x
)
F
(
H
(
x
),
y
)
→
F
(
H
(
x
),
G
(
y
))
F
(
x
,
I
(
y
))
→
F
(
G
(
x
),
I
(
y
))
G
(
x
)
→
x
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