Certification Problem

Input (COPS 353)

The rewrite relation of the following conditional TRS is considered.

ssp'(xs,0) → nil
ssp'(cons(y',ws),v) → cons(y',ys') | sub(v,y') ≈ w, ssp'(ws,w) ≈ ys'
ssp'(cons(x',xs'),v) → cons(y',ys') | get(xs') ≈ tp2(y',zs), sub(v,y') ≈ w, ssp'(cons(x',zs),w) ≈ ys'
sub(z,0) → z
sub(s(v),s(w)) → z | sub(v,w) ≈ z
get(cons(y,ys)) → tp2(y,ys)
get(cons(x',xs')) → tp2(y,cons(x',zs)) | get(xs') ≈ tp2(y,zs)

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

1.1 Non-Joinable Fork

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