Certification Problem

Input (COPS 384)

The rewrite relation of the following conditional TRS is considered.

f(x) → A | s(x) ≈ t
f(x) → B | s(x) ≈ t
s(a) → t
s(b) → t
a → c
b → c
g(x,x) → h(x,x)

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by ConCon @ CoCo 2020)

1 Non-Joinable Fork

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