Certification Problem

Input (COPS 680)

We consider the TRS containing the following rules:

b	→	f(a)	(1)
a	→	c	(2)
a	→	a	(3)
h(c,f(f(f(a))))	→	h(f(f(c)),h(b,a))	(4)
f(f(f(f(h(h(c,h(f(c),f(f(h(h(h(h(f(a),a),c),a),h(h(h(b,a),f(h(f(h(f(b),f(f(b)))),a))),h(c,f(h(b,f(f(h(h(c,f(a)),a)))))))))))),f(f(b)))))))	→	c	(5)

The underlying signature is as follows:

{b/0, f/1, a/0, c/0, h/2}

Prove or disprove confluence.

No.

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

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

When applying the cap-function on both terms (where variables may be treated like constants) then the resulting terms do not unify.