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