Certification Problem
Input (COPS 927)
The rewrite relation of the following (conditional) TRS is considered.
| a |
→ |
a |
| b ≈ x, c ≈ x
|
| b |
→ |
d |
| d ≈ x, e ≈ x
|
| c |
→ |
d |
| d ≈ x, e ≈ x
|
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)
There are no rules.
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.