Certification Problem

Input (COPS 379)

The rewrite relation of the following conditional TRS is considered.

up(x) → x
down(x) → x
up(x) → up(s(x))
down(s(x)) → down(x)
between(x,y,z) → true | up(x) ≈ y, down(z) ≈ y

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