Proof

Proof Summary of Float.thy:723

Isabelle Statement

source: Float.thy:723 benchmark: isa/deeper/B-mesh-th0/train2k problem: problems/HOL-Library/0131_Float/prob_00723_022817.p

Lemma

lemma round_down_ge1:
  assumes x: "x ≥ 1"
  assumes prec: "p ≥ - log 2 x"
  shows "1 ≤ round_down p x"

Proof Excerpt

also have "… ≤ ⌊2 powr 0::real⌋" by simp
also have "… ≤ ⌊x * 2 powr (real_of_int p)⌋"
  unfolding of_int_le_iff
  using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
finally show ?thesis
  using prec x

Conjectures

c_0_52

ord_less_eq_real @ one_one_real @ ( round_down @ p @ x )

Axioms

c_0_0 c_0_1 c_0_2 c_0_3 c_0_4 c_0_5 c_0_6 c_0_7 c_0_8 c_0_9 c_0_10 c_0_11 c_0_12 c_0_13 c_0_14 c_0_15 c_0_16 c_0_17 c_0_18 c_0_19 c_0_20 c_0_21 c_0_22 c_0_23 c_0_24 c_0_25 c_0_26 c_0_27 c_0_28 c_0_29 c_0_30 c_0_31 c_0_32 c_0_33 c_0_34 c_0_35 c_0_36 c_0_37 c_0_38 c_0_39 c_0_40 c_0_41 c_0_42 c_0_43 c_0_44 c_0_45 c_0_46 c_0_47 c_0_48 c_0_49 c_0_50 c_0_51 c_0_53

Final Contradiction

c_0_327