YES
Confluence Proof
Confluence Proof
by ACP
Input
The rewrite relation of the following TRS is considered.
Ap
(
Ap
(
Ap
(
S
,
x
),
y
),
z
)
→
Ap
(
Ap
(
x
,
z
),
Ap
(
y
,
z
))
Ap
(
Ap
(
K
,
x
),
y
)
→
x
Ap
(
I
,
x
)
→
x
Proof
1 Development Closed
Confluence is proven since the TRS is development closed.
Tool configuration
ACP
version: 0.72