BT00WH

pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total

Alpha body-checked · checked-use disabled

The seed 3^5 <= 4^4 extends by blocks and one residual factor.

Exact expanded PA statement

forall m x y. (forall bpt_a_hj32_three_plus bpt_e_hj32_three_plus. exists bpt_x_hj32_three_plus. (exists ff_b_bpt_value_hj32_three_plus ff_c_bpt_value_hj32_three_plus. ((forall ff_i_bpt_value_hj32_three_plus_repeat. (exists ff_lt_bpt_value_hj32_three_plus_repeat_bound. ff_lt_bpt_value_hj32_three_plus_repeat_bound + S ff_i_bpt_value_hj32_three_plus_repeat = bpt_e_hj32_three_plus) -> (((exists ff_h_bpt_value_hj32_three_plus_repeat_decoded. ff_h_bpt_value_hj32_three_plus_repeat_decoded + S (bpt_a_hj32_three_plus) = S ((S (ff_i_bpt_value_hj32_three_plus_repeat)) * ff_c_bpt_value_hj32_three_plus)) /\ exists ff_q_bpt_value_hj32_three_plus_repeat_decoded. ff_b_bpt_value_hj32_three_plus = ff_q_bpt_value_hj32_three_plus_repeat_decoded * S ((S (ff_i_bpt_value_hj32_three_plus_repeat)) * ff_c_bpt_value_hj32_three_plus) + (bpt_a_hj32_three_plus)))) /\ (exists ff_u_bpt_value_hj32_three_plus_product ff_v_bpt_value_hj32_three_plus_product. ((((exists ff_h_bpt_value_hj32_three_plus_product_start. ff_h_bpt_value_hj32_three_plus_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_start. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_start * S ((S (0)) * ff_v_bpt_value_hj32_three_plus_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_three_plus_product_terminal. ff_h_bpt_value_hj32_three_plus_product_terminal + S (bpt_x_hj32_three_plus) = S ((S (bpt_e_hj32_three_plus)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_terminal. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_terminal * S ((S (bpt_e_hj32_three_plus)) * ff_v_bpt_value_hj32_three_plus_product) + (bpt_x_hj32_three_plus))) /\ forall ff_i_bpt_value_hj32_three_plus_product. (exists ff_lt_bpt_value_hj32_three_plus_product_bound. ff_lt_bpt_value_hj32_three_plus_product_bound + S ff_i_bpt_value_hj32_three_plus_product = bpt_e_hj32_three_plus) -> exists ff_p_bpt_value_hj32_three_plus_product ff_r_bpt_value_hj32_three_plus_product ff_s_bpt_value_hj32_three_plus_product. ((((exists ff_h_bpt_value_hj32_three_plus_product_factor. ff_h_bpt_value_hj32_three_plus_product_factor + S (ff_p_bpt_value_hj32_three_plus_product) = S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_c_bpt_value_hj32_three_plus)) /\ exists ff_q_bpt_value_hj32_three_plus_product_factor. ff_b_bpt_value_hj32_three_plus = ff_q_bpt_value_hj32_three_plus_product_factor * S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_c_bpt_value_hj32_three_plus) + (ff_p_bpt_value_hj32_three_plus_product))) /\ ((((exists ff_h_bpt_value_hj32_three_plus_product_partial. ff_h_bpt_value_hj32_three_plus_product_partial + S (ff_r_bpt_value_hj32_three_plus_product) = S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_partial. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_partial * S ((S (ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product) + (ff_r_bpt_value_hj32_three_plus_product))) /\ ((((exists ff_h_bpt_value_hj32_three_plus_product_successor. ff_h_bpt_value_hj32_three_plus_product_successor + S (ff_s_bpt_value_hj32_three_plus_product) = S ((S (S ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product)) /\ exists ff_q_bpt_value_hj32_three_plus_product_successor. ff_u_bpt_value_hj32_three_plus_product = ff_q_bpt_value_hj32_three_plus_product_successor * S ((S (S ff_i_bpt_value_hj32_three_plus_product)) * ff_v_bpt_value_hj32_three_plus_product) + (ff_s_bpt_value_hj32_three_plus_product))) /\ ff_s_bpt_value_hj32_three_plus_product = ff_r_bpt_value_hj32_three_plus_product * ff_p_bpt_value_hj32_three_plus_product))))))))) -> (exists pa_b_hj32_three_plus_left pa_c_hj32_three_plus_left. ((forall pa_i_hj32_three_plus_left_repeat. (exists pa_lt_hj32_three_plus_left_repeat_bound. pa_lt_hj32_three_plus_left_repeat_bound + S pa_i_hj32_three_plus_left_repeat = 5 * m + 1) -> (((exists pa_h_hj32_three_plus_left_repeat_decoded. pa_h_hj32_three_plus_left_repeat_decoded + S (3) = S ((S (pa_i_hj32_three_plus_left_repeat)) * pa_c_hj32_three_plus_left)) /\ exists pa_q_hj32_three_plus_left_repeat_decoded. pa_b_hj32_three_plus_left = pa_q_hj32_three_plus_left_repeat_decoded * S ((S (pa_i_hj32_three_plus_left_repeat)) * pa_c_hj32_three_plus_left) + (3)))) /\ (exists pa_u_hj32_three_plus_left_product pa_v_hj32_three_plus_left_product. ((((exists pa_h_hj32_three_plus_left_product_start. pa_h_hj32_three_plus_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_start. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_start * S ((S (0)) * pa_v_hj32_three_plus_left_product) + (1))) /\ ((((exists pa_h_hj32_three_plus_left_product_terminal. pa_h_hj32_three_plus_left_product_terminal + S (x) = S ((S (5 * m + 1)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_terminal. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_terminal * S ((S (5 * m + 1)) * pa_v_hj32_three_plus_left_product) + (x))) /\ forall pa_i_hj32_three_plus_left_product. (exists pa_lt_hj32_three_plus_left_product_bound. pa_lt_hj32_three_plus_left_product_bound + S pa_i_hj32_three_plus_left_product = 5 * m + 1) -> exists pa_p_hj32_three_plus_left_product pa_r_hj32_three_plus_left_product pa_s_hj32_three_plus_left_product. ((((exists pa_h_hj32_three_plus_left_product_factor. pa_h_hj32_three_plus_left_product_factor + S (pa_p_hj32_three_plus_left_product) = S ((S (pa_i_hj32_three_plus_left_product)) * pa_c_hj32_three_plus_left)) /\ exists pa_q_hj32_three_plus_left_product_factor. pa_b_hj32_three_plus_left = pa_q_hj32_three_plus_left_product_factor * S ((S (pa_i_hj32_three_plus_left_product)) * pa_c_hj32_three_plus_left) + (pa_p_hj32_three_plus_left_product))) /\ ((((exists pa_h_hj32_three_plus_left_product_partial. pa_h_hj32_three_plus_left_product_partial + S (pa_r_hj32_three_plus_left_product) = S ((S (pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_partial. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_partial * S ((S (pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product) + (pa_r_hj32_three_plus_left_product))) /\ ((((exists pa_h_hj32_three_plus_left_product_successor. pa_h_hj32_three_plus_left_product_successor + S (pa_s_hj32_three_plus_left_product) = S ((S (S pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product)) /\ exists pa_q_hj32_three_plus_left_product_successor. pa_u_hj32_three_plus_left_product = pa_q_hj32_three_plus_left_product_successor * S ((S (S pa_i_hj32_three_plus_left_product)) * pa_v_hj32_three_plus_left_product) + (pa_s_hj32_three_plus_left_product))) /\ pa_s_hj32_three_plus_left_product = pa_r_hj32_three_plus_left_product * pa_p_hj32_three_plus_left_product)))))))) -> (exists pa_b_hj32_three_plus_right pa_c_hj32_three_plus_right. ((forall pa_i_hj32_three_plus_right_repeat. (exists pa_lt_hj32_three_plus_right_repeat_bound. pa_lt_hj32_three_plus_right_repeat_bound + S pa_i_hj32_three_plus_right_repeat = 4 * m + 1) -> (((exists pa_h_hj32_three_plus_right_repeat_decoded. pa_h_hj32_three_plus_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_three_plus_right_repeat)) * pa_c_hj32_three_plus_right)) /\ exists pa_q_hj32_three_plus_right_repeat_decoded. pa_b_hj32_three_plus_right = pa_q_hj32_three_plus_right_repeat_decoded * S ((S (pa_i_hj32_three_plus_right_repeat)) * pa_c_hj32_three_plus_right) + (4)))) /\ (exists pa_u_hj32_three_plus_right_product pa_v_hj32_three_plus_right_product. ((((exists pa_h_hj32_three_plus_right_product_start. pa_h_hj32_three_plus_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_start. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_start * S ((S (0)) * pa_v_hj32_three_plus_right_product) + (1))) /\ ((((exists pa_h_hj32_three_plus_right_product_terminal. pa_h_hj32_three_plus_right_product_terminal + S (y) = S ((S (4 * m + 1)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_terminal. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_terminal * S ((S (4 * m + 1)) * pa_v_hj32_three_plus_right_product) + (y))) /\ forall pa_i_hj32_three_plus_right_product. (exists pa_lt_hj32_three_plus_right_product_bound. pa_lt_hj32_three_plus_right_product_bound + S pa_i_hj32_three_plus_right_product = 4 * m + 1) -> exists pa_p_hj32_three_plus_right_product pa_r_hj32_three_plus_right_product pa_s_hj32_three_plus_right_product. ((((exists pa_h_hj32_three_plus_right_product_factor. pa_h_hj32_three_plus_right_product_factor + S (pa_p_hj32_three_plus_right_product) = S ((S (pa_i_hj32_three_plus_right_product)) * pa_c_hj32_three_plus_right)) /\ exists pa_q_hj32_three_plus_right_product_factor. pa_b_hj32_three_plus_right = pa_q_hj32_three_plus_right_product_factor * S ((S (pa_i_hj32_three_plus_right_product)) * pa_c_hj32_three_plus_right) + (pa_p_hj32_three_plus_right_product))) /\ ((((exists pa_h_hj32_three_plus_right_product_partial. pa_h_hj32_three_plus_right_product_partial + S (pa_r_hj32_three_plus_right_product) = S ((S (pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_partial. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_partial * S ((S (pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product) + (pa_r_hj32_three_plus_right_product))) /\ ((((exists pa_h_hj32_three_plus_right_product_successor. pa_h_hj32_three_plus_right_product_successor + S (pa_s_hj32_three_plus_right_product) = S ((S (S pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product)) /\ exists pa_q_hj32_three_plus_right_product_successor. pa_u_hj32_three_plus_right_product = pa_q_hj32_three_plus_right_product_successor * S ((S (S pa_i_hj32_three_plus_right_product)) * pa_v_hj32_three_plus_right_product) + (pa_s_hj32_three_plus_right_product))) /\ pa_s_hj32_three_plus_right_product = pa_r_hj32_three_plus_right_product * pa_p_hj32_three_plus_right_product)))))))) -> (exists bqb_le_gap_hj32_three_plus_result. bqb_le_gap_hj32_three_plus_result + (x) = (y))

Structural proof guide

The seed 3^5 <= 4^4 extends by blocks and one residual factor.

Direct prerequisites: pow_block_bound_from_total, pow_three_five_le_pow_four_four_from_total, pow_add, pow_base_monotone, mul_le_mul. The authored body proceeds by case analysis (6), intermediate claims (13), equality transport (2), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT00W3 pow_block_bound_from_total BT00W4 pow_three_five_le_pow_four_four_from_total BT009X pow_add BT00PY pow_base_monotone BT00PV mul_le_mul

Direct dependents

BT00WP bertrand_h_root_32_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 m
  2. 0002intro x
  3. 0003intro y
  4. 0004intro htotal
  5. 0005intro hx
  6. 0006intro hy
  7. 0007have tp_p3_five : exists hj32_local_value_tp_p3_five. (exists pa_b_hj32_local_total_tp_p3_five pa_c_hj32_local_total_tp_p3_five. ((forall pa_i_hj32_local_total_tp_p3_five_repeat. (exists pa_lt_hj32_local_total_tp_p3_five_repeat_bound. pa_lt_hj32_local_total_tp_p3_five_repeat_bound + S pa_i_hj32_local_total_tp_p3_five_repeat = 5) -> (((exists pa_h_hj32_local_total_tp_p3_five_repeat_decoded. pa_h_hj32_local_total_tp_p3_five_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_tp_p3_five_repeat)) * pa_c_hj32_local_total_tp_p3_five)) /\ exists pa_q_hj32_local_total_tp_p3_five_repeat_decoded. pa_b_hj32_local_total_tp_p3_five = pa_q_hj32_local_total_tp_p3_five_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p3_five_repeat)) * pa_c_hj32_local_total_tp_p3_five) + (3)))) /\ (exists pa_u_hj32_local_total_tp_p3_five_product pa_v_hj32_local_total_tp_p3_five_product. ((((exists pa_h_hj32_local_total_tp_p3_five_product_start. pa_h_hj32_local_total_tp_p3_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_start. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p3_five_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p3_five_product_terminal. pa_h_hj32_local_total_tp_p3_five_product_terminal + S (hj32_local_value_tp_p3_five) = S ((S (5)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_terminal. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_terminal * S ((S (5)) * pa_v_hj32_local_total_tp_p3_five_product) + (hj32_local_value_tp_p3_five))) /\ forall pa_i_hj32_local_total_tp_p3_five_product. (exists pa_lt_hj32_local_total_tp_p3_five_product_bound. pa_lt_hj32_local_total_tp_p3_five_product_bound + S pa_i_hj32_local_total_tp_p3_five_product = 5) -> exists pa_p_hj32_local_total_tp_p3_five_product pa_r_hj32_local_total_tp_p3_five_product pa_s_hj32_local_total_tp_p3_five_product. ((((exists pa_h_hj32_local_total_tp_p3_five_product_factor. pa_h_hj32_local_total_tp_p3_five_product_factor + S (pa_p_hj32_local_total_tp_p3_five_product) = S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_c_hj32_local_total_tp_p3_five)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_factor. pa_b_hj32_local_total_tp_p3_five = pa_q_hj32_local_total_tp_p3_five_product_factor * S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_c_hj32_local_total_tp_p3_five) + (pa_p_hj32_local_total_tp_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_five_product_partial. pa_h_hj32_local_total_tp_p3_five_product_partial + S (pa_r_hj32_local_total_tp_p3_five_product) = S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_partial. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_partial * S ((S (pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product) + (pa_r_hj32_local_total_tp_p3_five_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_five_product_successor. pa_h_hj32_local_total_tp_p3_five_product_successor + S (pa_s_hj32_local_total_tp_p3_five_product) = S ((S (S pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product)) /\ exists pa_q_hj32_local_total_tp_p3_five_product_successor. pa_u_hj32_local_total_tp_p3_five_product = pa_q_hj32_local_total_tp_p3_five_product_successor * S ((S (S pa_i_hj32_local_total_tp_p3_five_product)) * pa_v_hj32_local_total_tp_p3_five_product) + (pa_s_hj32_local_total_tp_p3_five_product))) /\ pa_s_hj32_local_total_tp_p3_five_product = pa_r_hj32_local_total_tp_p3_five_product * pa_p_hj32_local_total_tp_p3_five_product))))))))
  8. 0008specialize htotal 3
  9. 0009specialize htotal 5
  10. 0010exact htotal
  11. 0011cases tp_p3_five
  12. 0012have tp_p4_four : exists hj32_local_value_tp_p4_four. (exists pa_b_hj32_local_total_tp_p4_four pa_c_hj32_local_total_tp_p4_four. ((forall pa_i_hj32_local_total_tp_p4_four_repeat. (exists pa_lt_hj32_local_total_tp_p4_four_repeat_bound. pa_lt_hj32_local_total_tp_p4_four_repeat_bound + S pa_i_hj32_local_total_tp_p4_four_repeat = 4) -> (((exists pa_h_hj32_local_total_tp_p4_four_repeat_decoded. pa_h_hj32_local_total_tp_p4_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_tp_p4_four_repeat)) * pa_c_hj32_local_total_tp_p4_four)) /\ exists pa_q_hj32_local_total_tp_p4_four_repeat_decoded. pa_b_hj32_local_total_tp_p4_four = pa_q_hj32_local_total_tp_p4_four_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p4_four_repeat)) * pa_c_hj32_local_total_tp_p4_four) + (4)))) /\ (exists pa_u_hj32_local_total_tp_p4_four_product pa_v_hj32_local_total_tp_p4_four_product. ((((exists pa_h_hj32_local_total_tp_p4_four_product_start. pa_h_hj32_local_total_tp_p4_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_start. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p4_four_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p4_four_product_terminal. pa_h_hj32_local_total_tp_p4_four_product_terminal + S (hj32_local_value_tp_p4_four) = S ((S (4)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_terminal. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_terminal * S ((S (4)) * pa_v_hj32_local_total_tp_p4_four_product) + (hj32_local_value_tp_p4_four))) /\ forall pa_i_hj32_local_total_tp_p4_four_product. (exists pa_lt_hj32_local_total_tp_p4_four_product_bound. pa_lt_hj32_local_total_tp_p4_four_product_bound + S pa_i_hj32_local_total_tp_p4_four_product = 4) -> exists pa_p_hj32_local_total_tp_p4_four_product pa_r_hj32_local_total_tp_p4_four_product pa_s_hj32_local_total_tp_p4_four_product. ((((exists pa_h_hj32_local_total_tp_p4_four_product_factor. pa_h_hj32_local_total_tp_p4_four_product_factor + S (pa_p_hj32_local_total_tp_p4_four_product) = S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_c_hj32_local_total_tp_p4_four)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_factor. pa_b_hj32_local_total_tp_p4_four = pa_q_hj32_local_total_tp_p4_four_product_factor * S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_c_hj32_local_total_tp_p4_four) + (pa_p_hj32_local_total_tp_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_four_product_partial. pa_h_hj32_local_total_tp_p4_four_product_partial + S (pa_r_hj32_local_total_tp_p4_four_product) = S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_partial. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_partial * S ((S (pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product) + (pa_r_hj32_local_total_tp_p4_four_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_four_product_successor. pa_h_hj32_local_total_tp_p4_four_product_successor + S (pa_s_hj32_local_total_tp_p4_four_product) = S ((S (S pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product)) /\ exists pa_q_hj32_local_total_tp_p4_four_product_successor. pa_u_hj32_local_total_tp_p4_four_product = pa_q_hj32_local_total_tp_p4_four_product_successor * S ((S (S pa_i_hj32_local_total_tp_p4_four_product)) * pa_v_hj32_local_total_tp_p4_four_product) + (pa_s_hj32_local_total_tp_p4_four_product))) /\ pa_s_hj32_local_total_tp_p4_four_product = pa_r_hj32_local_total_tp_p4_four_product * pa_p_hj32_local_total_tp_p4_four_product))))))))
  13. 0013specialize htotal 4
  14. 0014specialize htotal 4
  15. 0015exact htotal
  16. 0016cases tp_p4_four
  17. 0017have tp_seed : exists bqb_le_gap_hj32_tp_seed. bqb_le_gap_hj32_tp_seed + (x1) = (x2)
  18. 0018specialize pow_three_five_le_pow_four_four_from_total x1
  19. 0019specialize pow_three_five_le_pow_four_four_from_total x2
  20. 0020apply pow_three_five_le_pow_four_four_from_total
  21. 0021exact htotal
  22. 0022exact tp_p3_five_witness
  23. 0023exact tp_p4_four_witness
  24. 0024have tp_p3_block : exists hj32_local_value_tp_p3_block. (exists pa_b_hj32_local_total_tp_p3_block pa_c_hj32_local_total_tp_p3_block. ((forall pa_i_hj32_local_total_tp_p3_block_repeat. (exists pa_lt_hj32_local_total_tp_p3_block_repeat_bound. pa_lt_hj32_local_total_tp_p3_block_repeat_bound + S pa_i_hj32_local_total_tp_p3_block_repeat = 5 * m) -> (((exists pa_h_hj32_local_total_tp_p3_block_repeat_decoded. pa_h_hj32_local_total_tp_p3_block_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_tp_p3_block_repeat)) * pa_c_hj32_local_total_tp_p3_block)) /\ exists pa_q_hj32_local_total_tp_p3_block_repeat_decoded. pa_b_hj32_local_total_tp_p3_block = pa_q_hj32_local_total_tp_p3_block_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p3_block_repeat)) * pa_c_hj32_local_total_tp_p3_block) + (3)))) /\ (exists pa_u_hj32_local_total_tp_p3_block_product pa_v_hj32_local_total_tp_p3_block_product. ((((exists pa_h_hj32_local_total_tp_p3_block_product_start. pa_h_hj32_local_total_tp_p3_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_start. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p3_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p3_block_product_terminal. pa_h_hj32_local_total_tp_p3_block_product_terminal + S (hj32_local_value_tp_p3_block) = S ((S (5 * m)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_terminal. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_terminal * S ((S (5 * m)) * pa_v_hj32_local_total_tp_p3_block_product) + (hj32_local_value_tp_p3_block))) /\ forall pa_i_hj32_local_total_tp_p3_block_product. (exists pa_lt_hj32_local_total_tp_p3_block_product_bound. pa_lt_hj32_local_total_tp_p3_block_product_bound + S pa_i_hj32_local_total_tp_p3_block_product = 5 * m) -> exists pa_p_hj32_local_total_tp_p3_block_product pa_r_hj32_local_total_tp_p3_block_product pa_s_hj32_local_total_tp_p3_block_product. ((((exists pa_h_hj32_local_total_tp_p3_block_product_factor. pa_h_hj32_local_total_tp_p3_block_product_factor + S (pa_p_hj32_local_total_tp_p3_block_product) = S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_c_hj32_local_total_tp_p3_block)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_factor. pa_b_hj32_local_total_tp_p3_block = pa_q_hj32_local_total_tp_p3_block_product_factor * S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_c_hj32_local_total_tp_p3_block) + (pa_p_hj32_local_total_tp_p3_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_block_product_partial. pa_h_hj32_local_total_tp_p3_block_product_partial + S (pa_r_hj32_local_total_tp_p3_block_product) = S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_partial. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_partial * S ((S (pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product) + (pa_r_hj32_local_total_tp_p3_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_block_product_successor. pa_h_hj32_local_total_tp_p3_block_product_successor + S (pa_s_hj32_local_total_tp_p3_block_product) = S ((S (S pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product)) /\ exists pa_q_hj32_local_total_tp_p3_block_product_successor. pa_u_hj32_local_total_tp_p3_block_product = pa_q_hj32_local_total_tp_p3_block_product_successor * S ((S (S pa_i_hj32_local_total_tp_p3_block_product)) * pa_v_hj32_local_total_tp_p3_block_product) + (pa_s_hj32_local_total_tp_p3_block_product))) /\ pa_s_hj32_local_total_tp_p3_block_product = pa_r_hj32_local_total_tp_p3_block_product * pa_p_hj32_local_total_tp_p3_block_product))))))))
  25. 0025specialize htotal 3
  26. 0026specialize htotal 5 * m
  27. 0027exact htotal
  28. 0028cases tp_p3_block
  29. 0029have tp_p4_block : exists hj32_local_value_tp_p4_block. (exists pa_b_hj32_local_total_tp_p4_block pa_c_hj32_local_total_tp_p4_block. ((forall pa_i_hj32_local_total_tp_p4_block_repeat. (exists pa_lt_hj32_local_total_tp_p4_block_repeat_bound. pa_lt_hj32_local_total_tp_p4_block_repeat_bound + S pa_i_hj32_local_total_tp_p4_block_repeat = 4 * m) -> (((exists pa_h_hj32_local_total_tp_p4_block_repeat_decoded. pa_h_hj32_local_total_tp_p4_block_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_tp_p4_block_repeat)) * pa_c_hj32_local_total_tp_p4_block)) /\ exists pa_q_hj32_local_total_tp_p4_block_repeat_decoded. pa_b_hj32_local_total_tp_p4_block = pa_q_hj32_local_total_tp_p4_block_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p4_block_repeat)) * pa_c_hj32_local_total_tp_p4_block) + (4)))) /\ (exists pa_u_hj32_local_total_tp_p4_block_product pa_v_hj32_local_total_tp_p4_block_product. ((((exists pa_h_hj32_local_total_tp_p4_block_product_start. pa_h_hj32_local_total_tp_p4_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_start. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p4_block_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p4_block_product_terminal. pa_h_hj32_local_total_tp_p4_block_product_terminal + S (hj32_local_value_tp_p4_block) = S ((S (4 * m)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_terminal. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_terminal * S ((S (4 * m)) * pa_v_hj32_local_total_tp_p4_block_product) + (hj32_local_value_tp_p4_block))) /\ forall pa_i_hj32_local_total_tp_p4_block_product. (exists pa_lt_hj32_local_total_tp_p4_block_product_bound. pa_lt_hj32_local_total_tp_p4_block_product_bound + S pa_i_hj32_local_total_tp_p4_block_product = 4 * m) -> exists pa_p_hj32_local_total_tp_p4_block_product pa_r_hj32_local_total_tp_p4_block_product pa_s_hj32_local_total_tp_p4_block_product. ((((exists pa_h_hj32_local_total_tp_p4_block_product_factor. pa_h_hj32_local_total_tp_p4_block_product_factor + S (pa_p_hj32_local_total_tp_p4_block_product) = S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_c_hj32_local_total_tp_p4_block)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_factor. pa_b_hj32_local_total_tp_p4_block = pa_q_hj32_local_total_tp_p4_block_product_factor * S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_c_hj32_local_total_tp_p4_block) + (pa_p_hj32_local_total_tp_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_block_product_partial. pa_h_hj32_local_total_tp_p4_block_product_partial + S (pa_r_hj32_local_total_tp_p4_block_product) = S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_partial. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_partial * S ((S (pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product) + (pa_r_hj32_local_total_tp_p4_block_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_block_product_successor. pa_h_hj32_local_total_tp_p4_block_product_successor + S (pa_s_hj32_local_total_tp_p4_block_product) = S ((S (S pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product)) /\ exists pa_q_hj32_local_total_tp_p4_block_product_successor. pa_u_hj32_local_total_tp_p4_block_product = pa_q_hj32_local_total_tp_p4_block_product_successor * S ((S (S pa_i_hj32_local_total_tp_p4_block_product)) * pa_v_hj32_local_total_tp_p4_block_product) + (pa_s_hj32_local_total_tp_p4_block_product))) /\ pa_s_hj32_local_total_tp_p4_block_product = pa_r_hj32_local_total_tp_p4_block_product * pa_p_hj32_local_total_tp_p4_block_product))))))))
  30. 0030specialize htotal 4
  31. 0031specialize htotal 4 * m
  32. 0032exact htotal
  33. 0033cases tp_p4_block
  34. 0034have tp_block_bound : exists bqb_le_gap_hj32_local_block_bound_tp_block_bound. bqb_le_gap_hj32_local_block_bound_tp_block_bound + (x3) = (x4)
  35. 0035specialize pow_block_bound_from_total 3
  36. 0036specialize pow_block_bound_from_total 4
  37. 0037specialize pow_block_bound_from_total 5
  38. 0038specialize pow_block_bound_from_total 4
  39. 0039specialize pow_block_bound_from_total m
  40. 0040specialize pow_block_bound_from_total x1
  41. 0041specialize pow_block_bound_from_total x2
  42. 0042specialize pow_block_bound_from_total x3
  43. 0043specialize pow_block_bound_from_total x4
  44. 0044apply pow_block_bound_from_total
  45. 0045exact htotal
  46. 0046exact tp_p3_five_witness
  47. 0047exact tp_p4_four_witness
  48. 0048exact tp_seed
  49. 0049exact tp_p3_block_witness
  50. 0050exact tp_p4_block_witness
  51. 0051have tp_p3_one : exists hj32_local_value_tp_p3_one. (exists pa_b_hj32_local_total_tp_p3_one pa_c_hj32_local_total_tp_p3_one. ((forall pa_i_hj32_local_total_tp_p3_one_repeat. (exists pa_lt_hj32_local_total_tp_p3_one_repeat_bound. pa_lt_hj32_local_total_tp_p3_one_repeat_bound + S pa_i_hj32_local_total_tp_p3_one_repeat = 1) -> (((exists pa_h_hj32_local_total_tp_p3_one_repeat_decoded. pa_h_hj32_local_total_tp_p3_one_repeat_decoded + S (3) = S ((S (pa_i_hj32_local_total_tp_p3_one_repeat)) * pa_c_hj32_local_total_tp_p3_one)) /\ exists pa_q_hj32_local_total_tp_p3_one_repeat_decoded. pa_b_hj32_local_total_tp_p3_one = pa_q_hj32_local_total_tp_p3_one_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p3_one_repeat)) * pa_c_hj32_local_total_tp_p3_one) + (3)))) /\ (exists pa_u_hj32_local_total_tp_p3_one_product pa_v_hj32_local_total_tp_p3_one_product. ((((exists pa_h_hj32_local_total_tp_p3_one_product_start. pa_h_hj32_local_total_tp_p3_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_start. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p3_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p3_one_product_terminal. pa_h_hj32_local_total_tp_p3_one_product_terminal + S (hj32_local_value_tp_p3_one) = S ((S (1)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_terminal. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_tp_p3_one_product) + (hj32_local_value_tp_p3_one))) /\ forall pa_i_hj32_local_total_tp_p3_one_product. (exists pa_lt_hj32_local_total_tp_p3_one_product_bound. pa_lt_hj32_local_total_tp_p3_one_product_bound + S pa_i_hj32_local_total_tp_p3_one_product = 1) -> exists pa_p_hj32_local_total_tp_p3_one_product pa_r_hj32_local_total_tp_p3_one_product pa_s_hj32_local_total_tp_p3_one_product. ((((exists pa_h_hj32_local_total_tp_p3_one_product_factor. pa_h_hj32_local_total_tp_p3_one_product_factor + S (pa_p_hj32_local_total_tp_p3_one_product) = S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_c_hj32_local_total_tp_p3_one)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_factor. pa_b_hj32_local_total_tp_p3_one = pa_q_hj32_local_total_tp_p3_one_product_factor * S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_c_hj32_local_total_tp_p3_one) + (pa_p_hj32_local_total_tp_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_one_product_partial. pa_h_hj32_local_total_tp_p3_one_product_partial + S (pa_r_hj32_local_total_tp_p3_one_product) = S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_partial. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_partial * S ((S (pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product) + (pa_r_hj32_local_total_tp_p3_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p3_one_product_successor. pa_h_hj32_local_total_tp_p3_one_product_successor + S (pa_s_hj32_local_total_tp_p3_one_product) = S ((S (S pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product)) /\ exists pa_q_hj32_local_total_tp_p3_one_product_successor. pa_u_hj32_local_total_tp_p3_one_product = pa_q_hj32_local_total_tp_p3_one_product_successor * S ((S (S pa_i_hj32_local_total_tp_p3_one_product)) * pa_v_hj32_local_total_tp_p3_one_product) + (pa_s_hj32_local_total_tp_p3_one_product))) /\ pa_s_hj32_local_total_tp_p3_one_product = pa_r_hj32_local_total_tp_p3_one_product * pa_p_hj32_local_total_tp_p3_one_product))))))))
  52. 0052specialize htotal 3
  53. 0053specialize htotal 1
  54. 0054exact htotal
  55. 0055cases tp_p3_one
  56. 0056have tp_p4_one : exists hj32_local_value_tp_p4_one. (exists pa_b_hj32_local_total_tp_p4_one pa_c_hj32_local_total_tp_p4_one. ((forall pa_i_hj32_local_total_tp_p4_one_repeat. (exists pa_lt_hj32_local_total_tp_p4_one_repeat_bound. pa_lt_hj32_local_total_tp_p4_one_repeat_bound + S pa_i_hj32_local_total_tp_p4_one_repeat = 1) -> (((exists pa_h_hj32_local_total_tp_p4_one_repeat_decoded. pa_h_hj32_local_total_tp_p4_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_tp_p4_one_repeat)) * pa_c_hj32_local_total_tp_p4_one)) /\ exists pa_q_hj32_local_total_tp_p4_one_repeat_decoded. pa_b_hj32_local_total_tp_p4_one = pa_q_hj32_local_total_tp_p4_one_repeat_decoded * S ((S (pa_i_hj32_local_total_tp_p4_one_repeat)) * pa_c_hj32_local_total_tp_p4_one) + (4)))) /\ (exists pa_u_hj32_local_total_tp_p4_one_product pa_v_hj32_local_total_tp_p4_one_product. ((((exists pa_h_hj32_local_total_tp_p4_one_product_start. pa_h_hj32_local_total_tp_p4_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_start. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_start * S ((S (0)) * pa_v_hj32_local_total_tp_p4_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_tp_p4_one_product_terminal. pa_h_hj32_local_total_tp_p4_one_product_terminal + S (hj32_local_value_tp_p4_one) = S ((S (1)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_terminal. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_tp_p4_one_product) + (hj32_local_value_tp_p4_one))) /\ forall pa_i_hj32_local_total_tp_p4_one_product. (exists pa_lt_hj32_local_total_tp_p4_one_product_bound. pa_lt_hj32_local_total_tp_p4_one_product_bound + S pa_i_hj32_local_total_tp_p4_one_product = 1) -> exists pa_p_hj32_local_total_tp_p4_one_product pa_r_hj32_local_total_tp_p4_one_product pa_s_hj32_local_total_tp_p4_one_product. ((((exists pa_h_hj32_local_total_tp_p4_one_product_factor. pa_h_hj32_local_total_tp_p4_one_product_factor + S (pa_p_hj32_local_total_tp_p4_one_product) = S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_c_hj32_local_total_tp_p4_one)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_factor. pa_b_hj32_local_total_tp_p4_one = pa_q_hj32_local_total_tp_p4_one_product_factor * S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_c_hj32_local_total_tp_p4_one) + (pa_p_hj32_local_total_tp_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_one_product_partial. pa_h_hj32_local_total_tp_p4_one_product_partial + S (pa_r_hj32_local_total_tp_p4_one_product) = S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_partial. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_partial * S ((S (pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product) + (pa_r_hj32_local_total_tp_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_tp_p4_one_product_successor. pa_h_hj32_local_total_tp_p4_one_product_successor + S (pa_s_hj32_local_total_tp_p4_one_product) = S ((S (S pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product)) /\ exists pa_q_hj32_local_total_tp_p4_one_product_successor. pa_u_hj32_local_total_tp_p4_one_product = pa_q_hj32_local_total_tp_p4_one_product_successor * S ((S (S pa_i_hj32_local_total_tp_p4_one_product)) * pa_v_hj32_local_total_tp_p4_one_product) + (pa_s_hj32_local_total_tp_p4_one_product))) /\ pa_s_hj32_local_total_tp_p4_one_product = pa_r_hj32_local_total_tp_p4_one_product * pa_p_hj32_local_total_tp_p4_one_product))))))))
  57. 0057specialize htotal 4
  58. 0058specialize htotal 1
  59. 0059exact htotal
  60. 0060cases tp_p4_one
  61. 0061have tp_base : exists bqb_le_gap_hj32_tp_base. bqb_le_gap_hj32_tp_base + (3) = (4)
  62. 0062exists 1
  63. 0063norm_num
  64. 0064have tp_one_bound : exists bqb_le_gap_hj32_local_base_bound_tp_one_bound. bqb_le_gap_hj32_local_base_bound_tp_one_bound + (x5) = (x6)
  65. 0065specialize pow_base_monotone 3
  66. 0066specialize pow_base_monotone 4
  67. 0067specialize pow_base_monotone 1
  68. 0068specialize pow_base_monotone x5
  69. 0069specialize pow_base_monotone x6
  70. 0070apply pow_base_monotone
  71. 0071exact tp_base
  72. 0072exact tp_p3_one_witness
  73. 0073exact tp_p4_one_witness
  74. 0074have tp_left_product : x = x3 * x5
  75. 0075specialize pow_add 3
  76. 0076specialize pow_add 5 * m
  77. 0077specialize pow_add 1
  78. 0078specialize pow_add 5 * m + 1
  79. 0079specialize pow_add x3
  80. 0080specialize pow_add x5
  81. 0081specialize pow_add x
  82. 0082apply pow_add
  83. 0083refl
  84. 0084exact tp_p3_block_witness
  85. 0085exact tp_p3_one_witness
  86. 0086exact hx
  87. 0087have tp_right_product : y = x4 * x6
  88. 0088specialize pow_add 4
  89. 0089specialize pow_add 4 * m
  90. 0090specialize pow_add 1
  91. 0091specialize pow_add 4 * m + 1
  92. 0092specialize pow_add x4
  93. 0093specialize pow_add x6
  94. 0094specialize pow_add y
  95. 0095apply pow_add
  96. 0096refl
  97. 0097exact tp_p4_block_witness
  98. 0098exact tp_p4_one_witness
  99. 0099exact hy
  100. 0100have tp_result : exists bqb_le_gap_hj32_local_product_bound_tp_result. bqb_le_gap_hj32_local_product_bound_tp_result + (x3 * x5) = (x4 * x6)
  101. 0101specialize mul_le_mul x3
  102. 0102specialize mul_le_mul x4
  103. 0103specialize mul_le_mul x5
  104. 0104specialize mul_le_mul x6
  105. 0105apply mul_le_mul
  106. 0106exact tp_block_bound
  107. 0107exact tp_one_bound
  108. 0108rewrite <- tp_left_product at tp_result
  109. 0109rewrite <- tp_right_product at tp_result
  110. 0110exact tp_result