Certification Problem

Input (COPS 792)

The rewrite relation of the following conditional TRS is considered.

f(x) x | xa, bx
a b
b c
c b

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

1 Removal of Infeasible Rules

We may safely remove rules with infeasible conditions. They do not influence the rewrite relation in any way.

1.1 Rules with Infeasible Conditions

1.2 Almost-orthogonal

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