NO Non-Confluence Proof

Non-Confluence Proof

by csi

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

Proof

1 Non-Joinable Fork

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

t0 = h(c,f(f(f(a))))
2.1.1.1 h(c,f(f(f(c))))
= t1

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

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

Tool configuration

csi