Certification Problem
Input (COPS 362)
The rewrite relation of the following conditional TRS is considered.
|
f(x) |
→ |
c |
| a ≈ b
|
|
g(x,x) |
→ |
g(f(a),f(b)) |
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 |
g(x,x)g(f(a),f(b)) we get |
1.2.1.1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
g#(x,x) |
→ |
g#(f(a),f(b)) |
(3) |
1.2.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
1.2.2 All CCPs are joinable
A CCP is joinable if it is context-joinable, infeasible, or unfeasible.