NO Non-Confluence Proof

Non-Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Non-Joinable Fork

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

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

→_{1.1.1.1.1.1.2.2.2} h(h(h(h(h(h(h(a,h(c,h(f(c),f(b)))),h(b,h(b,h(f(f(h(c,b))),a)))),h(a,a)),b),f(h(h(f(a),a),c))),a),h(c,a))

= t₁

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

→_ε f(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.

Tool configuration

Hakusan

version: 0.10

t₀	=	h(h(h(h(h(h(h(a,h(c,h(f(c),b))),h(b,h(b,h(f(f(h(c,b))),a)))),h(a,a)),b),f(h(h(f(a),a),c))),a),h(c,a))
	→_{1.1.1.1.1.1.2.2.2}	h(h(h(h(h(h(h(a,h(c,h(f(c),f(b)))),h(b,h(b,h(f(f(h(c,b))),a)))),h(a,a)),b),f(h(h(f(a),a),c))),a),h(c,a))
	=	t₁

t₀	=	h(h(h(h(h(h(h(a,h(c,h(f(c),b))),h(b,h(b,h(f(f(h(c,b))),a)))),h(a,a)),b),f(h(h(f(a),a),c))),a),h(c,a))
	→_ε	f(a)
	=	t₁