Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] try0 says "Please inform Tobias Nipkow"


view this post on Zulip Email Gateway (Aug 14 2021 at 03:08):

From: Jeremy Sylvestre <jsylvest@ualberta.ca>
Got the following output from try0, the second-last line of the output
asked me to inform someone, hence this email to the list. Let me know if
the actual theory that caused this output is needed.

---- try0 output -----------------------------------------
Trying "simp", "auto", "blast", "metis", "argo", "linarith", "presburger",
"algebra", "fast", "fastforce", "force", "meson", and "satx"...
Assumptions:
0 ≤ dtR * (D - (q t1 - q t) / dtR) [0 ≤ dtR * (D - (q t1 - q t) / dtR)]
0 ≤ dtL * (D - (q t - q t0) / dtL) [0 ≤ dtL * (D - (q t - q t0) / dtL)]
dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL) < 0
[dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL) < 0]

Proved:

Linear arithmetic should have refuted the assumptions.
Please inform Tobias Nipkow.
No proof found


Last updated: Dec 05 2021 at 23:19 UTC