Theory Dense_Linear_Order_Ex

(* Author:     Amine Chaieb, TU Muenchen *)

section ‹Examples for Ferrante and Rackoff's quantifier elimination procedure›

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.
  (¦5 * x + 3 * y + z¦ ≤ 5 * x + 3 * y + z ∧ ¦5 * x + 3 * y + z¦ ≥ - (5 * x + 3 * y + z)) ∨
  (¦5 * x + 3 * y + z¦ ≥ 5 * x + 3 * y + z ∧ ¦5 * x + 3 * y + z¦ ≤ - (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.
  ¦4 * x + 17¦ < 4 ∧ (∀y. ¦x * 34 - 34 * y - 9¦ ≠ 0 ⟶ (∃z. 5 * x - 3 * ¦y¦ ≤ 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.
  ∃y < ¦3 * x - 1¦. ∀z ≥ 3 * ¦x¦ - 1. ¦12 * x - 13 * y + 19 * z¦ > ¦23 * x¦"
  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 ⟶ 5 * y < 7 * z ⟶ z < 2 * w ⟶ 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) ≤ max y (7 * z - x + w)"
  by ferrack

lemma "∃(x::'a::linordered_field) y z w.
  min (5 * x + 3 * z) (17 * w) + 5 * ¦y - 8 * x + z¦ ≤ 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 ∧ x + y < z ∧ x > w ∧ 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 * ¦y - 8 * x + z¦ ≤ 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 * ¦y - 8 * x + z¦ ≤ 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.
  ∀w. 5 * w + 10 * x - z ≥ y ⟶ w + 7 * x + 3 * z ≥ 2 * y"
  by ferrack

lemma "∃x::'a::linordered_field. ∀y. ∃z > y.
  ∀w. w < 13 ⟶ w + 10 * x - z ≥ y ⟶ 5 * w + 7 * x + 13 * z ≥ 2 * y"
  by ferrack

lemma "∃(x::'a::linordered_field) y z w.
  min (5 * x + 3 * z) (17 * w) + 5 * ¦y - 8 * x + z¦ ≤ 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.
  ¦y¦ ≠ ¦x¦ ∧ (∀z > max x y. ∃w. w ≠ y ∧ w ≠ z ∧ 3 * w - z ≥ x + y)"
  by ferrack

end