Certification Problem

Input (COPS 374)

The rewrite relation of the following conditional TRS is considered.

a → c
a → d
f(x,y) → z | c ≈ x, y ≈ z

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.
a → c
a → d
f(x,y) → y | c ≈ x

1.1 Non-Joinable Fork

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