BT00WU

bertrand_h_root_37_from_total

Alpha body-checked · checked-use disabled

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

Exact expanded PA statement

forall e h u. (forall bpt_a_hj32_h_root_37 bpt_e_hj32_h_root_37. exists bpt_x_hj32_h_root_37. (exists ff_b_bpt_value_hj32_h_root_37 ff_c_bpt_value_hj32_h_root_37. ((forall ff_i_bpt_value_hj32_h_root_37_repeat. (exists ff_lt_bpt_value_hj32_h_root_37_repeat_bound. ff_lt_bpt_value_hj32_h_root_37_repeat_bound + S ff_i_bpt_value_hj32_h_root_37_repeat = bpt_e_hj32_h_root_37) -> (((exists ff_h_bpt_value_hj32_h_root_37_repeat_decoded. ff_h_bpt_value_hj32_h_root_37_repeat_decoded + S (bpt_a_hj32_h_root_37) = S ((S (ff_i_bpt_value_hj32_h_root_37_repeat)) * ff_c_bpt_value_hj32_h_root_37)) /\ exists ff_q_bpt_value_hj32_h_root_37_repeat_decoded. ff_b_bpt_value_hj32_h_root_37 = ff_q_bpt_value_hj32_h_root_37_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_37_repeat)) * ff_c_bpt_value_hj32_h_root_37) + (bpt_a_hj32_h_root_37)))) /\ (exists ff_u_bpt_value_hj32_h_root_37_product ff_v_bpt_value_hj32_h_root_37_product. ((((exists ff_h_bpt_value_hj32_h_root_37_product_start. ff_h_bpt_value_hj32_h_root_37_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_start. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_37_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_37_product_terminal. ff_h_bpt_value_hj32_h_root_37_product_terminal + S (bpt_x_hj32_h_root_37) = S ((S (bpt_e_hj32_h_root_37)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_terminal. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_terminal * S ((S (bpt_e_hj32_h_root_37)) * ff_v_bpt_value_hj32_h_root_37_product) + (bpt_x_hj32_h_root_37))) /\ forall ff_i_bpt_value_hj32_h_root_37_product. (exists ff_lt_bpt_value_hj32_h_root_37_product_bound. ff_lt_bpt_value_hj32_h_root_37_product_bound + S ff_i_bpt_value_hj32_h_root_37_product = bpt_e_hj32_h_root_37) -> exists ff_p_bpt_value_hj32_h_root_37_product ff_r_bpt_value_hj32_h_root_37_product ff_s_bpt_value_hj32_h_root_37_product. ((((exists ff_h_bpt_value_hj32_h_root_37_product_factor. ff_h_bpt_value_hj32_h_root_37_product_factor + S (ff_p_bpt_value_hj32_h_root_37_product) = S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_c_bpt_value_hj32_h_root_37)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_factor. ff_b_bpt_value_hj32_h_root_37 = ff_q_bpt_value_hj32_h_root_37_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_c_bpt_value_hj32_h_root_37) + (ff_p_bpt_value_hj32_h_root_37_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_37_product_partial. ff_h_bpt_value_hj32_h_root_37_product_partial + S (ff_r_bpt_value_hj32_h_root_37_product) = S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_partial. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product) + (ff_r_bpt_value_hj32_h_root_37_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_37_product_successor. ff_h_bpt_value_hj32_h_root_37_product_successor + S (ff_s_bpt_value_hj32_h_root_37_product) = S ((S (S ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product)) /\ exists ff_q_bpt_value_hj32_h_root_37_product_successor. ff_u_bpt_value_hj32_h_root_37_product = ff_q_bpt_value_hj32_h_root_37_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_37_product)) * ff_v_bpt_value_hj32_h_root_37_product) + (ff_s_bpt_value_hj32_h_root_37_product))) /\ ff_s_bpt_value_hj32_h_root_37_product = ff_r_bpt_value_hj32_h_root_37_product * ff_p_bpt_value_hj32_h_root_37_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_37_ceiling. bcs_lower_gap_hj32_h_root_37_ceiling + (37 * 37) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_37_ceiling. bcs_upper_gap_hj32_h_root_37_ceiling + S (6 * (e)) = (37 * 37) + 6)) -> (exists pa_b_hj32_h_root_37_h pa_c_hj32_h_root_37_h. ((forall pa_i_hj32_h_root_37_h_repeat. (exists pa_lt_hj32_h_root_37_h_repeat_bound. pa_lt_hj32_h_root_37_h_repeat_bound + S pa_i_hj32_h_root_37_h_repeat = 2 * 37 + 2) -> (((exists pa_h_hj32_h_root_37_h_repeat_decoded. pa_h_hj32_h_root_37_h_repeat_decoded + S (37 + 1) = S ((S (pa_i_hj32_h_root_37_h_repeat)) * pa_c_hj32_h_root_37_h)) /\ exists pa_q_hj32_h_root_37_h_repeat_decoded. pa_b_hj32_h_root_37_h = pa_q_hj32_h_root_37_h_repeat_decoded * S ((S (pa_i_hj32_h_root_37_h_repeat)) * pa_c_hj32_h_root_37_h) + (37 + 1)))) /\ (exists pa_u_hj32_h_root_37_h_product pa_v_hj32_h_root_37_h_product. ((((exists pa_h_hj32_h_root_37_h_product_start. pa_h_hj32_h_root_37_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_start. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_start * S ((S (0)) * pa_v_hj32_h_root_37_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_37_h_product_terminal. pa_h_hj32_h_root_37_h_product_terminal + S (h) = S ((S (2 * 37 + 2)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_terminal. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_terminal * S ((S (2 * 37 + 2)) * pa_v_hj32_h_root_37_h_product) + (h))) /\ forall pa_i_hj32_h_root_37_h_product. (exists pa_lt_hj32_h_root_37_h_product_bound. pa_lt_hj32_h_root_37_h_product_bound + S pa_i_hj32_h_root_37_h_product = 2 * 37 + 2) -> exists pa_p_hj32_h_root_37_h_product pa_r_hj32_h_root_37_h_product pa_s_hj32_h_root_37_h_product. ((((exists pa_h_hj32_h_root_37_h_product_factor. pa_h_hj32_h_root_37_h_product_factor + S (pa_p_hj32_h_root_37_h_product) = S ((S (pa_i_hj32_h_root_37_h_product)) * pa_c_hj32_h_root_37_h)) /\ exists pa_q_hj32_h_root_37_h_product_factor. pa_b_hj32_h_root_37_h = pa_q_hj32_h_root_37_h_product_factor * S ((S (pa_i_hj32_h_root_37_h_product)) * pa_c_hj32_h_root_37_h) + (pa_p_hj32_h_root_37_h_product))) /\ ((((exists pa_h_hj32_h_root_37_h_product_partial. pa_h_hj32_h_root_37_h_product_partial + S (pa_r_hj32_h_root_37_h_product) = S ((S (pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_partial. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_partial * S ((S (pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product) + (pa_r_hj32_h_root_37_h_product))) /\ ((((exists pa_h_hj32_h_root_37_h_product_successor. pa_h_hj32_h_root_37_h_product_successor + S (pa_s_hj32_h_root_37_h_product) = S ((S (S pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product)) /\ exists pa_q_hj32_h_root_37_h_product_successor. pa_u_hj32_h_root_37_h_product = pa_q_hj32_h_root_37_h_product_successor * S ((S (S pa_i_hj32_h_root_37_h_product)) * pa_v_hj32_h_root_37_h_product) + (pa_s_hj32_h_root_37_h_product))) /\ pa_s_hj32_h_root_37_h_product = pa_r_hj32_h_root_37_h_product * pa_p_hj32_h_root_37_h_product)))))))) -> (exists pa_b_hj32_h_root_37_u pa_c_hj32_h_root_37_u. ((forall pa_i_hj32_h_root_37_u_repeat. (exists pa_lt_hj32_h_root_37_u_repeat_bound. pa_lt_hj32_h_root_37_u_repeat_bound + S pa_i_hj32_h_root_37_u_repeat = e) -> (((exists pa_h_hj32_h_root_37_u_repeat_decoded. pa_h_hj32_h_root_37_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_37_u_repeat)) * pa_c_hj32_h_root_37_u)) /\ exists pa_q_hj32_h_root_37_u_repeat_decoded. pa_b_hj32_h_root_37_u = pa_q_hj32_h_root_37_u_repeat_decoded * S ((S (pa_i_hj32_h_root_37_u_repeat)) * pa_c_hj32_h_root_37_u) + (4)))) /\ (exists pa_u_hj32_h_root_37_u_product pa_v_hj32_h_root_37_u_product. ((((exists pa_h_hj32_h_root_37_u_product_start. pa_h_hj32_h_root_37_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_start. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_start * S ((S (0)) * pa_v_hj32_h_root_37_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_37_u_product_terminal. pa_h_hj32_h_root_37_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_terminal. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_37_u_product) + (u))) /\ forall pa_i_hj32_h_root_37_u_product. (exists pa_lt_hj32_h_root_37_u_product_bound. pa_lt_hj32_h_root_37_u_product_bound + S pa_i_hj32_h_root_37_u_product = e) -> exists pa_p_hj32_h_root_37_u_product pa_r_hj32_h_root_37_u_product pa_s_hj32_h_root_37_u_product. ((((exists pa_h_hj32_h_root_37_u_product_factor. pa_h_hj32_h_root_37_u_product_factor + S (pa_p_hj32_h_root_37_u_product) = S ((S (pa_i_hj32_h_root_37_u_product)) * pa_c_hj32_h_root_37_u)) /\ exists pa_q_hj32_h_root_37_u_product_factor. pa_b_hj32_h_root_37_u = pa_q_hj32_h_root_37_u_product_factor * S ((S (pa_i_hj32_h_root_37_u_product)) * pa_c_hj32_h_root_37_u) + (pa_p_hj32_h_root_37_u_product))) /\ ((((exists pa_h_hj32_h_root_37_u_product_partial. pa_h_hj32_h_root_37_u_product_partial + S (pa_r_hj32_h_root_37_u_product) = S ((S (pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_partial. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_partial * S ((S (pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product) + (pa_r_hj32_h_root_37_u_product))) /\ ((((exists pa_h_hj32_h_root_37_u_product_successor. pa_h_hj32_h_root_37_u_product_successor + S (pa_s_hj32_h_root_37_u_product) = S ((S (S pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product)) /\ exists pa_q_hj32_h_root_37_u_product_successor. pa_u_hj32_h_root_37_u_product = pa_q_hj32_h_root_37_u_product_successor * S ((S (S pa_i_hj32_h_root_37_u_product)) * pa_v_hj32_h_root_37_u_product) + (pa_s_hj32_h_root_37_u_product))) /\ pa_s_hj32_h_root_37_u_product = pa_r_hj32_h_root_37_u_product * pa_p_hj32_h_root_37_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_37_result. bqb_le_gap_hj32_h_root_37_result + (h) = (u))

Structural proof guide

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

Direct prerequisites: bertrand_scaled_budget_root_37, ceil_div_six_budget_of_scaled_le, pow_eleven_double_block_le_pow_four_even_from_total, pow_mul_base, pow_add, pow_base_monotone, pow_exponent_monotone_from_total, mul_le_mul, le_refl, le_trans, mul_assoc, mul_comm. The authored body proceeds by case analysis (5), intermediate claims (24), equality transport (11), closed numeral normalization (6).

Proof neighborhood

Direct dependencies

BT00WD bertrand_scaled_budget_root_37 BT00WE ceil_div_six_budget_of_scaled_le BT00WL pow_eleven_double_block_le_pow_four_even_from_total BT00QV pow_mul_base BT009X pow_add BT00PY pow_base_monotone BT00SN pow_exponent_monotone_from_total BT00PV mul_le_mul BT000E le_refl BT000F le_trans BT0008 mul_assoc BT0006 mul_comm

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_37_route pa_c_hj32_h_37_route. ((forall pa_i_hj32_h_37_route_repeat. (exists pa_lt_hj32_h_37_route_repeat_bound. pa_lt_hj32_h_37_route_repeat_bound + S pa_i_hj32_h_37_route_repeat = 2 * 38) -> (((exists pa_h_hj32_h_37_route_repeat_decoded. pa_h_hj32_h_37_route_repeat_decoded + S (38) = S ((S (pa_i_hj32_h_37_route_repeat)) * pa_c_hj32_h_37_route)) /\ exists pa_q_hj32_h_37_route_repeat_decoded. pa_b_hj32_h_37_route = pa_q_hj32_h_37_route_repeat_decoded * S ((S (pa_i_hj32_h_37_route_repeat)) * pa_c_hj32_h_37_route) + (38)))) /\ (exists pa_u_hj32_h_37_route_product pa_v_hj32_h_37_route_product. ((((exists pa_h_hj32_h_37_route_product_start. pa_h_hj32_h_37_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_start. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_start * S ((S (0)) * pa_v_hj32_h_37_route_product) + (1))) /\ ((((exists pa_h_hj32_h_37_route_product_terminal. pa_h_hj32_h_37_route_product_terminal + S (h) = S ((S (2 * 38)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_terminal. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_terminal * S ((S (2 * 38)) * pa_v_hj32_h_37_route_product) + (h))) /\ forall pa_i_hj32_h_37_route_product. (exists pa_lt_hj32_h_37_route_product_bound. pa_lt_hj32_h_37_route_product_bound + S pa_i_hj32_h_37_route_product = 2 * 38) -> exists pa_p_hj32_h_37_route_product pa_r_hj32_h_37_route_product pa_s_hj32_h_37_route_product. ((((exists pa_h_hj32_h_37_route_product_factor. pa_h_hj32_h_37_route_product_factor + S (pa_p_hj32_h_37_route_product) = S ((S (pa_i_hj32_h_37_route_product)) * pa_c_hj32_h_37_route)) /\ exists pa_q_hj32_h_37_route_product_factor. pa_b_hj32_h_37_route = pa_q_hj32_h_37_route_product_factor * S ((S (pa_i_hj32_h_37_route_product)) * pa_c_hj32_h_37_route) + (pa_p_hj32_h_37_route_product))) /\ ((((exists pa_h_hj32_h_37_route_product_partial. pa_h_hj32_h_37_route_product_partial + S (pa_r_hj32_h_37_route_product) = S ((S (pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_partial. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_partial * S ((S (pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product) + (pa_r_hj32_h_37_route_product))) /\ ((((exists pa_h_hj32_h_37_route_product_successor. pa_h_hj32_h_37_route_product_successor + S (pa_s_hj32_h_37_route_product) = S ((S (S pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product)) /\ exists pa_q_hj32_h_37_route_product_successor. pa_u_hj32_h_37_route_product = pa_q_hj32_h_37_route_product_successor * S ((S (S pa_i_hj32_h_37_route_product)) * pa_v_hj32_h_37_route_product) + (pa_s_hj32_h_37_route_product))) /\ pa_s_hj32_h_37_route_product = pa_r_hj32_h_37_route_product * pa_p_hj32_h_37_route_product)))))))
  9. 0009have hh_base : 37 + 1 = 38
  10. 0010norm_num
  11. 0011have hh_exponent : 2 * 37 + 2 = 2 * 38
  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 h37t_p44 : exists hj32_local_value_h37t_p44. (exists pa_b_hj32_local_total_h37t_p44 pa_c_hj32_local_total_h37t_p44. ((forall pa_i_hj32_local_total_h37t_p44_repeat. (exists pa_lt_hj32_local_total_h37t_p44_repeat_bound. pa_lt_hj32_local_total_h37t_p44_repeat_bound + S pa_i_hj32_local_total_h37t_p44_repeat = 2 * 38) -> (((exists pa_h_hj32_local_total_h37t_p44_repeat_decoded. pa_h_hj32_local_total_h37t_p44_repeat_decoded + S (44) = S ((S (pa_i_hj32_local_total_h37t_p44_repeat)) * pa_c_hj32_local_total_h37t_p44)) /\ exists pa_q_hj32_local_total_h37t_p44_repeat_decoded. pa_b_hj32_local_total_h37t_p44 = pa_q_hj32_local_total_h37t_p44_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p44_repeat)) * pa_c_hj32_local_total_h37t_p44) + (44)))) /\ (exists pa_u_hj32_local_total_h37t_p44_product pa_v_hj32_local_total_h37t_p44_product. ((((exists pa_h_hj32_local_total_h37t_p44_product_start. pa_h_hj32_local_total_h37t_p44_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_start. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p44_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p44_product_terminal. pa_h_hj32_local_total_h37t_p44_product_terminal + S (hj32_local_value_h37t_p44) = S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_terminal. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p44_product) + (hj32_local_value_h37t_p44))) /\ forall pa_i_hj32_local_total_h37t_p44_product. (exists pa_lt_hj32_local_total_h37t_p44_product_bound. pa_lt_hj32_local_total_h37t_p44_product_bound + S pa_i_hj32_local_total_h37t_p44_product = 2 * 38) -> exists pa_p_hj32_local_total_h37t_p44_product pa_r_hj32_local_total_h37t_p44_product pa_s_hj32_local_total_h37t_p44_product. ((((exists pa_h_hj32_local_total_h37t_p44_product_factor. pa_h_hj32_local_total_h37t_p44_product_factor + S (pa_p_hj32_local_total_h37t_p44_product) = S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_c_hj32_local_total_h37t_p44)) /\ exists pa_q_hj32_local_total_h37t_p44_product_factor. pa_b_hj32_local_total_h37t_p44 = pa_q_hj32_local_total_h37t_p44_product_factor * S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_c_hj32_local_total_h37t_p44) + (pa_p_hj32_local_total_h37t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p44_product_partial. pa_h_hj32_local_total_h37t_p44_product_partial + S (pa_r_hj32_local_total_h37t_p44_product) = S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_partial. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_partial * S ((S (pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product) + (pa_r_hj32_local_total_h37t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p44_product_successor. pa_h_hj32_local_total_h37t_p44_product_successor + S (pa_s_hj32_local_total_h37t_p44_product) = S ((S (S pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product)) /\ exists pa_q_hj32_local_total_h37t_p44_product_successor. pa_u_hj32_local_total_h37t_p44_product = pa_q_hj32_local_total_h37t_p44_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p44_product)) * pa_v_hj32_local_total_h37t_p44_product) + (pa_s_hj32_local_total_h37t_p44_product))) /\ pa_s_hj32_local_total_h37t_p44_product = pa_r_hj32_local_total_h37t_p44_product * pa_p_hj32_local_total_h37t_p44_product))))))))
  21. 0021specialize htotal 44
  22. 0022specialize htotal 2 * 38
  23. 0023exact htotal
  24. 0024cases h37t_p44
  25. 0025have h37t_base : exists bqb_le_gap_hj32_h37t_base. bqb_le_gap_hj32_h37t_base + (38) = (44)
  26. 0026exists 6
  27. 0027norm_num
  28. 0028have h37t_to_44 : exists bqb_le_gap_hj32_local_base_bound_h37t_to_44. bqb_le_gap_hj32_local_base_bound_h37t_to_44 + (h) = (x)
  29. 0029specialize pow_base_monotone 38
  30. 0030specialize pow_base_monotone 44
  31. 0031specialize pow_base_monotone 2 * 38
  32. 0032specialize pow_base_monotone h
  33. 0033specialize pow_base_monotone x
  34. 0034apply pow_base_monotone
  35. 0035exact h37t_base
  36. 0036exact hh_route
  37. 0037exact h37t_p44_witness
  38. 0038have h37t_p4_exp : exists hj32_local_value_h37t_p4_exp. (exists pa_b_hj32_local_total_h37t_p4_exp pa_c_hj32_local_total_h37t_p4_exp. ((forall pa_i_hj32_local_total_h37t_p4_exp_repeat. (exists pa_lt_hj32_local_total_h37t_p4_exp_repeat_bound. pa_lt_hj32_local_total_h37t_p4_exp_repeat_bound + S pa_i_hj32_local_total_h37t_p4_exp_repeat = 2 * 38) -> (((exists pa_h_hj32_local_total_h37t_p4_exp_repeat_decoded. pa_h_hj32_local_total_h37t_p4_exp_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h37t_p4_exp_repeat)) * pa_c_hj32_local_total_h37t_p4_exp)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_repeat_decoded. pa_b_hj32_local_total_h37t_p4_exp = pa_q_hj32_local_total_h37t_p4_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p4_exp_repeat)) * pa_c_hj32_local_total_h37t_p4_exp) + (4)))) /\ (exists pa_u_hj32_local_total_h37t_p4_exp_product pa_v_hj32_local_total_h37t_p4_exp_product. ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_start. pa_h_hj32_local_total_h37t_p4_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_start. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_terminal. pa_h_hj32_local_total_h37t_p4_exp_product_terminal + S (hj32_local_value_h37t_p4_exp) = S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_terminal. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (hj32_local_value_h37t_p4_exp))) /\ forall pa_i_hj32_local_total_h37t_p4_exp_product. (exists pa_lt_hj32_local_total_h37t_p4_exp_product_bound. pa_lt_hj32_local_total_h37t_p4_exp_product_bound + S pa_i_hj32_local_total_h37t_p4_exp_product = 2 * 38) -> exists pa_p_hj32_local_total_h37t_p4_exp_product pa_r_hj32_local_total_h37t_p4_exp_product pa_s_hj32_local_total_h37t_p4_exp_product. ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_factor. pa_h_hj32_local_total_h37t_p4_exp_product_factor + S (pa_p_hj32_local_total_h37t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_c_hj32_local_total_h37t_p4_exp)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_factor. pa_b_hj32_local_total_h37t_p4_exp = pa_q_hj32_local_total_h37t_p4_exp_product_factor * S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_c_hj32_local_total_h37t_p4_exp) + (pa_p_hj32_local_total_h37t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_partial. pa_h_hj32_local_total_h37t_p4_exp_product_partial + S (pa_r_hj32_local_total_h37t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_partial. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_partial * S ((S (pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (pa_r_hj32_local_total_h37t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_exp_product_successor. pa_h_hj32_local_total_h37t_p4_exp_product_successor + S (pa_s_hj32_local_total_h37t_p4_exp_product) = S ((S (S pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p4_exp_product_successor. pa_u_hj32_local_total_h37t_p4_exp_product = pa_q_hj32_local_total_h37t_p4_exp_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p4_exp_product)) * pa_v_hj32_local_total_h37t_p4_exp_product) + (pa_s_hj32_local_total_h37t_p4_exp_product))) /\ pa_s_hj32_local_total_h37t_p4_exp_product = pa_r_hj32_local_total_h37t_p4_exp_product * pa_p_hj32_local_total_h37t_p4_exp_product))))))))
  39. 0039specialize htotal 4
  40. 0040specialize htotal 2 * 38
  41. 0041exact htotal
  42. 0042cases h37t_p4_exp
  43. 0043have h37t_p11_exp : exists hj32_local_value_h37t_p11_exp. (exists pa_b_hj32_local_total_h37t_p11_exp pa_c_hj32_local_total_h37t_p11_exp. ((forall pa_i_hj32_local_total_h37t_p11_exp_repeat. (exists pa_lt_hj32_local_total_h37t_p11_exp_repeat_bound. pa_lt_hj32_local_total_h37t_p11_exp_repeat_bound + S pa_i_hj32_local_total_h37t_p11_exp_repeat = 2 * 38) -> (((exists pa_h_hj32_local_total_h37t_p11_exp_repeat_decoded. pa_h_hj32_local_total_h37t_p11_exp_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_h37t_p11_exp_repeat)) * pa_c_hj32_local_total_h37t_p11_exp)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_repeat_decoded. pa_b_hj32_local_total_h37t_p11_exp = pa_q_hj32_local_total_h37t_p11_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p11_exp_repeat)) * pa_c_hj32_local_total_h37t_p11_exp) + (11)))) /\ (exists pa_u_hj32_local_total_h37t_p11_exp_product pa_v_hj32_local_total_h37t_p11_exp_product. ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_start. pa_h_hj32_local_total_h37t_p11_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_start. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_terminal. pa_h_hj32_local_total_h37t_p11_exp_product_terminal + S (hj32_local_value_h37t_p11_exp) = S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_terminal. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (hj32_local_value_h37t_p11_exp))) /\ forall pa_i_hj32_local_total_h37t_p11_exp_product. (exists pa_lt_hj32_local_total_h37t_p11_exp_product_bound. pa_lt_hj32_local_total_h37t_p11_exp_product_bound + S pa_i_hj32_local_total_h37t_p11_exp_product = 2 * 38) -> exists pa_p_hj32_local_total_h37t_p11_exp_product pa_r_hj32_local_total_h37t_p11_exp_product pa_s_hj32_local_total_h37t_p11_exp_product. ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_factor. pa_h_hj32_local_total_h37t_p11_exp_product_factor + S (pa_p_hj32_local_total_h37t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_c_hj32_local_total_h37t_p11_exp)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_factor. pa_b_hj32_local_total_h37t_p11_exp = pa_q_hj32_local_total_h37t_p11_exp_product_factor * S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_c_hj32_local_total_h37t_p11_exp) + (pa_p_hj32_local_total_h37t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_partial. pa_h_hj32_local_total_h37t_p11_exp_product_partial + S (pa_r_hj32_local_total_h37t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_partial. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_partial * S ((S (pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (pa_r_hj32_local_total_h37t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p11_exp_product_successor. pa_h_hj32_local_total_h37t_p11_exp_product_successor + S (pa_s_hj32_local_total_h37t_p11_exp_product) = S ((S (S pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h37t_p11_exp_product_successor. pa_u_hj32_local_total_h37t_p11_exp_product = pa_q_hj32_local_total_h37t_p11_exp_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p11_exp_product)) * pa_v_hj32_local_total_h37t_p11_exp_product) + (pa_s_hj32_local_total_h37t_p11_exp_product))) /\ pa_s_hj32_local_total_h37t_p11_exp_product = pa_r_hj32_local_total_h37t_p11_exp_product * pa_p_hj32_local_total_h37t_p11_exp_product))))))))
  44. 0044specialize htotal 11
  45. 0045specialize htotal 2 * 38
  46. 0046exact htotal
  47. 0047cases h37t_p11_exp
  48. 0048have h37t_p44_product_graph : exists pa_b_hj32_local_product_h37t_p44_product pa_c_hj32_local_product_h37t_p44_product. ((forall pa_i_hj32_local_product_h37t_p44_product_repeat. (exists pa_lt_hj32_local_product_h37t_p44_product_repeat_bound. pa_lt_hj32_local_product_h37t_p44_product_repeat_bound + S pa_i_hj32_local_product_h37t_p44_product_repeat = 2 * 38) -> (((exists pa_h_hj32_local_product_h37t_p44_product_repeat_decoded. pa_h_hj32_local_product_h37t_p44_product_repeat_decoded + S (4 * 11) = S ((S (pa_i_hj32_local_product_h37t_p44_product_repeat)) * pa_c_hj32_local_product_h37t_p44_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_repeat_decoded. pa_b_hj32_local_product_h37t_p44_product = pa_q_hj32_local_product_h37t_p44_product_repeat_decoded * S ((S (pa_i_hj32_local_product_h37t_p44_product_repeat)) * pa_c_hj32_local_product_h37t_p44_product) + (4 * 11)))) /\ (exists pa_u_hj32_local_product_h37t_p44_product_product pa_v_hj32_local_product_h37t_p44_product_product. ((((exists pa_h_hj32_local_product_h37t_p44_product_product_start. pa_h_hj32_local_product_h37t_p44_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_start. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_start * S ((S (0)) * pa_v_hj32_local_product_h37t_p44_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_h37t_p44_product_product_terminal. pa_h_hj32_local_product_h37t_p44_product_product_terminal + S (x) = S ((S (2 * 38)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_terminal. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_terminal * S ((S (2 * 38)) * pa_v_hj32_local_product_h37t_p44_product_product) + (x))) /\ forall pa_i_hj32_local_product_h37t_p44_product_product. (exists pa_lt_hj32_local_product_h37t_p44_product_product_bound. pa_lt_hj32_local_product_h37t_p44_product_product_bound + S pa_i_hj32_local_product_h37t_p44_product_product = 2 * 38) -> exists pa_p_hj32_local_product_h37t_p44_product_product pa_r_hj32_local_product_h37t_p44_product_product pa_s_hj32_local_product_h37t_p44_product_product. ((((exists pa_h_hj32_local_product_h37t_p44_product_product_factor. pa_h_hj32_local_product_h37t_p44_product_product_factor + S (pa_p_hj32_local_product_h37t_p44_product_product) = S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_c_hj32_local_product_h37t_p44_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_factor. pa_b_hj32_local_product_h37t_p44_product = pa_q_hj32_local_product_h37t_p44_product_product_factor * S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_c_hj32_local_product_h37t_p44_product) + (pa_p_hj32_local_product_h37t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h37t_p44_product_product_partial. pa_h_hj32_local_product_h37t_p44_product_product_partial + S (pa_r_hj32_local_product_h37t_p44_product_product) = S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_partial. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_partial * S ((S (pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product) + (pa_r_hj32_local_product_h37t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h37t_p44_product_product_successor. pa_h_hj32_local_product_h37t_p44_product_product_successor + S (pa_s_hj32_local_product_h37t_p44_product_product) = S ((S (S pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product)) /\ exists pa_q_hj32_local_product_h37t_p44_product_product_successor. pa_u_hj32_local_product_h37t_p44_product_product = pa_q_hj32_local_product_h37t_p44_product_product_successor * S ((S (S pa_i_hj32_local_product_h37t_p44_product_product)) * pa_v_hj32_local_product_h37t_p44_product_product) + (pa_s_hj32_local_product_h37t_p44_product_product))) /\ pa_s_hj32_local_product_h37t_p44_product_product = pa_r_hj32_local_product_h37t_p44_product_product * pa_p_hj32_local_product_h37t_p44_product_product)))))))
  49. 0049have h37t_p44_product_base : 4 * 11 = 44
  50. 0050norm_num
  51. 0051rewrite h37t_p44_product_base
  52. 0052rewrite h37t_p44_product_base
  53. 0053exact h37t_p44_witness
  54. 0054have h37t_p44_product : x = x1 * x2
  55. 0055specialize pow_mul_base 4
  56. 0056specialize pow_mul_base 11
  57. 0057specialize pow_mul_base 2 * 38
  58. 0058specialize pow_mul_base x1
  59. 0059specialize pow_mul_base x2
  60. 0060specialize pow_mul_base x
  61. 0061apply pow_mul_base
  62. 0062exact h37t_p4_exp_witness
  63. 0063exact h37t_p11_exp_witness
  64. 0064exact h37t_p44_product_graph
  65. 0065have h37t_p4_tail : exists hj32_local_value_h37t_p4_tail. (exists pa_b_hj32_local_total_h37t_p4_tail pa_c_hj32_local_total_h37t_p4_tail. ((forall pa_i_hj32_local_total_h37t_p4_tail_repeat. (exists pa_lt_hj32_local_total_h37t_p4_tail_repeat_bound. pa_lt_hj32_local_total_h37t_p4_tail_repeat_bound + S pa_i_hj32_local_total_h37t_p4_tail_repeat = 7 * 19) -> (((exists pa_h_hj32_local_total_h37t_p4_tail_repeat_decoded. pa_h_hj32_local_total_h37t_p4_tail_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h37t_p4_tail_repeat)) * pa_c_hj32_local_total_h37t_p4_tail)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_repeat_decoded. pa_b_hj32_local_total_h37t_p4_tail = pa_q_hj32_local_total_h37t_p4_tail_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p4_tail_repeat)) * pa_c_hj32_local_total_h37t_p4_tail) + (4)))) /\ (exists pa_u_hj32_local_total_h37t_p4_tail_product pa_v_hj32_local_total_h37t_p4_tail_product. ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_start. pa_h_hj32_local_total_h37t_p4_tail_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_start. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_terminal. pa_h_hj32_local_total_h37t_p4_tail_product_terminal + S (hj32_local_value_h37t_p4_tail) = S ((S (7 * 19)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_terminal. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_terminal * S ((S (7 * 19)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (hj32_local_value_h37t_p4_tail))) /\ forall pa_i_hj32_local_total_h37t_p4_tail_product. (exists pa_lt_hj32_local_total_h37t_p4_tail_product_bound. pa_lt_hj32_local_total_h37t_p4_tail_product_bound + S pa_i_hj32_local_total_h37t_p4_tail_product = 7 * 19) -> exists pa_p_hj32_local_total_h37t_p4_tail_product pa_r_hj32_local_total_h37t_p4_tail_product pa_s_hj32_local_total_h37t_p4_tail_product. ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_factor. pa_h_hj32_local_total_h37t_p4_tail_product_factor + S (pa_p_hj32_local_total_h37t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_c_hj32_local_total_h37t_p4_tail)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_factor. pa_b_hj32_local_total_h37t_p4_tail = pa_q_hj32_local_total_h37t_p4_tail_product_factor * S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_c_hj32_local_total_h37t_p4_tail) + (pa_p_hj32_local_total_h37t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_partial. pa_h_hj32_local_total_h37t_p4_tail_product_partial + S (pa_r_hj32_local_total_h37t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_partial. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_partial * S ((S (pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (pa_r_hj32_local_total_h37t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_tail_product_successor. pa_h_hj32_local_total_h37t_p4_tail_product_successor + S (pa_s_hj32_local_total_h37t_p4_tail_product) = S ((S (S pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h37t_p4_tail_product_successor. pa_u_hj32_local_total_h37t_p4_tail_product = pa_q_hj32_local_total_h37t_p4_tail_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p4_tail_product)) * pa_v_hj32_local_total_h37t_p4_tail_product) + (pa_s_hj32_local_total_h37t_p4_tail_product))) /\ pa_s_hj32_local_total_h37t_p4_tail_product = pa_r_hj32_local_total_h37t_p4_tail_product * pa_p_hj32_local_total_h37t_p4_tail_product))))))))
  66. 0066specialize htotal 4
  67. 0067specialize htotal 7 * 19
  68. 0068exact htotal
  69. 0069cases h37t_p4_tail
  70. 0070have h37t_parity : 7 * 38 = 2 * (7 * 19)
  71. 0071have h37t_root : 38 = 2 * 19
  72. 0072norm_num
  73. 0073rewrite h37t_root
  74. 0074trans (7 * 2) * 19
  75. 0075symm
  76. 0076specialize mul_assoc 7
  77. 0077specialize mul_assoc 2
  78. 0078specialize mul_assoc 19
  79. 0079apply mul_assoc
  80. 0080trans (2 * 7) * 19
  81. 0081congr
  82. 0082specialize mul_comm 7
  83. 0083specialize mul_comm 2
  84. 0084apply mul_comm
  85. 0085refl
  86. 0086specialize mul_assoc 2
  87. 0087specialize mul_assoc 7
  88. 0088specialize mul_assoc 19
  89. 0089apply mul_assoc
  90. 0090have h37t_eleven_bound : exists bqb_le_gap_hj32_h37t_eleven_bound. bqb_le_gap_hj32_h37t_eleven_bound + (x2) = (x3)
  91. 0091specialize pow_eleven_double_block_le_pow_four_even_from_total 38
  92. 0092specialize pow_eleven_double_block_le_pow_four_even_from_total (7 * 19)
  93. 0093specialize pow_eleven_double_block_le_pow_four_even_from_total x2
  94. 0094specialize pow_eleven_double_block_le_pow_four_even_from_total x3
  95. 0095apply pow_eleven_double_block_le_pow_four_even_from_total
  96. 0096exact htotal
  97. 0097exact h37t_parity
  98. 0098exact h37t_p11_exp_witness
  99. 0099exact h37t_p4_tail_witness
  100. 0100have h37t_four_refl : exists bqb_le_gap_hj32_h37t_four_refl. bqb_le_gap_hj32_h37t_four_refl + (x1) = (x1)
  101. 0101specialize le_refl x1
  102. 0102exact le_refl
  103. 0103have h37t_product_bound : exists bqb_le_gap_hj32_local_product_bound_h37t_product_bound. bqb_le_gap_hj32_local_product_bound_h37t_product_bound + (x1 * x2) = (x1 * x3)
  104. 0104specialize mul_le_mul x1
  105. 0105specialize mul_le_mul x1
  106. 0106specialize mul_le_mul x2
  107. 0107specialize mul_le_mul x3
  108. 0108apply mul_le_mul
  109. 0109exact h37t_four_refl
  110. 0110exact h37t_eleven_bound
  111. 0111have h37t_p4_budget : exists hj32_local_value_h37t_p4_budget. (exists pa_b_hj32_local_total_h37t_p4_budget pa_c_hj32_local_total_h37t_p4_budget. ((forall pa_i_hj32_local_total_h37t_p4_budget_repeat. (exists pa_lt_hj32_local_total_h37t_p4_budget_repeat_bound. pa_lt_hj32_local_total_h37t_p4_budget_repeat_bound + S pa_i_hj32_local_total_h37t_p4_budget_repeat = 2 * 38 + 7 * 19) -> (((exists pa_h_hj32_local_total_h37t_p4_budget_repeat_decoded. pa_h_hj32_local_total_h37t_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h37t_p4_budget_repeat)) * pa_c_hj32_local_total_h37t_p4_budget)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_repeat_decoded. pa_b_hj32_local_total_h37t_p4_budget = pa_q_hj32_local_total_h37t_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h37t_p4_budget_repeat)) * pa_c_hj32_local_total_h37t_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h37t_p4_budget_product pa_v_hj32_local_total_h37t_p4_budget_product. ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_start. pa_h_hj32_local_total_h37t_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_start. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_terminal. pa_h_hj32_local_total_h37t_p4_budget_product_terminal + S (hj32_local_value_h37t_p4_budget) = S ((S (2 * 38 + 7 * 19)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_terminal. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_terminal * S ((S (2 * 38 + 7 * 19)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (hj32_local_value_h37t_p4_budget))) /\ forall pa_i_hj32_local_total_h37t_p4_budget_product. (exists pa_lt_hj32_local_total_h37t_p4_budget_product_bound. pa_lt_hj32_local_total_h37t_p4_budget_product_bound + S pa_i_hj32_local_total_h37t_p4_budget_product = 2 * 38 + 7 * 19) -> exists pa_p_hj32_local_total_h37t_p4_budget_product pa_r_hj32_local_total_h37t_p4_budget_product pa_s_hj32_local_total_h37t_p4_budget_product. ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_factor. pa_h_hj32_local_total_h37t_p4_budget_product_factor + S (pa_p_hj32_local_total_h37t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_c_hj32_local_total_h37t_p4_budget)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_factor. pa_b_hj32_local_total_h37t_p4_budget = pa_q_hj32_local_total_h37t_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_c_hj32_local_total_h37t_p4_budget) + (pa_p_hj32_local_total_h37t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_partial. pa_h_hj32_local_total_h37t_p4_budget_product_partial + S (pa_r_hj32_local_total_h37t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_partial. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (pa_r_hj32_local_total_h37t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h37t_p4_budget_product_successor. pa_h_hj32_local_total_h37t_p4_budget_product_successor + S (pa_s_hj32_local_total_h37t_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h37t_p4_budget_product_successor. pa_u_hj32_local_total_h37t_p4_budget_product = pa_q_hj32_local_total_h37t_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h37t_p4_budget_product)) * pa_v_hj32_local_total_h37t_p4_budget_product) + (pa_s_hj32_local_total_h37t_p4_budget_product))) /\ pa_s_hj32_local_total_h37t_p4_budget_product = pa_r_hj32_local_total_h37t_p4_budget_product * pa_p_hj32_local_total_h37t_p4_budget_product))))))))
  112. 0112specialize htotal 4
  113. 0113specialize htotal 2 * 38 + 7 * 19
  114. 0114exact htotal
  115. 0115cases h37t_p4_budget
  116. 0116have h37t_budget_product : x4 = x1 * x3
  117. 0117specialize pow_add 4
  118. 0118specialize pow_add 2 * 38
  119. 0119specialize pow_add 7 * 19
  120. 0120specialize pow_add 2 * 38 + 7 * 19
  121. 0121specialize pow_add x1
  122. 0122specialize pow_add x3
  123. 0123specialize pow_add x4
  124. 0124apply pow_add
  125. 0125refl
  126. 0126exact h37t_p4_exp_witness
  127. 0127exact h37t_p4_tail_witness
  128. 0128exact h37t_p4_budget_witness
  129. 0129rewrite <- h37t_p44_product at h37t_product_bound
  130. 0130rewrite <- h37t_budget_product at h37t_product_bound
  131. 0131have h37t_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h37t_to_budget. bqb_le_gap_hj32_local_trans_bound_h37t_to_budget + (h) = (x4)
  132. 0132specialize le_trans h
  133. 0133specialize le_trans x
  134. 0134specialize le_trans x4
  135. 0135apply le_trans
  136. 0136exact h37t_to_44
  137. 0137exact h37t_product_bound
  138. 0138have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_37. bqb_le_gap_hj32_scaled_budget_root_37 + (6 * (2 * 38 + 7 * 19)) = (37 * 37)
  139. 0139apply bertrand_scaled_budget_root_37
  140. 0140have hbudget_exponent : exists bqb_le_gap_hj32_h_37_budget_exponent. bqb_le_gap_hj32_h_37_budget_exponent + (2 * 38 + 7 * 19) = (e)
  141. 0141specialize ceil_div_six_budget_of_scaled_le (37 * 37)
  142. 0142specialize ceil_div_six_budget_of_scaled_le (2 * 38 + 7 * 19)
  143. 0143specialize ceil_div_six_budget_of_scaled_le e
  144. 0144apply ceil_div_six_budget_of_scaled_le
  145. 0145exact hceiling
  146. 0146exact hscaled
  147. 0147have h37_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h37_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h37_budget_growth + (x4) = (u)
  148. 0148specialize pow_exponent_monotone_from_total 4
  149. 0149specialize pow_exponent_monotone_from_total 2 * 38 + 7 * 19
  150. 0150specialize pow_exponent_monotone_from_total e
  151. 0151specialize pow_exponent_monotone_from_total x4
  152. 0152specialize pow_exponent_monotone_from_total u
  153. 0153apply pow_exponent_monotone_from_total
  154. 0154exact htotal
  155. 0155exists 3
  156. 0156norm_num
  157. 0157exact hbudget_exponent
  158. 0158exact h37t_p4_budget_witness
  159. 0159exact hu
  160. 0160have h37_result : exists bqb_le_gap_hj32_local_trans_bound_h37_result. bqb_le_gap_hj32_local_trans_bound_h37_result + (h) = (u)
  161. 0161specialize le_trans h
  162. 0162specialize le_trans x4
  163. 0163specialize le_trans u
  164. 0164apply le_trans
  165. 0165exact h37t_to_budget
  166. 0166exact h37_budget_growth
  167. 0167exact h37_result