Certification Problem

Input (COPS 328)

The rewrite relation of the following conditional TRS is considered.

eq(0,0) → true
eq(s(x),0) → false
eq(0,s(y)) → false
eq(s(x),s(y)) → eq(x,y)
lte(0,y) → true
lte(s(x),0) → false
lte(s(x),s(y)) → lte(x,y)
m(0,s(y)) → 0
m(x,0) → x
m(s(x),s(y)) → m(x,y)
mod(0,y) → 0
mod(s(x),0) → 0
mod(s(x),s(y)) → mod(m(x,y),s(y)) | lte(y,x) ≈ true
mod(s(x),s(y)) → s(x) | lte(y,x) ≈ false
filter(n,r,nil) → nil
filter(n,r,cons(x,xs)) → cons(x,filter(n,r,xs)) | mod(x,n) ≈ r', eq(r,r') ≈ true
filter(n,r,cons(x,xs)) → filter(n,r,xs) | mod(x,n) ≈ n', eq(r,r') ≈ false

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.
eq(0,0) → true
eq(s(x),0) → false
eq(0,s(y)) → false
eq(s(x),s(y)) → eq(x,y)
lte(0,y) → true
lte(s(x),0) → false
lte(s(x),s(y)) → lte(x,y)
m(0,s(y)) → 0
m(x,0) → x
m(s(x),s(y)) → m(x,y)
mod(0,y) → 0
mod(s(x),0) → 0
mod(s(x),s(y)) → mod(m(x,y),s(y)) | lte(y,x) ≈ true
mod(s(x),s(y)) → s(x) | lte(y,x) ≈ false
filter(n,r,nil) → nil
filter(n,r,cons(x,xs)) → cons(x,filter(n,r,xs)) | eq(r,mod(x,n)) ≈ true
filter(n,r,cons(x,xs)) → filter(n,r,xs) | eq(r,r') ≈ false

1.1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.
filter(__NN142,0,cons(0,__NN146)) →* cons(0,filter(__NN142,0,__NN146))
filter(__NN142,0,cons(0,__NN146)) →* filter(__NN142,0,__NN146)
The two resulting terms cannot be joined for the following reason: