Certification Problem

Input (COPS 551)

The rewrite relation of the following conditional TRS is considered.

le(x,0) → false
le(0,s(y)) → true
le(s(x),s(y)) → le(x,y)
min(cons(x,nil)) → x
min(cons(x,xs)) → x | min(xs) ≈ y, le(x,y) ≈ true
min(cons(x,xs)) → y | min(xs) ≈ y, le(x,y) ≈ false

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

1 Inlining of Conditions

Inlining of conditions results in the following transformed CTRS having the same multistep rewrite relation.
le(x,0) → false
le(0,s(y)) → true
le(s(x),s(y)) → le(x,y)
min(cons(x,nil)) → x
min(cons(x,xs)) → x | le(x,min(xs)) ≈ true
min(cons(x,xs)) → min(xs) | le(x,min(xs)) ≈ false

1.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.