Certification Problem

Input (COPS 550)

The rewrite relation of the following conditional TRS is considered.

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

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(b)f(a) we get
For bc we get
For acbc we get

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (5 x 5)-matrices with strict dimension 1 over the naturals
[U1(x1)] =
1 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
· x1 +
0 0 0 0 0
1 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
[f(x1)] =
1 0 1 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
· x1 +
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
[c] =
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
[b] =
0 0 0 0 0
0 0 0 0 0
1 0 0 0 0
0 0 0 0 0
0 0 0 0 0
[a] =
0 0 0 0 0
1 0 0 0 0
0 0 0 0 0
0 0 0 0 0
0 0 0 0 0
all of the following rules can be deleted.
f(b) → f(a) (1)

1.1.1.1.1 Rule Removal

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

1.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.