Certification Problem

Input (COPS 322)

The rewrite relation of the following conditional TRS is considered.

split(x,nil)	→	tp2(nil,nil)
split(x,cons(y,ys))	→	tp2(zs1,cons(y,zs2))	\| split(x,ys) ≈ tp2(zs1,zs2), le(x,y) ≈ true
split(x,cons(y,ys))	→	tp2(cons(y,zs1),zs2)	\| split(x,ys) ≈ tp2(zs1,zs2), le(x,y) ≈ false
le(0,y)	→	true
le(s(x),0)	→	false
le(s(x),s(y))	→	le(x,y)

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

1 Almost-orthogonal modulo infeasibility

The given (extended) properly oriented, right-stable, oriented 3-CTRS is almost-orthogonal modulo infeasibility, since all its conditional critical pairs are infeasible.

The 1^st CCP contains the conditions split($3,$5) ≈ tp2(y',z), le($3,$6) ≈ false from the first rule and the conditions split($3,$5) ≈ tp2($4,$2), le($3,$6) ≈ true from the second rule.
1.1 Equal Left-Hand Sides
There are two conditions with left-hand side le($3,$6) and respective right-hand sides false and true.
1.1.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The 2^nd CCP contains the conditions split($3,$5) ≈ tp2(y',z), le($3,$6) ≈ true from the first rule and the conditions split($3,$5) ≈ tp2($4,$2), le($3,$6) ≈ false from the second rule.
1.2 Equal Left-Hand Sides
There are two conditions with left-hand side le($3,$6) and respective right-hand sides true and false.
1.2.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.

Certification Problem

Input (COPS 322)

Property / Task

Answer / Result

Proof (by ConCon @ CoCo 2020)

1 Almost-orthogonal modulo infeasibility

1.1 Equal Left-Hand Sides

1.1.1 Non-joinability by TCAP

1.2 Equal Left-Hand Sides

1.2.1 Non-joinability by TCAP