BT00WT

bertrand_h_root_36_from_total

Alpha body-checked · checked-use disabled

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

Exact expanded PA statement

forall e h u. (forall bpt_a_hj32_h_root_36 bpt_e_hj32_h_root_36. exists bpt_x_hj32_h_root_36. (exists ff_b_bpt_value_hj32_h_root_36 ff_c_bpt_value_hj32_h_root_36. ((forall ff_i_bpt_value_hj32_h_root_36_repeat. (exists ff_lt_bpt_value_hj32_h_root_36_repeat_bound. ff_lt_bpt_value_hj32_h_root_36_repeat_bound + S ff_i_bpt_value_hj32_h_root_36_repeat = bpt_e_hj32_h_root_36) -> (((exists ff_h_bpt_value_hj32_h_root_36_repeat_decoded. ff_h_bpt_value_hj32_h_root_36_repeat_decoded + S (bpt_a_hj32_h_root_36) = S ((S (ff_i_bpt_value_hj32_h_root_36_repeat)) * ff_c_bpt_value_hj32_h_root_36)) /\ exists ff_q_bpt_value_hj32_h_root_36_repeat_decoded. ff_b_bpt_value_hj32_h_root_36 = ff_q_bpt_value_hj32_h_root_36_repeat_decoded * S ((S (ff_i_bpt_value_hj32_h_root_36_repeat)) * ff_c_bpt_value_hj32_h_root_36) + (bpt_a_hj32_h_root_36)))) /\ (exists ff_u_bpt_value_hj32_h_root_36_product ff_v_bpt_value_hj32_h_root_36_product. ((((exists ff_h_bpt_value_hj32_h_root_36_product_start. ff_h_bpt_value_hj32_h_root_36_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_start. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_start * S ((S (0)) * ff_v_bpt_value_hj32_h_root_36_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_h_root_36_product_terminal. ff_h_bpt_value_hj32_h_root_36_product_terminal + S (bpt_x_hj32_h_root_36) = S ((S (bpt_e_hj32_h_root_36)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_terminal. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_terminal * S ((S (bpt_e_hj32_h_root_36)) * ff_v_bpt_value_hj32_h_root_36_product) + (bpt_x_hj32_h_root_36))) /\ forall ff_i_bpt_value_hj32_h_root_36_product. (exists ff_lt_bpt_value_hj32_h_root_36_product_bound. ff_lt_bpt_value_hj32_h_root_36_product_bound + S ff_i_bpt_value_hj32_h_root_36_product = bpt_e_hj32_h_root_36) -> exists ff_p_bpt_value_hj32_h_root_36_product ff_r_bpt_value_hj32_h_root_36_product ff_s_bpt_value_hj32_h_root_36_product. ((((exists ff_h_bpt_value_hj32_h_root_36_product_factor. ff_h_bpt_value_hj32_h_root_36_product_factor + S (ff_p_bpt_value_hj32_h_root_36_product) = S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_c_bpt_value_hj32_h_root_36)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_factor. ff_b_bpt_value_hj32_h_root_36 = ff_q_bpt_value_hj32_h_root_36_product_factor * S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_c_bpt_value_hj32_h_root_36) + (ff_p_bpt_value_hj32_h_root_36_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_36_product_partial. ff_h_bpt_value_hj32_h_root_36_product_partial + S (ff_r_bpt_value_hj32_h_root_36_product) = S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_partial. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_partial * S ((S (ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product) + (ff_r_bpt_value_hj32_h_root_36_product))) /\ ((((exists ff_h_bpt_value_hj32_h_root_36_product_successor. ff_h_bpt_value_hj32_h_root_36_product_successor + S (ff_s_bpt_value_hj32_h_root_36_product) = S ((S (S ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product)) /\ exists ff_q_bpt_value_hj32_h_root_36_product_successor. ff_u_bpt_value_hj32_h_root_36_product = ff_q_bpt_value_hj32_h_root_36_product_successor * S ((S (S ff_i_bpt_value_hj32_h_root_36_product)) * ff_v_bpt_value_hj32_h_root_36_product) + (ff_s_bpt_value_hj32_h_root_36_product))) /\ ff_s_bpt_value_hj32_h_root_36_product = ff_r_bpt_value_hj32_h_root_36_product * ff_p_bpt_value_hj32_h_root_36_product))))))))) -> (((exists bcs_lower_gap_hj32_h_root_36_ceiling. bcs_lower_gap_hj32_h_root_36_ceiling + (36 * 36) = 6 * (e)) /\ exists bcs_upper_gap_hj32_h_root_36_ceiling. bcs_upper_gap_hj32_h_root_36_ceiling + S (6 * (e)) = (36 * 36) + 6)) -> (exists pa_b_hj32_h_root_36_h pa_c_hj32_h_root_36_h. ((forall pa_i_hj32_h_root_36_h_repeat. (exists pa_lt_hj32_h_root_36_h_repeat_bound. pa_lt_hj32_h_root_36_h_repeat_bound + S pa_i_hj32_h_root_36_h_repeat = 2 * 36 + 2) -> (((exists pa_h_hj32_h_root_36_h_repeat_decoded. pa_h_hj32_h_root_36_h_repeat_decoded + S (36 + 1) = S ((S (pa_i_hj32_h_root_36_h_repeat)) * pa_c_hj32_h_root_36_h)) /\ exists pa_q_hj32_h_root_36_h_repeat_decoded. pa_b_hj32_h_root_36_h = pa_q_hj32_h_root_36_h_repeat_decoded * S ((S (pa_i_hj32_h_root_36_h_repeat)) * pa_c_hj32_h_root_36_h) + (36 + 1)))) /\ (exists pa_u_hj32_h_root_36_h_product pa_v_hj32_h_root_36_h_product. ((((exists pa_h_hj32_h_root_36_h_product_start. pa_h_hj32_h_root_36_h_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_start. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_start * S ((S (0)) * pa_v_hj32_h_root_36_h_product) + (1))) /\ ((((exists pa_h_hj32_h_root_36_h_product_terminal. pa_h_hj32_h_root_36_h_product_terminal + S (h) = S ((S (2 * 36 + 2)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_terminal. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_terminal * S ((S (2 * 36 + 2)) * pa_v_hj32_h_root_36_h_product) + (h))) /\ forall pa_i_hj32_h_root_36_h_product. (exists pa_lt_hj32_h_root_36_h_product_bound. pa_lt_hj32_h_root_36_h_product_bound + S pa_i_hj32_h_root_36_h_product = 2 * 36 + 2) -> exists pa_p_hj32_h_root_36_h_product pa_r_hj32_h_root_36_h_product pa_s_hj32_h_root_36_h_product. ((((exists pa_h_hj32_h_root_36_h_product_factor. pa_h_hj32_h_root_36_h_product_factor + S (pa_p_hj32_h_root_36_h_product) = S ((S (pa_i_hj32_h_root_36_h_product)) * pa_c_hj32_h_root_36_h)) /\ exists pa_q_hj32_h_root_36_h_product_factor. pa_b_hj32_h_root_36_h = pa_q_hj32_h_root_36_h_product_factor * S ((S (pa_i_hj32_h_root_36_h_product)) * pa_c_hj32_h_root_36_h) + (pa_p_hj32_h_root_36_h_product))) /\ ((((exists pa_h_hj32_h_root_36_h_product_partial. pa_h_hj32_h_root_36_h_product_partial + S (pa_r_hj32_h_root_36_h_product) = S ((S (pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_partial. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_partial * S ((S (pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product) + (pa_r_hj32_h_root_36_h_product))) /\ ((((exists pa_h_hj32_h_root_36_h_product_successor. pa_h_hj32_h_root_36_h_product_successor + S (pa_s_hj32_h_root_36_h_product) = S ((S (S pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product)) /\ exists pa_q_hj32_h_root_36_h_product_successor. pa_u_hj32_h_root_36_h_product = pa_q_hj32_h_root_36_h_product_successor * S ((S (S pa_i_hj32_h_root_36_h_product)) * pa_v_hj32_h_root_36_h_product) + (pa_s_hj32_h_root_36_h_product))) /\ pa_s_hj32_h_root_36_h_product = pa_r_hj32_h_root_36_h_product * pa_p_hj32_h_root_36_h_product)))))))) -> (exists pa_b_hj32_h_root_36_u pa_c_hj32_h_root_36_u. ((forall pa_i_hj32_h_root_36_u_repeat. (exists pa_lt_hj32_h_root_36_u_repeat_bound. pa_lt_hj32_h_root_36_u_repeat_bound + S pa_i_hj32_h_root_36_u_repeat = e) -> (((exists pa_h_hj32_h_root_36_u_repeat_decoded. pa_h_hj32_h_root_36_u_repeat_decoded + S (4) = S ((S (pa_i_hj32_h_root_36_u_repeat)) * pa_c_hj32_h_root_36_u)) /\ exists pa_q_hj32_h_root_36_u_repeat_decoded. pa_b_hj32_h_root_36_u = pa_q_hj32_h_root_36_u_repeat_decoded * S ((S (pa_i_hj32_h_root_36_u_repeat)) * pa_c_hj32_h_root_36_u) + (4)))) /\ (exists pa_u_hj32_h_root_36_u_product pa_v_hj32_h_root_36_u_product. ((((exists pa_h_hj32_h_root_36_u_product_start. pa_h_hj32_h_root_36_u_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_start. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_start * S ((S (0)) * pa_v_hj32_h_root_36_u_product) + (1))) /\ ((((exists pa_h_hj32_h_root_36_u_product_terminal. pa_h_hj32_h_root_36_u_product_terminal + S (u) = S ((S (e)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_terminal. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_terminal * S ((S (e)) * pa_v_hj32_h_root_36_u_product) + (u))) /\ forall pa_i_hj32_h_root_36_u_product. (exists pa_lt_hj32_h_root_36_u_product_bound. pa_lt_hj32_h_root_36_u_product_bound + S pa_i_hj32_h_root_36_u_product = e) -> exists pa_p_hj32_h_root_36_u_product pa_r_hj32_h_root_36_u_product pa_s_hj32_h_root_36_u_product. ((((exists pa_h_hj32_h_root_36_u_product_factor. pa_h_hj32_h_root_36_u_product_factor + S (pa_p_hj32_h_root_36_u_product) = S ((S (pa_i_hj32_h_root_36_u_product)) * pa_c_hj32_h_root_36_u)) /\ exists pa_q_hj32_h_root_36_u_product_factor. pa_b_hj32_h_root_36_u = pa_q_hj32_h_root_36_u_product_factor * S ((S (pa_i_hj32_h_root_36_u_product)) * pa_c_hj32_h_root_36_u) + (pa_p_hj32_h_root_36_u_product))) /\ ((((exists pa_h_hj32_h_root_36_u_product_partial. pa_h_hj32_h_root_36_u_product_partial + S (pa_r_hj32_h_root_36_u_product) = S ((S (pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_partial. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_partial * S ((S (pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product) + (pa_r_hj32_h_root_36_u_product))) /\ ((((exists pa_h_hj32_h_root_36_u_product_successor. pa_h_hj32_h_root_36_u_product_successor + S (pa_s_hj32_h_root_36_u_product) = S ((S (S pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product)) /\ exists pa_q_hj32_h_root_36_u_product_successor. pa_u_hj32_h_root_36_u_product = pa_q_hj32_h_root_36_u_product_successor * S ((S (S pa_i_hj32_h_root_36_u_product)) * pa_v_hj32_h_root_36_u_product) + (pa_s_hj32_h_root_36_u_product))) /\ pa_s_hj32_h_root_36_u_product = pa_r_hj32_h_root_36_u_product * pa_p_hj32_h_root_36_u_product)))))))) -> (exists bqb_le_gap_hj32_h_root_36_result. bqb_le_gap_hj32_h_root_36_result + (h) = (u))

Structural proof guide

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

Direct prerequisites: bertrand_scaled_budget_root_36, ceil_div_six_budget_of_scaled_le, pow_eleven_double_block_le_pow_four_odd_from_total, pow_mul_base, pow_add, pow_base_monotone, pow_exponent_monotone_from_total, mul_le_mul, le_refl, le_trans, mul_add, mul_assoc, add_assoc. The authored body proceeds by case analysis (5), intermediate claims (45), equality transport (30), closed numeral normalization (13).

Proof neighborhood

Direct dependencies

BT00WC bertrand_scaled_budget_root_36 BT00WE ceil_div_six_budget_of_scaled_le BT00WM pow_eleven_double_block_le_pow_four_odd_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 BT0007 mul_add BT0008 mul_assoc BT0003 add_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_36_route pa_c_hj32_h_36_route. ((forall pa_i_hj32_h_36_route_repeat. (exists pa_lt_hj32_h_36_route_repeat_bound. pa_lt_hj32_h_36_route_repeat_bound + S pa_i_hj32_h_36_route_repeat = 2 * 37) -> (((exists pa_h_hj32_h_36_route_repeat_decoded. pa_h_hj32_h_36_route_repeat_decoded + S (37) = S ((S (pa_i_hj32_h_36_route_repeat)) * pa_c_hj32_h_36_route)) /\ exists pa_q_hj32_h_36_route_repeat_decoded. pa_b_hj32_h_36_route = pa_q_hj32_h_36_route_repeat_decoded * S ((S (pa_i_hj32_h_36_route_repeat)) * pa_c_hj32_h_36_route) + (37)))) /\ (exists pa_u_hj32_h_36_route_product pa_v_hj32_h_36_route_product. ((((exists pa_h_hj32_h_36_route_product_start. pa_h_hj32_h_36_route_product_start + S (1) = S ((S (0)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_start. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_start * S ((S (0)) * pa_v_hj32_h_36_route_product) + (1))) /\ ((((exists pa_h_hj32_h_36_route_product_terminal. pa_h_hj32_h_36_route_product_terminal + S (h) = S ((S (2 * 37)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_terminal. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_terminal * S ((S (2 * 37)) * pa_v_hj32_h_36_route_product) + (h))) /\ forall pa_i_hj32_h_36_route_product. (exists pa_lt_hj32_h_36_route_product_bound. pa_lt_hj32_h_36_route_product_bound + S pa_i_hj32_h_36_route_product = 2 * 37) -> exists pa_p_hj32_h_36_route_product pa_r_hj32_h_36_route_product pa_s_hj32_h_36_route_product. ((((exists pa_h_hj32_h_36_route_product_factor. pa_h_hj32_h_36_route_product_factor + S (pa_p_hj32_h_36_route_product) = S ((S (pa_i_hj32_h_36_route_product)) * pa_c_hj32_h_36_route)) /\ exists pa_q_hj32_h_36_route_product_factor. pa_b_hj32_h_36_route = pa_q_hj32_h_36_route_product_factor * S ((S (pa_i_hj32_h_36_route_product)) * pa_c_hj32_h_36_route) + (pa_p_hj32_h_36_route_product))) /\ ((((exists pa_h_hj32_h_36_route_product_partial. pa_h_hj32_h_36_route_product_partial + S (pa_r_hj32_h_36_route_product) = S ((S (pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_partial. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_partial * S ((S (pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product) + (pa_r_hj32_h_36_route_product))) /\ ((((exists pa_h_hj32_h_36_route_product_successor. pa_h_hj32_h_36_route_product_successor + S (pa_s_hj32_h_36_route_product) = S ((S (S pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product)) /\ exists pa_q_hj32_h_36_route_product_successor. pa_u_hj32_h_36_route_product = pa_q_hj32_h_36_route_product_successor * S ((S (S pa_i_hj32_h_36_route_product)) * pa_v_hj32_h_36_route_product) + (pa_s_hj32_h_36_route_product))) /\ pa_s_hj32_h_36_route_product = pa_r_hj32_h_36_route_product * pa_p_hj32_h_36_route_product)))))))
  9. 0009have hh_base : 36 + 1 = 37
  10. 0010norm_num
  11. 0011have hh_exponent : 2 * 36 + 2 = 2 * 37
  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 h36t_p44 : exists hj32_local_value_h36t_p44. (exists pa_b_hj32_local_total_h36t_p44 pa_c_hj32_local_total_h36t_p44. ((forall pa_i_hj32_local_total_h36t_p44_repeat. (exists pa_lt_hj32_local_total_h36t_p44_repeat_bound. pa_lt_hj32_local_total_h36t_p44_repeat_bound + S pa_i_hj32_local_total_h36t_p44_repeat = 2 * 37) -> (((exists pa_h_hj32_local_total_h36t_p44_repeat_decoded. pa_h_hj32_local_total_h36t_p44_repeat_decoded + S (44) = S ((S (pa_i_hj32_local_total_h36t_p44_repeat)) * pa_c_hj32_local_total_h36t_p44)) /\ exists pa_q_hj32_local_total_h36t_p44_repeat_decoded. pa_b_hj32_local_total_h36t_p44 = pa_q_hj32_local_total_h36t_p44_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p44_repeat)) * pa_c_hj32_local_total_h36t_p44) + (44)))) /\ (exists pa_u_hj32_local_total_h36t_p44_product pa_v_hj32_local_total_h36t_p44_product. ((((exists pa_h_hj32_local_total_h36t_p44_product_start. pa_h_hj32_local_total_h36t_p44_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_start. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p44_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p44_product_terminal. pa_h_hj32_local_total_h36t_p44_product_terminal + S (hj32_local_value_h36t_p44) = S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_terminal. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p44_product) + (hj32_local_value_h36t_p44))) /\ forall pa_i_hj32_local_total_h36t_p44_product. (exists pa_lt_hj32_local_total_h36t_p44_product_bound. pa_lt_hj32_local_total_h36t_p44_product_bound + S pa_i_hj32_local_total_h36t_p44_product = 2 * 37) -> exists pa_p_hj32_local_total_h36t_p44_product pa_r_hj32_local_total_h36t_p44_product pa_s_hj32_local_total_h36t_p44_product. ((((exists pa_h_hj32_local_total_h36t_p44_product_factor. pa_h_hj32_local_total_h36t_p44_product_factor + S (pa_p_hj32_local_total_h36t_p44_product) = S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_c_hj32_local_total_h36t_p44)) /\ exists pa_q_hj32_local_total_h36t_p44_product_factor. pa_b_hj32_local_total_h36t_p44 = pa_q_hj32_local_total_h36t_p44_product_factor * S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_c_hj32_local_total_h36t_p44) + (pa_p_hj32_local_total_h36t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p44_product_partial. pa_h_hj32_local_total_h36t_p44_product_partial + S (pa_r_hj32_local_total_h36t_p44_product) = S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_partial. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_partial * S ((S (pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product) + (pa_r_hj32_local_total_h36t_p44_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p44_product_successor. pa_h_hj32_local_total_h36t_p44_product_successor + S (pa_s_hj32_local_total_h36t_p44_product) = S ((S (S pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product)) /\ exists pa_q_hj32_local_total_h36t_p44_product_successor. pa_u_hj32_local_total_h36t_p44_product = pa_q_hj32_local_total_h36t_p44_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p44_product)) * pa_v_hj32_local_total_h36t_p44_product) + (pa_s_hj32_local_total_h36t_p44_product))) /\ pa_s_hj32_local_total_h36t_p44_product = pa_r_hj32_local_total_h36t_p44_product * pa_p_hj32_local_total_h36t_p44_product))))))))
  21. 0021specialize htotal 44
  22. 0022specialize htotal 2 * 37
  23. 0023exact htotal
  24. 0024cases h36t_p44
  25. 0025have h36t_base : exists bqb_le_gap_hj32_h36t_base. bqb_le_gap_hj32_h36t_base + (37) = (44)
  26. 0026exists 7
  27. 0027norm_num
  28. 0028have h36t_to_44 : exists bqb_le_gap_hj32_local_base_bound_h36t_to_44. bqb_le_gap_hj32_local_base_bound_h36t_to_44 + (h) = (x)
  29. 0029specialize pow_base_monotone 37
  30. 0030specialize pow_base_monotone 44
  31. 0031specialize pow_base_monotone 2 * 37
  32. 0032specialize pow_base_monotone h
  33. 0033specialize pow_base_monotone x
  34. 0034apply pow_base_monotone
  35. 0035exact h36t_base
  36. 0036exact hh_route
  37. 0037exact h36t_p44_witness
  38. 0038have h36t_p4_exp : exists hj32_local_value_h36t_p4_exp. (exists pa_b_hj32_local_total_h36t_p4_exp pa_c_hj32_local_total_h36t_p4_exp. ((forall pa_i_hj32_local_total_h36t_p4_exp_repeat. (exists pa_lt_hj32_local_total_h36t_p4_exp_repeat_bound. pa_lt_hj32_local_total_h36t_p4_exp_repeat_bound + S pa_i_hj32_local_total_h36t_p4_exp_repeat = 2 * 37) -> (((exists pa_h_hj32_local_total_h36t_p4_exp_repeat_decoded. pa_h_hj32_local_total_h36t_p4_exp_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h36t_p4_exp_repeat)) * pa_c_hj32_local_total_h36t_p4_exp)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_repeat_decoded. pa_b_hj32_local_total_h36t_p4_exp = pa_q_hj32_local_total_h36t_p4_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p4_exp_repeat)) * pa_c_hj32_local_total_h36t_p4_exp) + (4)))) /\ (exists pa_u_hj32_local_total_h36t_p4_exp_product pa_v_hj32_local_total_h36t_p4_exp_product. ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_start. pa_h_hj32_local_total_h36t_p4_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_start. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_terminal. pa_h_hj32_local_total_h36t_p4_exp_product_terminal + S (hj32_local_value_h36t_p4_exp) = S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_terminal. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (hj32_local_value_h36t_p4_exp))) /\ forall pa_i_hj32_local_total_h36t_p4_exp_product. (exists pa_lt_hj32_local_total_h36t_p4_exp_product_bound. pa_lt_hj32_local_total_h36t_p4_exp_product_bound + S pa_i_hj32_local_total_h36t_p4_exp_product = 2 * 37) -> exists pa_p_hj32_local_total_h36t_p4_exp_product pa_r_hj32_local_total_h36t_p4_exp_product pa_s_hj32_local_total_h36t_p4_exp_product. ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_factor. pa_h_hj32_local_total_h36t_p4_exp_product_factor + S (pa_p_hj32_local_total_h36t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_c_hj32_local_total_h36t_p4_exp)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_factor. pa_b_hj32_local_total_h36t_p4_exp = pa_q_hj32_local_total_h36t_p4_exp_product_factor * S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_c_hj32_local_total_h36t_p4_exp) + (pa_p_hj32_local_total_h36t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_partial. pa_h_hj32_local_total_h36t_p4_exp_product_partial + S (pa_r_hj32_local_total_h36t_p4_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_partial. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_partial * S ((S (pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (pa_r_hj32_local_total_h36t_p4_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_exp_product_successor. pa_h_hj32_local_total_h36t_p4_exp_product_successor + S (pa_s_hj32_local_total_h36t_p4_exp_product) = S ((S (S pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p4_exp_product_successor. pa_u_hj32_local_total_h36t_p4_exp_product = pa_q_hj32_local_total_h36t_p4_exp_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p4_exp_product)) * pa_v_hj32_local_total_h36t_p4_exp_product) + (pa_s_hj32_local_total_h36t_p4_exp_product))) /\ pa_s_hj32_local_total_h36t_p4_exp_product = pa_r_hj32_local_total_h36t_p4_exp_product * pa_p_hj32_local_total_h36t_p4_exp_product))))))))
  39. 0039specialize htotal 4
  40. 0040specialize htotal 2 * 37
  41. 0041exact htotal
  42. 0042cases h36t_p4_exp
  43. 0043have h36t_p11_exp : exists hj32_local_value_h36t_p11_exp. (exists pa_b_hj32_local_total_h36t_p11_exp pa_c_hj32_local_total_h36t_p11_exp. ((forall pa_i_hj32_local_total_h36t_p11_exp_repeat. (exists pa_lt_hj32_local_total_h36t_p11_exp_repeat_bound. pa_lt_hj32_local_total_h36t_p11_exp_repeat_bound + S pa_i_hj32_local_total_h36t_p11_exp_repeat = 2 * 37) -> (((exists pa_h_hj32_local_total_h36t_p11_exp_repeat_decoded. pa_h_hj32_local_total_h36t_p11_exp_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_h36t_p11_exp_repeat)) * pa_c_hj32_local_total_h36t_p11_exp)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_repeat_decoded. pa_b_hj32_local_total_h36t_p11_exp = pa_q_hj32_local_total_h36t_p11_exp_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p11_exp_repeat)) * pa_c_hj32_local_total_h36t_p11_exp) + (11)))) /\ (exists pa_u_hj32_local_total_h36t_p11_exp_product pa_v_hj32_local_total_h36t_p11_exp_product. ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_start. pa_h_hj32_local_total_h36t_p11_exp_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_start. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_terminal. pa_h_hj32_local_total_h36t_p11_exp_product_terminal + S (hj32_local_value_h36t_p11_exp) = S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_terminal. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (hj32_local_value_h36t_p11_exp))) /\ forall pa_i_hj32_local_total_h36t_p11_exp_product. (exists pa_lt_hj32_local_total_h36t_p11_exp_product_bound. pa_lt_hj32_local_total_h36t_p11_exp_product_bound + S pa_i_hj32_local_total_h36t_p11_exp_product = 2 * 37) -> exists pa_p_hj32_local_total_h36t_p11_exp_product pa_r_hj32_local_total_h36t_p11_exp_product pa_s_hj32_local_total_h36t_p11_exp_product. ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_factor. pa_h_hj32_local_total_h36t_p11_exp_product_factor + S (pa_p_hj32_local_total_h36t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_c_hj32_local_total_h36t_p11_exp)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_factor. pa_b_hj32_local_total_h36t_p11_exp = pa_q_hj32_local_total_h36t_p11_exp_product_factor * S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_c_hj32_local_total_h36t_p11_exp) + (pa_p_hj32_local_total_h36t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_partial. pa_h_hj32_local_total_h36t_p11_exp_product_partial + S (pa_r_hj32_local_total_h36t_p11_exp_product) = S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_partial. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_partial * S ((S (pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (pa_r_hj32_local_total_h36t_p11_exp_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p11_exp_product_successor. pa_h_hj32_local_total_h36t_p11_exp_product_successor + S (pa_s_hj32_local_total_h36t_p11_exp_product) = S ((S (S pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product)) /\ exists pa_q_hj32_local_total_h36t_p11_exp_product_successor. pa_u_hj32_local_total_h36t_p11_exp_product = pa_q_hj32_local_total_h36t_p11_exp_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p11_exp_product)) * pa_v_hj32_local_total_h36t_p11_exp_product) + (pa_s_hj32_local_total_h36t_p11_exp_product))) /\ pa_s_hj32_local_total_h36t_p11_exp_product = pa_r_hj32_local_total_h36t_p11_exp_product * pa_p_hj32_local_total_h36t_p11_exp_product))))))))
  44. 0044specialize htotal 11
  45. 0045specialize htotal 2 * 37
  46. 0046exact htotal
  47. 0047cases h36t_p11_exp
  48. 0048have h36t_p44_product_graph : exists pa_b_hj32_local_product_h36t_p44_product pa_c_hj32_local_product_h36t_p44_product. ((forall pa_i_hj32_local_product_h36t_p44_product_repeat. (exists pa_lt_hj32_local_product_h36t_p44_product_repeat_bound. pa_lt_hj32_local_product_h36t_p44_product_repeat_bound + S pa_i_hj32_local_product_h36t_p44_product_repeat = 2 * 37) -> (((exists pa_h_hj32_local_product_h36t_p44_product_repeat_decoded. pa_h_hj32_local_product_h36t_p44_product_repeat_decoded + S (4 * 11) = S ((S (pa_i_hj32_local_product_h36t_p44_product_repeat)) * pa_c_hj32_local_product_h36t_p44_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_repeat_decoded. pa_b_hj32_local_product_h36t_p44_product = pa_q_hj32_local_product_h36t_p44_product_repeat_decoded * S ((S (pa_i_hj32_local_product_h36t_p44_product_repeat)) * pa_c_hj32_local_product_h36t_p44_product) + (4 * 11)))) /\ (exists pa_u_hj32_local_product_h36t_p44_product_product pa_v_hj32_local_product_h36t_p44_product_product. ((((exists pa_h_hj32_local_product_h36t_p44_product_product_start. pa_h_hj32_local_product_h36t_p44_product_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_start. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_start * S ((S (0)) * pa_v_hj32_local_product_h36t_p44_product_product) + (1))) /\ ((((exists pa_h_hj32_local_product_h36t_p44_product_product_terminal. pa_h_hj32_local_product_h36t_p44_product_product_terminal + S (x) = S ((S (2 * 37)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_terminal. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_terminal * S ((S (2 * 37)) * pa_v_hj32_local_product_h36t_p44_product_product) + (x))) /\ forall pa_i_hj32_local_product_h36t_p44_product_product. (exists pa_lt_hj32_local_product_h36t_p44_product_product_bound. pa_lt_hj32_local_product_h36t_p44_product_product_bound + S pa_i_hj32_local_product_h36t_p44_product_product = 2 * 37) -> exists pa_p_hj32_local_product_h36t_p44_product_product pa_r_hj32_local_product_h36t_p44_product_product pa_s_hj32_local_product_h36t_p44_product_product. ((((exists pa_h_hj32_local_product_h36t_p44_product_product_factor. pa_h_hj32_local_product_h36t_p44_product_product_factor + S (pa_p_hj32_local_product_h36t_p44_product_product) = S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_c_hj32_local_product_h36t_p44_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_factor. pa_b_hj32_local_product_h36t_p44_product = pa_q_hj32_local_product_h36t_p44_product_product_factor * S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_c_hj32_local_product_h36t_p44_product) + (pa_p_hj32_local_product_h36t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h36t_p44_product_product_partial. pa_h_hj32_local_product_h36t_p44_product_product_partial + S (pa_r_hj32_local_product_h36t_p44_product_product) = S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_partial. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_partial * S ((S (pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product) + (pa_r_hj32_local_product_h36t_p44_product_product))) /\ ((((exists pa_h_hj32_local_product_h36t_p44_product_product_successor. pa_h_hj32_local_product_h36t_p44_product_product_successor + S (pa_s_hj32_local_product_h36t_p44_product_product) = S ((S (S pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product)) /\ exists pa_q_hj32_local_product_h36t_p44_product_product_successor. pa_u_hj32_local_product_h36t_p44_product_product = pa_q_hj32_local_product_h36t_p44_product_product_successor * S ((S (S pa_i_hj32_local_product_h36t_p44_product_product)) * pa_v_hj32_local_product_h36t_p44_product_product) + (pa_s_hj32_local_product_h36t_p44_product_product))) /\ pa_s_hj32_local_product_h36t_p44_product_product = pa_r_hj32_local_product_h36t_p44_product_product * pa_p_hj32_local_product_h36t_p44_product_product)))))))
  49. 0049have h36t_p44_product_base : 4 * 11 = 44
  50. 0050norm_num
  51. 0051rewrite h36t_p44_product_base
  52. 0052rewrite h36t_p44_product_base
  53. 0053exact h36t_p44_witness
  54. 0054have h36t_p44_product : x = x1 * x2
  55. 0055specialize pow_mul_base 4
  56. 0056specialize pow_mul_base 11
  57. 0057specialize pow_mul_base 2 * 37
  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 h36t_p4_exp_witness
  63. 0063exact h36t_p11_exp_witness
  64. 0064exact h36t_p44_product_graph
  65. 0065have h36t_p4_tail : exists hj32_local_value_h36t_p4_tail. (exists pa_b_hj32_local_total_h36t_p4_tail pa_c_hj32_local_total_h36t_p4_tail. ((forall pa_i_hj32_local_total_h36t_p4_tail_repeat. (exists pa_lt_hj32_local_total_h36t_p4_tail_repeat_bound. pa_lt_hj32_local_total_h36t_p4_tail_repeat_bound + S pa_i_hj32_local_total_h36t_p4_tail_repeat = 2 * (5 * 13)) -> (((exists pa_h_hj32_local_total_h36t_p4_tail_repeat_decoded. pa_h_hj32_local_total_h36t_p4_tail_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h36t_p4_tail_repeat)) * pa_c_hj32_local_total_h36t_p4_tail)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_repeat_decoded. pa_b_hj32_local_total_h36t_p4_tail = pa_q_hj32_local_total_h36t_p4_tail_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p4_tail_repeat)) * pa_c_hj32_local_total_h36t_p4_tail) + (4)))) /\ (exists pa_u_hj32_local_total_h36t_p4_tail_product pa_v_hj32_local_total_h36t_p4_tail_product. ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_start. pa_h_hj32_local_total_h36t_p4_tail_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_start. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p4_tail_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_terminal. pa_h_hj32_local_total_h36t_p4_tail_product_terminal + S (hj32_local_value_h36t_p4_tail) = S ((S (2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_terminal. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_terminal * S ((S (2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_tail_product) + (hj32_local_value_h36t_p4_tail))) /\ forall pa_i_hj32_local_total_h36t_p4_tail_product. (exists pa_lt_hj32_local_total_h36t_p4_tail_product_bound. pa_lt_hj32_local_total_h36t_p4_tail_product_bound + S pa_i_hj32_local_total_h36t_p4_tail_product = 2 * (5 * 13)) -> exists pa_p_hj32_local_total_h36t_p4_tail_product pa_r_hj32_local_total_h36t_p4_tail_product pa_s_hj32_local_total_h36t_p4_tail_product. ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_factor. pa_h_hj32_local_total_h36t_p4_tail_product_factor + S (pa_p_hj32_local_total_h36t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_c_hj32_local_total_h36t_p4_tail)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_factor. pa_b_hj32_local_total_h36t_p4_tail = pa_q_hj32_local_total_h36t_p4_tail_product_factor * S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_c_hj32_local_total_h36t_p4_tail) + (pa_p_hj32_local_total_h36t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_partial. pa_h_hj32_local_total_h36t_p4_tail_product_partial + S (pa_r_hj32_local_total_h36t_p4_tail_product) = S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_partial. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_partial * S ((S (pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product) + (pa_r_hj32_local_total_h36t_p4_tail_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_tail_product_successor. pa_h_hj32_local_total_h36t_p4_tail_product_successor + S (pa_s_hj32_local_total_h36t_p4_tail_product) = S ((S (S pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product)) /\ exists pa_q_hj32_local_total_h36t_p4_tail_product_successor. pa_u_hj32_local_total_h36t_p4_tail_product = pa_q_hj32_local_total_h36t_p4_tail_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p4_tail_product)) * pa_v_hj32_local_total_h36t_p4_tail_product) + (pa_s_hj32_local_total_h36t_p4_tail_product))) /\ pa_s_hj32_local_total_h36t_p4_tail_product = pa_r_hj32_local_total_h36t_p4_tail_product * pa_p_hj32_local_total_h36t_p4_tail_product))))))))
  66. 0066specialize htotal 4
  67. 0067specialize htotal 2 * (5 * 13)
  68. 0068exact htotal
  69. 0069cases h36t_p4_tail
  70. 0070have h36t_tail_power : exists pa_b_hj32_h36t_tail_power pa_c_hj32_h36t_tail_power. ((forall pa_i_hj32_h36t_tail_power_repeat. (exists pa_lt_hj32_h36t_tail_power_repeat_bound. pa_lt_hj32_h36t_tail_power_repeat_bound + S pa_i_hj32_h36t_tail_power_repeat = (14 * 9 + 3) + 1) -> (((exists pa_h_hj32_h36t_tail_power_repeat_decoded. pa_h_hj32_h36t_tail_power_repeat_decoded + S (4) = S ((S (pa_i_hj32_h36t_tail_power_repeat)) * pa_c_hj32_h36t_tail_power)) /\ exists pa_q_hj32_h36t_tail_power_repeat_decoded. pa_b_hj32_h36t_tail_power = pa_q_hj32_h36t_tail_power_repeat_decoded * S ((S (pa_i_hj32_h36t_tail_power_repeat)) * pa_c_hj32_h36t_tail_power) + (4)))) /\ (exists pa_u_hj32_h36t_tail_power_product pa_v_hj32_h36t_tail_power_product. ((((exists pa_h_hj32_h36t_tail_power_product_start. pa_h_hj32_h36t_tail_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_start. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_start * S ((S (0)) * pa_v_hj32_h36t_tail_power_product) + (1))) /\ ((((exists pa_h_hj32_h36t_tail_power_product_terminal. pa_h_hj32_h36t_tail_power_product_terminal + S (x3) = S ((S ((14 * 9 + 3) + 1)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_terminal. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_terminal * S ((S ((14 * 9 + 3) + 1)) * pa_v_hj32_h36t_tail_power_product) + (x3))) /\ forall pa_i_hj32_h36t_tail_power_product. (exists pa_lt_hj32_h36t_tail_power_product_bound. pa_lt_hj32_h36t_tail_power_product_bound + S pa_i_hj32_h36t_tail_power_product = (14 * 9 + 3) + 1) -> exists pa_p_hj32_h36t_tail_power_product pa_r_hj32_h36t_tail_power_product pa_s_hj32_h36t_tail_power_product. ((((exists pa_h_hj32_h36t_tail_power_product_factor. pa_h_hj32_h36t_tail_power_product_factor + S (pa_p_hj32_h36t_tail_power_product) = S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_c_hj32_h36t_tail_power)) /\ exists pa_q_hj32_h36t_tail_power_product_factor. pa_b_hj32_h36t_tail_power = pa_q_hj32_h36t_tail_power_product_factor * S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_c_hj32_h36t_tail_power) + (pa_p_hj32_h36t_tail_power_product))) /\ ((((exists pa_h_hj32_h36t_tail_power_product_partial. pa_h_hj32_h36t_tail_power_product_partial + S (pa_r_hj32_h36t_tail_power_product) = S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_partial. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_partial * S ((S (pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product) + (pa_r_hj32_h36t_tail_power_product))) /\ ((((exists pa_h_hj32_h36t_tail_power_product_successor. pa_h_hj32_h36t_tail_power_product_successor + S (pa_s_hj32_h36t_tail_power_product) = S ((S (S pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product)) /\ exists pa_q_hj32_h36t_tail_power_product_successor. pa_u_hj32_h36t_tail_power_product = pa_q_hj32_h36t_tail_power_product_successor * S ((S (S pa_i_hj32_h36t_tail_power_product)) * pa_v_hj32_h36t_tail_power_product) + (pa_s_hj32_h36t_tail_power_product))) /\ pa_s_hj32_h36t_tail_power_product = pa_r_hj32_h36t_tail_power_product * pa_p_hj32_h36t_tail_power_product)))))))
  71. 0071have h36t_tail_exponent : (14 * 9 + 3) + 1 = 2 * (5 * 13)
  72. 0072have h36t_tail_left : (14 * 9 + 3) + 1 = 2 * (7 * 9 + 2)
  73. 0073have h36t_tail_assoc : (14 * 9 + 3) + 1 = 14 * 9 + (3 + 1)
  74. 0074specialize add_assoc (14 * 9)
  75. 0075specialize add_assoc 3
  76. 0076specialize add_assoc 1
  77. 0077apply add_assoc
  78. 0078rewrite h36t_tail_assoc
  79. 0079have h36t_four : 3 + 1 = 2 * 2
  80. 0080norm_num
  81. 0081rewrite h36t_four
  82. 0082have h36t_fourteen : 14 = 2 * 7
  83. 0083norm_num
  84. 0084rewrite h36t_fourteen
  85. 0085have h36t_assoc_mul : (2 * 7) * 9 = 2 * (7 * 9)
  86. 0086specialize mul_assoc 2
  87. 0087specialize mul_assoc 7
  88. 0088specialize mul_assoc 9
  89. 0089apply mul_assoc
  90. 0090rewrite h36t_assoc_mul
  91. 0091have h36t_factor : 2 * (7 * 9 + 2) = 2 * (7 * 9) + 2 * 2
  92. 0092specialize mul_add 2
  93. 0093specialize mul_add (7 * 9)
  94. 0094specialize mul_add 2
  95. 0095apply mul_add
  96. 0096rewrite <- h36t_factor
  97. 0097refl
  98. 0098have h36t_tail_right : 2 * (7 * 9 + 2) = 2 * (5 * 13)
  99. 0099have h36t_inside : 7 * 9 + 2 = 5 * 13
  100. 0100norm_num
  101. 0101rewrite h36t_inside
  102. 0102refl
  103. 0103trans 2 * (7 * 9 + 2)
  104. 0104exact h36t_tail_left
  105. 0105exact h36t_tail_right
  106. 0106rewrite h36t_tail_exponent
  107. 0107rewrite h36t_tail_exponent
  108. 0108rewrite h36t_tail_exponent
  109. 0109rewrite h36t_tail_exponent
  110. 0110exact h36t_p4_tail_witness
  111. 0111have h36t_parity : 7 * 37 = 2 * (14 * 9 + 3) + 1
  112. 0112have h36t_left : 7 * 37 = 28 * 9 + 7
  113. 0113have h36t_root : 37 = 4 * 9 + 1
  114. 0114norm_num
  115. 0115rewrite h36t_root
  116. 0116have h36t_left_distrib : 7 * (4 * 9 + 1) = 7 * (4 * 9) + 7 * 1
  117. 0117specialize mul_add 7
  118. 0118specialize mul_add (4 * 9)
  119. 0119specialize mul_add 1
  120. 0120apply mul_add
  121. 0121rewrite h36t_left_distrib
  122. 0122have h36t_left_assoc : 7 * (4 * 9) = (7 * 4) * 9
  123. 0123symm
  124. 0124specialize mul_assoc 7
  125. 0125specialize mul_assoc 4
  126. 0126specialize mul_assoc 9
  127. 0127apply mul_assoc
  128. 0128rewrite h36t_left_assoc
  129. 0129have h36t_twenty_eight : 7 * 4 = 28
  130. 0130norm_num
  131. 0131rewrite h36t_twenty_eight
  132. 0132have h36t_seven : 7 * 1 = 7
  133. 0133norm_num
  134. 0134rewrite h36t_seven
  135. 0135refl
  136. 0136have h36t_right : 2 * (14 * 9 + 3) + 1 = 28 * 9 + 7
  137. 0137have h36t_right_distrib : 2 * (14 * 9 + 3) = 2 * (14 * 9) + 2 * 3
  138. 0138specialize mul_add 2
  139. 0139specialize mul_add (14 * 9)
  140. 0140specialize mul_add 3
  141. 0141apply mul_add
  142. 0142rewrite h36t_right_distrib
  143. 0143have h36t_right_assoc : 2 * (14 * 9) = (2 * 14) * 9
  144. 0144symm
  145. 0145specialize mul_assoc 2
  146. 0146specialize mul_assoc 14
  147. 0147specialize mul_assoc 9
  148. 0148apply mul_assoc
  149. 0149rewrite h36t_right_assoc
  150. 0150have h36t_right_twenty_eight : 2 * 14 = 28
  151. 0151norm_num
  152. 0152rewrite h36t_right_twenty_eight
  153. 0153have h36t_right_add : (28 * 9 + 2 * 3) + 1 = 28 * 9 + (2 * 3 + 1)
  154. 0154specialize add_assoc (28 * 9)
  155. 0155specialize add_assoc (2 * 3)
  156. 0156specialize add_assoc 1
  157. 0157apply add_assoc
  158. 0158rewrite h36t_right_add
  159. 0159have h36t_right_seven : 2 * 3 + 1 = 7
  160. 0160norm_num
  161. 0161rewrite h36t_right_seven
  162. 0162refl
  163. 0163trans 28 * 9 + 7
  164. 0164exact h36t_left
  165. 0165symm
  166. 0166exact h36t_right
  167. 0167have h36t_eleven_bound : exists bqb_le_gap_hj32_h36t_eleven_bound. bqb_le_gap_hj32_h36t_eleven_bound + (x2) = (x3)
  168. 0168specialize pow_eleven_double_block_le_pow_four_odd_from_total 37
  169. 0169specialize pow_eleven_double_block_le_pow_four_odd_from_total (14 * 9 + 3)
  170. 0170specialize pow_eleven_double_block_le_pow_four_odd_from_total x2
  171. 0171specialize pow_eleven_double_block_le_pow_four_odd_from_total x3
  172. 0172apply pow_eleven_double_block_le_pow_four_odd_from_total
  173. 0173exact htotal
  174. 0174exact h36t_parity
  175. 0175exact h36t_p11_exp_witness
  176. 0176exact h36t_tail_power
  177. 0177have h36t_four_refl : exists bqb_le_gap_hj32_h36t_four_refl. bqb_le_gap_hj32_h36t_four_refl + (x1) = (x1)
  178. 0178specialize le_refl x1
  179. 0179exact le_refl
  180. 0180have h36t_product_bound : exists bqb_le_gap_hj32_local_product_bound_h36t_product_bound. bqb_le_gap_hj32_local_product_bound_h36t_product_bound + (x1 * x2) = (x1 * x3)
  181. 0181specialize mul_le_mul x1
  182. 0182specialize mul_le_mul x1
  183. 0183specialize mul_le_mul x2
  184. 0184specialize mul_le_mul x3
  185. 0185apply mul_le_mul
  186. 0186exact h36t_four_refl
  187. 0187exact h36t_eleven_bound
  188. 0188have h36t_p4_budget : exists hj32_local_value_h36t_p4_budget. (exists pa_b_hj32_local_total_h36t_p4_budget pa_c_hj32_local_total_h36t_p4_budget. ((forall pa_i_hj32_local_total_h36t_p4_budget_repeat. (exists pa_lt_hj32_local_total_h36t_p4_budget_repeat_bound. pa_lt_hj32_local_total_h36t_p4_budget_repeat_bound + S pa_i_hj32_local_total_h36t_p4_budget_repeat = 2 * 37 + 2 * (5 * 13)) -> (((exists pa_h_hj32_local_total_h36t_p4_budget_repeat_decoded. pa_h_hj32_local_total_h36t_p4_budget_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_h36t_p4_budget_repeat)) * pa_c_hj32_local_total_h36t_p4_budget)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_repeat_decoded. pa_b_hj32_local_total_h36t_p4_budget = pa_q_hj32_local_total_h36t_p4_budget_repeat_decoded * S ((S (pa_i_hj32_local_total_h36t_p4_budget_repeat)) * pa_c_hj32_local_total_h36t_p4_budget) + (4)))) /\ (exists pa_u_hj32_local_total_h36t_p4_budget_product pa_v_hj32_local_total_h36t_p4_budget_product. ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_start. pa_h_hj32_local_total_h36t_p4_budget_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_start. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_start * S ((S (0)) * pa_v_hj32_local_total_h36t_p4_budget_product) + (1))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_terminal. pa_h_hj32_local_total_h36t_p4_budget_product_terminal + S (hj32_local_value_h36t_p4_budget) = S ((S (2 * 37 + 2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_terminal. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_terminal * S ((S (2 * 37 + 2 * (5 * 13))) * pa_v_hj32_local_total_h36t_p4_budget_product) + (hj32_local_value_h36t_p4_budget))) /\ forall pa_i_hj32_local_total_h36t_p4_budget_product. (exists pa_lt_hj32_local_total_h36t_p4_budget_product_bound. pa_lt_hj32_local_total_h36t_p4_budget_product_bound + S pa_i_hj32_local_total_h36t_p4_budget_product = 2 * 37 + 2 * (5 * 13)) -> exists pa_p_hj32_local_total_h36t_p4_budget_product pa_r_hj32_local_total_h36t_p4_budget_product pa_s_hj32_local_total_h36t_p4_budget_product. ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_factor. pa_h_hj32_local_total_h36t_p4_budget_product_factor + S (pa_p_hj32_local_total_h36t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_c_hj32_local_total_h36t_p4_budget)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_factor. pa_b_hj32_local_total_h36t_p4_budget = pa_q_hj32_local_total_h36t_p4_budget_product_factor * S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_c_hj32_local_total_h36t_p4_budget) + (pa_p_hj32_local_total_h36t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_partial. pa_h_hj32_local_total_h36t_p4_budget_product_partial + S (pa_r_hj32_local_total_h36t_p4_budget_product) = S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_partial. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_partial * S ((S (pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product) + (pa_r_hj32_local_total_h36t_p4_budget_product))) /\ ((((exists pa_h_hj32_local_total_h36t_p4_budget_product_successor. pa_h_hj32_local_total_h36t_p4_budget_product_successor + S (pa_s_hj32_local_total_h36t_p4_budget_product) = S ((S (S pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product)) /\ exists pa_q_hj32_local_total_h36t_p4_budget_product_successor. pa_u_hj32_local_total_h36t_p4_budget_product = pa_q_hj32_local_total_h36t_p4_budget_product_successor * S ((S (S pa_i_hj32_local_total_h36t_p4_budget_product)) * pa_v_hj32_local_total_h36t_p4_budget_product) + (pa_s_hj32_local_total_h36t_p4_budget_product))) /\ pa_s_hj32_local_total_h36t_p4_budget_product = pa_r_hj32_local_total_h36t_p4_budget_product * pa_p_hj32_local_total_h36t_p4_budget_product))))))))
  189. 0189specialize htotal 4
  190. 0190specialize htotal 2 * 37 + 2 * (5 * 13)
  191. 0191exact htotal
  192. 0192cases h36t_p4_budget
  193. 0193have h36t_budget_product : x4 = x1 * x3
  194. 0194specialize pow_add 4
  195. 0195specialize pow_add 2 * 37
  196. 0196specialize pow_add 2 * (5 * 13)
  197. 0197specialize pow_add 2 * 37 + 2 * (5 * 13)
  198. 0198specialize pow_add x1
  199. 0199specialize pow_add x3
  200. 0200specialize pow_add x4
  201. 0201apply pow_add
  202. 0202refl
  203. 0203exact h36t_p4_exp_witness
  204. 0204exact h36t_p4_tail_witness
  205. 0205exact h36t_p4_budget_witness
  206. 0206rewrite <- h36t_p44_product at h36t_product_bound
  207. 0207rewrite <- h36t_budget_product at h36t_product_bound
  208. 0208have h36t_to_budget : exists bqb_le_gap_hj32_local_trans_bound_h36t_to_budget. bqb_le_gap_hj32_local_trans_bound_h36t_to_budget + (h) = (x4)
  209. 0209specialize le_trans h
  210. 0210specialize le_trans x
  211. 0211specialize le_trans x4
  212. 0212apply le_trans
  213. 0213exact h36t_to_44
  214. 0214exact h36t_product_bound
  215. 0215have hscaled : exists bqb_le_gap_hj32_scaled_budget_root_36. bqb_le_gap_hj32_scaled_budget_root_36 + (6 * (2 * 37 + 2 * (5 * 13))) = (36 * 36)
  216. 0216apply bertrand_scaled_budget_root_36
  217. 0217have hbudget_exponent : exists bqb_le_gap_hj32_h_36_budget_exponent. bqb_le_gap_hj32_h_36_budget_exponent + (2 * 37 + 2 * (5 * 13)) = (e)
  218. 0218specialize ceil_div_six_budget_of_scaled_le (36 * 36)
  219. 0219specialize ceil_div_six_budget_of_scaled_le (2 * 37 + 2 * (5 * 13))
  220. 0220specialize ceil_div_six_budget_of_scaled_le e
  221. 0221apply ceil_div_six_budget_of_scaled_le
  222. 0222exact hceiling
  223. 0223exact hscaled
  224. 0224have h36_budget_growth : exists bqb_le_gap_hj32_local_exponent_bound_h36_budget_growth. bqb_le_gap_hj32_local_exponent_bound_h36_budget_growth + (x4) = (u)
  225. 0225specialize pow_exponent_monotone_from_total 4
  226. 0226specialize pow_exponent_monotone_from_total 2 * 37 + 2 * (5 * 13)
  227. 0227specialize pow_exponent_monotone_from_total e
  228. 0228specialize pow_exponent_monotone_from_total x4
  229. 0229specialize pow_exponent_monotone_from_total u
  230. 0230apply pow_exponent_monotone_from_total
  231. 0231exact htotal
  232. 0232exists 3
  233. 0233norm_num
  234. 0234exact hbudget_exponent
  235. 0235exact h36t_p4_budget_witness
  236. 0236exact hu
  237. 0237have h36_result : exists bqb_le_gap_hj32_local_trans_bound_h36_result. bqb_le_gap_hj32_local_trans_bound_h36_result + (h) = (u)
  238. 0238specialize le_trans h
  239. 0239specialize le_trans x4
  240. 0240specialize le_trans u
  241. 0241apply le_trans
  242. 0242exact h36t_to_budget
  243. 0243exact h36_budget_growth
  244. 0244exact h36_result