BT00WR

bertrand_h_root_34_from_total

Alpha body-checked · checked-use disabled

The RFC-v1 H envelope at the fixed root 34.

Exact expanded PA statement

forall e h u. (forall bpt_a_hj32_h_root_34 bpt_e_hj32_h_root_34. exists bpt_x_hj32_h_root_34. (exists ff_b_bpt_value_hj32_h_root_34 ff_c_bpt_value_hj32_h_root_34. ((forall ff_i_bpt_value_hj32_h_root_34_repeat. (exists ff_lt_bpt_value_hj32_h_root_34_repeat_bound. ff_lt_bpt_value_hj32_h_root_34_repeat_bound + S ff_i_bpt_value_hj32_h_root_34_repeat = bpt_e_hj32_h_root_34) -> (((exists ff_h_bpt_value_hj32_h_root_34_repeat_decoded. ff_h_bpt_value_hj32_h_root_34_repeat_decoded + S (bpt_a_hj32_h_root_34) = S ((S (ff_i_bpt_value_hj32_h_root_34_repeat)) * ff_c_bpt_value_hj32_h_root_34)) /\ exists ff_q_bpt_value_hj32_h_root_34_repeat_decoded. ff_b_bpt_value_hj32_h_root_34 = ff_q_bpt_value_hj32_h_root_34_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_34_repeat)) * ff_c_bpt_value_hj32_h_root_34) + (bpt_a_hj32_h_root_34)))) /\ (exists ff_u_bpt_value_hj32_h_root_34_product ff_v_bpt_value_hj32_h_root_34_product. ((((exists ff_h_bpt_value_hj32_h_root_34_product_start. ff_h_bpt_value_hj32_h_root_34_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_start. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_34_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_34_product_terminal. ff_h_bpt_value_hj32_h_root_34_product_terminal + S (bpt_x_hj32_h_root_34) = S ((S (bpt_e_hj32_h_root_34)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_terminal. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_terminal * S ((S (bpt_e_hj32_h_root_34)) * ff_v_bpt_value_hj32_h_root_34_product) + (bpt_x_hj32_h_root_34))) /\ forall ff_i_bpt_value_hj32_h_root_34_product. (exists ff_lt_bpt_value_hj32_h_root_34_product_bound. ff_lt_bpt_value_hj32_h_root_34_product_bound + S ff_i_bpt_value_hj32_h_root_34_product = bpt_e_hj32_h_root_34) -> exists ff_p_bpt_value_hj32_h_root_34_product ff_r_bpt_value_hj32_h_root_34_product ff_s_bpt_value_hj32_h_root_34_product. ((((exists ff_h_bpt_value_hj32_h_root_34_product_factor. ff_h_bpt_value_hj32_h_root_34_product_factor + S (ff_p_bpt_value_hj32_h_root_34_product) = S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_c_bpt_value_hj32_h_root_34)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_factor. ff_b_bpt_value_hj32_h_root_34 = ff_q_bpt_value_hj32_h_root_34_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_c_bpt_value_hj32_h_root_34) + (ff_p_bpt_value_hj32_h_root_34_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_34_product_partial. ff_h_bpt_value_hj32_h_root_34_product_partial + S (ff_r_bpt_value_hj32_h_root_34_product) = S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_partial. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product) + (ff_r_bpt_value_hj32_h_root_34_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_34_product_successor. ff_h_bpt_value_hj32_h_root_34_product_successor + S (ff_s_bpt_value_hj32_h_root_34_product) = S ((S (S ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product)) /\ exists ff_q_bpt_value_hj32_h_root_34_product_successor. ff_u_bpt_value_hj32_h_root_34_product = ff_q_bpt_value_hj32_h_root_34_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_34_product)) * ff_v_bpt_value_hj32_h_root_34_product) + (ff_s_bpt_value_hj32_h_root_34_product))) /\ ff_s_bpt_value_hj32_h_root_34_product = ff_r_bpt_value_hj32_h_root_34_product * ff_p_bpt_value_hj32_h_root_34_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_34_ceiling. bcs_lower_gap_hj32_h_root_34_ceiling + (34 * 34) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_34_ceiling. bcs_upper_gap_hj32_h_root_34_ceiling + S (6 * (e)) = (34 * 34) + 6)) -> (exists pa_b_hj32_h_root_34_h pa_c_hj32_h_root_34_h. ((forall pa_i_hj32_h_root_34_h_repeat. (exists pa_lt_hj32_h_root_34_h_repeat_bound. pa_lt_hj32_h_root_34_h_repeat_bound + S pa_i_hj32_h_root_34_h_repeat = 2 * 34 + 2) -> (((exists pa_h_hj32_h_root_34_h_repeat_decoded. pa_h_hj32_h_root_34_h_repeat_decoded + S (34 + 1) = S ((S (pa_i_hj32_h_root_34_h_repeat)) * pa_c_hj32_h_root_34_h)) /\ exists pa_q_hj32_h_root_34_h_repeat_decoded. pa_b_hj32_h_root_34_h = pa_q_hj32_h_root_34_h_repeat_decoded * S ((S (pa_i_hj32_h_root_34_h_repeat)) * pa_c_hj32_h_root_34_h) + (34 + 1)))) /\ (exists pa_u_hj32_h_root_34_h_product pa_v_hj32_h_root_34_h_product. ((((exists pa_h_hj32_h_root_34_h_product_start. pa_h_hj32_h_root_34_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_start. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_start * S ((S (0)) * pa_v_hj32_h_root_34_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_34_h_product_terminal. pa_h_hj32_h_root_34_h_product_terminal + S (h) = S ((S (2 * 34 + 2)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_terminal. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_terminal * S ((S (2 * 34 + 2)) * pa_v_hj32_h_root_34_h_product) + (h))) /\ forall pa_i_hj32_h_root_34_h_product. (exists pa_lt_hj32_h_root_34_h_product_bound. pa_lt_hj32_h_root_34_h_product_bound + S pa_i_hj32_h_root_34_h_product = 2 * 34 + 2) -> exists pa_p_hj32_h_root_34_h_product pa_r_hj32_h_root_34_h_product pa_s_hj32_h_root_34_h_product. ((((exists pa_h_hj32_h_root_34_h_product_factor. pa_h_hj32_h_root_34_h_product_factor + S (pa_p_hj32_h_root_34_h_product) = S ((S (pa_i_hj32_h_root_34_h_product)) * pa_c_hj32_h_root_34_h)) /\ exists pa_q_hj32_h_root_34_h_product_factor. pa_b_hj32_h_root_34_h = pa_q_hj32_h_root_34_h_product_factor * S ((S (pa_i_hj32_h_root_34_h_product)) * pa_c_hj32_h_root_34_h) + (pa_p_hj32_h_root_34_h_product))) /\ ((((exists pa_h_hj32_h_root_34_h_product_partial. pa_h_hj32_h_root_34_h_product_partial + S (pa_r_hj32_h_root_34_h_product) = S ((S (pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_partial. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_partial * S ((S (pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product) + (pa_r_hj32_h_root_34_h_product))) /\ ((((exists pa_h_hj32_h_root_34_h_product_successor. pa_h_hj32_h_root_34_h_product_successor + S (pa_s_hj32_h_root_34_h_product) = S ((S (S pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product)) /\ exists pa_q_hj32_h_root_34_h_product_successor. pa_u_hj32_h_root_34_h_product = pa_q_hj32_h_root_34_h_product_successor * S ((S (S pa_i_hj32_h_root_34_h_product)) * pa_v_hj32_h_root_34_h_product) + (pa_s_hj32_h_root_34_h_product))) /\ pa_s_hj32_h_root_34_h_product = pa_r_hj32_h_root_34_h_product * pa_p_hj32_h_root_34_h_product)))))))) -> (exists pa_b_hj32_h_root_34_u pa_c_hj32_h_root_34_u. ((forall pa_i_hj32_h_root_34_u_repeat. (exists pa_lt_hj32_h_root_34_u_repeat_bound. pa_lt_hj32_h_root_34_u_repeat_bound + S pa_i_hj32_h_root_34_u_repeat = e) -> (((exists pa_h_hj32_h_root_34_u_repeat_decoded. pa_h_hj32_h_root_34_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_34_u_repeat)) * pa_c_hj32_h_root_34_u)) /\ exists pa_q_hj32_h_root_34_u_repeat_decoded. pa_b_hj32_h_root_34_u = pa_q_hj32_h_root_34_u_repeat_decoded * S ((S (pa_i_hj32_h_root_34_u_repeat)) * pa_c_hj32_h_root_34_u) + (4)))) /\ (exists pa_u_hj32_h_root_34_u_product pa_v_hj32_h_root_34_u_product. ((((exists pa_h_hj32_h_root_34_u_product_start. pa_h_hj32_h_root_34_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_start. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_start * S ((S (0)) * pa_v_hj32_h_root_34_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_34_u_product_terminal. pa_h_hj32_h_root_34_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_terminal. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_34_u_product) + (u))) /\ forall pa_i_hj32_h_root_34_u_product. (exists pa_lt_hj32_h_root_34_u_product_bound. pa_lt_hj32_h_root_34_u_product_bound + S pa_i_hj32_h_root_34_u_product = e) -> exists pa_p_hj32_h_root_34_u_product pa_r_hj32_h_root_34_u_product pa_s_hj32_h_root_34_u_product. ((((exists pa_h_hj32_h_root_34_u_product_factor. pa_h_hj32_h_root_34_u_product_factor + S (pa_p_hj32_h_root_34_u_product) = S ((S (pa_i_hj32_h_root_34_u_product)) * pa_c_hj32_h_root_34_u)) /\ exists pa_q_hj32_h_root_34_u_product_factor. pa_b_hj32_h_root_34_u = pa_q_hj32_h_root_34_u_product_factor * S ((S (pa_i_hj32_h_root_34_u_product)) * pa_c_hj32_h_root_34_u) + (pa_p_hj32_h_root_34_u_product))) /\ ((((exists pa_h_hj32_h_root_34_u_product_partial. pa_h_hj32_h_root_34_u_product_partial + S (pa_r_hj32_h_root_34_u_product) = S ((S (pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_partial. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_partial * S ((S (pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product) + (pa_r_hj32_h_root_34_u_product))) /\ ((((exists pa_h_hj32_h_root_34_u_product_successor. pa_h_hj32_h_root_34_u_product_successor + S (pa_s_hj32_h_root_34_u_product) = S ((S (S pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product)) /\ exists pa_q_hj32_h_root_34_u_product_successor. pa_u_hj32_h_root_34_u_product = pa_q_hj32_h_root_34_u_product_successor * S ((S (S pa_i_hj32_h_root_34_u_product)) * pa_v_hj32_h_root_34_u_product) + (pa_s_hj32_h_root_34_u_product))) /\ pa_s_hj32_h_root_34_u_product = pa_r_hj32_h_root_34_u_product * pa_p_hj32_h_root_34_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_34_result. bqb_le_gap_hj32_h_root_34_result + (h) = (u))

Structural proof guide

The RFC-v1 H envelope at the fixed root 34.

Direct prerequisites: bertrand_scaled_budget_root_34, ceil_div_six_budget_of_scaled_le, pow_thirty_six_double_block_eq_pow_six_four_block_from_total, pow_six_ten_block_le_pow_four_thirteen_block_from_total, pow_base_monotone, pow_exponent_monotone_from_total, le_trans, mul_assoc. The authored body proceeds by case analysis (4), intermediate claims (25), equality transport (17), closed numeral normalization (8).

Proof neighborhood

Direct dependencies

BT00WA bertrand_scaled_budget_root_34 BT00WE ceil_div_six_budget_of_scaled_le BT00WO pow_thirty_six_double_block_eq_pow_six_four_block_from_total BT00WN pow_six_ten_block_le_pow_four_thirteen_block_from_total BT00PY pow_base_monotone BT00SN pow_exponent_monotone_from_total BT000F le_trans BT0008 mul_assoc

Direct dependents

BT00WW bertrand_hj_base_window_thirty_two_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 e
  2. 0002intro h
  3. 0003intro u
  4. 0004intro htotal
  5. 0005intro hceiling
  6. 0006intro hh
  7. 0007intro hu
  8. 0008have hh_route : exists pa_b_hj32_h_34_route pa_c_hj32_h_34_route. ((forall pa_i_hj32_h_34_route_repeat. (exists pa_lt_hj32_h_34_route_repeat_bound. pa_lt_hj32_h_34_route_repeat_bound + S pa_i_hj32_h_34_route_repeat = 2 * 35) -> (((exists pa_h_hj32_h_34_route_repeat_decoded. pa_h_hj32_h_34_route_repeat_decoded + S (35) = S ((S (pa_i_hj32_h_34_route_repeat)) * pa_c_hj32_h_34_route)) /\ exists pa_q_hj32_h_34_route_repeat_decoded. pa_b_hj32_h_34_route = pa_q_hj32_h_34_route_repeat_decoded * S ((S (pa_i_hj32_h_34_route_repeat)) * pa_c_hj32_h_34_route) + (35)))) /\ (exists pa_u_hj32_h_34_route_product pa_v_hj32_h_34_route_product. ((((exists pa_h_hj32_h_34_route_product_start. pa_h_hj32_h_34_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_start. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_start * S ((S (0)) * pa_v_hj32_h_34_route_product) + (1))) /\ ((((exists pa_h_hj32_h_34_route_product_terminal. pa_h_hj32_h_34_route_product_terminal + S (h) = S ((S (2 * 35)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_terminal. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_terminal * S ((S (2 * 35)) * pa_v_hj32_h_34_route_product) + (h))) /\ forall pa_i_hj32_h_34_route_product. (exists pa_lt_hj32_h_34_route_product_bound. pa_lt_hj32_h_34_route_product_bound + S pa_i_hj32_h_34_route_product = 2 * 35) -> exists pa_p_hj32_h_34_route_product pa_r_hj32_h_34_route_product pa_s_hj32_h_34_route_product. ((((exists pa_h_hj32_h_34_route_product_factor. pa_h_hj32_h_34_route_product_factor + S (pa_p_hj32_h_34_route_product) = S ((S (pa_i_hj32_h_34_route_product)) * pa_c_hj32_h_34_route)) /\ exists pa_q_hj32_h_34_route_product_factor. pa_b_hj32_h_34_route = pa_q_hj32_h_34_route_product_factor * S ((S (pa_i_hj32_h_34_route_product)) * pa_c_hj32_h_34_route) + (pa_p_hj32_h_34_route_product))) /\ ((((exists pa_h_hj32_h_34_route_product_partial. pa_h_hj32_h_34_route_product_partial + S (pa_r_hj32_h_34_route_product) = S ((S (pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_partial. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_partial * S ((S (pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product) + (pa_r_hj32_h_34_route_product))) /\ ((((exists pa_h_hj32_h_34_route_product_successor. pa_h_hj32_h_34_route_product_successor + S (pa_s_hj32_h_34_route_product) = S ((S (S pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product)) /\ exists pa_q_hj32_h_34_route_product_successor. pa_u_hj32_h_34_route_product = pa_q_hj32_h_34_route_product_successor * S ((S (S pa_i_hj32_h_34_route_product)) * pa_v_hj32_h_34_route_product) + (pa_s_hj32_h_34_route_product))) /\ pa_s_hj32_h_34_route_product = pa_r_hj32_h_34_route_product * pa_p_hj32_h_34_route_product)))))))
  9. 0009have hh_base : 34 + 1 = 35
  10. 0010norm_num
  11. 0011have hh_exponent : 2 * 34 + 2 = 2 * 35
  12. 0012norm_num
  13. 0013rewrite <- hh_exponent
  14. 0014rewrite <- hh_exponent
  15. 0015rewrite <- hh_exponent
  16. 0016rewrite <- hh_exponent
  17. 0017rewrite <- hh_base
  18. 0018rewrite <- hh_base
  19. 0019exact hh
  20. 0020have h34s_p36 : exists hj32_local_value_h34s_p36. (exists pa_b_hj32_local_total_h34s_p36 pa_c_hj32_local_total_h34s_p36. ((forall pa_i_hj32_local_total_h34s_p36_repeat. (exists pa_lt_hj32_local_total_h34s_p36_repeat_bound. pa_lt_hj32_local_total_h34s_p36_repeat_bound + S pa_i_hj32_local_total_h34s_p36_repeat = 2 * 35) -> (((exists pa_h_hj32_local_total_h34s_p36_repeat_decoded. pa_h_hj32_local_total_h34s_p36_repeat_decoded + S (36) = S ((S (pa_i_hj32_local_total_h34s_p36_repeat)) * pa_c_hj32_local_total_h34s_p36)) /\ exists pa_q_hj32_local_total_h34s_p36_repeat_decoded. pa_b_hj32_local_total_h34s_p36 = pa_q_hj32_local_total_h34s_p36_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p36_repeat)) * pa_c_hj32_local_total_h34s_p36) + (36)))) /\ (exists pa_u_hj32_local_total_h34s_p36_product pa_v_hj32_local_total_h34s_p36_product. ((((exists pa_h_hj32_local_total_h34s_p36_product_start. pa_h_hj32_local_total_h34s_p36_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_start. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p36_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p36_product_terminal. pa_h_hj32_local_total_h34s_p36_product_terminal + S (hj32_local_value_h34s_p36) = S ((S (2 * 35)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_terminal. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_terminal * S ((S (2 * 35)) * pa_v_hj32_local_total_h34s_p36_product) + (hj32_local_value_h34s_p36))) /\ forall pa_i_hj32_local_total_h34s_p36_product. (exists pa_lt_hj32_local_total_h34s_p36_product_bound. pa_lt_hj32_local_total_h34s_p36_product_bound + S pa_i_hj32_local_total_h34s_p36_product = 2 * 35) -> exists pa_p_hj32_local_total_h34s_p36_product pa_r_hj32_local_total_h34s_p36_product pa_s_hj32_local_total_h34s_p36_product. ((((exists pa_h_hj32_local_total_h34s_p36_product_factor. pa_h_hj32_local_total_h34s_p36_product_factor + S (pa_p_hj32_local_total_h34s_p36_product) = S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_c_hj32_local_total_h34s_p36)) /\ exists pa_q_hj32_local_total_h34s_p36_product_factor. pa_b_hj32_local_total_h34s_p36 = pa_q_hj32_local_total_h34s_p36_product_factor * S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_c_hj32_local_total_h34s_p36) + (pa_p_hj32_local_total_h34s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p36_product_partial. pa_h_hj32_local_total_h34s_p36_product_partial + S (pa_r_hj32_local_total_h34s_p36_product) = S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_partial. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_partial * S ((S (pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product) + (pa_r_hj32_local_total_h34s_p36_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p36_product_successor. pa_h_hj32_local_total_h34s_p36_product_successor + S (pa_s_hj32_local_total_h34s_p36_product) = S ((S (S pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product)) /\ exists pa_q_hj32_local_total_h34s_p36_product_successor. pa_u_hj32_local_total_h34s_p36_product = pa_q_hj32_local_total_h34s_p36_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p36_product)) * pa_v_hj32_local_total_h34s_p36_product) + (pa_s_hj32_local_total_h34s_p36_product))) /\ pa_s_hj32_local_total_h34s_p36_product = pa_r_hj32_local_total_h34s_p36_product * pa_p_hj32_local_total_h34s_p36_product))))))))
  21. 0021specialize htotal 36
  22. 0022specialize htotal 2 * 35
  23. 0023exact htotal
  24. 0024cases h34s_p36
  25. 0025have h34s_base : exists bqb_le_gap_hj32_h34s_base. bqb_le_gap_hj32_h34s_base + (35) = (36)
  26. 0026exists 1
  27. 0027norm_num
  28. 0028have h34s_to_36 : exists bqb_le_gap_hj32_local_base_bound_h34s_to_36. bqb_le_gap_hj32_local_base_bound_h34s_to_36 + (h) = (x)
  29. 0029specialize pow_base_monotone 35
  30. 0030specialize pow_base_monotone 36
  31. 0031specialize pow_base_monotone 2 * 35
  32. 0032specialize pow_base_monotone h
  33. 0033specialize pow_base_monotone x
  34. 0034apply pow_base_monotone
  35. 0035exact h34s_base
  36. 0036exact hh_route
  37. 0037exact h34s_p36_witness
  38. 0038have h34s_p6_total : exists hj32_local_value_h34s_p6_total. (exists pa_b_hj32_local_total_h34s_p6_total pa_c_hj32_local_total_h34s_p6_total. ((forall pa_i_hj32_local_total_h34s_p6_total_repeat. (exists pa_lt_hj32_local_total_h34s_p6_total_repeat_bound. pa_lt_hj32_local_total_h34s_p6_total_repeat_bound + S pa_i_hj32_local_total_h34s_p6_total_repeat = 4 * 35) -> (((exists pa_h_hj32_local_total_h34s_p6_total_repeat_decoded. pa_h_hj32_local_total_h34s_p6_total_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h34s_p6_total_repeat)) * pa_c_hj32_local_total_h34s_p6_total)) /\ exists pa_q_hj32_local_total_h34s_p6_total_repeat_decoded. pa_b_hj32_local_total_h34s_p6_total = pa_q_hj32_local_total_h34s_p6_total_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p6_total_repeat)) * pa_c_hj32_local_total_h34s_p6_total) + (6)))) /\ (exists pa_u_hj32_local_total_h34s_p6_total_product pa_v_hj32_local_total_h34s_p6_total_product. ((((exists pa_h_hj32_local_total_h34s_p6_total_product_start. pa_h_hj32_local_total_h34s_p6_total_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_start. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p6_total_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_total_product_terminal. pa_h_hj32_local_total_h34s_p6_total_product_terminal + S (hj32_local_value_h34s_p6_total) = S ((S (4 * 35)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_terminal. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_terminal * S ((S (4 * 35)) * pa_v_hj32_local_total_h34s_p6_total_product) + (hj32_local_value_h34s_p6_total))) /\ forall pa_i_hj32_local_total_h34s_p6_total_product. (exists pa_lt_hj32_local_total_h34s_p6_total_product_bound. pa_lt_hj32_local_total_h34s_p6_total_product_bound + S pa_i_hj32_local_total_h34s_p6_total_product = 4 * 35) -> exists pa_p_hj32_local_total_h34s_p6_total_product pa_r_hj32_local_total_h34s_p6_total_product pa_s_hj32_local_total_h34s_p6_total_product. ((((exists pa_h_hj32_local_total_h34s_p6_total_product_factor. pa_h_hj32_local_total_h34s_p6_total_product_factor + S (pa_p_hj32_local_total_h34s_p6_total_product) = S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_c_hj32_local_total_h34s_p6_total)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_factor. pa_b_hj32_local_total_h34s_p6_total = pa_q_hj32_local_total_h34s_p6_total_product_factor * S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_c_hj32_local_total_h34s_p6_total) + (pa_p_hj32_local_total_h34s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_total_product_partial. pa_h_hj32_local_total_h34s_p6_total_product_partial + S (pa_r_hj32_local_total_h34s_p6_total_product) = S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_partial. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_partial * S ((S (pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product) + (pa_r_hj32_local_total_h34s_p6_total_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_total_product_successor. pa_h_hj32_local_total_h34s_p6_total_product_successor + S (pa_s_hj32_local_total_h34s_p6_total_product) = S ((S (S pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product)) /\ exists pa_q_hj32_local_total_h34s_p6_total_product_successor. pa_u_hj32_local_total_h34s_p6_total_product = pa_q_hj32_local_total_h34s_p6_total_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p6_total_product)) * pa_v_hj32_local_total_h34s_p6_total_product) + (pa_s_hj32_local_total_h34s_p6_total_product))) /\ pa_s_hj32_local_total_h34s_p6_total_product = pa_r_hj32_local_total_h34s_p6_total_product * pa_p_hj32_local_total_h34s_p6_total_product))))))))
  39. 0039specialize htotal 6
  40. 0040specialize htotal 4 * 35
  41. 0041exact htotal
  42. 0042cases h34s_p6_total
  43. 0043have h34s_conversion : x = x1
  44. 0044specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total 35
  45. 0045specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x
  46. 0046specialize pow_thirty_six_double_block_eq_pow_six_four_block_from_total x1
  47. 0047apply pow_thirty_six_double_block_eq_pow_six_four_block_from_total
  48. 0048exact htotal
  49. 0049exact h34s_p36_witness
  50. 0050exact h34s_p6_total_witness
  51. 0051rewrite h34s_conversion at h34s_to_36
  52. 0052have h34s_p6_main : exists hj32_local_value_h34s_p6_main. (exists pa_b_hj32_local_total_h34s_p6_main pa_c_hj32_local_total_h34s_p6_main. ((forall pa_i_hj32_local_total_h34s_p6_main_repeat. (exists pa_lt_hj32_local_total_h34s_p6_main_repeat_bound. pa_lt_hj32_local_total_h34s_p6_main_repeat_bound + S pa_i_hj32_local_total_h34s_p6_main_repeat = 10 * 14) -> (((exists pa_h_hj32_local_total_h34s_p6_main_repeat_decoded. pa_h_hj32_local_total_h34s_p6_main_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_h34s_p6_main_repeat)) * pa_c_hj32_local_total_h34s_p6_main)) /\ exists pa_q_hj32_local_total_h34s_p6_main_repeat_decoded. pa_b_hj32_local_total_h34s_p6_main = pa_q_hj32_local_total_h34s_p6_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p6_main_repeat)) * pa_c_hj32_local_total_h34s_p6_main) + (6)))) /\ (exists pa_u_hj32_local_total_h34s_p6_main_product pa_v_hj32_local_total_h34s_p6_main_product. ((((exists pa_h_hj32_local_total_h34s_p6_main_product_start. pa_h_hj32_local_total_h34s_p6_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_start. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p6_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_main_product_terminal. pa_h_hj32_local_total_h34s_p6_main_product_terminal + S (hj32_local_value_h34s_p6_main) = S ((S (10 * 14)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_terminal. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_terminal * S ((S (10 * 14)) * pa_v_hj32_local_total_h34s_p6_main_product) + (hj32_local_value_h34s_p6_main))) /\ forall pa_i_hj32_local_total_h34s_p6_main_product. (exists pa_lt_hj32_local_total_h34s_p6_main_product_bound. pa_lt_hj32_local_total_h34s_p6_main_product_bound + S pa_i_hj32_local_total_h34s_p6_main_product = 10 * 14) -> exists pa_p_hj32_local_total_h34s_p6_main_product pa_r_hj32_local_total_h34s_p6_main_product pa_s_hj32_local_total_h34s_p6_main_product. ((((exists pa_h_hj32_local_total_h34s_p6_main_product_factor. pa_h_hj32_local_total_h34s_p6_main_product_factor + S (pa_p_hj32_local_total_h34s_p6_main_product) = S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_c_hj32_local_total_h34s_p6_main)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_factor. pa_b_hj32_local_total_h34s_p6_main = pa_q_hj32_local_total_h34s_p6_main_product_factor * S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_c_hj32_local_total_h34s_p6_main) + (pa_p_hj32_local_total_h34s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_main_product_partial. pa_h_hj32_local_total_h34s_p6_main_product_partial + S (pa_r_hj32_local_total_h34s_p6_main_product) = S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_partial. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_partial * S ((S (pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product) + (pa_r_hj32_local_total_h34s_p6_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p6_main_product_successor. pa_h_hj32_local_total_h34s_p6_main_product_successor + S (pa_s_hj32_local_total_h34s_p6_main_product) = S ((S (S pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product)) /\ exists pa_q_hj32_local_total_h34s_p6_main_product_successor. pa_u_hj32_local_total_h34s_p6_main_product = pa_q_hj32_local_total_h34s_p6_main_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p6_main_product)) * pa_v_hj32_local_total_h34s_p6_main_product) + (pa_s_hj32_local_total_h34s_p6_main_product))) /\ pa_s_hj32_local_total_h34s_p6_main_product = pa_r_hj32_local_total_h34s_p6_main_product * pa_p_hj32_local_total_h34s_p6_main_product))))))))
  53. 0053specialize htotal 6
  54. 0054specialize htotal 10 * 14
  55. 0055exact htotal
  56. 0056cases h34s_p6_main
  57. 0057have h34s_p4_main : exists hj32_local_value_h34s_p4_main. (exists pa_b_hj32_local_total_h34s_p4_main pa_c_hj32_local_total_h34s_p4_main. ((forall pa_i_hj32_local_total_h34s_p4_main_repeat. (exists pa_lt_hj32_local_total_h34s_p4_main_repeat_bound. pa_lt_hj32_local_total_h34s_p4_main_repeat_bound + S pa_i_hj32_local_total_h34s_p4_main_repeat = 13 * 14) -> (((exists pa_h_hj32_local_total_h34s_p4_main_repeat_decoded. pa_h_hj32_local_total_h34s_p4_main_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h34s_p4_main_repeat)) * pa_c_hj32_local_total_h34s_p4_main)) /\ exists pa_q_hj32_local_total_h34s_p4_main_repeat_decoded. pa_b_hj32_local_total_h34s_p4_main = pa_q_hj32_local_total_h34s_p4_main_repeat_decoded * S ((S (pa_i_hj32_local_total_h34s_p4_main_repeat)) * pa_c_hj32_local_total_h34s_p4_main) + (4)))) /\ (exists pa_u_hj32_local_total_h34s_p4_main_product pa_v_hj32_local_total_h34s_p4_main_product. ((((exists pa_h_hj32_local_total_h34s_p4_main_product_start. pa_h_hj32_local_total_h34s_p4_main_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_start. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_start * S ((S (0)) * pa_v_hj32_local_total_h34s_p4_main_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h34s_p4_main_product_terminal. pa_h_hj32_local_total_h34s_p4_main_product_terminal + S (hj32_local_value_h34s_p4_main) = S ((S (13 * 14)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_terminal. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_terminal * S ((S (13 * 14)) * pa_v_hj32_local_total_h34s_p4_main_product) + (hj32_local_value_h34s_p4_main))) /\ forall pa_i_hj32_local_total_h34s_p4_main_product. (exists pa_lt_hj32_local_total_h34s_p4_main_product_bound. pa_lt_hj32_local_total_h34s_p4_main_product_bound + S pa_i_hj32_local_total_h34s_p4_main_product = 13 * 14) -> exists pa_p_hj32_local_total_h34s_p4_main_product pa_r_hj32_local_total_h34s_p4_main_product pa_s_hj32_local_total_h34s_p4_main_product. ((((exists pa_h_hj32_local_total_h34s_p4_main_product_factor. pa_h_hj32_local_total_h34s_p4_main_product_factor + S (pa_p_hj32_local_total_h34s_p4_main_product) = S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_c_hj32_local_total_h34s_p4_main)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_factor. pa_b_hj32_local_total_h34s_p4_main = pa_q_hj32_local_total_h34s_p4_main_product_factor * S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_c_hj32_local_total_h34s_p4_main) + (pa_p_hj32_local_total_h34s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p4_main_product_partial. pa_h_hj32_local_total_h34s_p4_main_product_partial + S (pa_r_hj32_local_total_h34s_p4_main_product) = S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_partial. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_partial * S ((S (pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product) + (pa_r_hj32_local_total_h34s_p4_main_product))) /\ ((((exists pa_h_hj32_local_total_h34s_p4_main_product_successor. pa_h_hj32_local_total_h34s_p4_main_product_successor + S (pa_s_hj32_local_total_h34s_p4_main_product) = S ((S (S pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product)) /\ exists pa_q_hj32_local_total_h34s_p4_main_product_successor. pa_u_hj32_local_total_h34s_p4_main_product = pa_q_hj32_local_total_h34s_p4_main_product_successor * S ((S (S pa_i_hj32_local_total_h34s_p4_main_product)) * pa_v_hj32_local_total_h34s_p4_main_product) + (pa_s_hj32_local_total_h34s_p4_main_product))) /\ pa_s_hj32_local_total_h34s_p4_main_product = pa_r_hj32_local_total_h34s_p4_main_product * pa_p_hj32_local_total_h34s_p4_main_product))))))))
  58. 0058specialize htotal 4
  59. 0059specialize htotal 13 * 14
  60. 0060exact htotal
  61. 0061cases h34s_p4_main
  62. 0062have h34s_main_bound : exists bqb_le_gap_hj32_h34s_main_bound. bqb_le_gap_hj32_h34s_main_bound + (x2) = (x3)
  63. 0063specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14
  64. 0064specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x2
  65. 0065specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3
  66. 0066apply pow_six_ten_block_le_pow_four_thirteen_block_from_total
  67. 0067exact htotal
  68. 0068exact h34s_p6_main_witness
  69. 0069exact h34s_p4_main_witness
  70. 0070have h34s_exponent : 4 * 35 = 10 * 14
  71. 0071have h34s_thirty_five : 35 = 5 * 7
  72. 0072norm_num
  73. 0073rewrite h34s_thirty_five
  74. 0074have h34s_left_assoc : 4 * (5 * 7) = (4 * 5) * 7
  75. 0075symm
  76. 0076specialize mul_assoc 4
  77. 0077specialize mul_assoc 5
  78. 0078specialize mul_assoc 7
  79. 0079apply mul_assoc
  80. 0080rewrite h34s_left_assoc
  81. 0081have h34s_fourteen : 14 = 2 * 7
  82. 0082norm_num
  83. 0083rewrite h34s_fourteen
  84. 0084have h34s_right_assoc : 10 * (2 * 7) = (10 * 2) * 7
  85. 0085symm
  86. 0086specialize mul_assoc 10
  87. 0087specialize mul_assoc 2
  88. 0088specialize mul_assoc 7
  89. 0089apply mul_assoc
  90. 0090rewrite h34s_right_assoc
  91. 0091have h34s_right_twenty : 10 * 2 = 20
  92. 0092norm_num
  93. 0093rewrite h34s_right_twenty
  94. 0094have h34s_left_twenty : 4 * 5 = 20
  95. 0095norm_num
  96. 0096rewrite h34s_left_twenty
  97. 0097refl
  98. 0098have h34s_main_power : exists pa_b_hj32_h34s_main_power pa_c_hj32_h34s_main_power. ((forall pa_i_hj32_h34s_main_power_repeat. (exists pa_lt_hj32_h34s_main_power_repeat_bound. pa_lt_hj32_h34s_main_power_repeat_bound + S pa_i_hj32_h34s_main_power_repeat = 10 * 14) -> (((exists pa_h_hj32_h34s_main_power_repeat_decoded. pa_h_hj32_h34s_main_power_repeat_decoded + S (6) = S ((S (pa_i_hj32_h34s_main_power_repeat)) * pa_c_hj32_h34s_main_power)) /\ exists pa_q_hj32_h34s_main_power_repeat_decoded. pa_b_hj32_h34s_main_power = pa_q_hj32_h34s_main_power_repeat_decoded * S ((S (pa_i_hj32_h34s_main_power_repeat)) * pa_c_hj32_h34s_main_power) + (6)))) /\ (exists pa_u_hj32_h34s_main_power_product pa_v_hj32_h34s_main_power_product. ((((exists pa_h_hj32_h34s_main_power_product_start. pa_h_hj32_h34s_main_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_start. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_start * S ((S (0)) * pa_v_hj32_h34s_main_power_product) + (1))) /\ ((((exists pa_h_hj32_h34s_main_power_product_terminal. pa_h_hj32_h34s_main_power_product_terminal + S (x1) = S ((S (10 * 14)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_terminal. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_terminal * S ((S (10 * 14)) * pa_v_hj32_h34s_main_power_product) + (x1))) /\ forall pa_i_hj32_h34s_main_power_product. (exists pa_lt_hj32_h34s_main_power_product_bound. pa_lt_hj32_h34s_main_power_product_bound + S pa_i_hj32_h34s_main_power_product = 10 * 14) -> exists pa_p_hj32_h34s_main_power_product pa_r_hj32_h34s_main_power_product pa_s_hj32_h34s_main_power_product. ((((exists pa_h_hj32_h34s_main_power_product_factor. pa_h_hj32_h34s_main_power_product_factor + S (pa_p_hj32_h34s_main_power_product) = S ((S (pa_i_hj32_h34s_main_power_product)) * pa_c_hj32_h34s_main_power)) /\ exists pa_q_hj32_h34s_main_power_product_factor. pa_b_hj32_h34s_main_power = pa_q_hj32_h34s_main_power_product_factor * S ((S (pa_i_hj32_h34s_main_power_product)) * pa_c_hj32_h34s_main_power) + (pa_p_hj32_h34s_main_power_product))) /\ ((((exists pa_h_hj32_h34s_main_power_product_partial. pa_h_hj32_h34s_main_power_product_partial + S (pa_r_hj32_h34s_main_power_product) = S ((S (pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_partial. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_partial * S ((S (pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product) + (pa_r_hj32_h34s_main_power_product))) /\ ((((exists pa_h_hj32_h34s_main_power_product_successor. pa_h_hj32_h34s_main_power_product_successor + S (pa_s_hj32_h34s_main_power_product) = S ((S (S pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product)) /\ exists pa_q_hj32_h34s_main_power_product_successor. pa_u_hj32_h34s_main_power_product = pa_q_hj32_h34s_main_power_product_successor * S ((S (S pa_i_hj32_h34s_main_power_product)) * pa_v_hj32_h34s_main_power_product) + (pa_s_hj32_h34s_main_power_product))) /\ pa_s_hj32_h34s_main_power_product = pa_r_hj32_h34s_main_power_product * pa_p_hj32_h34s_main_power_product)))))))
  99. 0099rewrite <- h34s_exponent
  100. 0100rewrite <- h34s_exponent
  101. 0101rewrite <- h34s_exponent
  102. 0102rewrite <- h34s_exponent
  103. 0103exact h34s_p6_total_witness
  104. 0104have h34s_direct_bound : exists bqb_le_gap_hj32_h34s_direct_bound. bqb_le_gap_hj32_h34s_direct_bound + (x1) = (x3)
  105. 0105specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total 14
  106. 0106specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x1
  107. 0107specialize pow_six_ten_block_le_pow_four_thirteen_block_from_total x3
  108. 0108apply pow_six_ten_block_le_pow_four_thirteen_block_from_total
  109. 0109exact htotal
  110. 0110exact h34s_main_power
  111. 0111exact h34s_p4_main_witness
  112. 0112have h34s_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h34s_to_budget. bqb_le_gap_hj32_local_trans_bound_h34s_to_budget + (h) = (x3)
  113. 0113specialize le_trans h
  114. 0114specialize le_trans x1
  115. 0115specialize le_trans x3
  116. 0116apply le_trans
  117. 0117exact h34s_to_36
  118. 0118exact h34s_direct_bound
  119. 0119have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_34. bqb_le_gap_hj32_scaled_budget_root_34 + (6 * (13 * 14)) = (34 * 34)
  120. 0120apply bertrand_scaled_budget_root_34
  121. 0121have hbudget_exponent : exists bqb_le_gap_hj32_h_34_budget_exponent. bqb_le_gap_hj32_h_34_budget_exponent + (13 * 14) = (e)
  122. 0122specialize ceil_div_six_budget_of_scaled_le (34 * 34)
  123. 0123specialize ceil_div_six_budget_of_scaled_le (13 * 14)
  124. 0124specialize ceil_div_six_budget_of_scaled_le e
  125. 0125apply ceil_div_six_budget_of_scaled_le
  126. 0126exact hceiling
  127. 0127exact hscaled
  128. 0128have h34_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h34_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h34_budget_growth + (x3) = (u)
  129. 0129specialize pow_exponent_monotone_from_total 4
  130. 0130specialize pow_exponent_monotone_from_total 13 * 14
  131. 0131specialize pow_exponent_monotone_from_total e
  132. 0132specialize pow_exponent_monotone_from_total x3
  133. 0133specialize pow_exponent_monotone_from_total u
  134. 0134apply pow_exponent_monotone_from_total
  135. 0135exact htotal
  136. 0136exists 3
  137. 0137norm_num
  138. 0138exact hbudget_exponent
  139. 0139exact h34s_p4_main_witness
  140. 0140exact hu
  141. 0141have h34_result : exists bqb_le_gap_hj32_local_trans_bound_h34_result. bqb_le_gap_hj32_local_trans_bound_h34_result + (h) = (u)
  142. 0142specialize le_trans h
  143. 0143specialize le_trans x3
  144. 0144specialize le_trans u
  145. 0145apply le_trans
  146. 0146exact h34s_to_budget
  147. 0147exact h34_budget_growth
  148. 0148exact h34_result