BT00WK

pow_eleven_double_block_le_pow_two_seven_block_from_total

Alpha body-checked · checked-use disabled

The seed 11^2 <= 2^7 extends through a common block count.

Exact expanded PA statement

forall m x y. (forall bpt_a_hj32_eleven_block bpt_e_hj32_eleven_block. exists bpt_x_hj32_eleven_block. (exists ff_b_bpt_value_hj32_eleven_block ff_c_bpt_value_hj32_eleven_block. ((forall ff_i_bpt_value_hj32_eleven_block_repeat. (exists ff_lt_bpt_value_hj32_eleven_block_repeat_bound. ff_lt_bpt_value_hj32_eleven_block_repeat_bound + S ff_i_bpt_value_hj32_eleven_block_repeat = bpt_e_hj32_eleven_block) -> (((exists ff_h_bpt_value_hj32_eleven_block_repeat_decoded. ff_h_bpt_value_hj32_eleven_block_repeat_decoded + S (bpt_a_hj32_eleven_block) = S ((S (ff_i_bpt_value_hj32_eleven_block_repeat)) * ff_c_bpt_value_hj32_eleven_block)) /\ exists ff_q_bpt_value_hj32_eleven_block_repeat_decoded. ff_b_bpt_value_hj32_eleven_block = ff_q_bpt_value_hj32_eleven_block_repeat_decoded * S ((S (ff_i_bpt_value_hj32_eleven_block_repeat)) * ff_c_bpt_value_hj32_eleven_block) + (bpt_a_hj32_eleven_block)))) /\ (exists ff_u_bpt_value_hj32_eleven_block_product ff_v_bpt_value_hj32_eleven_block_product. ((((exists ff_h_bpt_value_hj32_eleven_block_product_start. ff_h_bpt_value_hj32_eleven_block_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_eleven_block_product)) /\ exists ff_q_bpt_value_hj32_eleven_block_product_start. ff_u_bpt_value_hj32_eleven_block_product = ff_q_bpt_value_hj32_eleven_block_product_start * S ((S (0)) * ff_v_bpt_value_hj32_eleven_block_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_eleven_block_product_terminal. ff_h_bpt_value_hj32_eleven_block_product_terminal + S (bpt_x_hj32_eleven_block) = S ((S (bpt_e_hj32_eleven_block)) * ff_v_bpt_value_hj32_eleven_block_product)) /\ exists ff_q_bpt_value_hj32_eleven_block_product_terminal. ff_u_bpt_value_hj32_eleven_block_product = ff_q_bpt_value_hj32_eleven_block_product_terminal * S ((S (bpt_e_hj32_eleven_block)) * ff_v_bpt_value_hj32_eleven_block_product) + (bpt_x_hj32_eleven_block))) /\ forall ff_i_bpt_value_hj32_eleven_block_product. (exists ff_lt_bpt_value_hj32_eleven_block_product_bound. ff_lt_bpt_value_hj32_eleven_block_product_bound + S ff_i_bpt_value_hj32_eleven_block_product = bpt_e_hj32_eleven_block) -> exists ff_p_bpt_value_hj32_eleven_block_product ff_r_bpt_value_hj32_eleven_block_product ff_s_bpt_value_hj32_eleven_block_product. ((((exists ff_h_bpt_value_hj32_eleven_block_product_factor. ff_h_bpt_value_hj32_eleven_block_product_factor + S (ff_p_bpt_value_hj32_eleven_block_product) = S ((S (ff_i_bpt_value_hj32_eleven_block_product)) * ff_c_bpt_value_hj32_eleven_block)) /\ exists ff_q_bpt_value_hj32_eleven_block_product_factor. ff_b_bpt_value_hj32_eleven_block = ff_q_bpt_value_hj32_eleven_block_product_factor * S ((S (ff_i_bpt_value_hj32_eleven_block_product)) * ff_c_bpt_value_hj32_eleven_block) + (ff_p_bpt_value_hj32_eleven_block_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_block_product_partial. ff_h_bpt_value_hj32_eleven_block_product_partial + S (ff_r_bpt_value_hj32_eleven_block_product) = S ((S (ff_i_bpt_value_hj32_eleven_block_product)) * ff_v_bpt_value_hj32_eleven_block_product)) /\ exists ff_q_bpt_value_hj32_eleven_block_product_partial. ff_u_bpt_value_hj32_eleven_block_product = ff_q_bpt_value_hj32_eleven_block_product_partial * S ((S (ff_i_bpt_value_hj32_eleven_block_product)) * ff_v_bpt_value_hj32_eleven_block_product) + (ff_r_bpt_value_hj32_eleven_block_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_block_product_successor. ff_h_bpt_value_hj32_eleven_block_product_successor + S (ff_s_bpt_value_hj32_eleven_block_product) = S ((S (S ff_i_bpt_value_hj32_eleven_block_product)) * ff_v_bpt_value_hj32_eleven_block_product)) /\ exists ff_q_bpt_value_hj32_eleven_block_product_successor. ff_u_bpt_value_hj32_eleven_block_product = ff_q_bpt_value_hj32_eleven_block_product_successor * S ((S (S ff_i_bpt_value_hj32_eleven_block_product)) * ff_v_bpt_value_hj32_eleven_block_product) + (ff_s_bpt_value_hj32_eleven_block_product))) /\ ff_s_bpt_value_hj32_eleven_block_product = ff_r_bpt_value_hj32_eleven_block_product * ff_p_bpt_value_hj32_eleven_block_product))))))))) -> (exists pa_b_hj32_eleven_block_left pa_c_hj32_eleven_block_left. ((forall pa_i_hj32_eleven_block_left_repeat. (exists pa_lt_hj32_eleven_block_left_repeat_bound. pa_lt_hj32_eleven_block_left_repeat_bound + S pa_i_hj32_eleven_block_left_repeat = 2 * m) -> (((exists pa_h_hj32_eleven_block_left_repeat_decoded. pa_h_hj32_eleven_block_left_repeat_decoded + S (11) = S ((S (pa_i_hj32_eleven_block_left_repeat)) * pa_c_hj32_eleven_block_left)) /\ exists pa_q_hj32_eleven_block_left_repeat_decoded. pa_b_hj32_eleven_block_left = pa_q_hj32_eleven_block_left_repeat_decoded * S ((S (pa_i_hj32_eleven_block_left_repeat)) * pa_c_hj32_eleven_block_left) + (11)))) /\ (exists pa_u_hj32_eleven_block_left_product pa_v_hj32_eleven_block_left_product. ((((exists pa_h_hj32_eleven_block_left_product_start. pa_h_hj32_eleven_block_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_block_left_product)) /\ exists pa_q_hj32_eleven_block_left_product_start. pa_u_hj32_eleven_block_left_product = pa_q_hj32_eleven_block_left_product_start * S ((S (0)) * pa_v_hj32_eleven_block_left_product) + (1))) /\ ((((exists pa_h_hj32_eleven_block_left_product_terminal. pa_h_hj32_eleven_block_left_product_terminal + S (x) = S ((S (2 * m)) * pa_v_hj32_eleven_block_left_product)) /\ exists pa_q_hj32_eleven_block_left_product_terminal. pa_u_hj32_eleven_block_left_product = pa_q_hj32_eleven_block_left_product_terminal * S ((S (2 * m)) * pa_v_hj32_eleven_block_left_product) + (x))) /\ forall pa_i_hj32_eleven_block_left_product. (exists pa_lt_hj32_eleven_block_left_product_bound. pa_lt_hj32_eleven_block_left_product_bound + S pa_i_hj32_eleven_block_left_product = 2 * m) -> exists pa_p_hj32_eleven_block_left_product pa_r_hj32_eleven_block_left_product pa_s_hj32_eleven_block_left_product. ((((exists pa_h_hj32_eleven_block_left_product_factor. pa_h_hj32_eleven_block_left_product_factor + S (pa_p_hj32_eleven_block_left_product) = S ((S (pa_i_hj32_eleven_block_left_product)) * pa_c_hj32_eleven_block_left)) /\ exists pa_q_hj32_eleven_block_left_product_factor. pa_b_hj32_eleven_block_left = pa_q_hj32_eleven_block_left_product_factor * S ((S (pa_i_hj32_eleven_block_left_product)) * pa_c_hj32_eleven_block_left) + (pa_p_hj32_eleven_block_left_product))) /\ ((((exists pa_h_hj32_eleven_block_left_product_partial. pa_h_hj32_eleven_block_left_product_partial + S (pa_r_hj32_eleven_block_left_product) = S ((S (pa_i_hj32_eleven_block_left_product)) * pa_v_hj32_eleven_block_left_product)) /\ exists pa_q_hj32_eleven_block_left_product_partial. pa_u_hj32_eleven_block_left_product = pa_q_hj32_eleven_block_left_product_partial * S ((S (pa_i_hj32_eleven_block_left_product)) * pa_v_hj32_eleven_block_left_product) + (pa_r_hj32_eleven_block_left_product))) /\ ((((exists pa_h_hj32_eleven_block_left_product_successor. pa_h_hj32_eleven_block_left_product_successor + S (pa_s_hj32_eleven_block_left_product) = S ((S (S pa_i_hj32_eleven_block_left_product)) * pa_v_hj32_eleven_block_left_product)) /\ exists pa_q_hj32_eleven_block_left_product_successor. pa_u_hj32_eleven_block_left_product = pa_q_hj32_eleven_block_left_product_successor * S ((S (S pa_i_hj32_eleven_block_left_product)) * pa_v_hj32_eleven_block_left_product) + (pa_s_hj32_eleven_block_left_product))) /\ pa_s_hj32_eleven_block_left_product = pa_r_hj32_eleven_block_left_product * pa_p_hj32_eleven_block_left_product)))))))) -> (exists pa_b_hj32_eleven_block_right pa_c_hj32_eleven_block_right. ((forall pa_i_hj32_eleven_block_right_repeat. (exists pa_lt_hj32_eleven_block_right_repeat_bound. pa_lt_hj32_eleven_block_right_repeat_bound + S pa_i_hj32_eleven_block_right_repeat = 7 * m) -> (((exists pa_h_hj32_eleven_block_right_repeat_decoded. pa_h_hj32_eleven_block_right_repeat_decoded + S (2) = S ((S (pa_i_hj32_eleven_block_right_repeat)) * pa_c_hj32_eleven_block_right)) /\ exists pa_q_hj32_eleven_block_right_repeat_decoded. pa_b_hj32_eleven_block_right = pa_q_hj32_eleven_block_right_repeat_decoded * S ((S (pa_i_hj32_eleven_block_right_repeat)) * pa_c_hj32_eleven_block_right) + (2)))) /\ (exists pa_u_hj32_eleven_block_right_product pa_v_hj32_eleven_block_right_product. ((((exists pa_h_hj32_eleven_block_right_product_start. pa_h_hj32_eleven_block_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_block_right_product)) /\ exists pa_q_hj32_eleven_block_right_product_start. pa_u_hj32_eleven_block_right_product = pa_q_hj32_eleven_block_right_product_start * S ((S (0)) * pa_v_hj32_eleven_block_right_product) + (1))) /\ ((((exists pa_h_hj32_eleven_block_right_product_terminal. pa_h_hj32_eleven_block_right_product_terminal + S (y) = S ((S (7 * m)) * pa_v_hj32_eleven_block_right_product)) /\ exists pa_q_hj32_eleven_block_right_product_terminal. pa_u_hj32_eleven_block_right_product = pa_q_hj32_eleven_block_right_product_terminal * S ((S (7 * m)) * pa_v_hj32_eleven_block_right_product) + (y))) /\ forall pa_i_hj32_eleven_block_right_product. (exists pa_lt_hj32_eleven_block_right_product_bound. pa_lt_hj32_eleven_block_right_product_bound + S pa_i_hj32_eleven_block_right_product = 7 * m) -> exists pa_p_hj32_eleven_block_right_product pa_r_hj32_eleven_block_right_product pa_s_hj32_eleven_block_right_product. ((((exists pa_h_hj32_eleven_block_right_product_factor. pa_h_hj32_eleven_block_right_product_factor + S (pa_p_hj32_eleven_block_right_product) = S ((S (pa_i_hj32_eleven_block_right_product)) * pa_c_hj32_eleven_block_right)) /\ exists pa_q_hj32_eleven_block_right_product_factor. pa_b_hj32_eleven_block_right = pa_q_hj32_eleven_block_right_product_factor * S ((S (pa_i_hj32_eleven_block_right_product)) * pa_c_hj32_eleven_block_right) + (pa_p_hj32_eleven_block_right_product))) /\ ((((exists pa_h_hj32_eleven_block_right_product_partial. pa_h_hj32_eleven_block_right_product_partial + S (pa_r_hj32_eleven_block_right_product) = S ((S (pa_i_hj32_eleven_block_right_product)) * pa_v_hj32_eleven_block_right_product)) /\ exists pa_q_hj32_eleven_block_right_product_partial. pa_u_hj32_eleven_block_right_product = pa_q_hj32_eleven_block_right_product_partial * S ((S (pa_i_hj32_eleven_block_right_product)) * pa_v_hj32_eleven_block_right_product) + (pa_r_hj32_eleven_block_right_product))) /\ ((((exists pa_h_hj32_eleven_block_right_product_successor. pa_h_hj32_eleven_block_right_product_successor + S (pa_s_hj32_eleven_block_right_product) = S ((S (S pa_i_hj32_eleven_block_right_product)) * pa_v_hj32_eleven_block_right_product)) /\ exists pa_q_hj32_eleven_block_right_product_successor. pa_u_hj32_eleven_block_right_product = pa_q_hj32_eleven_block_right_product_successor * S ((S (S pa_i_hj32_eleven_block_right_product)) * pa_v_hj32_eleven_block_right_product) + (pa_s_hj32_eleven_block_right_product))) /\ pa_s_hj32_eleven_block_right_product = pa_r_hj32_eleven_block_right_product * pa_p_hj32_eleven_block_right_product)))))))) -> (exists bqb_le_gap_hj32_eleven_block_result. bqb_le_gap_hj32_eleven_block_result + (x) = (y))

