BT00WI

pow_two_double_eq_pow_four_from_total

Alpha body-checked · checked-use disabled

An even power of two is the matching power of four.

Exact expanded PA statement

forall k x y. (forall bpt_a_hj32_two_double bpt_e_hj32_two_double. exists bpt_x_hj32_two_double. (exists ff_b_bpt_value_hj32_two_double ff_c_bpt_value_hj32_two_double. ((forall ff_i_bpt_value_hj32_two_double_repeat. (exists ff_lt_bpt_value_hj32_two_double_repeat_bound. ff_lt_bpt_value_hj32_two_double_repeat_bound + S ff_i_bpt_value_hj32_two_double_repeat = bpt_e_hj32_two_double) -> (((exists ff_h_bpt_value_hj32_two_double_repeat_decoded. ff_h_bpt_value_hj32_two_double_repeat_decoded + S (bpt_a_hj32_two_double) = S ((S (ff_i_bpt_value_hj32_two_double_repeat)) * ff_c_bpt_value_hj32_two_double)) /\ exists ff_q_bpt_value_hj32_two_double_repeat_decoded. ff_b_bpt_value_hj32_two_double = ff_q_bpt_value_hj32_two_double_repeat_decoded * S ((S (ff_i_bpt_value_hj32_two_double_repeat)) * ff_c_bpt_value_hj32_two_double) + (bpt_a_hj32_two_double)))) /\ (exists ff_u_bpt_value_hj32_two_double_product ff_v_bpt_value_hj32_two_double_product. ((((exists ff_h_bpt_value_hj32_two_double_product_start. ff_h_bpt_value_hj32_two_double_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_two_double_product)) /\ exists ff_q_bpt_value_hj32_two_double_product_start. ff_u_bpt_value_hj32_two_double_product = ff_q_bpt_value_hj32_two_double_product_start * S ((S (0)) * ff_v_bpt_value_hj32_two_double_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_two_double_product_terminal. ff_h_bpt_value_hj32_two_double_product_terminal + S (bpt_x_hj32_two_double) = S ((S (bpt_e_hj32_two_double)) * ff_v_bpt_value_hj32_two_double_product)) /\ exists ff_q_bpt_value_hj32_two_double_product_terminal. ff_u_bpt_value_hj32_two_double_product = ff_q_bpt_value_hj32_two_double_product_terminal * S ((S (bpt_e_hj32_two_double)) * ff_v_bpt_value_hj32_two_double_product) + (bpt_x_hj32_two_double))) /\ forall ff_i_bpt_value_hj32_two_double_product. (exists ff_lt_bpt_value_hj32_two_double_product_bound. ff_lt_bpt_value_hj32_two_double_product_bound + S ff_i_bpt_value_hj32_two_double_product = bpt_e_hj32_two_double) -> exists ff_p_bpt_value_hj32_two_double_product ff_r_bpt_value_hj32_two_double_product ff_s_bpt_value_hj32_two_double_product. ((((exists ff_h_bpt_value_hj32_two_double_product_factor. ff_h_bpt_value_hj32_two_double_product_factor + S (ff_p_bpt_value_hj32_two_double_product) = S ((S (ff_i_bpt_value_hj32_two_double_product)) * ff_c_bpt_value_hj32_two_double)) /\ exists ff_q_bpt_value_hj32_two_double_product_factor. ff_b_bpt_value_hj32_two_double = ff_q_bpt_value_hj32_two_double_product_factor * S ((S (ff_i_bpt_value_hj32_two_double_product)) * ff_c_bpt_value_hj32_two_double) + (ff_p_bpt_value_hj32_two_double_product))) /\ ((((exists ff_h_bpt_value_hj32_two_double_product_partial. ff_h_bpt_value_hj32_two_double_product_partial + S (ff_r_bpt_value_hj32_two_double_product) = S ((S (ff_i_bpt_value_hj32_two_double_product)) * ff_v_bpt_value_hj32_two_double_product)) /\ exists ff_q_bpt_value_hj32_two_double_product_partial. ff_u_bpt_value_hj32_two_double_product = ff_q_bpt_value_hj32_two_double_product_partial * S ((S (ff_i_bpt_value_hj32_two_double_product)) * ff_v_bpt_value_hj32_two_double_product) + (ff_r_bpt_value_hj32_two_double_product))) /\ ((((exists ff_h_bpt_value_hj32_two_double_product_successor. ff_h_bpt_value_hj32_two_double_product_successor + S (ff_s_bpt_value_hj32_two_double_product) = S ((S (S ff_i_bpt_value_hj32_two_double_product)) * ff_v_bpt_value_hj32_two_double_product)) /\ exists ff_q_bpt_value_hj32_two_double_product_successor. ff_u_bpt_value_hj32_two_double_product = ff_q_bpt_value_hj32_two_double_product_successor * S ((S (S ff_i_bpt_value_hj32_two_double_product)) * ff_v_bpt_value_hj32_two_double_product) + (ff_s_bpt_value_hj32_two_double_product))) /\ ff_s_bpt_value_hj32_two_double_product = ff_r_bpt_value_hj32_two_double_product * ff_p_bpt_value_hj32_two_double_product))))))))) -> (exists pa_b_hj32_two_double_left pa_c_hj32_two_double_left. ((forall pa_i_hj32_two_double_left_repeat. (exists pa_lt_hj32_two_double_left_repeat_bound. pa_lt_hj32_two_double_left_repeat_bound + S pa_i_hj32_two_double_left_repeat = 2 * k) -> (((exists pa_h_hj32_two_double_left_repeat_decoded. pa_h_hj32_two_double_left_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_double_left_repeat)) * pa_c_hj32_two_double_left)) /\ exists pa_q_hj32_two_double_left_repeat_decoded. pa_b_hj32_two_double_left = pa_q_hj32_two_double_left_repeat_decoded * S ((S (pa_i_hj32_two_double_left_repeat)) * pa_c_hj32_two_double_left) + (2)))) /\ (exists pa_u_hj32_two_double_left_product pa_v_hj32_two_double_left_product. ((((exists pa_h_hj32_two_double_left_product_start. pa_h_hj32_two_double_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_double_left_product)) /\ exists pa_q_hj32_two_double_left_product_start. pa_u_hj32_two_double_left_product = pa_q_hj32_two_double_left_product_start * S ((S (0)) * pa_v_hj32_two_double_left_product) + (1))) /\ ((((exists pa_h_hj32_two_double_left_product_terminal. pa_h_hj32_two_double_left_product_terminal + S (x) = S ((S (2 * k)) * pa_v_hj32_two_double_left_product)) /\ exists pa_q_hj32_two_double_left_product_terminal. pa_u_hj32_two_double_left_product = pa_q_hj32_two_double_left_product_terminal * S ((S (2 * k)) * pa_v_hj32_two_double_left_product) + (x))) /\ forall pa_i_hj32_two_double_left_product. (exists pa_lt_hj32_two_double_left_product_bound. pa_lt_hj32_two_double_left_product_bound + S pa_i_hj32_two_double_left_product = 2 * k) -> exists pa_p_hj32_two_double_left_product pa_r_hj32_two_double_left_product pa_s_hj32_two_double_left_product. ((((exists pa_h_hj32_two_double_left_product_factor. pa_h_hj32_two_double_left_product_factor + S (pa_p_hj32_two_double_left_product) = S ((S (pa_i_hj32_two_double_left_product)) * pa_c_hj32_two_double_left)) /\ exists pa_q_hj32_two_double_left_product_factor. pa_b_hj32_two_double_left = pa_q_hj32_two_double_left_product_factor * S ((S (pa_i_hj32_two_double_left_product)) * pa_c_hj32_two_double_left) + (pa_p_hj32_two_double_left_product))) /\ ((((exists pa_h_hj32_two_double_left_product_partial. pa_h_hj32_two_double_left_product_partial + S (pa_r_hj32_two_double_left_product) = S ((S (pa_i_hj32_two_double_left_product)) * pa_v_hj32_two_double_left_product)) /\ exists pa_q_hj32_two_double_left_product_partial. pa_u_hj32_two_double_left_product = pa_q_hj32_two_double_left_product_partial * S ((S (pa_i_hj32_two_double_left_product)) * pa_v_hj32_two_double_left_product) + (pa_r_hj32_two_double_left_product))) /\ ((((exists pa_h_hj32_two_double_left_product_successor. pa_h_hj32_two_double_left_product_successor + S (pa_s_hj32_two_double_left_product) = S ((S (S pa_i_hj32_two_double_left_product)) * pa_v_hj32_two_double_left_product)) /\ exists pa_q_hj32_two_double_left_product_successor. pa_u_hj32_two_double_left_product = pa_q_hj32_two_double_left_product_successor * S ((S (S pa_i_hj32_two_double_left_product)) * pa_v_hj32_two_double_left_product) + (pa_s_hj32_two_double_left_product))) /\ pa_s_hj32_two_double_left_product = pa_r_hj32_two_double_left_product * pa_p_hj32_two_double_left_product)))))))) -> (exists pa_b_hj32_two_double_right pa_c_hj32_two_double_right. ((forall pa_i_hj32_two_double_right_repeat. (exists pa_lt_hj32_two_double_right_repeat_bound. pa_lt_hj32_two_double_right_repeat_bound + S pa_i_hj32_two_double_right_repeat = k) -> (((exists pa_h_hj32_two_double_right_repeat_decoded. pa_h_hj32_two_double_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_two_double_right_repeat)) * pa_c_hj32_two_double_right)) /\ exists pa_q_hj32_two_double_right_repeat_decoded. pa_b_hj32_two_double_right = pa_q_hj32_two_double_right_repeat_decoded * S ((S (pa_i_hj32_two_double_right_repeat)) * pa_c_hj32_two_double_right) + (4)))) /\ (exists pa_u_hj32_two_double_right_product pa_v_hj32_two_double_right_product. ((((exists pa_h_hj32_two_double_right_product_start. pa_h_hj32_two_double_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_double_right_product)) /\ exists pa_q_hj32_two_double_right_product_start. pa_u_hj32_two_double_right_product = pa_q_hj32_two_double_right_product_start * S ((S (0)) * pa_v_hj32_two_double_right_product) + (1))) /\ ((((exists pa_h_hj32_two_double_right_product_terminal. pa_h_hj32_two_double_right_product_terminal + S (y) = S ((S (k)) * pa_v_hj32_two_double_right_product)) /\ exists pa_q_hj32_two_double_right_product_terminal. pa_u_hj32_two_double_right_product = pa_q_hj32_two_double_right_product_terminal * S ((S (k)) * pa_v_hj32_two_double_right_product) + (y))) /\ forall pa_i_hj32_two_double_right_product. (exists pa_lt_hj32_two_double_right_product_bound. pa_lt_hj32_two_double_right_product_bound + S pa_i_hj32_two_double_right_product = k) -> exists pa_p_hj32_two_double_right_product pa_r_hj32_two_double_right_product pa_s_hj32_two_double_right_product. ((((exists pa_h_hj32_two_double_right_product_factor. pa_h_hj32_two_double_right_product_factor + S (pa_p_hj32_two_double_right_product) = S ((S (pa_i_hj32_two_double_right_product)) * pa_c_hj32_two_double_right)) /\ exists pa_q_hj32_two_double_right_product_factor. pa_b_hj32_two_double_right = pa_q_hj32_two_double_right_product_factor * S ((S (pa_i_hj32_two_double_right_product)) * pa_c_hj32_two_double_right) + (pa_p_hj32_two_double_right_product))) /\ ((((exists pa_h_hj32_two_double_right_product_partial. pa_h_hj32_two_double_right_product_partial + S (pa_r_hj32_two_double_right_product) = S ((S (pa_i_hj32_two_double_right_product)) * pa_v_hj32_two_double_right_product)) /\ exists pa_q_hj32_two_double_right_product_partial. pa_u_hj32_two_double_right_product = pa_q_hj32_two_double_right_product_partial * S ((S (pa_i_hj32_two_double_right_product)) * pa_v_hj32_two_double_right_product) + (pa_r_hj32_two_double_right_product))) /\ ((((exists pa_h_hj32_two_double_right_product_successor. pa_h_hj32_two_double_right_product_successor + S (pa_s_hj32_two_double_right_product) = S ((S (S pa_i_hj32_two_double_right_product)) * pa_v_hj32_two_double_right_product)) /\ exists pa_q_hj32_two_double_right_product_successor. pa_u_hj32_two_double_right_product = pa_q_hj32_two_double_right_product_successor * S ((S (S pa_i_hj32_two_double_right_product)) * pa_v_hj32_two_double_right_product) + (pa_s_hj32_two_double_right_product))) /\ pa_s_hj32_two_double_right_product = pa_r_hj32_two_double_right_product * pa_p_hj32_two_double_right_product)))))))) -> x = y

