Certification Problem

Input (COPS 1144)

The rewrite relation of the following (conditional) TRS is considered.

f(y,a) g(x,x) | h(z) ≈ x, yk(z), xb
f(y,z) k(x) | zh(a), yk(a), ax
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)) | yk(z), h(z) ≈ b
f(y,z) k(a) | zh(a), yk(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, yk(z), xb
h(z)x
f(y,z) k(x) | zh(a), yk(a), ax
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)) | yk(z), h(z) ≈ b
yk(z)
f(y,z) k(a) | zh(a), yk(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.