Certification Problem
Input (COPS 1144)
The rewrite relation of the following (conditional) TRS is considered.
|
f(y,a) |
→ |
g(x,x) |
| h(z) ≈ x, y ≈ k(z), x ≈ b
|
|
f(y,z) |
→ |
k(x) |
| z ≈ h(a), y ≈ k(a), a ≈ x
|
|
k(x) |
→ |
h(x) |
| |
|
k(x) |
→ |
b |
| |
|
k(x) |
→ |
a |
| |
| a |
→ |
b |
| |
|
g(x,x) |
→ |
a |
| |
The question is whether the following conditions are infeasible, i.e., there is no substitution σ
such that all of the following is true:
Property / Task
Prove or disprove an infeasibility problem.Answer / Result
Yes.Proof (by nonreach @ CoCo 2023)
|
f(y,a) |
→ |
g(h(z),h(z)) |
| y ≈ k(z), h(z) ≈ b
|
|
f(y,z) |
→ |
k(a) |
| z ≈ h(a), y ≈ k(a) |
|
k(x) |
→ |
h(x) |
| |
|
k(x) |
→ |
b |
| |
|
k(x) |
→ |
a |
| |
| a |
→ |
b |
| |
|
g(x,x) |
→ |
a |
| |
|
f(y,a) |
→ |
g(x,x) |
| h(z) ≈ x, y ≈ k(z), x ≈ b
|
h(z)x
|
f(y,z) |
→ |
k(x) |
| z ≈ h(a), y ≈ k(a), a ≈ x
|
ax
|
f(k(z),a) |
→ |
g(h(z),h(z)) |
| h(z) ≈ b
|
|
f(k(a),h(a)) |
→ |
k(a) |
| |
|
k(x) |
→ |
h(x) |
| |
|
k(x) |
→ |
b |
| |
|
k(x) |
→ |
a |
| |
| a |
→ |
b |
| |
|
g(x,x) |
→ |
a |
| |
|
f(y,a) |
→ |
g(h(z),h(z)) |
| y ≈ k(z), h(z) ≈ b
|
yk(z)
|
f(y,z) |
→ |
k(a) |
| z ≈ h(a), y ≈ k(a) |
yk(a)zh(a)
|
f(k(a),h(a)) |
→ |
k(a) |
| |
|
k(x) |
→ |
h(x) |
| |
|
k(x) |
→ |
b |
| |
|
k(x) |
→ |
a |
| |
| a |
→ |
b |
| |
|
g(x,x) |
→ |
a |
| |
1 Infeasible Compound Conditions
We collect the conditions in the fresh compound-symbol
|.
1.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.