Certification Problem

Input (COPS 410)

The rewrite relation of the following conditional TRS is considered.

f(x,y) → g(x) | a ≈ d
f(x,y) → h(x) | b ≈ d
g(s(x)) → x
h(s(x)) → x
a → d
b → d

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.
f(__N3,__N4) →* g(__N3)
f(__N3,__N4) →* h(__N3)
The two resulting terms cannot be joined for the following reason: