Certification Problem

Input (COPS 371)

The rewrite relation of the following conditional TRS is considered.

a c
b c
f(x) x | ax

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 ac we get
For bc we get
For f(x)xax we get

1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(U1) = 6 weight(U1) = 1
prec(f) = 7 weight(f) = 2
prec(b) = 5 weight(b) = 1
prec(c) = 0 weight(c) = 1
prec(a) = 1 weight(a) = 1
all of the following rules can be deleted.
a c (1)
b c (2)
f(x) U1(a,x) (3)
U1(x,x) x (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.