## Stream: Mirror: Isabelle Users Mailing List

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

#### 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]

• (dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL))
≤ dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL)
[- (dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL))
≤ dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL)]
¬ - (dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL)) / dt
≤ (dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL)) / dt
[¬ - (dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL)) /
dt
≤ (dtR * (D - (q t1 - q t) / dtR) + dtL * (D - (q t - q t0) / dtL)) /
dt]

Proved:

• (a__ * dtR / dtR) +
(b__ * dtR / dtR + (- (b__ * dtL / dtL) + c__ * dtL / dtL))
< - (dtR * a__ / dtR) +
(dtR * b__ / dtR + (- (dtL * b__ / dtL) + dtL * c__ / dtL))
[- (dtR * (D - (a__ - b__) / dtR) + dtL * (D - (b__ - c__) / dtL))
≤ dtR * (D - (a__ - b__) / dtR) + dtL * (D - (b__ - c__) / dtL),
dtR * (D - (a__ - b__) / dtR) + dtL * (D - (b__ - c__) / dtL) < 0]

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

Last updated: Jan 25 2022 at 01:11 UTC