Certification Problem

Input (COPS 375)

The rewrite relation of the following conditional TRS is considered.

a → b
f(x) → A | x ≈ b
g(x,x) → h(x)
h(x) → i(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 ab we get
For f(x)Axb we get
For g(x,x)h(x) we get
For h(x)i(x) we get

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[A] =
0 0 0
2 0 0
0 0 0
[b] =
0 0 0
1 0 0
0 0 0
[U1(x1, x2)] =
1 0 2
1 2 0
1 0 0
· x1 +
2 0 0
2 0 0
1 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[g(x1, x2)] =
2 1 0
0 1 1
0 0 0
· x1 +
1 1 0
0 1 1
1 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a] =
2 0 0
2 0 0
2 0 0
[i(x1)] =
3 2 0
0 2 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[h(x1)] =
3 2 0
0 2 2
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[f(x1)] =
3 0 2
3 3 0
3 1 0
· x1 +
0 0 0
2 0 0
1 0 0
all of the following rules can be deleted.
a → b (1)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[A] =
0 0 0
0 0 0
0 0 0
[b] =
0 0 0
1 0 0
3 0 0
[U1(x1, x2)] =
1 1 2
0 1 0
0 0 0
· x1 +
2 0 1
1 2 3
0 0 1
· x2 +
0 0 0
0 0 0
0 0 0
[g(x1, x2)] =
1 1 0
0 2 0
2 0 0
· x1 +
1 0 0
0 0 1
0 2 2
· x2 +
2 0 0
0 0 0
0 0 0
[i(x1)] =
2 0 0
0 2 0
2 2 2
· x1 +
0 0 0
0 0 0
0 0 0
[h(x1)] =
2 0 0
0 2 1
2 2 2
· x1 +
0 0 0
0 0 0
0 0 0
[f(x1)] =
3 2 3
1 3 3
0 0 2
· x1 +
0 0 0
1 0 0
2 0 0
all of the following rules can be deleted.
U1(b,x) → A (3)
g(x,x) → h(x) (4)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[U1(x1, x2)] =
2 0 0
0 0 0
0 1 0
· x1 +
1 0 0
0 0 0
2 1 0
· x2 +
0 0 0
0 0 0
0 0 0
[i(x1)] =
2 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[h(x1)] =
2 0 0
0 0 0
0 0 0
· x1 +
2 0 0
0 0 0
0 0 0
[f(x1)] =
3 0 0
0 0 0
2 2 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
h(x) → i(x) (5)

1.1.1.1.1.1.1 Rule Removal

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

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.