Certification Problem

Input (COPS 901)

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

add(0,x) x |
add(s(x),y) s(add(x,y)) |
mult(0,y) 0 |
mult(s(x),y) add(mult(x,y),y) |
lte(0,y) true |
lte(s(x),0) false |
lte(s(x),s(y)) lte(x,y) |
minus(0,s(y)) 0 |
minus(x,0) x |
minus(s(x),s(y)) minus(x,y) |
mod(0,y) 0 |
mod(x,0) x |
mod(x,s(y)) mod(minus(x,s(y)),s(y)) | lte(s(y),x) ≈ true
mod(x,s(y)) x | lte(s(y),x) ≈ false
div(0,s(x)) 0 |
div(s(x),s(y)) 0 | lte(s(x),y) ≈ true
div(s(x),s(y)) s(q) | lte(s(x),y) ≈ false, div(minus(x,y),s(y)) ≈ q
power(x,0) s(0) |
power(x,n) mult(mult(y,y),s(0)) | ns(n'), mod(n,s(s(0))) ≈ 0, power(x,div(n,s(s(0)))) ≈ y
power(x,n) mult(mult(y,y),x) | ns(n'), mod(n,s(s(0))) ≈ s(z), power(x,div(n,s(s(0)))) ≈ 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)

add(0,x) x |
add(s(x),y) s(add(x,y)) |
mult(0,y) 0 |
mult(s(x),y) add(mult(x,y),y) |
lte(0,y) true |
lte(s(x),0) false |
lte(s(x),s(y)) lte(x,y) |
minus(0,s(y)) 0 |
minus(x,0) x |
minus(s(x),s(y)) minus(x,y) |
mod(0,y) 0 |
mod(x,0) x |
mod(x,s(y)) mod(minus(x,s(y)),s(y)) | lte(s(y),x) ≈ true
mod(x,s(y)) x | lte(s(y),x) ≈ false
div(0,s(x)) 0 |
div(s(x),s(y)) 0 | lte(s(x),y) ≈ true
div(s(x),s(y)) s(div(minus(x,y),s(y))) | lte(s(x),y) ≈ false
power(x,0) s(0) |
power(x,n) mult(mult(power(x,div(n,s(s(0)))),power(x,div(n,s(s(0))))),s(0)) | ns(n'), mod(n,s(s(0))) ≈ 0
power(x,n) mult(mult(power(x,div(n,s(s(0)))),power(x,div(n,s(s(0))))),x) | ns(n'), mod(n,s(s(0))) ≈ s(z)
div(s(x),s(y)) s(q) | lte(s(x),y) ≈ false, div(minus(x,y),s(y)) ≈ q
div(minus(x,y),s(y))q
power(x,n) mult(mult(y,y),s(0)) | ns(n'), mod(n,s(s(0))) ≈ 0, power(x,div(n,s(s(0)))) ≈ y
power(x,div(n,s(s(0))))y
power(x,n) mult(mult(y,y),x) | ns(n'), mod(n,s(s(0))) ≈ s(z), power(x,div(n,s(s(0)))) ≈ y
power(x,div(n,s(s(0))))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.