BT00WJ

pow_two_successor_double_le_pow_four_successor_from_total

Alpha body-checked · checked-use disabled

An odd power of two is bounded by the next power of four.

Exact expanded PA statement

forall k x y. (forall bpt_a_hj32_two_odd bpt_e_hj32_two_odd. exists bpt_x_hj32_two_odd. (exists ff_b_bpt_value_hj32_two_odd ff_c_bpt_value_hj32_two_odd. ((forall ff_i_bpt_value_hj32_two_odd_repeat. (exists ff_lt_bpt_value_hj32_two_odd_repeat_bound. ff_lt_bpt_value_hj32_two_odd_repeat_bound + S ff_i_bpt_value_hj32_two_odd_repeat = bpt_e_hj32_two_odd) -> (((exists ff_h_bpt_value_hj32_two_odd_repeat_decoded. ff_h_bpt_value_hj32_two_odd_repeat_decoded + S (bpt_a_hj32_two_odd) = S ((S (ff_i_bpt_value_hj32_two_odd_repeat)) * ff_c_bpt_value_hj32_two_odd)) /\ exists ff_q_bpt_value_hj32_two_odd_repeat_decoded. ff_b_bpt_value_hj32_two_odd = ff_q_bpt_value_hj32_two_odd_repeat_decoded * S ((S (ff_i_bpt_value_hj32_two_odd_repeat)) * ff_c_bpt_value_hj32_two_odd) + (bpt_a_hj32_two_odd)))) /\ (exists ff_u_bpt_value_hj32_two_odd_product ff_v_bpt_value_hj32_two_odd_product. ((((exists ff_h_bpt_value_hj32_two_odd_product_start. ff_h_bpt_value_hj32_two_odd_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_start. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_start * S ((S (0)) * ff_v_bpt_value_hj32_two_odd_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_two_odd_product_terminal. ff_h_bpt_value_hj32_two_odd_product_terminal + S (bpt_x_hj32_two_odd) = S ((S (bpt_e_hj32_two_odd)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_terminal. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_terminal * S ((S (bpt_e_hj32_two_odd)) * ff_v_bpt_value_hj32_two_odd_product) + (bpt_x_hj32_two_odd))) /\ forall ff_i_bpt_value_hj32_two_odd_product. (exists ff_lt_bpt_value_hj32_two_odd_product_bound. ff_lt_bpt_value_hj32_two_odd_product_bound + S ff_i_bpt_value_hj32_two_odd_product = bpt_e_hj32_two_odd) -> exists ff_p_bpt_value_hj32_two_odd_product ff_r_bpt_value_hj32_two_odd_product ff_s_bpt_value_hj32_two_odd_product. ((((exists ff_h_bpt_value_hj32_two_odd_product_factor. ff_h_bpt_value_hj32_two_odd_product_factor + S (ff_p_bpt_value_hj32_two_odd_product) = S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_c_bpt_value_hj32_two_odd)) /\ exists ff_q_bpt_value_hj32_two_odd_product_factor. ff_b_bpt_value_hj32_two_odd = ff_q_bpt_value_hj32_two_odd_product_factor * S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_c_bpt_value_hj32_two_odd) + (ff_p_bpt_value_hj32_two_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_two_odd_product_partial. ff_h_bpt_value_hj32_two_odd_product_partial + S (ff_r_bpt_value_hj32_two_odd_product) = S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_partial. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_partial * S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product) + (ff_r_bpt_value_hj32_two_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_two_odd_product_successor. ff_h_bpt_value_hj32_two_odd_product_successor + S (ff_s_bpt_value_hj32_two_odd_product) = S ((S (S ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_successor. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_successor * S ((S (S ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product) + (ff_s_bpt_value_hj32_two_odd_product))) /\ ff_s_bpt_value_hj32_two_odd_product = ff_r_bpt_value_hj32_two_odd_product * ff_p_bpt_value_hj32_two_odd_product))))))))) -> (exists pa_b_hj32_two_odd_left pa_c_hj32_two_odd_left. ((forall pa_i_hj32_two_odd_left_repeat. (exists pa_lt_hj32_two_odd_left_repeat_bound. pa_lt_hj32_two_odd_left_repeat_bound + S pa_i_hj32_two_odd_left_repeat = 2 * k + 1) -> (((exists pa_h_hj32_two_odd_left_repeat_decoded. pa_h_hj32_two_odd_left_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_odd_left_repeat)) * pa_c_hj32_two_odd_left)) /\ exists pa_q_hj32_two_odd_left_repeat_decoded. pa_b_hj32_two_odd_left = pa_q_hj32_two_odd_left_repeat_decoded * S ((S (pa_i_hj32_two_odd_left_repeat)) * pa_c_hj32_two_odd_left) + (2)))) /\ (exists pa_u_hj32_two_odd_left_product pa_v_hj32_two_odd_left_product. ((((exists pa_h_hj32_two_odd_left_product_start. pa_h_hj32_two_odd_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_start. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_start * S ((S (0)) * pa_v_hj32_two_odd_left_product) + (1))) /\ ((((exists pa_h_hj32_two_odd_left_product_terminal. pa_h_hj32_two_odd_left_product_terminal + S (x) = S ((S (2 * k + 1)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_terminal. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_terminal * S ((S (2 * k + 1)) * pa_v_hj32_two_odd_left_product) + (x))) /\ forall pa_i_hj32_two_odd_left_product. (exists pa_lt_hj32_two_odd_left_product_bound. pa_lt_hj32_two_odd_left_product_bound + S pa_i_hj32_two_odd_left_product = 2 * k + 1) -> exists pa_p_hj32_two_odd_left_product pa_r_hj32_two_odd_left_product pa_s_hj32_two_odd_left_product. ((((exists pa_h_hj32_two_odd_left_product_factor. pa_h_hj32_two_odd_left_product_factor + S (pa_p_hj32_two_odd_left_product) = S ((S (pa_i_hj32_two_odd_left_product)) * pa_c_hj32_two_odd_left)) /\ exists pa_q_hj32_two_odd_left_product_factor. pa_b_hj32_two_odd_left = pa_q_hj32_two_odd_left_product_factor * S ((S (pa_i_hj32_two_odd_left_product)) * pa_c_hj32_two_odd_left) + (pa_p_hj32_two_odd_left_product))) /\ ((((exists pa_h_hj32_two_odd_left_product_partial. pa_h_hj32_two_odd_left_product_partial + S (pa_r_hj32_two_odd_left_product) = S ((S (pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_partial. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_partial * S ((S (pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product) + (pa_r_hj32_two_odd_left_product))) /\ ((((exists pa_h_hj32_two_odd_left_product_successor. pa_h_hj32_two_odd_left_product_successor + S (pa_s_hj32_two_odd_left_product) = S ((S (S pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_successor. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_successor * S ((S (S pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product) + (pa_s_hj32_two_odd_left_product))) /\ pa_s_hj32_two_odd_left_product = pa_r_hj32_two_odd_left_product * pa_p_hj32_two_odd_left_product)))))))) -> (exists pa_b_hj32_two_odd_right pa_c_hj32_two_odd_right. ((forall pa_i_hj32_two_odd_right_repeat. (exists pa_lt_hj32_two_odd_right_repeat_bound. pa_lt_hj32_two_odd_right_repeat_bound + S pa_i_hj32_two_odd_right_repeat = k + 1) -> (((exists pa_h_hj32_two_odd_right_repeat_decoded. pa_h_hj32_two_odd_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_two_odd_right_repeat)) * pa_c_hj32_two_odd_right)) /\ exists pa_q_hj32_two_odd_right_repeat_decoded. pa_b_hj32_two_odd_right = pa_q_hj32_two_odd_right_repeat_decoded * S ((S (pa_i_hj32_two_odd_right_repeat)) * pa_c_hj32_two_odd_right) + (4)))) /\ (exists pa_u_hj32_two_odd_right_product pa_v_hj32_two_odd_right_product. ((((exists pa_h_hj32_two_odd_right_product_start. pa_h_hj32_two_odd_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_start. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_start * S ((S (0)) * pa_v_hj32_two_odd_right_product) + (1))) /\ ((((exists pa_h_hj32_two_odd_right_product_terminal. pa_h_hj32_two_odd_right_product_terminal + S (y) = S ((S (k + 1)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_terminal. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_terminal * S ((S (k + 1)) * pa_v_hj32_two_odd_right_product) + (y))) /\ forall pa_i_hj32_two_odd_right_product. (exists pa_lt_hj32_two_odd_right_product_bound. pa_lt_hj32_two_odd_right_product_bound + S pa_i_hj32_two_odd_right_product = k + 1) -> exists pa_p_hj32_two_odd_right_product pa_r_hj32_two_odd_right_product pa_s_hj32_two_odd_right_product. ((((exists pa_h_hj32_two_odd_right_product_factor. pa_h_hj32_two_odd_right_product_factor + S (pa_p_hj32_two_odd_right_product) = S ((S (pa_i_hj32_two_odd_right_product)) * pa_c_hj32_two_odd_right)) /\ exists pa_q_hj32_two_odd_right_product_factor. pa_b_hj32_two_odd_right = pa_q_hj32_two_odd_right_product_factor * S ((S (pa_i_hj32_two_odd_right_product)) * pa_c_hj32_two_odd_right) + (pa_p_hj32_two_odd_right_product))) /\ ((((exists pa_h_hj32_two_odd_right_product_partial. pa_h_hj32_two_odd_right_product_partial + S (pa_r_hj32_two_odd_right_product) = S ((S (pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_partial. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_partial * S ((S (pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product) + (pa_r_hj32_two_odd_right_product))) /\ ((((exists pa_h_hj32_two_odd_right_product_successor. pa_h_hj32_two_odd_right_product_successor + S (pa_s_hj32_two_odd_right_product) = S ((S (S pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_successor. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_successor * S ((S (S pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product) + (pa_s_hj32_two_odd_right_product))) /\ pa_s_hj32_two_odd_right_product = pa_r_hj32_two_odd_right_product * pa_p_hj32_two_odd_right_product)))))))) -> (exists bqb_le_gap_hj32_two_odd_result. bqb_le_gap_hj32_two_odd_result + (x) = (y))

Structural proof guide

An odd power of two is bounded by the next power of four.

Direct prerequisites: pow_two_double_eq_pow_four_from_total, pow_base_monotone, pow_add, mul_le_mul, le_refl. The authored body proceeds by case analysis (4), intermediate claims (11), equality transport (3), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT00WI pow_two_double_eq_pow_four_from_total BT00PY pow_base_monotone BT009X pow_add BT00PV mul_le_mul BT000E le_refl

Direct dependents

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 k
  2. 0002intro x
  3. 0003intro y
  4. 0004intro htotal
  5. 0005intro hx
  6. 0006intro hy
  7. 0007have to_p2_even : exists hj32_local_value_to_p2_even. (exists pa_b_hj32_local_total_to_p2_even pa_c_hj32_local_total_to_p2_even. ((forall pa_i_hj32_local_total_to_p2_even_repeat. (exists pa_lt_hj32_local_total_to_p2_even_repeat_bound. pa_lt_hj32_local_total_to_p2_even_repeat_bound + S pa_i_hj32_local_total_to_p2_even_repeat = 2 * k) -> (((exists pa_h_hj32_local_total_to_p2_even_repeat_decoded. pa_h_hj32_local_total_to_p2_even_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_to_p2_even_repeat)) * pa_c_hj32_local_total_to_p2_even)) /\ exists pa_q_hj32_local_total_to_p2_even_repeat_decoded. pa_b_hj32_local_total_to_p2_even = pa_q_hj32_local_total_to_p2_even_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p2_even_repeat)) * pa_c_hj32_local_total_to_p2_even) + (2)))) /\ (exists pa_u_hj32_local_total_to_p2_even_product pa_v_hj32_local_total_to_p2_even_product. ((((exists pa_h_hj32_local_total_to_p2_even_product_start. pa_h_hj32_local_total_to_p2_even_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_start. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p2_even_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p2_even_product_terminal. pa_h_hj32_local_total_to_p2_even_product_terminal + S (hj32_local_value_to_p2_even) = S ((S (2 * k)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_terminal. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_terminal * S ((S (2 * k)) * pa_v_hj32_local_total_to_p2_even_product) + (hj32_local_value_to_p2_even))) /\ forall pa_i_hj32_local_total_to_p2_even_product. (exists pa_lt_hj32_local_total_to_p2_even_product_bound. pa_lt_hj32_local_total_to_p2_even_product_bound + S pa_i_hj32_local_total_to_p2_even_product = 2 * k) -> exists pa_p_hj32_local_total_to_p2_even_product pa_r_hj32_local_total_to_p2_even_product pa_s_hj32_local_total_to_p2_even_product. ((((exists pa_h_hj32_local_total_to_p2_even_product_factor. pa_h_hj32_local_total_to_p2_even_product_factor + S (pa_p_hj32_local_total_to_p2_even_product) = S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_c_hj32_local_total_to_p2_even)) /\ exists pa_q_hj32_local_total_to_p2_even_product_factor. pa_b_hj32_local_total_to_p2_even = pa_q_hj32_local_total_to_p2_even_product_factor * S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_c_hj32_local_total_to_p2_even) + (pa_p_hj32_local_total_to_p2_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_even_product_partial. pa_h_hj32_local_total_to_p2_even_product_partial + S (pa_r_hj32_local_total_to_p2_even_product) = S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_partial. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_partial * S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product) + (pa_r_hj32_local_total_to_p2_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_even_product_successor. pa_h_hj32_local_total_to_p2_even_product_successor + S (pa_s_hj32_local_total_to_p2_even_product) = S ((S (S pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_successor. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_successor * S ((S (S pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product) + (pa_s_hj32_local_total_to_p2_even_product))) /\ pa_s_hj32_local_total_to_p2_even_product = pa_r_hj32_local_total_to_p2_even_product * pa_p_hj32_local_total_to_p2_even_product))))))))
  8. 0008specialize htotal 2
  9. 0009specialize htotal 2 * k
  10. 0010exact htotal
  11. 0011cases to_p2_even
  12. 0012have to_p2_one : exists hj32_local_value_to_p2_one. (exists pa_b_hj32_local_total_to_p2_one pa_c_hj32_local_total_to_p2_one. ((forall pa_i_hj32_local_total_to_p2_one_repeat. (exists pa_lt_hj32_local_total_to_p2_one_repeat_bound. pa_lt_hj32_local_total_to_p2_one_repeat_bound + S pa_i_hj32_local_total_to_p2_one_repeat = 1) -> (((exists pa_h_hj32_local_total_to_p2_one_repeat_decoded. pa_h_hj32_local_total_to_p2_one_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_to_p2_one_repeat)) * pa_c_hj32_local_total_to_p2_one)) /\ exists pa_q_hj32_local_total_to_p2_one_repeat_decoded. pa_b_hj32_local_total_to_p2_one = pa_q_hj32_local_total_to_p2_one_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p2_one_repeat)) * pa_c_hj32_local_total_to_p2_one) + (2)))) /\ (exists pa_u_hj32_local_total_to_p2_one_product pa_v_hj32_local_total_to_p2_one_product. ((((exists pa_h_hj32_local_total_to_p2_one_product_start. pa_h_hj32_local_total_to_p2_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_start. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p2_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p2_one_product_terminal. pa_h_hj32_local_total_to_p2_one_product_terminal + S (hj32_local_value_to_p2_one) = S ((S (1)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_terminal. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_to_p2_one_product) + (hj32_local_value_to_p2_one))) /\ forall pa_i_hj32_local_total_to_p2_one_product. (exists pa_lt_hj32_local_total_to_p2_one_product_bound. pa_lt_hj32_local_total_to_p2_one_product_bound + S pa_i_hj32_local_total_to_p2_one_product = 1) -> exists pa_p_hj32_local_total_to_p2_one_product pa_r_hj32_local_total_to_p2_one_product pa_s_hj32_local_total_to_p2_one_product. ((((exists pa_h_hj32_local_total_to_p2_one_product_factor. pa_h_hj32_local_total_to_p2_one_product_factor + S (pa_p_hj32_local_total_to_p2_one_product) = S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_c_hj32_local_total_to_p2_one)) /\ exists pa_q_hj32_local_total_to_p2_one_product_factor. pa_b_hj32_local_total_to_p2_one = pa_q_hj32_local_total_to_p2_one_product_factor * S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_c_hj32_local_total_to_p2_one) + (pa_p_hj32_local_total_to_p2_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_one_product_partial. pa_h_hj32_local_total_to_p2_one_product_partial + S (pa_r_hj32_local_total_to_p2_one_product) = S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_partial. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_partial * S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product) + (pa_r_hj32_local_total_to_p2_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_one_product_successor. pa_h_hj32_local_total_to_p2_one_product_successor + S (pa_s_hj32_local_total_to_p2_one_product) = S ((S (S pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_successor. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_successor * S ((S (S pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product) + (pa_s_hj32_local_total_to_p2_one_product))) /\ pa_s_hj32_local_total_to_p2_one_product = pa_r_hj32_local_total_to_p2_one_product * pa_p_hj32_local_total_to_p2_one_product))))))))
  13. 0013specialize htotal 2
  14. 0014specialize htotal 1
  15. 0015exact htotal
  16. 0016cases to_p2_one
  17. 0017have to_p4_even : exists hj32_local_value_to_p4_even. (exists pa_b_hj32_local_total_to_p4_even pa_c_hj32_local_total_to_p4_even. ((forall pa_i_hj32_local_total_to_p4_even_repeat. (exists pa_lt_hj32_local_total_to_p4_even_repeat_bound. pa_lt_hj32_local_total_to_p4_even_repeat_bound + S pa_i_hj32_local_total_to_p4_even_repeat = k) -> (((exists pa_h_hj32_local_total_to_p4_even_repeat_decoded. pa_h_hj32_local_total_to_p4_even_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_to_p4_even_repeat)) * pa_c_hj32_local_total_to_p4_even)) /\ exists pa_q_hj32_local_total_to_p4_even_repeat_decoded. pa_b_hj32_local_total_to_p4_even = pa_q_hj32_local_total_to_p4_even_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p4_even_repeat)) * pa_c_hj32_local_total_to_p4_even) + (4)))) /\ (exists pa_u_hj32_local_total_to_p4_even_product pa_v_hj32_local_total_to_p4_even_product. ((((exists pa_h_hj32_local_total_to_p4_even_product_start. pa_h_hj32_local_total_to_p4_even_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_start. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p4_even_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p4_even_product_terminal. pa_h_hj32_local_total_to_p4_even_product_terminal + S (hj32_local_value_to_p4_even) = S ((S (k)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_terminal. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_terminal * S ((S (k)) * pa_v_hj32_local_total_to_p4_even_product) + (hj32_local_value_to_p4_even))) /\ forall pa_i_hj32_local_total_to_p4_even_product. (exists pa_lt_hj32_local_total_to_p4_even_product_bound. pa_lt_hj32_local_total_to_p4_even_product_bound + S pa_i_hj32_local_total_to_p4_even_product = k) -> exists pa_p_hj32_local_total_to_p4_even_product pa_r_hj32_local_total_to_p4_even_product pa_s_hj32_local_total_to_p4_even_product. ((((exists pa_h_hj32_local_total_to_p4_even_product_factor. pa_h_hj32_local_total_to_p4_even_product_factor + S (pa_p_hj32_local_total_to_p4_even_product) = S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_c_hj32_local_total_to_p4_even)) /\ exists pa_q_hj32_local_total_to_p4_even_product_factor. pa_b_hj32_local_total_to_p4_even = pa_q_hj32_local_total_to_p4_even_product_factor * S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_c_hj32_local_total_to_p4_even) + (pa_p_hj32_local_total_to_p4_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_even_product_partial. pa_h_hj32_local_total_to_p4_even_product_partial + S (pa_r_hj32_local_total_to_p4_even_product) = S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_partial. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_partial * S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product) + (pa_r_hj32_local_total_to_p4_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_even_product_successor. pa_h_hj32_local_total_to_p4_even_product_successor + S (pa_s_hj32_local_total_to_p4_even_product) = S ((S (S pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_successor. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_successor * S ((S (S pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product) + (pa_s_hj32_local_total_to_p4_even_product))) /\ pa_s_hj32_local_total_to_p4_even_product = pa_r_hj32_local_total_to_p4_even_product * pa_p_hj32_local_total_to_p4_even_product))))))))
  18. 0018specialize htotal 4
  19. 0019specialize htotal k
  20. 0020exact htotal
  21. 0021cases to_p4_even
  22. 0022have to_p4_one : exists hj32_local_value_to_p4_one. (exists pa_b_hj32_local_total_to_p4_one pa_c_hj32_local_total_to_p4_one. ((forall pa_i_hj32_local_total_to_p4_one_repeat. (exists pa_lt_hj32_local_total_to_p4_one_repeat_bound. pa_lt_hj32_local_total_to_p4_one_repeat_bound + S pa_i_hj32_local_total_to_p4_one_repeat = 1) -> (((exists pa_h_hj32_local_total_to_p4_one_repeat_decoded. pa_h_hj32_local_total_to_p4_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_to_p4_one_repeat)) * pa_c_hj32_local_total_to_p4_one)) /\ exists pa_q_hj32_local_total_to_p4_one_repeat_decoded. pa_b_hj32_local_total_to_p4_one = pa_q_hj32_local_total_to_p4_one_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p4_one_repeat)) * pa_c_hj32_local_total_to_p4_one) + (4)))) /\ (exists pa_u_hj32_local_total_to_p4_one_product pa_v_hj32_local_total_to_p4_one_product. ((((exists pa_h_hj32_local_total_to_p4_one_product_start. pa_h_hj32_local_total_to_p4_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_start. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p4_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p4_one_product_terminal. pa_h_hj32_local_total_to_p4_one_product_terminal + S (hj32_local_value_to_p4_one) = S ((S (1)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_terminal. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_to_p4_one_product) + (hj32_local_value_to_p4_one))) /\ forall pa_i_hj32_local_total_to_p4_one_product. (exists pa_lt_hj32_local_total_to_p4_one_product_bound. pa_lt_hj32_local_total_to_p4_one_product_bound + S pa_i_hj32_local_total_to_p4_one_product = 1) -> exists pa_p_hj32_local_total_to_p4_one_product pa_r_hj32_local_total_to_p4_one_product pa_s_hj32_local_total_to_p4_one_product. ((((exists pa_h_hj32_local_total_to_p4_one_product_factor. pa_h_hj32_local_total_to_p4_one_product_factor + S (pa_p_hj32_local_total_to_p4_one_product) = S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_c_hj32_local_total_to_p4_one)) /\ exists pa_q_hj32_local_total_to_p4_one_product_factor. pa_b_hj32_local_total_to_p4_one = pa_q_hj32_local_total_to_p4_one_product_factor * S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_c_hj32_local_total_to_p4_one) + (pa_p_hj32_local_total_to_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_one_product_partial. pa_h_hj32_local_total_to_p4_one_product_partial + S (pa_r_hj32_local_total_to_p4_one_product) = S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_partial. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_partial * S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product) + (pa_r_hj32_local_total_to_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_one_product_successor. pa_h_hj32_local_total_to_p4_one_product_successor + S (pa_s_hj32_local_total_to_p4_one_product) = S ((S (S pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_successor. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_successor * S ((S (S pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product) + (pa_s_hj32_local_total_to_p4_one_product))) /\ pa_s_hj32_local_total_to_p4_one_product = pa_r_hj32_local_total_to_p4_one_product * pa_p_hj32_local_total_to_p4_one_product))))))))
  23. 0023specialize htotal 4
  24. 0024specialize htotal 1
  25. 0025exact htotal
  26. 0026cases to_p4_one
  27. 0027have to_even_eq : x1 = x3
  28. 0028specialize pow_two_double_eq_pow_four_from_total k
  29. 0029specialize pow_two_double_eq_pow_four_from_total x1
  30. 0030specialize pow_two_double_eq_pow_four_from_total x3
  31. 0031apply pow_two_double_eq_pow_four_from_total
  32. 0032exact htotal
  33. 0033exact to_p2_even_witness
  34. 0034exact to_p4_even_witness
  35. 0035have to_even_bound : exists bqb_le_gap_hj32_to_even_bound. bqb_le_gap_hj32_to_even_bound + (x1) = (x3)
  36. 0036rewrite to_even_eq
  37. 0037specialize le_refl x3
  38. 0038exact le_refl
  39. 0039have to_base : exists bqb_le_gap_hj32_to_base. bqb_le_gap_hj32_to_base + (2) = (4)
  40. 0040exists 2
  41. 0041norm_num
  42. 0042have to_one_bound : exists bqb_le_gap_hj32_local_base_bound_to_one_bound. bqb_le_gap_hj32_local_base_bound_to_one_bound + (x2) = (x4)
  43. 0043specialize pow_base_monotone 2
  44. 0044specialize pow_base_monotone 4
  45. 0045specialize pow_base_monotone 1
  46. 0046specialize pow_base_monotone x2
  47. 0047specialize pow_base_monotone x4
  48. 0048apply pow_base_monotone
  49. 0049exact to_base
  50. 0050exact to_p2_one_witness
  51. 0051exact to_p4_one_witness
  52. 0052have to_left_product : x = x1 * x2
  53. 0053specialize pow_add 2
  54. 0054specialize pow_add 2 * k
  55. 0055specialize pow_add 1
  56. 0056specialize pow_add 2 * k + 1
  57. 0057specialize pow_add x1
  58. 0058specialize pow_add x2
  59. 0059specialize pow_add x
  60. 0060apply pow_add
  61. 0061refl
  62. 0062exact to_p2_even_witness
  63. 0063exact to_p2_one_witness
  64. 0064exact hx
  65. 0065have to_right_product : y = x3 * x4
  66. 0066specialize pow_add 4
  67. 0067specialize pow_add k
  68. 0068specialize pow_add 1
  69. 0069specialize pow_add k + 1
  70. 0070specialize pow_add x3
  71. 0071specialize pow_add x4
  72. 0072specialize pow_add y
  73. 0073apply pow_add
  74. 0074refl
  75. 0075exact to_p4_even_witness
  76. 0076exact to_p4_one_witness
  77. 0077exact hy
  78. 0078have to_result : exists bqb_le_gap_hj32_local_product_bound_to_result. bqb_le_gap_hj32_local_product_bound_to_result + (x1 * x2) = (x3 * x4)
  79. 0079specialize mul_le_mul x1
  80. 0080specialize mul_le_mul x3
  81. 0081specialize mul_le_mul x2
  82. 0082specialize mul_le_mul x4
  83. 0083apply mul_le_mul
  84. 0084exact to_even_bound
  85. 0085exact to_one_bound
  86. 0086rewrite <- to_left_product at to_result
  87. 0087rewrite <- to_right_product at to_result
  88. 0088exact to_result