BT00WW

bertrand_hj_base_window_thirty_two_from_total

Alpha body-checked · checked-use disabled

All six roots 32 through 37 satisfy both RFC-v1 H/J base bounds.

Exact expanded PA statement

forall s e h u j g. (forall bpt_a_hj32_base bpt_e_hj32_base. exists bpt_x_hj32_base. (exists ff_b_bpt_value_hj32_base ff_c_bpt_value_hj32_base. ((forall ff_i_bpt_value_hj32_base_repeat. (exists ff_lt_bpt_value_hj32_base_repeat_bound. ff_lt_bpt_value_hj32_base_repeat_bound + S ff_i_bpt_value_hj32_base_repeat = bpt_e_hj32_base) -> (((exists ff_h_bpt_value_hj32_base_repeat_decoded. ff_h_bpt_value_hj32_base_repeat_decoded + S (bpt_a_hj32_base) = S ((S (ff_i_bpt_value_hj32_base_repeat)) * ff_c_bpt_value_hj32_base)) /\ exists ff_q_bpt_value_hj32_base_repeat_decoded. ff_b_bpt_value_hj32_base = ff_q_bpt_value_hj32_base_repeat_decoded * S ((S (ff_i_bpt_value_hj32_base_repeat)) * ff_c_bpt_value_hj32_base) + (bpt_a_hj32_base)))) /\ (exists ff_u_bpt_value_hj32_base_product ff_v_bpt_value_hj32_base_product. ((((exists ff_h_bpt_value_hj32_base_product_start. ff_h_bpt_value_hj32_base_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_start. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_start * S ((S (0)) * ff_v_bpt_value_hj32_base_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_base_product_terminal. ff_h_bpt_value_hj32_base_product_terminal + S (bpt_x_hj32_base) = S ((S (bpt_e_hj32_base)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_terminal. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_terminal * S ((S (bpt_e_hj32_base)) * ff_v_bpt_value_hj32_base_product) + (bpt_x_hj32_base))) /\ forall ff_i_bpt_value_hj32_base_product. (exists ff_lt_bpt_value_hj32_base_product_bound. ff_lt_bpt_value_hj32_base_product_bound + S ff_i_bpt_value_hj32_base_product = bpt_e_hj32_base) -> exists ff_p_bpt_value_hj32_base_product ff_r_bpt_value_hj32_base_product ff_s_bpt_value_hj32_base_product. ((((exists ff_h_bpt_value_hj32_base_product_factor. ff_h_bpt_value_hj32_base_product_factor + S (ff_p_bpt_value_hj32_base_product) = S ((S (ff_i_bpt_value_hj32_base_product)) * ff_c_bpt_value_hj32_base)) /\ exists ff_q_bpt_value_hj32_base_product_factor. ff_b_bpt_value_hj32_base = ff_q_bpt_value_hj32_base_product_factor * S ((S (ff_i_bpt_value_hj32_base_product)) * ff_c_bpt_value_hj32_base) + (ff_p_bpt_value_hj32_base_product))) /\ ((((exists ff_h_bpt_value_hj32_base_product_partial. ff_h_bpt_value_hj32_base_product_partial + S (ff_r_bpt_value_hj32_base_product) = S ((S (ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_partial. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_partial * S ((S (ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product) + (ff_r_bpt_value_hj32_base_product))) /\ ((((exists ff_h_bpt_value_hj32_base_product_successor. ff_h_bpt_value_hj32_base_product_successor + S (ff_s_bpt_value_hj32_base_product) = S ((S (S ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product)) /\ exists ff_q_bpt_value_hj32_base_product_successor. ff_u_bpt_value_hj32_base_product = ff_q_bpt_value_hj32_base_product_successor * S ((S (S ff_i_bpt_value_hj32_base_product)) * ff_v_bpt_value_hj32_base_product) + (ff_s_bpt_value_hj32_base_product))) /\ ff_s_bpt_value_hj32_base_product = ff_r_bpt_value_hj32_base_product * ff_p_bpt_value_hj32_base_product))))))))) -> (exists bqb_le_gap_hj32_base_lower. bqb_le_gap_hj32_base_lower + (32) = (s)) -> (exists bqb_le_gap_hj32_base_upper. bqb_le_gap_hj32_base_upper + (s) = (37)) -> (((exists bcs_lower_gap_hj32_base_ceiling. bcs_lower_gap_hj32_base_ceiling + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_hj32_base_ceiling. bcs_upper_gap_hj32_base_ceiling + S (6 * (e)) = (s * s) + 6)) -> (exists pa_b_hj32_base_h pa_c_hj32_base_h. ((forall pa_i_hj32_base_h_repeat. (exists pa_lt_hj32_base_h_repeat_bound. pa_lt_hj32_base_h_repeat_bound + S pa_i_hj32_base_h_repeat = 2 * s + 2) -> (((exists pa_h_hj32_base_h_repeat_decoded. pa_h_hj32_base_h_repeat_decoded + S (s + 1) = S ((S (pa_i_hj32_base_h_repeat)) * pa_c_hj32_base_h)) /\ exists pa_q_hj32_base_h_repeat_decoded. pa_b_hj32_base_h = pa_q_hj32_base_h_repeat_decoded * S ((S (pa_i_hj32_base_h_repeat)) * pa_c_hj32_base_h) + (s + 1)))) /\ (exists pa_u_hj32_base_h_product pa_v_hj32_base_h_product. ((((exists pa_h_hj32_base_h_product_start. pa_h_hj32_base_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_start. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_start * S ((S (0)) * pa_v_hj32_base_h_product) + (1))) /\ ((((exists pa_h_hj32_base_h_product_terminal. pa_h_hj32_base_h_product_terminal + S (h) = S ((S (2 * s + 2)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_terminal. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_terminal * S ((S (2 * s + 2)) * pa_v_hj32_base_h_product) + (h))) /\ forall pa_i_hj32_base_h_product. (exists pa_lt_hj32_base_h_product_bound. pa_lt_hj32_base_h_product_bound + S pa_i_hj32_base_h_product = 2 * s + 2) -> exists pa_p_hj32_base_h_product pa_r_hj32_base_h_product pa_s_hj32_base_h_product. ((((exists pa_h_hj32_base_h_product_factor. pa_h_hj32_base_h_product_factor + S (pa_p_hj32_base_h_product) = S ((S (pa_i_hj32_base_h_product)) * pa_c_hj32_base_h)) /\ exists pa_q_hj32_base_h_product_factor. pa_b_hj32_base_h = pa_q_hj32_base_h_product_factor * S ((S (pa_i_hj32_base_h_product)) * pa_c_hj32_base_h) + (pa_p_hj32_base_h_product))) /\ ((((exists pa_h_hj32_base_h_product_partial. pa_h_hj32_base_h_product_partial + S (pa_r_hj32_base_h_product) = S ((S (pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_partial. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_partial * S ((S (pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product) + (pa_r_hj32_base_h_product))) /\ ((((exists pa_h_hj32_base_h_product_successor. pa_h_hj32_base_h_product_successor + S (pa_s_hj32_base_h_product) = S ((S (S pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product)) /\ exists pa_q_hj32_base_h_product_successor. pa_u_hj32_base_h_product = pa_q_hj32_base_h_product_successor * S ((S (S pa_i_hj32_base_h_product)) * pa_v_hj32_base_h_product) + (pa_s_hj32_base_h_product))) /\ pa_s_hj32_base_h_product = pa_r_hj32_base_h_product * pa_p_hj32_base_h_product)))))))) -> (exists pa_b_hj32_base_h_bound pa_c_hj32_base_h_bound. ((forall pa_i_hj32_base_h_bound_repeat. (exists pa_lt_hj32_base_h_bound_repeat_bound. pa_lt_hj32_base_h_bound_repeat_bound + S pa_i_hj32_base_h_bound_repeat = e) -> (((exists pa_h_hj32_base_h_bound_repeat_decoded. pa_h_hj32_base_h_bound_repeat_decoded + S (4) = S ((S (pa_i_hj32_base_h_bound_repeat)) * pa_c_hj32_base_h_bound)) /\ exists pa_q_hj32_base_h_bound_repeat_decoded. pa_b_hj32_base_h_bound = pa_q_hj32_base_h_bound_repeat_decoded * S ((S (pa_i_hj32_base_h_bound_repeat)) * pa_c_hj32_base_h_bound) + (4)))) /\ (exists pa_u_hj32_base_h_bound_product pa_v_hj32_base_h_bound_product. ((((exists pa_h_hj32_base_h_bound_product_start. pa_h_hj32_base_h_bound_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_start. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_start * S ((S (0)) * pa_v_hj32_base_h_bound_product) + (1))) /\ ((((exists pa_h_hj32_base_h_bound_product_terminal. pa_h_hj32_base_h_bound_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_terminal. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_terminal * S ((S (e)) * pa_v_hj32_base_h_bound_product) + (u))) /\ forall pa_i_hj32_base_h_bound_product. (exists pa_lt_hj32_base_h_bound_product_bound. pa_lt_hj32_base_h_bound_product_bound + S pa_i_hj32_base_h_bound_product = e) -> exists pa_p_hj32_base_h_bound_product pa_r_hj32_base_h_bound_product pa_s_hj32_base_h_bound_product. ((((exists pa_h_hj32_base_h_bound_product_factor. pa_h_hj32_base_h_bound_product_factor + S (pa_p_hj32_base_h_bound_product) = S ((S (pa_i_hj32_base_h_bound_product)) * pa_c_hj32_base_h_bound)) /\ exists pa_q_hj32_base_h_bound_product_factor. pa_b_hj32_base_h_bound = pa_q_hj32_base_h_bound_product_factor * S ((S (pa_i_hj32_base_h_bound_product)) * pa_c_hj32_base_h_bound) + (pa_p_hj32_base_h_bound_product))) /\ ((((exists pa_h_hj32_base_h_bound_product_partial. pa_h_hj32_base_h_bound_product_partial + S (pa_r_hj32_base_h_bound_product) = S ((S (pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_partial. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_partial * S ((S (pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product) + (pa_r_hj32_base_h_bound_product))) /\ ((((exists pa_h_hj32_base_h_bound_product_successor. pa_h_hj32_base_h_bound_product_successor + S (pa_s_hj32_base_h_bound_product) = S ((S (S pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product)) /\ exists pa_q_hj32_base_h_bound_product_successor. pa_u_hj32_base_h_bound_product = pa_q_hj32_base_h_bound_product_successor * S ((S (S pa_i_hj32_base_h_bound_product)) * pa_v_hj32_base_h_bound_product) + (pa_s_hj32_base_h_bound_product))) /\ pa_s_hj32_base_h_bound_product = pa_r_hj32_base_h_bound_product * pa_p_hj32_base_h_bound_product)))))))) -> (exists pa_b_hj32_base_j pa_c_hj32_base_j. ((forall pa_i_hj32_base_j_repeat. (exists pa_lt_hj32_base_j_repeat_bound. pa_lt_hj32_base_j_repeat_bound + S pa_i_hj32_base_j_repeat = 12) -> (((exists pa_h_hj32_base_j_repeat_decoded. pa_h_hj32_base_j_repeat_decoded + S (s + 7) = S ((S (pa_i_hj32_base_j_repeat)) * pa_c_hj32_base_j)) /\ exists pa_q_hj32_base_j_repeat_decoded. pa_b_hj32_base_j = pa_q_hj32_base_j_repeat_decoded * S ((S (pa_i_hj32_base_j_repeat)) * pa_c_hj32_base_j) + (s + 7)))) /\ (exists pa_u_hj32_base_j_product pa_v_hj32_base_j_product. ((((exists pa_h_hj32_base_j_product_start. pa_h_hj32_base_j_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_start. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_start * S ((S (0)) * pa_v_hj32_base_j_product) + (1))) /\ ((((exists pa_h_hj32_base_j_product_terminal. pa_h_hj32_base_j_product_terminal + S (j) = S ((S (12)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_terminal. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_terminal * S ((S (12)) * pa_v_hj32_base_j_product) + (j))) /\ forall pa_i_hj32_base_j_product. (exists pa_lt_hj32_base_j_product_bound. pa_lt_hj32_base_j_product_bound + S pa_i_hj32_base_j_product = 12) -> exists pa_p_hj32_base_j_product pa_r_hj32_base_j_product pa_s_hj32_base_j_product. ((((exists pa_h_hj32_base_j_product_factor. pa_h_hj32_base_j_product_factor + S (pa_p_hj32_base_j_product) = S ((S (pa_i_hj32_base_j_product)) * pa_c_hj32_base_j)) /\ exists pa_q_hj32_base_j_product_factor. pa_b_hj32_base_j = pa_q_hj32_base_j_product_factor * S ((S (pa_i_hj32_base_j_product)) * pa_c_hj32_base_j) + (pa_p_hj32_base_j_product))) /\ ((((exists pa_h_hj32_base_j_product_partial. pa_h_hj32_base_j_product_partial + S (pa_r_hj32_base_j_product) = S ((S (pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_partial. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_partial * S ((S (pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product) + (pa_r_hj32_base_j_product))) /\ ((((exists pa_h_hj32_base_j_product_successor. pa_h_hj32_base_j_product_successor + S (pa_s_hj32_base_j_product) = S ((S (S pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product)) /\ exists pa_q_hj32_base_j_product_successor. pa_u_hj32_base_j_product = pa_q_hj32_base_j_product_successor * S ((S (S pa_i_hj32_base_j_product)) * pa_v_hj32_base_j_product) + (pa_s_hj32_base_j_product))) /\ pa_s_hj32_base_j_product = pa_r_hj32_base_j_product * pa_p_hj32_base_j_product)))))))) -> (exists pa_b_hj32_base_j_bound pa_c_hj32_base_j_bound. ((forall pa_i_hj32_base_j_bound_repeat. (exists pa_lt_hj32_base_j_bound_repeat_bound. pa_lt_hj32_base_j_bound_repeat_bound + S pa_i_hj32_base_j_bound_repeat = s + 5) -> (((exists pa_h_hj32_base_j_bound_repeat_decoded. pa_h_hj32_base_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hj32_base_j_bound_repeat)) * pa_c_hj32_base_j_bound)) /\ exists pa_q_hj32_base_j_bound_repeat_decoded. pa_b_hj32_base_j_bound = pa_q_hj32_base_j_bound_repeat_decoded * S ((S (pa_i_hj32_base_j_bound_repeat)) * pa_c_hj32_base_j_bound) + (4)))) /\ (exists pa_u_hj32_base_j_bound_product pa_v_hj32_base_j_bound_product. ((((exists pa_h_hj32_base_j_bound_product_start. pa_h_hj32_base_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_start. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_start * S ((S (0)) * pa_v_hj32_base_j_bound_product) + (1))) /\ ((((exists pa_h_hj32_base_j_bound_product_terminal. pa_h_hj32_base_j_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_terminal. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_terminal * S ((S (s + 5)) * pa_v_hj32_base_j_bound_product) + (g))) /\ forall pa_i_hj32_base_j_bound_product. (exists pa_lt_hj32_base_j_bound_product_bound. pa_lt_hj32_base_j_bound_product_bound + S pa_i_hj32_base_j_bound_product = s + 5) -> exists pa_p_hj32_base_j_bound_product pa_r_hj32_base_j_bound_product pa_s_hj32_base_j_bound_product. ((((exists pa_h_hj32_base_j_bound_product_factor. pa_h_hj32_base_j_bound_product_factor + S (pa_p_hj32_base_j_bound_product) = S ((S (pa_i_hj32_base_j_bound_product)) * pa_c_hj32_base_j_bound)) /\ exists pa_q_hj32_base_j_bound_product_factor. pa_b_hj32_base_j_bound = pa_q_hj32_base_j_bound_product_factor * S ((S (pa_i_hj32_base_j_bound_product)) * pa_c_hj32_base_j_bound) + (pa_p_hj32_base_j_bound_product))) /\ ((((exists pa_h_hj32_base_j_bound_product_partial. pa_h_hj32_base_j_bound_product_partial + S (pa_r_hj32_base_j_bound_product) = S ((S (pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_partial. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_partial * S ((S (pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product) + (pa_r_hj32_base_j_bound_product))) /\ ((((exists pa_h_hj32_base_j_bound_product_successor. pa_h_hj32_base_j_bound_product_successor + S (pa_s_hj32_base_j_bound_product) = S ((S (S pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product)) /\ exists pa_q_hj32_base_j_bound_product_successor. pa_u_hj32_base_j_bound_product = pa_q_hj32_base_j_bound_product_successor * S ((S (S pa_i_hj32_base_j_bound_product)) * pa_v_hj32_base_j_bound_product) + (pa_s_hj32_base_j_bound_product))) /\ pa_s_hj32_base_j_bound_product = pa_r_hj32_base_j_bound_product * pa_p_hj32_base_j_bound_product)))))))) -> ((exists bqb_le_gap_hj32_base_h_result. bqb_le_gap_hj32_base_h_result + (h) = (u)) /\ (exists bqb_le_gap_hj32_base_j_result. bqb_le_gap_hj32_base_j_result + (j) = (g)))

Structural proof guide

All six roots 32 through 37 satisfy both RFC-v1 H/J base bounds.

Direct prerequisites: le_eq_or_lt, le_of_succ_le_succ, le_antisymm, bertrand_h_root_32_from_total, bertrand_h_root_33_from_total, bertrand_h_root_34_from_total, bertrand_h_root_35_from_total, bertrand_h_root_36_from_total, bertrand_h_root_37_from_total, bertrand_j_base_thirty_two_window_from_total. The authored body proceeds by case analysis (5), intermediate claims (30), equality transport (60).

Proof neighborhood

Direct dependencies

BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT000J le_antisymm BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total

Direct dependents

BT00X2 bertrand_hj_six_block_iterate_from_total

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro s
  2. 0002intro e
  3. 0003intro h
  4. 0004intro u
  5. 0005intro j
  6. 0006intro g
  7. 0007intro htotal
  8. 0008intro hlower
  9. 0009intro hupper
  10. 0010intro hceiling
  11. 0011intro hh
  12. 0012intro hu
  13. 0013intro hj
  14. 0014intro hg
  15. 0015have hjresult : exists bqb_le_gap_hj32_capstone_j_result. bqb_le_gap_hj32_capstone_j_result + (j) = (g)
  16. 0016specialize bertrand_j_base_thirty_two_window_from_total s
  17. 0017specialize bertrand_j_base_thirty_two_window_from_total j
  18. 0018specialize bertrand_j_base_thirty_two_window_from_total g
  19. 0019apply bertrand_j_base_thirty_two_window_from_total
  20. 0020exact htotal
  21. 0021exact hlower
  22. 0022exact hupper
  23. 0023exact hj
  24. 0024exact hg
  25. 0025have hcap_cases_37 : s = 37 \/ exists bqb_le_gap_hj32_capstone_lt_37. bqb_le_gap_hj32_capstone_lt_37 + (S s) = (37)
  26. 0026specialize le_eq_or_lt s
  27. 0027specialize le_eq_or_lt 37
  28. 0028apply le_eq_or_lt
  29. 0029exact hupper
  30. 0030cases hcap_cases_37
  31. 0031have hcap_37_ceiling : ((exists bcs_lower_gap_hj32_capstone_37_ceiling. bcs_lower_gap_hj32_capstone_37_ceiling + (37 * 37) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_37_ceiling. bcs_upper_gap_hj32_capstone_37_ceiling + S (6 * (e)) = (37 * 37) + 6)
  32. 0032rewrite <- hcap_cases_37_left
  33. 0033rewrite <- hcap_cases_37_left
  34. 0034rewrite <- hcap_cases_37_left
  35. 0035rewrite <- hcap_cases_37_left
  36. 0036exact hceiling
  37. 0037have hcap_37_power : exists pa_b_hj32_capstone_37_h pa_c_hj32_capstone_37_h. ((forall pa_i_hj32_capstone_37_h_repeat. (exists pa_lt_hj32_capstone_37_h_repeat_bound. pa_lt_hj32_capstone_37_h_repeat_bound + S pa_i_hj32_capstone_37_h_repeat = 2 * 37 + 2) -> (((exists pa_h_hj32_capstone_37_h_repeat_decoded. pa_h_hj32_capstone_37_h_repeat_decoded + S (37 + 1) = S ((S (pa_i_hj32_capstone_37_h_repeat)) * pa_c_hj32_capstone_37_h)) /\ exists pa_q_hj32_capstone_37_h_repeat_decoded. pa_b_hj32_capstone_37_h = pa_q_hj32_capstone_37_h_repeat_decoded * S ((S (pa_i_hj32_capstone_37_h_repeat)) * pa_c_hj32_capstone_37_h) + (37 + 1)))) /\ (exists pa_u_hj32_capstone_37_h_product pa_v_hj32_capstone_37_h_product. ((((exists pa_h_hj32_capstone_37_h_product_start. pa_h_hj32_capstone_37_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_start. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_start * S ((S (0)) * pa_v_hj32_capstone_37_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_37_h_product_terminal. pa_h_hj32_capstone_37_h_product_terminal + S (h) = S ((S (2 * 37 + 2)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_terminal. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_terminal * S ((S (2 * 37 + 2)) * pa_v_hj32_capstone_37_h_product) + (h))) /\ forall pa_i_hj32_capstone_37_h_product. (exists pa_lt_hj32_capstone_37_h_product_bound. pa_lt_hj32_capstone_37_h_product_bound + S pa_i_hj32_capstone_37_h_product = 2 * 37 + 2) -> exists pa_p_hj32_capstone_37_h_product pa_r_hj32_capstone_37_h_product pa_s_hj32_capstone_37_h_product. ((((exists pa_h_hj32_capstone_37_h_product_factor. pa_h_hj32_capstone_37_h_product_factor + S (pa_p_hj32_capstone_37_h_product) = S ((S (pa_i_hj32_capstone_37_h_product)) * pa_c_hj32_capstone_37_h)) /\ exists pa_q_hj32_capstone_37_h_product_factor. pa_b_hj32_capstone_37_h = pa_q_hj32_capstone_37_h_product_factor * S ((S (pa_i_hj32_capstone_37_h_product)) * pa_c_hj32_capstone_37_h) + (pa_p_hj32_capstone_37_h_product))) /\ ((((exists pa_h_hj32_capstone_37_h_product_partial. pa_h_hj32_capstone_37_h_product_partial + S (pa_r_hj32_capstone_37_h_product) = S ((S (pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_partial. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_partial * S ((S (pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product) + (pa_r_hj32_capstone_37_h_product))) /\ ((((exists pa_h_hj32_capstone_37_h_product_successor. pa_h_hj32_capstone_37_h_product_successor + S (pa_s_hj32_capstone_37_h_product) = S ((S (S pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product)) /\ exists pa_q_hj32_capstone_37_h_product_successor. pa_u_hj32_capstone_37_h_product = pa_q_hj32_capstone_37_h_product_successor * S ((S (S pa_i_hj32_capstone_37_h_product)) * pa_v_hj32_capstone_37_h_product) + (pa_s_hj32_capstone_37_h_product))) /\ pa_s_hj32_capstone_37_h_product = pa_r_hj32_capstone_37_h_product * pa_p_hj32_capstone_37_h_product)))))))
  38. 0038rewrite <- hcap_cases_37_left
  39. 0039rewrite <- hcap_cases_37_left
  40. 0040rewrite <- hcap_cases_37_left
  41. 0041rewrite <- hcap_cases_37_left
  42. 0042rewrite <- hcap_cases_37_left
  43. 0043rewrite <- hcap_cases_37_left
  44. 0044exact hh
  45. 0045have hcap_37_result : exists bqb_le_gap_hj32_capstone_37_result. bqb_le_gap_hj32_capstone_37_result + (h) = (u)
  46. 0046specialize bertrand_h_root_37_from_total e
  47. 0047specialize bertrand_h_root_37_from_total h
  48. 0048specialize bertrand_h_root_37_from_total u
  49. 0049apply bertrand_h_root_37_from_total
  50. 0050exact htotal
  51. 0051exact hcap_37_ceiling
  52. 0052exact hcap_37_power
  53. 0053exact hu
  54. 0054split
  55. 0055exact hcap_37_result
  56. 0056exact hjresult
  57. 0057have hcap_le_36 : exists bqb_le_gap_hj32_capstone_le_36. bqb_le_gap_hj32_capstone_le_36 + (s) = (36)
  58. 0058specialize le_of_succ_le_succ s
  59. 0059specialize le_of_succ_le_succ 36
  60. 0060apply le_of_succ_le_succ
  61. 0061exact hcap_cases_37_right
  62. 0062have hcap_cases_36 : s = 36 \/ exists bqb_le_gap_hj32_capstone_lt_36. bqb_le_gap_hj32_capstone_lt_36 + (S s) = (36)
  63. 0063specialize le_eq_or_lt s
  64. 0064specialize le_eq_or_lt 36
  65. 0065apply le_eq_or_lt
  66. 0066exact hcap_le_36
  67. 0067cases hcap_cases_36
  68. 0068have hcap_36_ceiling : ((exists bcs_lower_gap_hj32_capstone_36_ceiling. bcs_lower_gap_hj32_capstone_36_ceiling + (36 * 36) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_36_ceiling. bcs_upper_gap_hj32_capstone_36_ceiling + S (6 * (e)) = (36 * 36) + 6)
  69. 0069rewrite <- hcap_cases_36_left
  70. 0070rewrite <- hcap_cases_36_left
  71. 0071rewrite <- hcap_cases_36_left
  72. 0072rewrite <- hcap_cases_36_left
  73. 0073exact hceiling
  74. 0074have hcap_36_power : exists pa_b_hj32_capstone_36_h pa_c_hj32_capstone_36_h. ((forall pa_i_hj32_capstone_36_h_repeat. (exists pa_lt_hj32_capstone_36_h_repeat_bound. pa_lt_hj32_capstone_36_h_repeat_bound + S pa_i_hj32_capstone_36_h_repeat = 2 * 36 + 2) -> (((exists pa_h_hj32_capstone_36_h_repeat_decoded. pa_h_hj32_capstone_36_h_repeat_decoded + S (36 + 1) = S ((S (pa_i_hj32_capstone_36_h_repeat)) * pa_c_hj32_capstone_36_h)) /\ exists pa_q_hj32_capstone_36_h_repeat_decoded. pa_b_hj32_capstone_36_h = pa_q_hj32_capstone_36_h_repeat_decoded * S ((S (pa_i_hj32_capstone_36_h_repeat)) * pa_c_hj32_capstone_36_h) + (36 + 1)))) /\ (exists pa_u_hj32_capstone_36_h_product pa_v_hj32_capstone_36_h_product. ((((exists pa_h_hj32_capstone_36_h_product_start. pa_h_hj32_capstone_36_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_start. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_start * S ((S (0)) * pa_v_hj32_capstone_36_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_36_h_product_terminal. pa_h_hj32_capstone_36_h_product_terminal + S (h) = S ((S (2 * 36 + 2)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_terminal. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_terminal * S ((S (2 * 36 + 2)) * pa_v_hj32_capstone_36_h_product) + (h))) /\ forall pa_i_hj32_capstone_36_h_product. (exists pa_lt_hj32_capstone_36_h_product_bound. pa_lt_hj32_capstone_36_h_product_bound + S pa_i_hj32_capstone_36_h_product = 2 * 36 + 2) -> exists pa_p_hj32_capstone_36_h_product pa_r_hj32_capstone_36_h_product pa_s_hj32_capstone_36_h_product. ((((exists pa_h_hj32_capstone_36_h_product_factor. pa_h_hj32_capstone_36_h_product_factor + S (pa_p_hj32_capstone_36_h_product) = S ((S (pa_i_hj32_capstone_36_h_product)) * pa_c_hj32_capstone_36_h)) /\ exists pa_q_hj32_capstone_36_h_product_factor. pa_b_hj32_capstone_36_h = pa_q_hj32_capstone_36_h_product_factor * S ((S (pa_i_hj32_capstone_36_h_product)) * pa_c_hj32_capstone_36_h) + (pa_p_hj32_capstone_36_h_product))) /\ ((((exists pa_h_hj32_capstone_36_h_product_partial. pa_h_hj32_capstone_36_h_product_partial + S (pa_r_hj32_capstone_36_h_product) = S ((S (pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_partial. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_partial * S ((S (pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product) + (pa_r_hj32_capstone_36_h_product))) /\ ((((exists pa_h_hj32_capstone_36_h_product_successor. pa_h_hj32_capstone_36_h_product_successor + S (pa_s_hj32_capstone_36_h_product) = S ((S (S pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product)) /\ exists pa_q_hj32_capstone_36_h_product_successor. pa_u_hj32_capstone_36_h_product = pa_q_hj32_capstone_36_h_product_successor * S ((S (S pa_i_hj32_capstone_36_h_product)) * pa_v_hj32_capstone_36_h_product) + (pa_s_hj32_capstone_36_h_product))) /\ pa_s_hj32_capstone_36_h_product = pa_r_hj32_capstone_36_h_product * pa_p_hj32_capstone_36_h_product)))))))
  75. 0075rewrite <- hcap_cases_36_left
  76. 0076rewrite <- hcap_cases_36_left
  77. 0077rewrite <- hcap_cases_36_left
  78. 0078rewrite <- hcap_cases_36_left
  79. 0079rewrite <- hcap_cases_36_left
  80. 0080rewrite <- hcap_cases_36_left
  81. 0081exact hh
  82. 0082have hcap_36_result : exists bqb_le_gap_hj32_capstone_36_result. bqb_le_gap_hj32_capstone_36_result + (h) = (u)
  83. 0083specialize bertrand_h_root_36_from_total e
  84. 0084specialize bertrand_h_root_36_from_total h
  85. 0085specialize bertrand_h_root_36_from_total u
  86. 0086apply bertrand_h_root_36_from_total
  87. 0087exact htotal
  88. 0088exact hcap_36_ceiling
  89. 0089exact hcap_36_power
  90. 0090exact hu
  91. 0091split
  92. 0092exact hcap_36_result
  93. 0093exact hjresult
  94. 0094have hcap_le_35 : exists bqb_le_gap_hj32_capstone_le_35. bqb_le_gap_hj32_capstone_le_35 + (s) = (35)
  95. 0095specialize le_of_succ_le_succ s
  96. 0096specialize le_of_succ_le_succ 35
  97. 0097apply le_of_succ_le_succ
  98. 0098exact hcap_cases_36_right
  99. 0099have hcap_cases_35 : s = 35 \/ exists bqb_le_gap_hj32_capstone_lt_35. bqb_le_gap_hj32_capstone_lt_35 + (S s) = (35)
  100. 0100specialize le_eq_or_lt s
  101. 0101specialize le_eq_or_lt 35
  102. 0102apply le_eq_or_lt
  103. 0103exact hcap_le_35
  104. 0104cases hcap_cases_35
  105. 0105have hcap_35_ceiling : ((exists bcs_lower_gap_hj32_capstone_35_ceiling. bcs_lower_gap_hj32_capstone_35_ceiling + (35 * 35) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_35_ceiling. bcs_upper_gap_hj32_capstone_35_ceiling + S (6 * (e)) = (35 * 35) + 6)
  106. 0106rewrite <- hcap_cases_35_left
  107. 0107rewrite <- hcap_cases_35_left
  108. 0108rewrite <- hcap_cases_35_left
  109. 0109rewrite <- hcap_cases_35_left
  110. 0110exact hceiling
  111. 0111have hcap_35_power : exists pa_b_hj32_capstone_35_h pa_c_hj32_capstone_35_h. ((forall pa_i_hj32_capstone_35_h_repeat. (exists pa_lt_hj32_capstone_35_h_repeat_bound. pa_lt_hj32_capstone_35_h_repeat_bound + S pa_i_hj32_capstone_35_h_repeat = 2 * 35 + 2) -> (((exists pa_h_hj32_capstone_35_h_repeat_decoded. pa_h_hj32_capstone_35_h_repeat_decoded + S (35 + 1) = S ((S (pa_i_hj32_capstone_35_h_repeat)) * pa_c_hj32_capstone_35_h)) /\ exists pa_q_hj32_capstone_35_h_repeat_decoded. pa_b_hj32_capstone_35_h = pa_q_hj32_capstone_35_h_repeat_decoded * S ((S (pa_i_hj32_capstone_35_h_repeat)) * pa_c_hj32_capstone_35_h) + (35 + 1)))) /\ (exists pa_u_hj32_capstone_35_h_product pa_v_hj32_capstone_35_h_product. ((((exists pa_h_hj32_capstone_35_h_product_start. pa_h_hj32_capstone_35_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_start. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_start * S ((S (0)) * pa_v_hj32_capstone_35_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_35_h_product_terminal. pa_h_hj32_capstone_35_h_product_terminal + S (h) = S ((S (2 * 35 + 2)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_terminal. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_terminal * S ((S (2 * 35 + 2)) * pa_v_hj32_capstone_35_h_product) + (h))) /\ forall pa_i_hj32_capstone_35_h_product. (exists pa_lt_hj32_capstone_35_h_product_bound. pa_lt_hj32_capstone_35_h_product_bound + S pa_i_hj32_capstone_35_h_product = 2 * 35 + 2) -> exists pa_p_hj32_capstone_35_h_product pa_r_hj32_capstone_35_h_product pa_s_hj32_capstone_35_h_product. ((((exists pa_h_hj32_capstone_35_h_product_factor. pa_h_hj32_capstone_35_h_product_factor + S (pa_p_hj32_capstone_35_h_product) = S ((S (pa_i_hj32_capstone_35_h_product)) * pa_c_hj32_capstone_35_h)) /\ exists pa_q_hj32_capstone_35_h_product_factor. pa_b_hj32_capstone_35_h = pa_q_hj32_capstone_35_h_product_factor * S ((S (pa_i_hj32_capstone_35_h_product)) * pa_c_hj32_capstone_35_h) + (pa_p_hj32_capstone_35_h_product))) /\ ((((exists pa_h_hj32_capstone_35_h_product_partial. pa_h_hj32_capstone_35_h_product_partial + S (pa_r_hj32_capstone_35_h_product) = S ((S (pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_partial. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_partial * S ((S (pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product) + (pa_r_hj32_capstone_35_h_product))) /\ ((((exists pa_h_hj32_capstone_35_h_product_successor. pa_h_hj32_capstone_35_h_product_successor + S (pa_s_hj32_capstone_35_h_product) = S ((S (S pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product)) /\ exists pa_q_hj32_capstone_35_h_product_successor. pa_u_hj32_capstone_35_h_product = pa_q_hj32_capstone_35_h_product_successor * S ((S (S pa_i_hj32_capstone_35_h_product)) * pa_v_hj32_capstone_35_h_product) + (pa_s_hj32_capstone_35_h_product))) /\ pa_s_hj32_capstone_35_h_product = pa_r_hj32_capstone_35_h_product * pa_p_hj32_capstone_35_h_product)))))))
  112. 0112rewrite <- hcap_cases_35_left
  113. 0113rewrite <- hcap_cases_35_left
  114. 0114rewrite <- hcap_cases_35_left
  115. 0115rewrite <- hcap_cases_35_left
  116. 0116rewrite <- hcap_cases_35_left
  117. 0117rewrite <- hcap_cases_35_left
  118. 0118exact hh
  119. 0119have hcap_35_result : exists bqb_le_gap_hj32_capstone_35_result. bqb_le_gap_hj32_capstone_35_result + (h) = (u)
  120. 0120specialize bertrand_h_root_35_from_total e
  121. 0121specialize bertrand_h_root_35_from_total h
  122. 0122specialize bertrand_h_root_35_from_total u
  123. 0123apply bertrand_h_root_35_from_total
  124. 0124exact htotal
  125. 0125exact hcap_35_ceiling
  126. 0126exact hcap_35_power
  127. 0127exact hu
  128. 0128split
  129. 0129exact hcap_35_result
  130. 0130exact hjresult
  131. 0131have hcap_le_34 : exists bqb_le_gap_hj32_capstone_le_34. bqb_le_gap_hj32_capstone_le_34 + (s) = (34)
  132. 0132specialize le_of_succ_le_succ s
  133. 0133specialize le_of_succ_le_succ 34
  134. 0134apply le_of_succ_le_succ
  135. 0135exact hcap_cases_35_right
  136. 0136have hcap_cases_34 : s = 34 \/ exists bqb_le_gap_hj32_capstone_lt_34. bqb_le_gap_hj32_capstone_lt_34 + (S s) = (34)
  137. 0137specialize le_eq_or_lt s
  138. 0138specialize le_eq_or_lt 34
  139. 0139apply le_eq_or_lt
  140. 0140exact hcap_le_34
  141. 0141cases hcap_cases_34
  142. 0142have hcap_34_ceiling : ((exists bcs_lower_gap_hj32_capstone_34_ceiling. bcs_lower_gap_hj32_capstone_34_ceiling + (34 * 34) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_34_ceiling. bcs_upper_gap_hj32_capstone_34_ceiling + S (6 * (e)) = (34 * 34) + 6)
  143. 0143rewrite <- hcap_cases_34_left
  144. 0144rewrite <- hcap_cases_34_left
  145. 0145rewrite <- hcap_cases_34_left
  146. 0146rewrite <- hcap_cases_34_left
  147. 0147exact hceiling
  148. 0148have hcap_34_power : exists pa_b_hj32_capstone_34_h pa_c_hj32_capstone_34_h. ((forall pa_i_hj32_capstone_34_h_repeat. (exists pa_lt_hj32_capstone_34_h_repeat_bound. pa_lt_hj32_capstone_34_h_repeat_bound + S pa_i_hj32_capstone_34_h_repeat = 2 * 34 + 2) -> (((exists pa_h_hj32_capstone_34_h_repeat_decoded. pa_h_hj32_capstone_34_h_repeat_decoded + S (34 + 1) = S ((S (pa_i_hj32_capstone_34_h_repeat)) * pa_c_hj32_capstone_34_h)) /\ exists pa_q_hj32_capstone_34_h_repeat_decoded. pa_b_hj32_capstone_34_h = pa_q_hj32_capstone_34_h_repeat_decoded * S ((S (pa_i_hj32_capstone_34_h_repeat)) * pa_c_hj32_capstone_34_h) + (34 + 1)))) /\ (exists pa_u_hj32_capstone_34_h_product pa_v_hj32_capstone_34_h_product. ((((exists pa_h_hj32_capstone_34_h_product_start. pa_h_hj32_capstone_34_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_start. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_start * S ((S (0)) * pa_v_hj32_capstone_34_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_34_h_product_terminal. pa_h_hj32_capstone_34_h_product_terminal + S (h) = S ((S (2 * 34 + 2)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_terminal. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_terminal * S ((S (2 * 34 + 2)) * pa_v_hj32_capstone_34_h_product) + (h))) /\ forall pa_i_hj32_capstone_34_h_product. (exists pa_lt_hj32_capstone_34_h_product_bound. pa_lt_hj32_capstone_34_h_product_bound + S pa_i_hj32_capstone_34_h_product = 2 * 34 + 2) -> exists pa_p_hj32_capstone_34_h_product pa_r_hj32_capstone_34_h_product pa_s_hj32_capstone_34_h_product. ((((exists pa_h_hj32_capstone_34_h_product_factor. pa_h_hj32_capstone_34_h_product_factor + S (pa_p_hj32_capstone_34_h_product) = S ((S (pa_i_hj32_capstone_34_h_product)) * pa_c_hj32_capstone_34_h)) /\ exists pa_q_hj32_capstone_34_h_product_factor. pa_b_hj32_capstone_34_h = pa_q_hj32_capstone_34_h_product_factor * S ((S (pa_i_hj32_capstone_34_h_product)) * pa_c_hj32_capstone_34_h) + (pa_p_hj32_capstone_34_h_product))) /\ ((((exists pa_h_hj32_capstone_34_h_product_partial. pa_h_hj32_capstone_34_h_product_partial + S (pa_r_hj32_capstone_34_h_product) = S ((S (pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_partial. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_partial * S ((S (pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product) + (pa_r_hj32_capstone_34_h_product))) /\ ((((exists pa_h_hj32_capstone_34_h_product_successor. pa_h_hj32_capstone_34_h_product_successor + S (pa_s_hj32_capstone_34_h_product) = S ((S (S pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product)) /\ exists pa_q_hj32_capstone_34_h_product_successor. pa_u_hj32_capstone_34_h_product = pa_q_hj32_capstone_34_h_product_successor * S ((S (S pa_i_hj32_capstone_34_h_product)) * pa_v_hj32_capstone_34_h_product) + (pa_s_hj32_capstone_34_h_product))) /\ pa_s_hj32_capstone_34_h_product = pa_r_hj32_capstone_34_h_product * pa_p_hj32_capstone_34_h_product)))))))
  149. 0149rewrite <- hcap_cases_34_left
  150. 0150rewrite <- hcap_cases_34_left
  151. 0151rewrite <- hcap_cases_34_left
  152. 0152rewrite <- hcap_cases_34_left
  153. 0153rewrite <- hcap_cases_34_left
  154. 0154rewrite <- hcap_cases_34_left
  155. 0155exact hh
  156. 0156have hcap_34_result : exists bqb_le_gap_hj32_capstone_34_result. bqb_le_gap_hj32_capstone_34_result + (h) = (u)
  157. 0157specialize bertrand_h_root_34_from_total e
  158. 0158specialize bertrand_h_root_34_from_total h
  159. 0159specialize bertrand_h_root_34_from_total u
  160. 0160apply bertrand_h_root_34_from_total
  161. 0161exact htotal
  162. 0162exact hcap_34_ceiling
  163. 0163exact hcap_34_power
  164. 0164exact hu
  165. 0165split
  166. 0166exact hcap_34_result
  167. 0167exact hjresult
  168. 0168have hcap_le_33 : exists bqb_le_gap_hj32_capstone_le_33. bqb_le_gap_hj32_capstone_le_33 + (s) = (33)
  169. 0169specialize le_of_succ_le_succ s
  170. 0170specialize le_of_succ_le_succ 33
  171. 0171apply le_of_succ_le_succ
  172. 0172exact hcap_cases_34_right
  173. 0173have hcap_cases_33 : s = 33 \/ exists bqb_le_gap_hj32_capstone_lt_33. bqb_le_gap_hj32_capstone_lt_33 + (S s) = (33)
  174. 0174specialize le_eq_or_lt s
  175. 0175specialize le_eq_or_lt 33
  176. 0176apply le_eq_or_lt
  177. 0177exact hcap_le_33
  178. 0178cases hcap_cases_33
  179. 0179have hcap_33_ceiling : ((exists bcs_lower_gap_hj32_capstone_33_ceiling. bcs_lower_gap_hj32_capstone_33_ceiling + (33 * 33) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_33_ceiling. bcs_upper_gap_hj32_capstone_33_ceiling + S (6 * (e)) = (33 * 33) + 6)
  180. 0180rewrite <- hcap_cases_33_left
  181. 0181rewrite <- hcap_cases_33_left
  182. 0182rewrite <- hcap_cases_33_left
  183. 0183rewrite <- hcap_cases_33_left
  184. 0184exact hceiling
  185. 0185have hcap_33_power : exists pa_b_hj32_capstone_33_h pa_c_hj32_capstone_33_h. ((forall pa_i_hj32_capstone_33_h_repeat. (exists pa_lt_hj32_capstone_33_h_repeat_bound. pa_lt_hj32_capstone_33_h_repeat_bound + S pa_i_hj32_capstone_33_h_repeat = 2 * 33 + 2) -> (((exists pa_h_hj32_capstone_33_h_repeat_decoded. pa_h_hj32_capstone_33_h_repeat_decoded + S (33 + 1) = S ((S (pa_i_hj32_capstone_33_h_repeat)) * pa_c_hj32_capstone_33_h)) /\ exists pa_q_hj32_capstone_33_h_repeat_decoded. pa_b_hj32_capstone_33_h = pa_q_hj32_capstone_33_h_repeat_decoded * S ((S (pa_i_hj32_capstone_33_h_repeat)) * pa_c_hj32_capstone_33_h) + (33 + 1)))) /\ (exists pa_u_hj32_capstone_33_h_product pa_v_hj32_capstone_33_h_product. ((((exists pa_h_hj32_capstone_33_h_product_start. pa_h_hj32_capstone_33_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_start. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_start * S ((S (0)) * pa_v_hj32_capstone_33_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_33_h_product_terminal. pa_h_hj32_capstone_33_h_product_terminal + S (h) = S ((S (2 * 33 + 2)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_terminal. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_terminal * S ((S (2 * 33 + 2)) * pa_v_hj32_capstone_33_h_product) + (h))) /\ forall pa_i_hj32_capstone_33_h_product. (exists pa_lt_hj32_capstone_33_h_product_bound. pa_lt_hj32_capstone_33_h_product_bound + S pa_i_hj32_capstone_33_h_product = 2 * 33 + 2) -> exists pa_p_hj32_capstone_33_h_product pa_r_hj32_capstone_33_h_product pa_s_hj32_capstone_33_h_product. ((((exists pa_h_hj32_capstone_33_h_product_factor. pa_h_hj32_capstone_33_h_product_factor + S (pa_p_hj32_capstone_33_h_product) = S ((S (pa_i_hj32_capstone_33_h_product)) * pa_c_hj32_capstone_33_h)) /\ exists pa_q_hj32_capstone_33_h_product_factor. pa_b_hj32_capstone_33_h = pa_q_hj32_capstone_33_h_product_factor * S ((S (pa_i_hj32_capstone_33_h_product)) * pa_c_hj32_capstone_33_h) + (pa_p_hj32_capstone_33_h_product))) /\ ((((exists pa_h_hj32_capstone_33_h_product_partial. pa_h_hj32_capstone_33_h_product_partial + S (pa_r_hj32_capstone_33_h_product) = S ((S (pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_partial. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_partial * S ((S (pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product) + (pa_r_hj32_capstone_33_h_product))) /\ ((((exists pa_h_hj32_capstone_33_h_product_successor. pa_h_hj32_capstone_33_h_product_successor + S (pa_s_hj32_capstone_33_h_product) = S ((S (S pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product)) /\ exists pa_q_hj32_capstone_33_h_product_successor. pa_u_hj32_capstone_33_h_product = pa_q_hj32_capstone_33_h_product_successor * S ((S (S pa_i_hj32_capstone_33_h_product)) * pa_v_hj32_capstone_33_h_product) + (pa_s_hj32_capstone_33_h_product))) /\ pa_s_hj32_capstone_33_h_product = pa_r_hj32_capstone_33_h_product * pa_p_hj32_capstone_33_h_product)))))))
  186. 0186rewrite <- hcap_cases_33_left
  187. 0187rewrite <- hcap_cases_33_left
  188. 0188rewrite <- hcap_cases_33_left
  189. 0189rewrite <- hcap_cases_33_left
  190. 0190rewrite <- hcap_cases_33_left
  191. 0191rewrite <- hcap_cases_33_left
  192. 0192exact hh
  193. 0193have hcap_33_result : exists bqb_le_gap_hj32_capstone_33_result. bqb_le_gap_hj32_capstone_33_result + (h) = (u)
  194. 0194specialize bertrand_h_root_33_from_total e
  195. 0195specialize bertrand_h_root_33_from_total h
  196. 0196specialize bertrand_h_root_33_from_total u
  197. 0197apply bertrand_h_root_33_from_total
  198. 0198exact htotal
  199. 0199exact hcap_33_ceiling
  200. 0200exact hcap_33_power
  201. 0201exact hu
  202. 0202split
  203. 0203exact hcap_33_result
  204. 0204exact hjresult
  205. 0205have hcap_le_32 : exists bqb_le_gap_hj32_capstone_le_32. bqb_le_gap_hj32_capstone_le_32 + (s) = (32)
  206. 0206specialize le_of_succ_le_succ s
  207. 0207specialize le_of_succ_le_succ 32
  208. 0208apply le_of_succ_le_succ
  209. 0209exact hcap_cases_33_right
  210. 0210have hcap_eq_32 : s = 32
  211. 0211specialize le_antisymm s
  212. 0212specialize le_antisymm 32
  213. 0213apply le_antisymm
  214. 0214exact hcap_le_32
  215. 0215exact hlower
  216. 0216have hcap_32_ceiling : ((exists bcs_lower_gap_hj32_capstone_32_ceiling. bcs_lower_gap_hj32_capstone_32_ceiling + (32 * 32) = 6 * (e)) /\ exists bcs_upper_gap_hj32_capstone_32_ceiling. bcs_upper_gap_hj32_capstone_32_ceiling + S (6 * (e)) = (32 * 32) + 6)
  217. 0217rewrite <- hcap_eq_32
  218. 0218rewrite <- hcap_eq_32
  219. 0219rewrite <- hcap_eq_32
  220. 0220rewrite <- hcap_eq_32
  221. 0221exact hceiling
  222. 0222have hcap_32_power : exists pa_b_hj32_capstone_32_h pa_c_hj32_capstone_32_h. ((forall pa_i_hj32_capstone_32_h_repeat. (exists pa_lt_hj32_capstone_32_h_repeat_bound. pa_lt_hj32_capstone_32_h_repeat_bound + S pa_i_hj32_capstone_32_h_repeat = 2 * 32 + 2) -> (((exists pa_h_hj32_capstone_32_h_repeat_decoded. pa_h_hj32_capstone_32_h_repeat_decoded + S (32 + 1) = S ((S (pa_i_hj32_capstone_32_h_repeat)) * pa_c_hj32_capstone_32_h)) /\ exists pa_q_hj32_capstone_32_h_repeat_decoded. pa_b_hj32_capstone_32_h = pa_q_hj32_capstone_32_h_repeat_decoded * S ((S (pa_i_hj32_capstone_32_h_repeat)) * pa_c_hj32_capstone_32_h) + (32 + 1)))) /\ (exists pa_u_hj32_capstone_32_h_product pa_v_hj32_capstone_32_h_product. ((((exists pa_h_hj32_capstone_32_h_product_start. pa_h_hj32_capstone_32_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_start. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_start * S ((S (0)) * pa_v_hj32_capstone_32_h_product) + (1))) /\ ((((exists pa_h_hj32_capstone_32_h_product_terminal. pa_h_hj32_capstone_32_h_product_terminal + S (h) = S ((S (2 * 32 + 2)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_terminal. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_terminal * S ((S (2 * 32 + 2)) * pa_v_hj32_capstone_32_h_product) + (h))) /\ forall pa_i_hj32_capstone_32_h_product. (exists pa_lt_hj32_capstone_32_h_product_bound. pa_lt_hj32_capstone_32_h_product_bound + S pa_i_hj32_capstone_32_h_product = 2 * 32 + 2) -> exists pa_p_hj32_capstone_32_h_product pa_r_hj32_capstone_32_h_product pa_s_hj32_capstone_32_h_product. ((((exists pa_h_hj32_capstone_32_h_product_factor. pa_h_hj32_capstone_32_h_product_factor + S (pa_p_hj32_capstone_32_h_product) = S ((S (pa_i_hj32_capstone_32_h_product)) * pa_c_hj32_capstone_32_h)) /\ exists pa_q_hj32_capstone_32_h_product_factor. pa_b_hj32_capstone_32_h = pa_q_hj32_capstone_32_h_product_factor * S ((S (pa_i_hj32_capstone_32_h_product)) * pa_c_hj32_capstone_32_h) + (pa_p_hj32_capstone_32_h_product))) /\ ((((exists pa_h_hj32_capstone_32_h_product_partial. pa_h_hj32_capstone_32_h_product_partial + S (pa_r_hj32_capstone_32_h_product) = S ((S (pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_partial. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_partial * S ((S (pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product) + (pa_r_hj32_capstone_32_h_product))) /\ ((((exists pa_h_hj32_capstone_32_h_product_successor. pa_h_hj32_capstone_32_h_product_successor + S (pa_s_hj32_capstone_32_h_product) = S ((S (S pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product)) /\ exists pa_q_hj32_capstone_32_h_product_successor. pa_u_hj32_capstone_32_h_product = pa_q_hj32_capstone_32_h_product_successor * S ((S (S pa_i_hj32_capstone_32_h_product)) * pa_v_hj32_capstone_32_h_product) + (pa_s_hj32_capstone_32_h_product))) /\ pa_s_hj32_capstone_32_h_product = pa_r_hj32_capstone_32_h_product * pa_p_hj32_capstone_32_h_product)))))))
  223. 0223rewrite <- hcap_eq_32
  224. 0224rewrite <- hcap_eq_32
  225. 0225rewrite <- hcap_eq_32
  226. 0226rewrite <- hcap_eq_32
  227. 0227rewrite <- hcap_eq_32
  228. 0228rewrite <- hcap_eq_32
  229. 0229exact hh
  230. 0230have hcap_32_result : exists bqb_le_gap_hj32_capstone_32_result. bqb_le_gap_hj32_capstone_32_result + (h) = (u)
  231. 0231specialize bertrand_h_root_32_from_total e
  232. 0232specialize bertrand_h_root_32_from_total h
  233. 0233specialize bertrand_h_root_32_from_total u
  234. 0234apply bertrand_h_root_32_from_total
  235. 0235exact htotal
  236. 0236exact hcap_32_ceiling
  237. 0237exact hcap_32_power
  238. 0238exact hu
  239. 0239split
  240. 0240exact hcap_32_result
  241. 0241exact hjresult