Certification Problem

Input (COPS 801)

We consider the TRS containing the following rules:

f(x,x) → f(a,b) (1)

The underlying signature is as follows:

{f/2, a/0, b/0}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2023)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

f(x,x) → f(a,b) (1)

All redundant rules that were added or removed can be simulated in 2 steps .

1.1 Locally confluent and terminating

Confluence is proven by showing local confluence and termination.

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(x,x) → f#(a,b) (2)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

1.1.2 Local Confluence Proof

All critical pairs are joinable which can be seen by computing normal forms of all critical pairs.