NO Non-Confluence Proof

Non-Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

b	→	f(a)
a	→	c
a	→	a
h(c,f(f(f(a))))	→	h(f(f(c)),h(b,a))
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

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

t₀ = h(c,f(f(f(a))))

→_2.1.1.1 h(c,f(f(f(c))))

= t₁

t₀ = h(c,f(f(f(a))))

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

= t₁

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.

Hakusan