Certification Problem

Input (COPS 1140)

The rewrite relation of the following conditional TRS is considered.

f(y,a) g(x,x) | h(z) ≈ x, yk(z)
k(x) h(x)
k(x) b
k(x) a
a b

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ConCon @ CoCo 2020)

1 Inlining of Conditions

Inlining of conditions results in the following transformed CTRS having the same multistep rewrite relation.
f(y,a) g(h(z),h(z)) | yk(z)
k(x) h(x)
k(x) b
k(x) a
a b

1.1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.
k(z) * b
k(z) * h(z)
The two resulting terms cannot be joined for the following reason: