Certification Problem

Input (COPS 323)

The rewrite relation of the following conditional TRS is considered.

f(x) → c(x,y) | g(x) ≈ y, y ≈ h(x)
a → b
g(a) → h(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(x) → c(x,g(x)) | g(x) ≈ h(x)
a → b
g(a) → h(b)

1.1 Non-Joinable Fork

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