NO Non-Confluence Proof

Non-Confluence Proof

by csi

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

csi