Certification Problem

Input (COPS 528)

The rewrite relation of the following conditional TRS is considered.

plus(0,y) → y
plus(s(x),y) → s(plus(x,y))
fib(0) → pair(s(0),0)
fib(s(x)) → pair(z3,z1) | fib(x) ≈ pair(z1,z2), plus(z1,z2) ≈ z3

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.
plus(0,y) → y
plus(s(x),y) → s(plus(x,y))
fib(0) → pair(s(0),0)
fib(s(x)) → pair(plus(z1,z2),z1) | fib(x) ≈ pair(z1,z2)

1.1 Almost-orthogonal

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