YES Confluence Proof

Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

H(F(x,y)) → F(H(R(x)),y)
F(x,K(y,z)) → G(P(y),Q(z,x))
H(Q(x,y)) → Q(x,H(R(y)))
Q(x,H(R(y))) → H(Q(x,y))
H(G(x,y)) → G(x,H(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