Certification Problem
Input (COPS 547)
The rewrite relation of the following conditional TRS is considered.
|
f(x) |
→ |
a |
| x ≈ a
|
|
f(x) |
→ |
b |
| x ≈ b
|
Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by ConCon @ CoCo 2020)
1 Almost-orthogonal modulo infeasibility
The given (extended) properly oriented, right-stable, oriented 3-CTRS
is almost-orthogonal modulo infeasibility,
since all its conditional critical pairs are infeasible.
-
The
1st
CCP contains
the condition z ≈ b
from the first rule
and
the condition z ≈ a
from the second rule.
1.1 Equal Left-Hand Sides
There are two conditions with left-hand side
z
and respective right-hand sides
b
and
a.
1.1.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
-
The
2nd
CCP contains
the condition z ≈ a
from the first rule
and
the condition z ≈ b
from the second rule.
1.2 Equal Left-Hand Sides
There are two conditions with left-hand side
z
and respective right-hand sides
a
and
b.
1.2.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.