NO Non-Confluence Proof

Non-Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

c → h(a,h(f(f(f(f(c)))),h(a,h(b,b))))
h(h(c,f(f(a))),f(b)) → a
h(c,f(f(c))) → f(f(a))
h(f(h(c,b)),h(h(h(b,a),h(c,f(h(h(b,a),a)))),c)) → c

Proof

1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.

t0 = h(h(c,f(f(a))),f(b))
→1.1 h(h(h(a,h(f(f(f(f(c)))),h(a,h(b,b)))),f(f(a))),f(b))
= t1

t0 = h(h(c,f(f(a))),f(b))
→ε a
= t1

The two resulting terms cannot be joined for the following reason:

Tool configuration

Hakusan