Certification Problem
Input (COPS 794)
The rewrite relation of the following conditional TRS is considered.
| a |
→ |
c |
| f(a) ≈ f(b) |
|
f(b) |
→ |
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 Almost-orthogonal
The given (extended) properly oriented, right-stable, oriented 3-CTRS
is almost-orthogonal,
since there are no conditional critical pairs.