Certification Problem
Input (COPS 316)
The rewrite relation of the following conditional TRS is considered.
|
f(x,y) |
→ |
x |
| g(x) ≈ z, g(y) ≈ z
|
|
g(x) |
→ |
c |
| d ≈ c
|
Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by ConCon @ CoCo 2020)
1 Removal of Infeasible Rules
We may safely remove rules with infeasible conditions. They do not
influence the rewrite relation in any way.
1.1 Rules with Infeasible Conditions
-
1.1.1 Rule with Infeasible Conditions
The rule
has infeasible conditions.
1.1.1.1 Infeasible Equation
The equation
is infeasible.
1.1.1.1.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.1.1.1.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.
1.2 Quasi-reductive SDTRS where all CCPs are joinable
The given strongly deterministic oriented 3-CTRS is quasi-reductive and all CCPs are joinable.
1.2.1 Quasi-Reductive CTRS
The given CTRS is quasi-reductive
1.2.1.1 Unraveling
To prove that the CTRS is quasi-reductive, we show termination of the following
unraveled system.
| For |
f(x,y)xg(x)zg(y)z we get |
1.2.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [g(x1)] |
= |
2 · x1 + 0 |
| [U2(x1,...,x4)] |
= |
4 · x1 + 2 · x2 + 1 · x3 + 6 · x4 + 8 |
| [f(x1, x2)] |
= |
26 · x1 + 9 · x2 + 16 |
| [U1(x1, x2, x3)] |
= |
12 · x1 + 2 · x2 + 9 · x3 + 16 |
all of the following rules can be deleted.
|
U1(z,x,y) |
→ |
U2(g(y),x,y,z) |
(3) |
|
U2(z,x,y,z) |
→ |
x |
(4) |
1.2.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the naturals
| [g(x1)] |
= |
· x1 +
|
| [f(x1, x2)] |
= |
· x1 + · x2 +
|
| [U1(x1, x2, x3)] |
= |
· x1 + · x2 + · x3 +
|
all of the following rules can be deleted.
|
f(x,y) |
→ |
U1(g(x),x,y) |
(2) |
1.2.1.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
1.2.2 All CCPs are joinable
A CCP is joinable if it is context-joinable, infeasible, or unfeasible.