Certification Problem

Input (COPS 343)

The rewrite relation of the following conditional TRS is considered.

add(x,0) x
add(x,s(y)) s(z) | add(x,y) ≈ z

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.
add(x,0) x
add(x,s(y)) s(add(x,y))

1.1 Almost-orthogonal

The given (extended) properly oriented, right-stable, oriented 3-CTRS is almost-orthogonal, since there are no conditional critical pairs.