Certification Problem

Input (COPS 837)

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:

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.