NO Non-Confluence Proof

Non-Confluence Proof

by ACP

Input

The rewrite relation of the following TRS is considered.

g(x) h(k(x))
g(x) x
h(k(x)) f(x)
f(x) x
k(c) c
f(c) g(c)

Proof

1 Non-Joinable Fork

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

t0 = g(c)
ε h(k(c))
1 h(c)
= t2

t0 = g(c)
ε c
= t1

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

Tool configuration

ACP