Certification Problem

Input (COPS 391)

The rewrite relation of the following conditional TRS is considered.

pin(a) → pout(b)
pin(b) → pout(c)
tc(x) → x
tc(x) → y | pin(x) ≈ pout(z), tc(z) ≈ y

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.
pin(a) → pout(b)
pin(b) → pout(c)
tc(x) → x
tc(x) → tc(z) | pin(x) ≈ pout(z)

1.1 Non-Joinable Fork

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