Certification Problem
Input (COPS 326)
The rewrite relation of the following conditional TRS is considered.
|
isnoc(cons(y,nil)) |
→ |
tp2(nil,y) |
|
isnoc(cons(x,ys)) |
→ |
tp2(cons(x,xs),y) |
| isnoc(ys) ≈ tp2(xs,y) |
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 isnoc(nil) ≈ tp2(x',y')
from the first rule
and
no conditions
from the second rule.
1.1 Infeasible Equation
The equation
is infeasible.
1.1.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.1.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.
-
The
2nd
CCP contains
no conditions
from the first rule
and
the condition isnoc(nil) ≈ tp2(x',y')
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.