Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] unsolvable system of inequalities

Email Gateway (Aug 22 2022 at 17:45):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
Is there an automatic way to verify that a system of inequalities is
unsolvable?

In particular, I want to automatically prove following lemma:

lemma G1:
fixes a b u v x y :: real
assumes "a ≥ 0" and "b ≥ 0" and "u ≥ 0" and "v ≥ 0" and "x ≥ 0" and "y ≥
0"
and "b * v < a * u" and "b * u * y + a * v * y < a * u * x - b * v * x"
and
"¬ v * y < u * x" and "b * (v * y) - b * (u * x) < a * (v * x) + a * (u * y)"
shows False

Thank you in advance,
José M.

Last updated: Apr 19 2024 at 08:19 UTC