Certification Problem

Input (COPS 404)

The rewrite relation of the following conditional TRS is considered.

e(0) → true
e(s(x)) → true | o(x) ≈ true
e(s(x)) → false | e(x) ≈ true
o(0) → true
o(s(x)) → true | e(x) ≈ true
o(s(x)) → false | o(x) ≈ true

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.
e(s(0)) →* true
e(s(0)) →* false
The two resulting terms cannot be joined for the following reason: