Certification Problem

Input (COPS 352)

The rewrite relation of the following conditional TRS is considered.

ssp'(xs,v) → ys | subseteq_m(ys,xs) ≈ tt, sum(ys) ≈ v
subseteq_m(nil,ys) → tt
subseteq_m(cons(x,xs),ys) → z | del(x,ys) ≈ some(ws), subseteq_m(xs,ws) ≈ z
del(x,nil) → none
del(x,cons(x,ys)) → some(ys)
del(x,cons(y,ys)) → some(cons(y,zs)) | del(x,ys) ≈ some(zs)
sum(nil) → 0
add(x,0) → x
add(x,s(y)) → s(z) | add(x,y) ≈ z

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.
ssp'(xs,v) → ys | subseteq_m(ys,xs) ≈ tt, sum(ys) ≈ v
subseteq_m(nil,ys) → tt
subseteq_m(cons(x,xs),ys) → subseteq_m(xs,ws) | del(x,ys) ≈ some(ws)
del(x,nil) → none
del(x,cons(x,ys)) → some(ys)
del(x,cons(y,ys)) → some(cons(y,zs)) | del(x,ys) ≈ some(zs)
sum(nil) → 0
add(x,0) → x
add(x,s(y)) → s(add(x,y))

1.1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.
del(__NN147,cons(__NN147,cons(__NN143,cons(__NN147,__NN148)))) →* some(cons(__NN143,cons(__NN147,__NN148)))
del(__NN147,cons(__NN147,cons(__NN143,cons(__NN147,__NN148)))) →* some(cons(__NN147,cons(__NN143,__NN148)))
The two resulting terms cannot be joined for the following reason: