Certification Problem

Input (COPS 492)

The rewrite relation of the following conditional TRS is considered.

f(x) → a | a ≈ x
f(x) → b | b ≈ x

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

1 Quasi-reductive SDTRS where all CCPs are joinable

The given strongly deterministic oriented 3-CTRS is quasi-reductive and all CCPs are joinable.

1.1 Quasi-Reductive CTRS

The given CTRS is quasi-reductive

1.1.1 Unraveling

To prove that the CTRS is quasi-reductive, we show termination of the following unraveled system.

For f(x)aax we get
For f(x)bbx we get

1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(U2) = 4 weight(U2) = 1
prec(b) = 0 weight(b) = 3
prec(U1) = 4 weight(U1) = 1
prec(a) = 0 weight(a) = 3
prec(f) = 5 weight(f) = 4
all of the following rules can be deleted.
f(x) → U1(a,x) (1)
U1(x,x) → a (2)
f(x) → U2(b,x) (3)
U2(x,x) → b (4)

1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.

1.2 All CCPs are joinable

A CCP is joinable if it is context-joinable, infeasible, or unfeasible.