Certification Problem

Input (COPS 632)

We consider the TRS containing the following rules:

inv(0) 0 (1)
inv(s(x)) p(inv(x)) (2)
inv(p(x)) s(inv(x)) (3)
minus(x,0) x (4)
minus(x,p(y)) s(minus(x,y)) (5)
minus(x,s(y)) p(minus(x,y)) (6)
minus(0,x) inv(x) (7)
inv(x) minus(0,x) (8)
inv(minus(x,y)) minus(y,x) (9)
s(p(x)) x (10)
p(s(x)) x (11)

The underlying signature is as follows:

{inv/1, 0/0, s/1, p/1, minus/2}

Property / Task

Prove or disprove confluence.

Answer / Result

No.

Proof (by csi @ CoCo 2022)

1 Non-Joinable Fork

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

t0 = inv(minus(x,p(x630)))
inv(s(minus(x,x630)))
p(inv(minus(x,x630)))
p(minus(x630,x))
= t3

t0 = inv(minus(x,p(x630)))
minus(p(x630),x)
= t1

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