Certification Problem

Input (COPS 351)

The rewrite relation of the following conditional TRS is considered.

ssp(nil,0) → nil
ssp(cons(y,ys'),v) → xs | ssp(ys',v) ≈ xs
ssp(cons(y,ys'),v) → cons(y,xs') | sub(v,y) ≈ w, ssp(ys',w) ≈ xs'
sub(z,0) → z
sub(s(v),s(w)) → z | sub(v,w) ≈ 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(nil,0) → nil
ssp(cons(y,ys'),v) → ssp(ys',v)
ssp(cons(y,ys'),v) → cons(y,ssp(ys',sub(v,y)))
sub(z,0) → z
sub(s(v),s(w)) → sub(v,w)

1.1 Non-Joinable Fork

The system is not confluent due to the following forking derivations.
ssp(cons(z',$1),y') →* ssp($1,y')
ssp(cons(z',$1),y') →* cons(z',ssp($1,sub(y',z')))
The two resulting terms cannot be joined for the following reason: