BT00WM

pow_eleven_double_block_le_pow_four_odd_from_total

Alpha body-checked · checked-use disabled

An odd 11-to-2 block exponent converts to the next base-four power.

Exact expanded PA statement

forall m k x y. (forall bpt_a_hj32_eleven_odd bpt_e_hj32_eleven_odd. exists bpt_x_hj32_eleven_odd. (exists ff_b_bpt_value_hj32_eleven_odd ff_c_bpt_value_hj32_eleven_odd. ((forall ff_i_bpt_value_hj32_eleven_odd_repeat. (exists ff_lt_bpt_value_hj32_eleven_odd_repeat_bound. ff_lt_bpt_value_hj32_eleven_odd_repeat_bound + S ff_i_bpt_value_hj32_eleven_odd_repeat = bpt_e_hj32_eleven_odd) -> (((exists ff_h_bpt_value_hj32_eleven_odd_repeat_decoded. ff_h_bpt_value_hj32_eleven_odd_repeat_decoded + S (bpt_a_hj32_eleven_odd) = S ((S (ff_i_bpt_value_hj32_eleven_odd_repeat)) * ff_c_bpt_value_hj32_eleven_odd)) /\ exists ff_q_bpt_value_hj32_eleven_odd_repeat_decoded. ff_b_bpt_value_hj32_eleven_odd = ff_q_bpt_value_hj32_eleven_odd_repeat_decoded * S ((S (ff_i_bpt_value_hj32_eleven_odd_repeat)) * ff_c_bpt_value_hj32_eleven_odd) + (bpt_a_hj32_eleven_odd)))) /\ (exists ff_u_bpt_value_hj32_eleven_odd_product ff_v_bpt_value_hj32_eleven_odd_product. ((((exists ff_h_bpt_value_hj32_eleven_odd_product_start. ff_h_bpt_value_hj32_eleven_odd_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_start. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_start * S ((S (0)) * ff_v_bpt_value_hj32_eleven_odd_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_eleven_odd_product_terminal. ff_h_bpt_value_hj32_eleven_odd_product_terminal + S (bpt_x_hj32_eleven_odd) = S ((S (bpt_e_hj32_eleven_odd)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_terminal. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_terminal * S ((S (bpt_e_hj32_eleven_odd)) * ff_v_bpt_value_hj32_eleven_odd_product) + (bpt_x_hj32_eleven_odd))) /\ forall ff_i_bpt_value_hj32_eleven_odd_product. (exists ff_lt_bpt_value_hj32_eleven_odd_product_bound. ff_lt_bpt_value_hj32_eleven_odd_product_bound + S ff_i_bpt_value_hj32_eleven_odd_product = bpt_e_hj32_eleven_odd) -> exists ff_p_bpt_value_hj32_eleven_odd_product ff_r_bpt_value_hj32_eleven_odd_product ff_s_bpt_value_hj32_eleven_odd_product. ((((exists ff_h_bpt_value_hj32_eleven_odd_product_factor. ff_h_bpt_value_hj32_eleven_odd_product_factor + S (ff_p_bpt_value_hj32_eleven_odd_product) = S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_c_bpt_value_hj32_eleven_odd)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_factor. ff_b_bpt_value_hj32_eleven_odd = ff_q_bpt_value_hj32_eleven_odd_product_factor * S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_c_bpt_value_hj32_eleven_odd) + (ff_p_bpt_value_hj32_eleven_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_odd_product_partial. ff_h_bpt_value_hj32_eleven_odd_product_partial + S (ff_r_bpt_value_hj32_eleven_odd_product) = S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_partial. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_partial * S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product) + (ff_r_bpt_value_hj32_eleven_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_odd_product_successor. ff_h_bpt_value_hj32_eleven_odd_product_successor + S (ff_s_bpt_value_hj32_eleven_odd_product) = S ((S (S ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_successor. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_successor * S ((S (S ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product) + (ff_s_bpt_value_hj32_eleven_odd_product))) /\ ff_s_bpt_value_hj32_eleven_odd_product = ff_r_bpt_value_hj32_eleven_odd_product * ff_p_bpt_value_hj32_eleven_odd_product))))))))) -> 7 * m = 2 * k + 1 -> (exists pa_b_hj32_eleven_odd_left pa_c_hj32_eleven_odd_left. ((forall pa_i_hj32_eleven_odd_left_repeat. (exists pa_lt_hj32_eleven_odd_left_repeat_bound. pa_lt_hj32_eleven_odd_left_repeat_bound + S pa_i_hj32_eleven_odd_left_repeat = 2 * m) -> (((exists pa_h_hj32_eleven_odd_left_repeat_decoded. pa_h_hj32_eleven_odd_left_repeat_decoded + S (11) = S ((S (pa_i_hj32_eleven_odd_left_repeat)) * pa_c_hj32_eleven_odd_left)) /\ exists pa_q_hj32_eleven_odd_left_repeat_decoded. pa_b_hj32_eleven_odd_left = pa_q_hj32_eleven_odd_left_repeat_decoded * S ((S (pa_i_hj32_eleven_odd_left_repeat)) * pa_c_hj32_eleven_odd_left) + (11)))) /\ (exists pa_u_hj32_eleven_odd_left_product pa_v_hj32_eleven_odd_left_product. ((((exists pa_h_hj32_eleven_odd_left_product_start. pa_h_hj32_eleven_odd_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_start. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_start * S ((S (0)) * pa_v_hj32_eleven_odd_left_product) + (1))) /\ ((((exists pa_h_hj32_eleven_odd_left_product_terminal. pa_h_hj32_eleven_odd_left_product_terminal + S (x) = S ((S (2 * m)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_terminal. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_terminal * S ((S (2 * m)) * pa_v_hj32_eleven_odd_left_product) + (x))) /\ forall pa_i_hj32_eleven_odd_left_product. (exists pa_lt_hj32_eleven_odd_left_product_bound. pa_lt_hj32_eleven_odd_left_product_bound + S pa_i_hj32_eleven_odd_left_product = 2 * m) -> exists pa_p_hj32_eleven_odd_left_product pa_r_hj32_eleven_odd_left_product pa_s_hj32_eleven_odd_left_product. ((((exists pa_h_hj32_eleven_odd_left_product_factor. pa_h_hj32_eleven_odd_left_product_factor + S (pa_p_hj32_eleven_odd_left_product) = S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_c_hj32_eleven_odd_left)) /\ exists pa_q_hj32_eleven_odd_left_product_factor. pa_b_hj32_eleven_odd_left = pa_q_hj32_eleven_odd_left_product_factor * S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_c_hj32_eleven_odd_left) + (pa_p_hj32_eleven_odd_left_product))) /\ ((((exists pa_h_hj32_eleven_odd_left_product_partial. pa_h_hj32_eleven_odd_left_product_partial + S (pa_r_hj32_eleven_odd_left_product) = S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_partial. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_partial * S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product) + (pa_r_hj32_eleven_odd_left_product))) /\ ((((exists pa_h_hj32_eleven_odd_left_product_successor. pa_h_hj32_eleven_odd_left_product_successor + S (pa_s_hj32_eleven_odd_left_product) = S ((S (S pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_successor. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_successor * S ((S (S pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product) + (pa_s_hj32_eleven_odd_left_product))) /\ pa_s_hj32_eleven_odd_left_product = pa_r_hj32_eleven_odd_left_product * pa_p_hj32_eleven_odd_left_product)))))))) -> (exists pa_b_hj32_eleven_odd_right pa_c_hj32_eleven_odd_right. ((forall pa_i_hj32_eleven_odd_right_repeat. (exists pa_lt_hj32_eleven_odd_right_repeat_bound. pa_lt_hj32_eleven_odd_right_repeat_bound + S pa_i_hj32_eleven_odd_right_repeat = k + 1) -> (((exists pa_h_hj32_eleven_odd_right_repeat_decoded. pa_h_hj32_eleven_odd_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_eleven_odd_right_repeat)) * pa_c_hj32_eleven_odd_right)) /\ exists pa_q_hj32_eleven_odd_right_repeat_decoded. pa_b_hj32_eleven_odd_right = pa_q_hj32_eleven_odd_right_repeat_decoded * S ((S (pa_i_hj32_eleven_odd_right_repeat)) * pa_c_hj32_eleven_odd_right) + (4)))) /\ (exists pa_u_hj32_eleven_odd_right_product pa_v_hj32_eleven_odd_right_product. ((((exists pa_h_hj32_eleven_odd_right_product_start. pa_h_hj32_eleven_odd_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_start. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_start * S ((S (0)) * pa_v_hj32_eleven_odd_right_product) + (1))) /\ ((((exists pa_h_hj32_eleven_odd_right_product_terminal. pa_h_hj32_eleven_odd_right_product_terminal + S (y) = S ((S (k + 1)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_terminal. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_terminal * S ((S (k + 1)) * pa_v_hj32_eleven_odd_right_product) + (y))) /\ forall pa_i_hj32_eleven_odd_right_product. (exists pa_lt_hj32_eleven_odd_right_product_bound. pa_lt_hj32_eleven_odd_right_product_bound + S pa_i_hj32_eleven_odd_right_product = k + 1) -> exists pa_p_hj32_eleven_odd_right_product pa_r_hj32_eleven_odd_right_product pa_s_hj32_eleven_odd_right_product. ((((exists pa_h_hj32_eleven_odd_right_product_factor. pa_h_hj32_eleven_odd_right_product_factor + S (pa_p_hj32_eleven_odd_right_product) = S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_c_hj32_eleven_odd_right)) /\ exists pa_q_hj32_eleven_odd_right_product_factor. pa_b_hj32_eleven_odd_right = pa_q_hj32_eleven_odd_right_product_factor * S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_c_hj32_eleven_odd_right) + (pa_p_hj32_eleven_odd_right_product))) /\ ((((exists pa_h_hj32_eleven_odd_right_product_partial. pa_h_hj32_eleven_odd_right_product_partial + S (pa_r_hj32_eleven_odd_right_product) = S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_partial. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_partial * S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product) + (pa_r_hj32_eleven_odd_right_product))) /\ ((((exists pa_h_hj32_eleven_odd_right_product_successor. pa_h_hj32_eleven_odd_right_product_successor + S (pa_s_hj32_eleven_odd_right_product) = S ((S (S pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_successor. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_successor * S ((S (S pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product) + (pa_s_hj32_eleven_odd_right_product))) /\ pa_s_hj32_eleven_odd_right_product = pa_r_hj32_eleven_odd_right_product * pa_p_hj32_eleven_odd_right_product)))))))) -> (exists bqb_le_gap_hj32_eleven_odd_result. bqb_le_gap_hj32_eleven_odd_result + (x) = (y))

Structural proof guide

An odd 11-to-2 block exponent converts to the next base-four power.

Direct prerequisites: pow_eleven_double_block_le_pow_two_seven_block_from_total, pow_two_successor_double_le_pow_four_successor_from_total, le_trans. The authored body proceeds by case analysis (1), intermediate claims (4), equality transport (4).

Proof neighborhood

Direct dependencies

BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT000F le_trans

Direct dependents

BT00WP bertrand_h_root_32_from_total BT00WT bertrand_h_root_36_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 k
  3. 0003intro x
  4. 0004intro y
  5. 0005intro htotal
  6. 0006intro hparity
  7. 0007intro hx
  8. 0008intro hy
  9. 0009have eo_p2 : exists hj32_local_value_eo_p2. (exists pa_b_hj32_local_total_eo_p2 pa_c_hj32_local_total_eo_p2. ((forall pa_i_hj32_local_total_eo_p2_repeat. (exists pa_lt_hj32_local_total_eo_p2_repeat_bound. pa_lt_hj32_local_total_eo_p2_repeat_bound + S pa_i_hj32_local_total_eo_p2_repeat = 7 * m) -> (((exists pa_h_hj32_local_total_eo_p2_repeat_decoded. pa_h_hj32_local_total_eo_p2_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_eo_p2_repeat)) * pa_c_hj32_local_total_eo_p2)) /\ exists pa_q_hj32_local_total_eo_p2_repeat_decoded. pa_b_hj32_local_total_eo_p2 = pa_q_hj32_local_total_eo_p2_repeat_decoded * S ((S (pa_i_hj32_local_total_eo_p2_repeat)) * pa_c_hj32_local_total_eo_p2) + (2)))) /\ (exists pa_u_hj32_local_total_eo_p2_product pa_v_hj32_local_total_eo_p2_product. ((((exists pa_h_hj32_local_total_eo_p2_product_start. pa_h_hj32_local_total_eo_p2_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_start. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_start * S ((S (0)) * pa_v_hj32_local_total_eo_p2_product) + (1))) /\ ((((exists pa_h_hj32_local_total_eo_p2_product_terminal. pa_h_hj32_local_total_eo_p2_product_terminal + S (hj32_local_value_eo_p2) = S ((S (7 * m)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_terminal. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_terminal * S ((S (7 * m)) * pa_v_hj32_local_total_eo_p2_product) + (hj32_local_value_eo_p2))) /\ forall pa_i_hj32_local_total_eo_p2_product. (exists pa_lt_hj32_local_total_eo_p2_product_bound. pa_lt_hj32_local_total_eo_p2_product_bound + S pa_i_hj32_local_total_eo_p2_product = 7 * m) -> exists pa_p_hj32_local_total_eo_p2_product pa_r_hj32_local_total_eo_p2_product pa_s_hj32_local_total_eo_p2_product. ((((exists pa_h_hj32_local_total_eo_p2_product_factor. pa_h_hj32_local_total_eo_p2_product_factor + S (pa_p_hj32_local_total_eo_p2_product) = S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_c_hj32_local_total_eo_p2)) /\ exists pa_q_hj32_local_total_eo_p2_product_factor. pa_b_hj32_local_total_eo_p2 = pa_q_hj32_local_total_eo_p2_product_factor * S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_c_hj32_local_total_eo_p2) + (pa_p_hj32_local_total_eo_p2_product))) /\ ((((exists pa_h_hj32_local_total_eo_p2_product_partial. pa_h_hj32_local_total_eo_p2_product_partial + S (pa_r_hj32_local_total_eo_p2_product) = S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_partial. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_partial * S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product) + (pa_r_hj32_local_total_eo_p2_product))) /\ ((((exists pa_h_hj32_local_total_eo_p2_product_successor. pa_h_hj32_local_total_eo_p2_product_successor + S (pa_s_hj32_local_total_eo_p2_product) = S ((S (S pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_successor. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_successor * S ((S (S pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product) + (pa_s_hj32_local_total_eo_p2_product))) /\ pa_s_hj32_local_total_eo_p2_product = pa_r_hj32_local_total_eo_p2_product * pa_p_hj32_local_total_eo_p2_product))))))))
  10. 0010specialize htotal 2
  11. 0011specialize htotal 7 * m
  12. 0012exact htotal
  13. 0013cases eo_p2
  14. 0014have eo_block : exists bqb_le_gap_hj32_eo_block. bqb_le_gap_hj32_eo_block + (x) = (x1)
  15. 0015specialize pow_eleven_double_block_le_pow_two_seven_block_from_total m
  16. 0016specialize pow_eleven_double_block_le_pow_two_seven_block_from_total x
  17. 0017specialize pow_eleven_double_block_le_pow_two_seven_block_from_total x1
  18. 0018apply pow_eleven_double_block_le_pow_two_seven_block_from_total
  19. 0019exact htotal
  20. 0020exact hx
  21. 0021exact eo_p2_witness
  22. 0022have eo_parity_power : exists pa_b_hj32_eo_parity_power pa_c_hj32_eo_parity_power. ((forall pa_i_hj32_eo_parity_power_repeat. (exists pa_lt_hj32_eo_parity_power_repeat_bound. pa_lt_hj32_eo_parity_power_repeat_bound + S pa_i_hj32_eo_parity_power_repeat = 2 * k + 1) -> (((exists pa_h_hj32_eo_parity_power_repeat_decoded. pa_h_hj32_eo_parity_power_repeat_decoded + S (2) = S ((S (pa_i_hj32_eo_parity_power_repeat)) * pa_c_hj32_eo_parity_power)) /\ exists pa_q_hj32_eo_parity_power_repeat_decoded. pa_b_hj32_eo_parity_power = pa_q_hj32_eo_parity_power_repeat_decoded * S ((S (pa_i_hj32_eo_parity_power_repeat)) * pa_c_hj32_eo_parity_power) + (2)))) /\ (exists pa_u_hj32_eo_parity_power_product pa_v_hj32_eo_parity_power_product. ((((exists pa_h_hj32_eo_parity_power_product_start. pa_h_hj32_eo_parity_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_start. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_start * S ((S (0)) * pa_v_hj32_eo_parity_power_product) + (1))) /\ ((((exists pa_h_hj32_eo_parity_power_product_terminal. pa_h_hj32_eo_parity_power_product_terminal + S (x1) = S ((S (2 * k + 1)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_terminal. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_terminal * S ((S (2 * k + 1)) * pa_v_hj32_eo_parity_power_product) + (x1))) /\ forall pa_i_hj32_eo_parity_power_product. (exists pa_lt_hj32_eo_parity_power_product_bound. pa_lt_hj32_eo_parity_power_product_bound + S pa_i_hj32_eo_parity_power_product = 2 * k + 1) -> exists pa_p_hj32_eo_parity_power_product pa_r_hj32_eo_parity_power_product pa_s_hj32_eo_parity_power_product. ((((exists pa_h_hj32_eo_parity_power_product_factor. pa_h_hj32_eo_parity_power_product_factor + S (pa_p_hj32_eo_parity_power_product) = S ((S (pa_i_hj32_eo_parity_power_product)) * pa_c_hj32_eo_parity_power)) /\ exists pa_q_hj32_eo_parity_power_product_factor. pa_b_hj32_eo_parity_power = pa_q_hj32_eo_parity_power_product_factor * S ((S (pa_i_hj32_eo_parity_power_product)) * pa_c_hj32_eo_parity_power) + (pa_p_hj32_eo_parity_power_product))) /\ ((((exists pa_h_hj32_eo_parity_power_product_partial. pa_h_hj32_eo_parity_power_product_partial + S (pa_r_hj32_eo_parity_power_product) = S ((S (pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_partial. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_partial * S ((S (pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product) + (pa_r_hj32_eo_parity_power_product))) /\ ((((exists pa_h_hj32_eo_parity_power_product_successor. pa_h_hj32_eo_parity_power_product_successor + S (pa_s_hj32_eo_parity_power_product) = S ((S (S pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_successor. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_successor * S ((S (S pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product) + (pa_s_hj32_eo_parity_power_product))) /\ pa_s_hj32_eo_parity_power_product = pa_r_hj32_eo_parity_power_product * pa_p_hj32_eo_parity_power_product)))))))
  23. 0023rewrite <- hparity
  24. 0024rewrite <- hparity
  25. 0025rewrite <- hparity
  26. 0026rewrite <- hparity
  27. 0027exact eo_p2_witness
  28. 0028have eo_bound : exists bqb_le_gap_hj32_eo_bound. bqb_le_gap_hj32_eo_bound + (x1) = (y)
  29. 0029specialize pow_two_successor_double_le_pow_four_successor_from_total k
  30. 0030specialize pow_two_successor_double_le_pow_four_successor_from_total x1
  31. 0031specialize pow_two_successor_double_le_pow_four_successor_from_total y
  32. 0032apply pow_two_successor_double_le_pow_four_successor_from_total
  33. 0033exact htotal
  34. 0034exact eo_parity_power
  35. 0035exact hy
  36. 0036specialize le_trans x
  37. 0037specialize le_trans x1
  38. 0038specialize le_trans y
  39. 0039apply le_trans
  40. 0040exact eo_block
  41. 0041exact eo_bound