Structural proof guide

The seed 11^2 <= 2^7 extends through a common block count.

Direct prerequisites: pow_block_bound_from_total, pow_eleven_two_le_pow_two_seven_from_total. The authored body proceeds by case analysis (2), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT00W3 pow_block_bound_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total

Direct dependents

BT00WL pow_eleven_double_block_le_pow_four_even_from_total BT00WM pow_eleven_double_block_le_pow_four_odd_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 eb_p11_two : exists hj32_local_value_eb_p11_two. (exists pa_b_hj32_local_total_eb_p11_two pa_c_hj32_local_total_eb_p11_two. ((forall pa_i_hj32_local_total_eb_p11_two_repeat. (exists pa_lt_hj32_local_total_eb_p11_two_repeat_bound. pa_lt_hj32_local_total_eb_p11_two_repeat_bound + S pa_i_hj32_local_total_eb_p11_two_repeat = 2) -> (((exists pa_h_hj32_local_total_eb_p11_two_repeat_decoded. pa_h_hj32_local_total_eb_p11_two_repeat_decoded + S (11) = S ((S (pa_i_hj32_local_total_eb_p11_two_repeat)) * pa_c_hj32_local_total_eb_p11_two)) /\ exists pa_q_hj32_local_total_eb_p11_two_repeat_decoded. pa_b_hj32_local_total_eb_p11_two = pa_q_hj32_local_total_eb_p11_two_repeat_decoded * S ((S (pa_i_hj32_local_total_eb_p11_two_repeat)) * pa_c_hj32_local_total_eb_p11_two) + (11)))) /\ (exists pa_u_hj32_local_total_eb_p11_two_product pa_v_hj32_local_total_eb_p11_two_product. ((((exists pa_h_hj32_local_total_eb_p11_two_product_start. pa_h_hj32_local_total_eb_p11_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_eb_p11_two_product)) /\ exists pa_q_hj32_local_total_eb_p11_two_product_start. pa_u_hj32_local_total_eb_p11_two_product = pa_q_hj32_local_total_eb_p11_two_product_start * S ((S (0)) * pa_v_hj32_local_total_eb_p11_two_product) + (1))) /\ ((((exists pa_h_hj32_local_total_eb_p11_two_product_terminal. pa_h_hj32_local_total_eb_p11_two_product_terminal + S (hj32_local_value_eb_p11_two) = S ((S (2)) * pa_v_hj32_local_total_eb_p11_two_product)) /\ exists pa_q_hj32_local_total_eb_p11_two_product_terminal. pa_u_hj32_local_total_eb_p11_two_product = pa_q_hj32_local_total_eb_p11_two_product_terminal * S ((S (2)) * pa_v_hj32_local_total_eb_p11_two_product) + (hj32_local_value_eb_p11_two))) /\ forall pa_i_hj32_local_total_eb_p11_two_product. (exists pa_lt_hj32_local_total_eb_p11_two_product_bound. pa_lt_hj32_local_total_eb_p11_two_product_bound + S pa_i_hj32_local_total_eb_p11_two_product = 2) -> exists pa_p_hj32_local_total_eb_p11_two_product pa_r_hj32_local_total_eb_p11_two_product pa_s_hj32_local_total_eb_p11_two_product. ((((exists pa_h_hj32_local_total_eb_p11_two_product_factor. pa_h_hj32_local_total_eb_p11_two_product_factor + S (pa_p_hj32_local_total_eb_p11_two_product) = S ((S (pa_i_hj32_local_total_eb_p11_two_product)) * pa_c_hj32_local_total_eb_p11_two)) /\ exists pa_q_hj32_local_total_eb_p11_two_product_factor. pa_b_hj32_local_total_eb_p11_two = pa_q_hj32_local_total_eb_p11_two_product_factor * S ((S (pa_i_hj32_local_total_eb_p11_two_product)) * pa_c_hj32_local_total_eb_p11_two) + (pa_p_hj32_local_total_eb_p11_two_product))) /\ ((((exists pa_h_hj32_local_total_eb_p11_two_product_partial. pa_h_hj32_local_total_eb_p11_two_product_partial + S (pa_r_hj32_local_total_eb_p11_two_product) = S ((S (pa_i_hj32_local_total_eb_p11_two_product)) * pa_v_hj32_local_total_eb_p11_two_product)) /\ exists pa_q_hj32_local_total_eb_p11_two_product_partial. pa_u_hj32_local_total_eb_p11_two_product = pa_q_hj32_local_total_eb_p11_two_product_partial * S ((S (pa_i_hj32_local_total_eb_p11_two_product)) * pa_v_hj32_local_total_eb_p11_two_product) + (pa_r_hj32_local_total_eb_p11_two_product))) /\ ((((exists pa_h_hj32_local_total_eb_p11_two_product_successor. pa_h_hj32_local_total_eb_p11_two_product_successor + S (pa_s_hj32_local_total_eb_p11_two_product) = S ((S (S pa_i_hj32_local_total_eb_p11_two_product)) * pa_v_hj32_local_total_eb_p11_two_product)) /\ exists pa_q_hj32_local_total_eb_p11_two_product_successor. pa_u_hj32_local_total_eb_p11_two_product = pa_q_hj32_local_total_eb_p11_two_product_successor * S ((S (S pa_i_hj32_local_total_eb_p11_two_product)) * pa_v_hj32_local_total_eb_p11_two_product) + (pa_s_hj32_local_total_eb_p11_two_product))) /\ pa_s_hj32_local_total_eb_p11_two_product = pa_r_hj32_local_total_eb_p11_two_product * pa_p_hj32_local_total_eb_p11_two_product))))))))
  8. 0008specialize htotal 11
  9. 0009specialize htotal 2
  10. 0010exact htotal
  11. 0011cases eb_p11_two
  12. 0012have eb_p2_seven : exists hj32_local_value_eb_p2_seven. (exists pa_b_hj32_local_total_eb_p2_seven pa_c_hj32_local_total_eb_p2_seven. ((forall pa_i_hj32_local_total_eb_p2_seven_repeat. (exists pa_lt_hj32_local_total_eb_p2_seven_repeat_bound. pa_lt_hj32_local_total_eb_p2_seven_repeat_bound + S pa_i_hj32_local_total_eb_p2_seven_repeat = 7) -> (((exists pa_h_hj32_local_total_eb_p2_seven_repeat_decoded. pa_h_hj32_local_total_eb_p2_seven_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_eb_p2_seven_repeat)) * pa_c_hj32_local_total_eb_p2_seven)) /\ exists pa_q_hj32_local_total_eb_p2_seven_repeat_decoded. pa_b_hj32_local_total_eb_p2_seven = pa_q_hj32_local_total_eb_p2_seven_repeat_decoded * S ((S (pa_i_hj32_local_total_eb_p2_seven_repeat)) * pa_c_hj32_local_total_eb_p2_seven) + (2)))) /\ (exists pa_u_hj32_local_total_eb_p2_seven_product pa_v_hj32_local_total_eb_p2_seven_product. ((((exists pa_h_hj32_local_total_eb_p2_seven_product_start. pa_h_hj32_local_total_eb_p2_seven_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_eb_p2_seven_product)) /\ exists pa_q_hj32_local_total_eb_p2_seven_product_start. pa_u_hj32_local_total_eb_p2_seven_product = pa_q_hj32_local_total_eb_p2_seven_product_start * S ((S (0)) * pa_v_hj32_local_total_eb_p2_seven_product) + (1))) /\ ((((exists pa_h_hj32_local_total_eb_p2_seven_product_terminal. pa_h_hj32_local_total_eb_p2_seven_product_terminal + S (hj32_local_value_eb_p2_seven) = S ((S (7)) * pa_v_hj32_local_total_eb_p2_seven_product)) /\ exists pa_q_hj32_local_total_eb_p2_seven_product_terminal. pa_u_hj32_local_total_eb_p2_seven_product = pa_q_hj32_local_total_eb_p2_seven_product_terminal * S ((S (7)) * pa_v_hj32_local_total_eb_p2_seven_product) + (hj32_local_value_eb_p2_seven))) /\ forall pa_i_hj32_local_total_eb_p2_seven_product. (exists pa_lt_hj32_local_total_eb_p2_seven_product_bound. pa_lt_hj32_local_total_eb_p2_seven_product_bound + S pa_i_hj32_local_total_eb_p2_seven_product = 7) -> exists pa_p_hj32_local_total_eb_p2_seven_product pa_r_hj32_local_total_eb_p2_seven_product pa_s_hj32_local_total_eb_p2_seven_product. ((((exists pa_h_hj32_local_total_eb_p2_seven_product_factor. pa_h_hj32_local_total_eb_p2_seven_product_factor + S (pa_p_hj32_local_total_eb_p2_seven_product) = S ((S (pa_i_hj32_local_total_eb_p2_seven_product)) * pa_c_hj32_local_total_eb_p2_seven)) /\ exists pa_q_hj32_local_total_eb_p2_seven_product_factor. pa_b_hj32_local_total_eb_p2_seven = pa_q_hj32_local_total_eb_p2_seven_product_factor * S ((S (pa_i_hj32_local_total_eb_p2_seven_product)) * pa_c_hj32_local_total_eb_p2_seven) + (pa_p_hj32_local_total_eb_p2_seven_product))) /\ ((((exists pa_h_hj32_local_total_eb_p2_seven_product_partial. pa_h_hj32_local_total_eb_p2_seven_product_partial + S (pa_r_hj32_local_total_eb_p2_seven_product) = S ((S (pa_i_hj32_local_total_eb_p2_seven_product)) * pa_v_hj32_local_total_eb_p2_seven_product)) /\ exists pa_q_hj32_local_total_eb_p2_seven_product_partial. pa_u_hj32_local_total_eb_p2_seven_product = pa_q_hj32_local_total_eb_p2_seven_product_partial * S ((S (pa_i_hj32_local_total_eb_p2_seven_product)) * pa_v_hj32_local_total_eb_p2_seven_product) + (pa_r_hj32_local_total_eb_p2_seven_product))) /\ ((((exists pa_h_hj32_local_total_eb_p2_seven_product_successor. pa_h_hj32_local_total_eb_p2_seven_product_successor + S (pa_s_hj32_local_total_eb_p2_seven_product) = S ((S (S pa_i_hj32_local_total_eb_p2_seven_product)) * pa_v_hj32_local_total_eb_p2_seven_product)) /\ exists pa_q_hj32_local_total_eb_p2_seven_product_successor. pa_u_hj32_local_total_eb_p2_seven_product = pa_q_hj32_local_total_eb_p2_seven_product_successor * S ((S (S pa_i_hj32_local_total_eb_p2_seven_product)) * pa_v_hj32_local_total_eb_p2_seven_product) + (pa_s_hj32_local_total_eb_p2_seven_product))) /\ pa_s_hj32_local_total_eb_p2_seven_product = pa_r_hj32_local_total_eb_p2_seven_product * pa_p_hj32_local_total_eb_p2_seven_product))))))))
  13. 0013specialize htotal 2
  14. 0014specialize htotal 7
  15. 0015exact htotal
  16. 0016cases eb_p2_seven
  17. 0017have eb_seed : exists bqb_le_gap_hj32_eb_seed. bqb_le_gap_hj32_eb_seed + (x1) = (x2)
  18. 0018specialize pow_eleven_two_le_pow_two_seven_from_total x1
  19. 0019specialize pow_eleven_two_le_pow_two_seven_from_total x2
  20. 0020apply pow_eleven_two_le_pow_two_seven_from_total
  21. 0021exact htotal
  22. 0022exact eb_p11_two_witness
  23. 0023exact eb_p2_seven_witness
  24. 0024have eb_bound : exists bqb_le_gap_hj32_local_block_bound_eb_bound. bqb_le_gap_hj32_local_block_bound_eb_bound + (x) = (y)
  25. 0025specialize pow_block_bound_from_total 11
  26. 0026specialize pow_block_bound_from_total 2
  27. 0027specialize pow_block_bound_from_total 2
  28. 0028specialize pow_block_bound_from_total 7
  29. 0029specialize pow_block_bound_from_total m
  30. 0030specialize pow_block_bound_from_total x1
  31. 0031specialize pow_block_bound_from_total x2
  32. 0032specialize pow_block_bound_from_total x
  33. 0033specialize pow_block_bound_from_total y
  34. 0034apply pow_block_bound_from_total
  35. 0035exact htotal
  36. 0036exact eb_p11_two_witness
  37. 0037exact eb_p2_seven_witness
  38. 0038exact eb_seed
  39. 0039exact hx
  40. 0040exact hy
  41. 0041exact eb_bound