Theory Bridge_Theorem

theory Bridge_Theorem
  imports Bridge_Theorem_Rev
begin

theorem (in bridge_variables) theorem_II:
  fixes b Y X g :: int
  assumes "b ≥ 0" and "Y ≥ b ∧ Y ≥ 2^8" and "X ≥ 3*b" and "g ≥ 1"
  shows "statement2 b Y X g = statement1 b Y X"
    and "statement2a b Y X g = statement1 b Y X"
  using theorem_II_1_3[of b Y X g] theorem_II_3_2[of b Y X g] theorem_II_2_1[of b Y X g] assms by argo+

(* The following theorems are for exposition only. *)

definition (in bridge_variables) bridge_relations
  where "bridge_relations k l w h x y b g Y X ≡
    is_square (D l w h g Y X * F l w h x g Y X * I l w h x y g Y X)
    ∧ is_square ((U l X Y^4*V w g Y^2-4)*J k l w g Y X^2+4)
    ∧ S l w g Y X dvd T l w h g Y X b 
    ∧ ((4*g*(C l w h g Y X)-4*g*l*Y*(J k l w g Y X))^2 < (J k l w g Y X)^2)"

theorem (in bridge_variables) bridge_theorem_simplified:
  fixes b Y X g :: int
  assumes "b ≥ 0" and "Y ≥ b" and "Y ≥ 2^8" and "X ≥ 3*b" and "g ≥ 1"
  shows "(is_power2 b ∧ Y dvd int (2 * nat X choose nat X))
        = (∃h k l w x y :: int. bridge_relations k l w h x y b g Y X
                                ∧ (h≥b)∧(k≥b)∧(l≥b)∧(w≥b)∧(x≥b)∧(y≥b))"
  unfolding bridge_relations_def J_def
  using assms theorem_II(2) statement1_def
        statement2a_def[unfolded d2a_def d2b_def d2c_def d2e_def L_def]
  by (auto simp: mult.assoc)

end