NO Non-Confluence Proof

Non-Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Non-Joinable Fork

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

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

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

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

Tool configuration

Hakusan