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