Certification Problem
Input (COPS 552)
The rewrite relation of the following conditional TRS is considered.
|
le(x,0) |
→ |
false |
|
le(0,s(y)) |
→ |
true |
|
le(s(x),s(y)) |
→ |
le(x,y) |
|
min(cons(x,nil)) |
→ |
x |
|
min(cons(x,xs)) |
→ |
x |
| le(x,min(xs)) ≈ true
|
|
min(cons(x,xs)) |
→ |
min(xs) |
| le(x,min(xs)) ≈ 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 le(x',min(y')) ≈ false
from the first rule
and
the condition le(x',min(y')) ≈ true
from the second rule.
1.1 Equal Left-Hand Sides
There are two conditions with left-hand side
le(x',min(y'))
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 le(x',min(nil)) ≈ false
from the first rule
and
no conditions
from the second rule.
1.2 Infeasible Equation
The equation
is infeasible.
1.2.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.2.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.
-
The
3rd
CCP contains
no conditions
from the first rule
and
the condition le(z,min(nil)) ≈ false
from the second rule.
1.3 Infeasible Equation
The equation
is infeasible.
1.3.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.3.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.
-
The
4th
CCP contains
the condition le(x',min(y')) ≈ true
from the first rule
and
the condition le(x',min(y')) ≈ false
from the second rule.
1.4 Equal Left-Hand Sides
There are two conditions with left-hand side
le(x',min(y'))
and respective right-hand sides
true
and
false.
1.4.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.