Certification Problem

Input (COPS 606)

We consider the TRS containing the following rules:

not(true) false (1)
not(false) true (2)
or(true,y) true (3)
or(x,true) true (4)
or(false,false) false (5)
implies(true,y) y (6)
implies(false,y) true (7)
implies(x,y) or(not(x),y) (8)

The underlying signature is as follows:

{not/1, true/0, false/0, or/2, implies/2}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2020)

1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.

t0 = implies(true,y)
y
= t1

t0 = implies(true,y)
or(not(true),y)
or(false,y)
= t2

The two resulting terms cannot be joined for the following reason: