Certification Problem
Input (COPS 883)
The rewrite relation of the following (conditional) TRS is considered.
|
f(c(x),c(c(y))) |
→ |
a(a(x)) |
| c(f(x,y)) ≈ c(a(b)) |
|
f(c(c(c(x))),y) |
→ |
a(y) |
| c(f(c(x),c(c(y)))) ≈ c(a(a(b))) |
|
h(b) |
→ |
b |
| |
|
h(a(a(x))) |
→ |
a(b) |
| h(x) ≈ b
|
The question is whether the following conditions are infeasible, i.e., there is no substitution σ
such that all of the following is true:
-
c(f(c(c(x1)),y))σ→*c(a(b))σ
-
c(f(c(x1),c(c(c(c(y))))))σ→*c(a(a(b)))σ
Property / Task
Prove or disprove an infeasibility problem.Answer / Result
Yes.Proof (by nonreach @ CoCo 2023)
|
h(a(a(x))) |
→ |
a(b) |
| h(x) ≈ b
|
|
h(b) |
→ |
b |
| |
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.