Certification Problem

Input (COPS 339)

The rewrite relation of the following conditional TRS is considered.

f(x,x') → g(y,y) | x ≈ y, x' ≈ y
h(x,x',x'') → c | x ≈ y, x' ≈ y, x'' ≈ y

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,x')g(y,y)xyx'y we get
For h(x,x',x'')cxyx'yx''y we get

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[h(x1, x2, x3)] = 16 · x1 + 16 · x2 + 20 · x3 + 1
[c] = 0
[U1(x1, x2, x3)] = 8 · x1 + 1 · x2 + 22 · x3 + 0
[g(x1, x2)] = 7 · x1 + 19 · x2 + 0
[U3(x1,...,x4)] = 4 · x1 + 4 · x2 + 6 · x3 + 18 · x4 + 0
[f(x1, x2)] = 9 · x1 + 26 · x2 + 0
[U5(x1,...,x5)] = 12 · x1 + 2 · x2 + 4 · x3 + 2 · x4 + 3 · x5 + 0
[U4(x1,...,x5)] = 1 · x1 + 4 · x2 + 4 · x3 + 18 · x4 + 2 · x5 + 0
[U2(x1,...,x4)] = 18 · x1 + 1 · x2 + 4 · x3 + 8 · x4 + 0
all of the following rules can be deleted.
h(x,x',x'') → U3(x,x,x',x'') (4)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[c] = 0
[U1(x1, x2, x3)] = 8 · x1 + 2 · x2 + 7 · x3 + 0
[g(x1, x2)] = 7 · x1 + 6 · x2 + 0
[U3(x1,...,x4)] = 3 · x1 + 16 · x2 + 22 · x3 + 19 · x4 + 16
[f(x1, x2)] = 10 · x1 + 7 · x2 + 0
[U5(x1,...,x5)] = 3 · x1 + 1 · x2 + 4 · x3 + 16 · x4 + 2 · x5 + 0
[U4(x1,...,x5)] = 17 · x1 + 1 · x2 + 4 · x3 + 19 · x4 + 3 · x5 + 16
[U2(x1,...,x4)] = 5 · x1 + 2 · x2 + 2 · x3 + 8 · x4 + 0
all of the following rules can be deleted.
U4(y,x,x',x'',y) → U5(x'',x,x',x'',y) (6)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[c] = 0
[U1(x1, x2, x3)] = 16 · x1 + 1 · x2 + 19 · x3 + 1
[g(x1, x2)] = 4 · x1 + 16 · x2 + 0
[U3(x1,...,x4)] = 4 · x1 + 16 · x2 + 20 · x3 + 2 · x4 + 16
[f(x1, x2)] = 22 · x1 + 19 · x2 + 1
[U5(x1,...,x5)] = 16 · x1 + 4 · x2 + 1 · x3 + 4 · x4 + 9 · x5 + 0
[U4(x1,...,x5)] = 16 · x1 + 16 · x2 + 4 · x3 + 2 · x4 + 4 · x5 + 0
[U2(x1,...,x4)] = 18 · x1 + 1 · x2 + 1 · x3 + 2 · x4 + 0
all of the following rules can be deleted.
U1(y,x,x') → U2(x',x,x',y) (2)
U3(y,x,x',x'') → U4(x',x,x',x'',y) (5)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[c] =
0 0
0 0
[U1(x1, x2, x3)] =
1 3
0 0
· x1 +
2 1
0 0
· x2 +
1 0
0 0
· x3 +
0 0
0 0
[g(x1, x2)] =
1 0
6 4
· x1 +
5 4
2 0
· x2 +
0 0
0 0
[f(x1, x2)] =
3 4
0 0
· x1 +
4 1
1 0
· x2 +
4 0
0 0
[U5(x1,...,x5)] =
3 1
1 0
· x1 +
1 0
0 0
· x2 +
2 0
2 0
· x3 +
4 0
0 0
· x4 +
4 0
2 1
· x5 +
0 0
0 0
[U2(x1,...,x4)] =
2 0
4 4
· x1 +
4 0
1 1
· x2 +
1 0
0 0
· x3 +
4 4
4 0
· x4 +
0 0
0 0
all of the following rules can be deleted.
f(x,x') → U1(x,x,x') (1)

1.1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(c) = 2 weight(c) = 5
prec(U5) = 3 weight(U5) = 0
prec(g) = 0 weight(g) = 4
prec(U2) = 1 weight(U2) = 2
all of the following rules can be deleted.
U2(y,x,x',y) → g(y,y) (3)
U5(y,x,x',x'',y) → c (7)

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