Structural proof guide

An even power of two is the matching power of four.

Direct prerequisites: pow_two_seed_bundle_from_total, pow_mul_exp_from_total. The authored body proceeds by case analysis (1), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT00SO pow_two_seed_bundle_from_total BT00SM pow_mul_exp_from_total

Direct dependents

BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WL pow_eleven_double_block_le_pow_four_even_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 td_seeds : (exists pa_b_hj32_seed_two_two pa_c_hj32_seed_two_two. ((forall pa_i_hj32_seed_two_two_repeat. (exists pa_lt_hj32_seed_two_two_repeat_bound. pa_lt_hj32_seed_two_two_repeat_bound + S pa_i_hj32_seed_two_two_repeat = 2) -> (((exists pa_h_hj32_seed_two_two_repeat_decoded. pa_h_hj32_seed_two_two_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_repeat_decoded. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_repeat_decoded * S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two) + (2)))) /\ (exists pa_u_hj32_seed_two_two_product pa_v_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_start. pa_h_hj32_seed_two_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_start. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_start * S ((S (0)) * pa_v_hj32_seed_two_two_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_two_product_terminal. pa_h_hj32_seed_two_two_product_terminal + S (4) = S ((S (2)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_terminal. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_terminal * S ((S (2)) * pa_v_hj32_seed_two_two_product) + (4))) /\ forall pa_i_hj32_seed_two_two_product. (exists pa_lt_hj32_seed_two_two_product_bound. pa_lt_hj32_seed_two_two_product_bound + S pa_i_hj32_seed_two_two_product = 2) -> exists pa_p_hj32_seed_two_two_product pa_r_hj32_seed_two_two_product pa_s_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_factor. pa_h_hj32_seed_two_two_product_factor + S (pa_p_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_product_factor. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_product_factor * S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two) + (pa_p_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_partial. pa_h_hj32_seed_two_two_product_partial + S (pa_r_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_partial. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_partial * S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_r_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_successor. pa_h_hj32_seed_two_two_product_successor + S (pa_s_hj32_seed_two_two_product) = S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_successor. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_successor * S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_s_hj32_seed_two_two_product))) /\ pa_s_hj32_seed_two_two_product = pa_r_hj32_seed_two_two_product * pa_p_hj32_seed_two_two_product)))))))) /\ (exists pa_b_hj32_seed_two_seven pa_c_hj32_seed_two_seven. ((forall pa_i_hj32_seed_two_seven_repeat. (exists pa_lt_hj32_seed_two_seven_repeat_bound. pa_lt_hj32_seed_two_seven_repeat_bound + S pa_i_hj32_seed_two_seven_repeat = 7) -> (((exists pa_h_hj32_seed_two_seven_repeat_decoded. pa_h_hj32_seed_two_seven_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_repeat_decoded. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_repeat_decoded * S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven) + (2)))) /\ (exists pa_u_hj32_seed_two_seven_product pa_v_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_start. pa_h_hj32_seed_two_seven_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_start. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_start * S ((S (0)) * pa_v_hj32_seed_two_seven_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_seven_product_terminal. pa_h_hj32_seed_two_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_terminal. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_terminal * S ((S (7)) * pa_v_hj32_seed_two_seven_product) + (128))) /\ forall pa_i_hj32_seed_two_seven_product. (exists pa_lt_hj32_seed_two_seven_product_bound. pa_lt_hj32_seed_two_seven_product_bound + S pa_i_hj32_seed_two_seven_product = 7) -> exists pa_p_hj32_seed_two_seven_product pa_r_hj32_seed_two_seven_product pa_s_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_factor. pa_h_hj32_seed_two_seven_product_factor + S (pa_p_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_product_factor. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_product_factor * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven) + (pa_p_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_partial. pa_h_hj32_seed_two_seven_product_partial + S (pa_r_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_partial. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_partial * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_r_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_successor. pa_h_hj32_seed_two_seven_product_successor + S (pa_s_hj32_seed_two_seven_product) = S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_successor. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_successor * S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_s_hj32_seed_two_seven_product))) /\ pa_s_hj32_seed_two_seven_product = pa_r_hj32_seed_two_seven_product * pa_p_hj32_seed_two_seven_product))))))))
  8. 0008apply pow_two_seed_bundle_from_total
  9. 0009exact htotal
  10. 0010cases td_seeds
  11. 0011have td_bridge : y = x
  12. 0012specialize pow_mul_exp_from_total 2
  13. 0013specialize pow_mul_exp_from_total 2
  14. 0014specialize pow_mul_exp_from_total k
  15. 0015specialize pow_mul_exp_from_total (2 * k)
  16. 0016specialize pow_mul_exp_from_total 4
  17. 0017specialize pow_mul_exp_from_total y
  18. 0018specialize pow_mul_exp_from_total x
  19. 0019apply pow_mul_exp_from_total
  20. 0020exact htotal
  21. 0021refl
  22. 0022exact td_seeds_left
  23. 0023exact hy
  24. 0024exact hx
  25. 0025symm
  26. 0026exact td_bridge