Certification Problem
Input (COPS 1139)
The rewrite relation of the following conditional TRS is considered.
|
f(k(z),a) |
→ |
g(x,x) |
| h(z) ≈ x, x ≈ b
|
|
f(k(a),h(a)) |
→ |
k(x) |
| a ≈ x
|
|
k(x) |
→ |
h(x) |
|
k(x) |
→ |
b |
|
k(x) |
→ |
a |
| a |
→ |
b |
|
g(x,x) |
→ |
a |
Property / Task
Prove or disprove confluence.Answer / Result
No.Proof (by ConCon @ CoCo 2020)
1 Removal of Infeasible Rules
We may safely remove rules with infeasible conditions. They do not
influence the rewrite relation in any way.
1.1 Rules with Infeasible Conditions
-
1.1.1 Rule with Infeasible Conditions
The rule
|
f(k(z),a) |
→ |
g(x,x) |
| h(z) ≈ x, x ≈ b
|
has infeasible conditions.
1.1.1.1 Transitive Condition Composition
The right-hand side of the condition
h(z) ≈ x
coincides with the left-hand side of the condition
x ≈ b.
Therefore, it suffices to show infeasibility of the combined condition
h(z) ≈ b.
1.1.1.1.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.1.1.1.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.
1.2 Inlining of Conditions
Inlining of conditions results in the following transformed CTRS having the
same multistep rewrite relation.
|
f(k(a),h(a)) |
→ |
k(a) |
|
k(x) |
→ |
h(x) |
|
k(x) |
→ |
b |
|
k(x) |
→ |
a |
| a |
→ |
b |
|
g(x,x) |
→ |
a |
1.2.1 Non-Joinable Fork
The system is not confluent due to the following forking derivations.
The two resulting terms cannot be joined for the following reason:
- When applying the cap-function on both terms (where variables may be treated like constants)
then the resulting terms do not unify.