section \<open>Examples for Ferrante and Rackoff's quantifier elimination procedure\<close>
theory Dense_Linear_Order_Ex imports"../Dense_Linear_Order" begin
lemma"\(y::'a::linordered_field) < 2. x + 3* y < 0 \ x - y > 0" by ferrack
lemma"\ (\x (y::'a::linordered_field). x < y \ 10 * x < 11 * y)" by ferrack
lemma"\(x::'a::linordered_field) y. x < y \ 10 * (x + 5 * y + -1) < 60 * y" by ferrack
lemma"\(x::'a::linordered_field) y. x \ y \ x < y" by ferrack
lemma"\(x::'a::linordered_field) y. x \ y \ 10 * x \ 9 * y \ 10 * x < y \ x < y" by ferrack
lemma"\(x::'a::linordered_field) y. x \ y \ 5 * x \ y \ 500 * x \ 100 * y" by ferrack
lemma"\x::'a::linordered_field. \y::'a::linordered_field. 4 * x + 3 * y \ 0 \ 4 * x + 3 * y \ -1" by ferrack
lemma"\(x::'a::linordered_field) < 0. \(y::'a::linordered_field) > 0. 7 * x + y > 0 \x - y \ 9" by ferrack
lemma"\x::'a::linordered_field. 0 < x \ x < 1 \ (\y > 1. x + y \ 1)" by ferrack
lemma"\x. \y::'a::linordered_field. y < 2 \ 2 * (y - x) \ 0" by ferrack
lemma"\x::'a::linordered_field. x < 10 \ x > 20 \ (\y. y \ 0 \ y \ 10 \ x + y = 20)" by ferrack
lemma"\(x::'a::linordered_field) y z. x + y < z \ y \ z \ x < 0" by ferrack
lemma"\(x::'a::linordered_field) y z. x + 7 * y < 5 * z \ 5 * y \ 7 * z \ x < 0" by ferrack
lemma"\(x::'a::linordered_field) y z. \x + y\ \ z \ \z\ = z" by ferrack
lemma"\(x::'a::linordered_field) y z. x + 7 * y - 5 * z < 0 \ 5 * y + 7 * z + 3 * x < 0" by ferrack
lemma"\(x::'a::linordered_field) y z.
(\<bar>5 * x + 3 * y + z\<bar> \<le> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<ge> - (5 * x + 3 * y + z)) \<or>
(\<bar>5 * x + 3 * y + z\<bar> \<ge> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<le> - (5 * x + 3 * y + z))" by ferrack
lemma"\(x::'a::linordered_field) y. x < y \ (\z>0. x + z = y)" by ferrack
lemma"\(x::'a::linordered_field) y. x < y \ (\z>0. x + z = y)" by ferrack
lemma"\(x::'a::linordered_field) y. \z>0. \x - y\ \ z" by ferrack
lemma"\(x::'a::linordered_field) y. \z<0. (z < x \ z \ y) \ (z > y \ z \ x)" by ferrack
lemma"\(x::'a::linordered_field) y. \z\0. \3 * x + 7 * y\ \ 2 * z + 1" by ferrack
lemma"\(x::'a::linordered_field) y. \z<0. (z < x \ z \ y) \ (z > y \ z \ x)" by ferrack
lemma"\(x::'a::linordered_field) > 0. \y. \z. 13 * \z\ \ \12 * y - x\ \ 5 * x - 3 * \y\ \ 7 * z" by ferrack
lemma"\x::'a::linordered_field. \<bar>4 * x + 17\<bar> < 4 \<and> (\<forall>y. \<bar>x * 34 - 34 * y - 9\<bar> \<noteq> 0 \<longrightarrow> (\<exists>z. 5 * x - 3 * \<bar>y\<bar> \<le> 7 * z))" by ferrack
lemma"\x::'a::linordered_field. \y > \23 * x - 9\. \z > \3 * y - 19 * \x\\. x + z > 2 * y" by ferrack
lemma"\x::'a::linordered_field. \<exists>y < \<bar>3 * x - 1\<bar>. \<forall>z \<ge> 3 * \<bar>x\<bar> - 1. \<bar>12 * x - 13 * y + 19 * z\<bar> > \<bar>23 * x\<bar>" by ferrack
lemma"\x::'a::linordered_field. \x\ < 100 \ (\y > x. (\z < 2 * y - x. 5 * x - 3 * y \ 7 * z))" by ferrack
lemma"\(x::'a::linordered_field) y z w.
7 * x < 3 * y \<longrightarrow> 5 * y < 7 * z \<longrightarrow> z < 2 * w \<longrightarrow> 7 * (2 * w - x) > 2 * y" by ferrack
lemma"\(x::'a::linordered_field) y z w. 5 * x + 3 * z - 17 * w + \y - 8 * x + z\ \ 89" by ferrack
lemma"\(x::'a::linordered_field) y z w.
5 * x + 3 * z - 17 * w + 7 * (y - 8 * x + z) \<le> max y (7 * z - x + w)" by ferrack
lemma"\(x::'a::linordered_field) y z w.
min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" by ferrack
lemma"\(x::'a::linordered_field) y z. \w \ x + y + z. w \ \x\ + \y\ + \z\" by ferrack
lemma"\ (\x::'a::linordered_field. \y z w.
3 * x + z * 4 = 3 * y \<and> x + y < z \<and> x > w \<and> 3 * x < w + y)" by ferrack
lemma"\(x::'a::linordered_field) y. \z w. \x - y\ = z - w \ z * 1234 < 233 * x \ w \ y" by ferrack
lemma"\x::'a::linordered_field. \y z w.
min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" by ferrack
lemma"\(x::'a::linordered_field) y z. \w \ \x + y + z\. w \ \x\ + \y\ + \z\" by ferrack
lemma"\z. \(x::'a::linordered_field) y. \w \ x + y + z. w \ \x\ + \y\ + \z\" by ferrack
lemma"\z. \(x::'a::linordered_field) < \z\. \y w. x < y \ x < z \ x > w \ 3 * x < w + y" by ferrack
lemma"\(x::'a::linordered_field) y. \z. \w. \x - y\ = \z - w\ \ z < x \ w \ y" by ferrack
lemma"\y. \x::'a::linordered_field. \z w.
min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" by ferrack
lemma"\(x::'a::linordered_field) z. \w \ 13 * x - 4 * z. \y. w \ \x\ + \y\ + z" by ferrack
lemma"\x::'a::linordered_field. \y < x. \z > x + y. \<forall>w. 5 * w + 10 * x - z \<ge> y \<longrightarrow> w + 7 * x + 3 * z \<ge> 2 * y" by ferrack
lemma"\x::'a::linordered_field. \y. \z > y. \<forall>w. w < 13 \<longrightarrow> w + 10 * x - z \<ge> y \<longrightarrow> 5 * w + 7 * x + 13 * z \<ge> 2 * y" by ferrack
lemma"\(x::'a::linordered_field) y z w.
min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" by ferrack
lemma"\x::'a::linordered_field. \y. \z>19. y \ x + z \ (\w. \y - x\ < w)" by ferrack
lemma"\x::'a::linordered_field. \y. \z>19. y \ x + z \ (\w. \x + z\ < w - y)" by ferrack
lemma"\x::'a::linordered_field. \y. \<bar>y\<bar> \<noteq> \<bar>x\<bar> \<and> (\<forall>z > max x y. \<exists>w. w \<noteq> y \<and> w \<noteq> z \<and> 3 * w - z \<ge> x + y)" by ferrack
end
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.11Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
