YES Confluence Proof

Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

f(g(x,a,b)) → x
g(f(h(c,d)),x,y) → h(k1(x),k2(y))
k1(a) → c
k2(b) → d
f(h(k1(a),k2(b))) → f(h(c,d))
f(h(c,k2(b))) → f(h(c,d))
f(h(k1(a),d)) → f(h(c,d))

Proof

1 Development Closed

Confluence is proven since the TRS is development closed.

Tool configuration

ACP