Certification Problem
Input (COPS 308)
The rewrite relation of the following conditional TRS is considered.
|
not(x) |
→ |
false |
| x ≈ true
|
|
not(x) |
→ |
true |
| x ≈ false
|
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 ≈ false
from the first rule
and
the condition z ≈ true
from the second rule.
1.1 Equal Left-Hand Sides
There are two conditions with left-hand side
z
and respective right-hand sides
false
and
true.
1.1.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
-
The
2nd
CCP contains
the condition z ≈ true
from the first rule
and
the condition z ≈ false
from the second rule.
1.2 Equal Left-Hand Sides
There are two conditions with left-hand side
z
and respective right-hand sides
true
and
false.
1.2.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.