BT00SO

pow_two_seed_bundle_from_total

Alpha body-checked · checked-use disabled

One totality premise yields the exact seeds 2^2=4 and 2^7=128.

Exact expanded PA statement

(forall bpt_a_seed bpt_e_seed. exists bpt_x_seed. (exists ff_b_bpt_value_seed ff_c_bpt_value_seed. ((forall ff_i_bpt_value_seed_repeat. (exists ff_lt_bpt_value_seed_repeat_bound. ff_lt_bpt_value_seed_repeat_bound + S ff_i_bpt_value_seed_repeat = bpt_e_seed) -> (((exists ff_h_bpt_value_seed_repeat_decoded. ff_h_bpt_value_seed_repeat_decoded + S (bpt_a_seed) = S ((S (ff_i_bpt_value_seed_repeat)) * ff_c_bpt_value_seed)) /\ exists ff_q_bpt_value_seed_repeat_decoded. ff_b_bpt_value_seed = ff_q_bpt_value_seed_repeat_decoded * S ((S (ff_i_bpt_value_seed_repeat)) * ff_c_bpt_value_seed) + (bpt_a_seed)))) /\ (exists ff_u_bpt_value_seed_product ff_v_bpt_value_seed_product. ((((exists ff_h_bpt_value_seed_product_start. ff_h_bpt_value_seed_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_start. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_start * S ((S (0)) * ff_v_bpt_value_seed_product) + (1))) /\ ((((exists ff_h_bpt_value_seed_product_terminal. ff_h_bpt_value_seed_product_terminal + S (bpt_x_seed) = S ((S (bpt_e_seed)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_terminal. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_terminal * S ((S (bpt_e_seed)) * ff_v_bpt_value_seed_product) + (bpt_x_seed))) /\ forall ff_i_bpt_value_seed_product. (exists ff_lt_bpt_value_seed_product_bound. ff_lt_bpt_value_seed_product_bound + S ff_i_bpt_value_seed_product = bpt_e_seed) -> exists ff_p_bpt_value_seed_product ff_r_bpt_value_seed_product ff_s_bpt_value_seed_product. ((((exists ff_h_bpt_value_seed_product_factor. ff_h_bpt_value_seed_product_factor + S (ff_p_bpt_value_seed_product) = S ((S (ff_i_bpt_value_seed_product)) * ff_c_bpt_value_seed)) /\ exists ff_q_bpt_value_seed_product_factor. ff_b_bpt_value_seed = ff_q_bpt_value_seed_product_factor * S ((S (ff_i_bpt_value_seed_product)) * ff_c_bpt_value_seed) + (ff_p_bpt_value_seed_product))) /\ ((((exists ff_h_bpt_value_seed_product_partial. ff_h_bpt_value_seed_product_partial + S (ff_r_bpt_value_seed_product) = S ((S (ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_partial. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_partial * S ((S (ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product) + (ff_r_bpt_value_seed_product))) /\ ((((exists ff_h_bpt_value_seed_product_successor. ff_h_bpt_value_seed_product_successor + S (ff_s_bpt_value_seed_product) = S ((S (S ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_successor. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_successor * S ((S (S ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product) + (ff_s_bpt_value_seed_product))) /\ ff_s_bpt_value_seed_product = ff_r_bpt_value_seed_product * ff_p_bpt_value_seed_product))))))))) -> ((exists pa_b_bpt_seed_two pa_c_bpt_seed_two. ((forall pa_i_bpt_seed_two_repeat. (exists pa_lt_bpt_seed_two_repeat_bound. pa_lt_bpt_seed_two_repeat_bound + S pa_i_bpt_seed_two_repeat = 2) -> (((exists pa_h_bpt_seed_two_repeat_decoded. pa_h_bpt_seed_two_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_repeat_decoded. pa_b_bpt_seed_two = pa_q_bpt_seed_two_repeat_decoded * S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two) + (2)))) /\ (exists pa_u_bpt_seed_two_product pa_v_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_start. pa_h_bpt_seed_two_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_start. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_start * S ((S (0)) * pa_v_bpt_seed_two_product) + (1))) /\ ((((exists pa_h_bpt_seed_two_product_terminal. pa_h_bpt_seed_two_product_terminal + S (4) = S ((S (2)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_terminal. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_terminal * S ((S (2)) * pa_v_bpt_seed_two_product) + (4))) /\ forall pa_i_bpt_seed_two_product. (exists pa_lt_bpt_seed_two_product_bound. pa_lt_bpt_seed_two_product_bound + S pa_i_bpt_seed_two_product = 2) -> exists pa_p_bpt_seed_two_product pa_r_bpt_seed_two_product pa_s_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_factor. pa_h_bpt_seed_two_product_factor + S (pa_p_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_product_factor. pa_b_bpt_seed_two = pa_q_bpt_seed_two_product_factor * S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two) + (pa_p_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_partial. pa_h_bpt_seed_two_product_partial + S (pa_r_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_partial. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_partial * S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_r_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_successor. pa_h_bpt_seed_two_product_successor + S (pa_s_bpt_seed_two_product) = S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_successor. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_successor * S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_s_bpt_seed_two_product))) /\ pa_s_bpt_seed_two_product = pa_r_bpt_seed_two_product * pa_p_bpt_seed_two_product)))))))) /\ (exists pa_b_bpt_seed_seven pa_c_bpt_seed_seven. ((forall pa_i_bpt_seed_seven_repeat. (exists pa_lt_bpt_seed_seven_repeat_bound. pa_lt_bpt_seed_seven_repeat_bound + S pa_i_bpt_seed_seven_repeat = 7) -> (((exists pa_h_bpt_seed_seven_repeat_decoded. pa_h_bpt_seed_seven_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_repeat_decoded. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_repeat_decoded * S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven) + (2)))) /\ (exists pa_u_bpt_seed_seven_product pa_v_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_start. pa_h_bpt_seed_seven_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_start. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_start * S ((S (0)) * pa_v_bpt_seed_seven_product) + (1))) /\ ((((exists pa_h_bpt_seed_seven_product_terminal. pa_h_bpt_seed_seven_product_terminal + S (128) = S ((S (7)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_terminal. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_terminal * S ((S (7)) * pa_v_bpt_seed_seven_product) + (128))) /\ forall pa_i_bpt_seed_seven_product. (exists pa_lt_bpt_seed_seven_product_bound. pa_lt_bpt_seed_seven_product_bound + S pa_i_bpt_seed_seven_product = 7) -> exists pa_p_bpt_seed_seven_product pa_r_bpt_seed_seven_product pa_s_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_factor. pa_h_bpt_seed_seven_product_factor + S (pa_p_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_product_factor. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_product_factor * S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven) + (pa_p_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_partial. pa_h_bpt_seed_seven_product_partial + S (pa_r_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_partial. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_partial * S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_r_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_successor. pa_h_bpt_seed_seven_product_successor + S (pa_s_bpt_seed_seven_product) = S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_successor. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_successor * S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_s_bpt_seed_seven_product))) /\ pa_s_bpt_seed_seven_product = pa_r_bpt_seed_seven_product * pa_p_bpt_seed_seven_product)))))))))

Structural proof guide

One totality premise yields the exact seeds 2^2=4 and 2^7=128.

Direct prerequisites: pow_successor_compose_from_total, pow_two_base_two_value_four. The authored body proceeds by case analysis (1), intermediate claims (8), equality transport (204), closed numeral normalization (3).

Proof neighborhood

Direct dependencies

BT00SL pow_successor_compose_from_total BT00QW pow_two_base_two_value_four

Direct dependents

BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WI pow_two_double_eq_pow_four_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 htotal
  2. 0002have htwo_exists : exists x. (exists pa_b_bpt_seed_two_any pa_c_bpt_seed_two_any. ((forall pa_i_bpt_seed_two_any_repeat. (exists pa_lt_bpt_seed_two_any_repeat_bound. pa_lt_bpt_seed_two_any_repeat_bound + S pa_i_bpt_seed_two_any_repeat = 2) -> (((exists pa_h_bpt_seed_two_any_repeat_decoded. pa_h_bpt_seed_two_any_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_two_any_repeat)) * pa_c_bpt_seed_two_any)) /\ exists pa_q_bpt_seed_two_any_repeat_decoded. pa_b_bpt_seed_two_any = pa_q_bpt_seed_two_any_repeat_decoded * S ((S (pa_i_bpt_seed_two_any_repeat)) * pa_c_bpt_seed_two_any) + (2)))) /\ (exists pa_u_bpt_seed_two_any_product pa_v_bpt_seed_two_any_product. ((((exists pa_h_bpt_seed_two_any_product_start. pa_h_bpt_seed_two_any_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_start. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_start * S ((S (0)) * pa_v_bpt_seed_two_any_product) + (1))) /\ ((((exists pa_h_bpt_seed_two_any_product_terminal. pa_h_bpt_seed_two_any_product_terminal + S (x) = S ((S (2)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_terminal. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_terminal * S ((S (2)) * pa_v_bpt_seed_two_any_product) + (x))) /\ forall pa_i_bpt_seed_two_any_product. (exists pa_lt_bpt_seed_two_any_product_bound. pa_lt_bpt_seed_two_any_product_bound + S pa_i_bpt_seed_two_any_product = 2) -> exists pa_p_bpt_seed_two_any_product pa_r_bpt_seed_two_any_product pa_s_bpt_seed_two_any_product. ((((exists pa_h_bpt_seed_two_any_product_factor. pa_h_bpt_seed_two_any_product_factor + S (pa_p_bpt_seed_two_any_product) = S ((S (pa_i_bpt_seed_two_any_product)) * pa_c_bpt_seed_two_any)) /\ exists pa_q_bpt_seed_two_any_product_factor. pa_b_bpt_seed_two_any = pa_q_bpt_seed_two_any_product_factor * S ((S (pa_i_bpt_seed_two_any_product)) * pa_c_bpt_seed_two_any) + (pa_p_bpt_seed_two_any_product))) /\ ((((exists pa_h_bpt_seed_two_any_product_partial. pa_h_bpt_seed_two_any_product_partial + S (pa_r_bpt_seed_two_any_product) = S ((S (pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_partial. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_partial * S ((S (pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product) + (pa_r_bpt_seed_two_any_product))) /\ ((((exists pa_h_bpt_seed_two_any_product_successor. pa_h_bpt_seed_two_any_product_successor + S (pa_s_bpt_seed_two_any_product) = S ((S (S pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_successor. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_successor * S ((S (S pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product) + (pa_s_bpt_seed_two_any_product))) /\ pa_s_bpt_seed_two_any_product = pa_r_bpt_seed_two_any_product * pa_p_bpt_seed_two_any_product))))))))
  3. 0003specialize htotal 2
  4. 0004specialize htotal 2
  5. 0005exact htotal
  6. 0006cases htwo_exists
  7. 0007have htwo_value : x = 4
  8. 0008specialize pow_two_base_two_value_four x
  9. 0009apply pow_two_base_two_value_four
  10. 0010exact htwo_exists_witness
  11. 0011have htwo : exists pa_b_bpt_seed_two pa_c_bpt_seed_two. ((forall pa_i_bpt_seed_two_repeat. (exists pa_lt_bpt_seed_two_repeat_bound. pa_lt_bpt_seed_two_repeat_bound + S pa_i_bpt_seed_two_repeat = 2) -> (((exists pa_h_bpt_seed_two_repeat_decoded. pa_h_bpt_seed_two_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_repeat_decoded. pa_b_bpt_seed_two = pa_q_bpt_seed_two_repeat_decoded * S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two) + (2)))) /\ (exists pa_u_bpt_seed_two_product pa_v_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_start. pa_h_bpt_seed_two_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_start. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_start * S ((S (0)) * pa_v_bpt_seed_two_product) + (1))) /\ ((((exists pa_h_bpt_seed_two_product_terminal. pa_h_bpt_seed_two_product_terminal + S (4) = S ((S (2)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_terminal. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_terminal * S ((S (2)) * pa_v_bpt_seed_two_product) + (4))) /\ forall pa_i_bpt_seed_two_product. (exists pa_lt_bpt_seed_two_product_bound. pa_lt_bpt_seed_two_product_bound + S pa_i_bpt_seed_two_product = 2) -> exists pa_p_bpt_seed_two_product pa_r_bpt_seed_two_product pa_s_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_factor. pa_h_bpt_seed_two_product_factor + S (pa_p_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_product_factor. pa_b_bpt_seed_two = pa_q_bpt_seed_two_product_factor * S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two) + (pa_p_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_partial. pa_h_bpt_seed_two_product_partial + S (pa_r_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_partial. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_partial * S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_r_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_successor. pa_h_bpt_seed_two_product_successor + S (pa_s_bpt_seed_two_product) = S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_successor. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_successor * S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_s_bpt_seed_two_product))) /\ pa_s_bpt_seed_two_product = pa_r_bpt_seed_two_product * pa_p_bpt_seed_two_product)))))))
  12. 0012rewrite <- htwo_value
  13. 0013rewrite <- htwo_value
  14. 0014exact htwo_exists_witness
  15. 0015have hthree : exists pa_b_bpt_seed_three pa_c_bpt_seed_three. ((forall pa_i_bpt_seed_three_repeat. (exists pa_lt_bpt_seed_three_repeat_bound. pa_lt_bpt_seed_three_repeat_bound + S pa_i_bpt_seed_three_repeat = 3) -> (((exists pa_h_bpt_seed_three_repeat_decoded. pa_h_bpt_seed_three_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_three_repeat)) * pa_c_bpt_seed_three)) /\ exists pa_q_bpt_seed_three_repeat_decoded. pa_b_bpt_seed_three = pa_q_bpt_seed_three_repeat_decoded * S ((S (pa_i_bpt_seed_three_repeat)) * pa_c_bpt_seed_three) + (2)))) /\ (exists pa_u_bpt_seed_three_product pa_v_bpt_seed_three_product. ((((exists pa_h_bpt_seed_three_product_start. pa_h_bpt_seed_three_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_start. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_start * S ((S (0)) * pa_v_bpt_seed_three_product) + (1))) /\ ((((exists pa_h_bpt_seed_three_product_terminal. pa_h_bpt_seed_three_product_terminal + S (8) = S ((S (3)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_terminal. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_terminal * S ((S (3)) * pa_v_bpt_seed_three_product) + (8))) /\ forall pa_i_bpt_seed_three_product. (exists pa_lt_bpt_seed_three_product_bound. pa_lt_bpt_seed_three_product_bound + S pa_i_bpt_seed_three_product = 3) -> exists pa_p_bpt_seed_three_product pa_r_bpt_seed_three_product pa_s_bpt_seed_three_product. ((((exists pa_h_bpt_seed_three_product_factor. pa_h_bpt_seed_three_product_factor + S (pa_p_bpt_seed_three_product) = S ((S (pa_i_bpt_seed_three_product)) * pa_c_bpt_seed_three)) /\ exists pa_q_bpt_seed_three_product_factor. pa_b_bpt_seed_three = pa_q_bpt_seed_three_product_factor * S ((S (pa_i_bpt_seed_three_product)) * pa_c_bpt_seed_three) + (pa_p_bpt_seed_three_product))) /\ ((((exists pa_h_bpt_seed_three_product_partial. pa_h_bpt_seed_three_product_partial + S (pa_r_bpt_seed_three_product) = S ((S (pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_partial. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_partial * S ((S (pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product) + (pa_r_bpt_seed_three_product))) /\ ((((exists pa_h_bpt_seed_three_product_successor. pa_h_bpt_seed_three_product_successor + S (pa_s_bpt_seed_three_product) = S ((S (S pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_successor. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_successor * S ((S (S pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product) + (pa_s_bpt_seed_three_product))) /\ pa_s_bpt_seed_three_product = pa_r_bpt_seed_three_product * pa_p_bpt_seed_three_product)))))))
  16. 0016specialize pow_successor_compose_from_total 2
  17. 0017specialize pow_successor_compose_from_total 2
  18. 0018specialize pow_successor_compose_from_total 4
  19. 0019specialize pow_successor_compose_from_total 8
  20. 0020apply pow_successor_compose_from_total
  21. 0021exact htotal
  22. 0022exact htwo
  23. 0023norm_num
  24. 0024have hfour : exists pa_b_bpt_seed_four pa_c_bpt_seed_four. ((forall pa_i_bpt_seed_four_repeat. (exists pa_lt_bpt_seed_four_repeat_bound. pa_lt_bpt_seed_four_repeat_bound + S pa_i_bpt_seed_four_repeat = 4) -> (((exists pa_h_bpt_seed_four_repeat_decoded. pa_h_bpt_seed_four_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_four_repeat)) * pa_c_bpt_seed_four)) /\ exists pa_q_bpt_seed_four_repeat_decoded. pa_b_bpt_seed_four = pa_q_bpt_seed_four_repeat_decoded * S ((S (pa_i_bpt_seed_four_repeat)) * pa_c_bpt_seed_four) + (2)))) /\ (exists pa_u_bpt_seed_four_product pa_v_bpt_seed_four_product. ((((exists pa_h_bpt_seed_four_product_start. pa_h_bpt_seed_four_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_start. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_start * S ((S (0)) * pa_v_bpt_seed_four_product) + (1))) /\ ((((exists pa_h_bpt_seed_four_product_terminal. pa_h_bpt_seed_four_product_terminal + S (16) = S ((S (4)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_terminal. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_terminal * S ((S (4)) * pa_v_bpt_seed_four_product) + (16))) /\ forall pa_i_bpt_seed_four_product. (exists pa_lt_bpt_seed_four_product_bound. pa_lt_bpt_seed_four_product_bound + S pa_i_bpt_seed_four_product = 4) -> exists pa_p_bpt_seed_four_product pa_r_bpt_seed_four_product pa_s_bpt_seed_four_product. ((((exists pa_h_bpt_seed_four_product_factor. pa_h_bpt_seed_four_product_factor + S (pa_p_bpt_seed_four_product) = S ((S (pa_i_bpt_seed_four_product)) * pa_c_bpt_seed_four)) /\ exists pa_q_bpt_seed_four_product_factor. pa_b_bpt_seed_four = pa_q_bpt_seed_four_product_factor * S ((S (pa_i_bpt_seed_four_product)) * pa_c_bpt_seed_four) + (pa_p_bpt_seed_four_product))) /\ ((((exists pa_h_bpt_seed_four_product_partial. pa_h_bpt_seed_four_product_partial + S (pa_r_bpt_seed_four_product) = S ((S (pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_partial. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_partial * S ((S (pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product) + (pa_r_bpt_seed_four_product))) /\ ((((exists pa_h_bpt_seed_four_product_successor. pa_h_bpt_seed_four_product_successor + S (pa_s_bpt_seed_four_product) = S ((S (S pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_successor. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_successor * S ((S (S pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product) + (pa_s_bpt_seed_four_product))) /\ pa_s_bpt_seed_four_product = pa_r_bpt_seed_four_product * pa_p_bpt_seed_four_product)))))))
  25. 0025specialize pow_successor_compose_from_total 2
  26. 0026specialize pow_successor_compose_from_total 3
  27. 0027specialize pow_successor_compose_from_total 8
  28. 0028specialize pow_successor_compose_from_total 16
  29. 0029apply pow_successor_compose_from_total
  30. 0030exact htotal
  31. 0031exact hthree
  32. 0032norm_num
  33. 0033have hfive : exists pa_b_bpt_seed_five pa_c_bpt_seed_five. ((forall pa_i_bpt_seed_five_repeat. (exists pa_lt_bpt_seed_five_repeat_bound. pa_lt_bpt_seed_five_repeat_bound + S pa_i_bpt_seed_five_repeat = 5) -> (((exists pa_h_bpt_seed_five_repeat_decoded. pa_h_bpt_seed_five_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_five_repeat)) * pa_c_bpt_seed_five)) /\ exists pa_q_bpt_seed_five_repeat_decoded. pa_b_bpt_seed_five = pa_q_bpt_seed_five_repeat_decoded * S ((S (pa_i_bpt_seed_five_repeat)) * pa_c_bpt_seed_five) + (2)))) /\ (exists pa_u_bpt_seed_five_product pa_v_bpt_seed_five_product. ((((exists pa_h_bpt_seed_five_product_start. pa_h_bpt_seed_five_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_start. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_start * S ((S (0)) * pa_v_bpt_seed_five_product) + (1))) /\ ((((exists pa_h_bpt_seed_five_product_terminal. pa_h_bpt_seed_five_product_terminal + S (32) = S ((S (5)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_terminal. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_terminal * S ((S (5)) * pa_v_bpt_seed_five_product) + (32))) /\ forall pa_i_bpt_seed_five_product. (exists pa_lt_bpt_seed_five_product_bound. pa_lt_bpt_seed_five_product_bound + S pa_i_bpt_seed_five_product = 5) -> exists pa_p_bpt_seed_five_product pa_r_bpt_seed_five_product pa_s_bpt_seed_five_product. ((((exists pa_h_bpt_seed_five_product_factor. pa_h_bpt_seed_five_product_factor + S (pa_p_bpt_seed_five_product) = S ((S (pa_i_bpt_seed_five_product)) * pa_c_bpt_seed_five)) /\ exists pa_q_bpt_seed_five_product_factor. pa_b_bpt_seed_five = pa_q_bpt_seed_five_product_factor * S ((S (pa_i_bpt_seed_five_product)) * pa_c_bpt_seed_five) + (pa_p_bpt_seed_five_product))) /\ ((((exists pa_h_bpt_seed_five_product_partial. pa_h_bpt_seed_five_product_partial + S (pa_r_bpt_seed_five_product) = S ((S (pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_partial. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_partial * S ((S (pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product) + (pa_r_bpt_seed_five_product))) /\ ((((exists pa_h_bpt_seed_five_product_successor. pa_h_bpt_seed_five_product_successor + S (pa_s_bpt_seed_five_product) = S ((S (S pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_successor. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_successor * S ((S (S pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product) + (pa_s_bpt_seed_five_product))) /\ pa_s_bpt_seed_five_product = pa_r_bpt_seed_five_product * pa_p_bpt_seed_five_product)))))))
  34. 0034specialize pow_successor_compose_from_total 2
  35. 0035specialize pow_successor_compose_from_total 4
  36. 0036specialize pow_successor_compose_from_total 16
  37. 0037specialize pow_successor_compose_from_total 32
  38. 0038apply pow_successor_compose_from_total
  39. 0039exact htotal
  40. 0040exact hfour
  41. 0041norm_num
  42. 0042have hsix : exists pa_b_bpt_seed_six pa_c_bpt_seed_six. ((forall pa_i_bpt_seed_six_repeat. (exists pa_lt_bpt_seed_six_repeat_bound. pa_lt_bpt_seed_six_repeat_bound + S pa_i_bpt_seed_six_repeat = 6) -> (((exists pa_h_bpt_seed_six_repeat_decoded. pa_h_bpt_seed_six_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_six_repeat)) * pa_c_bpt_seed_six)) /\ exists pa_q_bpt_seed_six_repeat_decoded. pa_b_bpt_seed_six = pa_q_bpt_seed_six_repeat_decoded * S ((S (pa_i_bpt_seed_six_repeat)) * pa_c_bpt_seed_six) + (2)))) /\ (exists pa_u_bpt_seed_six_product pa_v_bpt_seed_six_product. ((((exists pa_h_bpt_seed_six_product_start. pa_h_bpt_seed_six_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_start. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_start * S ((S (0)) * pa_v_bpt_seed_six_product) + (1))) /\ ((((exists pa_h_bpt_seed_six_product_terminal. pa_h_bpt_seed_six_product_terminal + S (64) = S ((S (6)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_terminal. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_terminal * S ((S (6)) * pa_v_bpt_seed_six_product) + (64))) /\ forall pa_i_bpt_seed_six_product. (exists pa_lt_bpt_seed_six_product_bound. pa_lt_bpt_seed_six_product_bound + S pa_i_bpt_seed_six_product = 6) -> exists pa_p_bpt_seed_six_product pa_r_bpt_seed_six_product pa_s_bpt_seed_six_product. ((((exists pa_h_bpt_seed_six_product_factor. pa_h_bpt_seed_six_product_factor + S (pa_p_bpt_seed_six_product) = S ((S (pa_i_bpt_seed_six_product)) * pa_c_bpt_seed_six)) /\ exists pa_q_bpt_seed_six_product_factor. pa_b_bpt_seed_six = pa_q_bpt_seed_six_product_factor * S ((S (pa_i_bpt_seed_six_product)) * pa_c_bpt_seed_six) + (pa_p_bpt_seed_six_product))) /\ ((((exists pa_h_bpt_seed_six_product_partial. pa_h_bpt_seed_six_product_partial + S (pa_r_bpt_seed_six_product) = S ((S (pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_partial. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_partial * S ((S (pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product) + (pa_r_bpt_seed_six_product))) /\ ((((exists pa_h_bpt_seed_six_product_successor. pa_h_bpt_seed_six_product_successor + S (pa_s_bpt_seed_six_product) = S ((S (S pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_successor. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_successor * S ((S (S pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product) + (pa_s_bpt_seed_six_product))) /\ pa_s_bpt_seed_six_product = pa_r_bpt_seed_six_product * pa_p_bpt_seed_six_product)))))))
  43. 0043specialize pow_successor_compose_from_total 2
  44. 0044specialize pow_successor_compose_from_total 5
  45. 0045specialize pow_successor_compose_from_total 32
  46. 0046specialize pow_successor_compose_from_total 64
  47. 0047apply pow_successor_compose_from_total
  48. 0048exact htotal
  49. 0049exact hfive
  50. 0050symm
  51. 0051rewrite PA6
  52. 0052rewrite PA6
  53. 0053rewrite PA5
  54. 0054rewrite PA4
  55. 0055rewrite PA4
  56. 0056rewrite PA4
  57. 0057rewrite PA4
  58. 0058rewrite PA4
  59. 0059rewrite PA4
  60. 0060rewrite PA4
  61. 0061rewrite PA4
  62. 0062rewrite PA4
  63. 0063rewrite PA4
  64. 0064rewrite PA4
  65. 0065rewrite PA4
  66. 0066rewrite PA4
  67. 0067rewrite PA4
  68. 0068rewrite PA4
  69. 0069rewrite PA4
  70. 0070rewrite PA4
  71. 0071rewrite PA4
  72. 0072rewrite PA4
  73. 0073rewrite PA4
  74. 0074rewrite PA4
  75. 0075rewrite PA4
  76. 0076rewrite PA4
  77. 0077rewrite PA4
  78. 0078rewrite PA4
  79. 0079rewrite PA4
  80. 0080rewrite PA4
  81. 0081rewrite PA4
  82. 0082rewrite PA4
  83. 0083rewrite PA4
  84. 0084rewrite PA4
  85. 0085rewrite PA4
  86. 0086rewrite PA3
  87. 0087rewrite PA4
  88. 0088rewrite PA4
  89. 0089rewrite PA4
  90. 0090rewrite PA4
  91. 0091rewrite PA4
  92. 0092rewrite PA4
  93. 0093rewrite PA4
  94. 0094rewrite PA4
  95. 0095rewrite PA4
  96. 0096rewrite PA4
  97. 0097rewrite PA4
  98. 0098rewrite PA4
  99. 0099rewrite PA4
  100. 0100rewrite PA4
  101. 0101rewrite PA4
  102. 0102rewrite PA4
  103. 0103rewrite PA4
  104. 0104rewrite PA4
  105. 0105rewrite PA4
  106. 0106rewrite PA4
  107. 0107rewrite PA4
  108. 0108rewrite PA4
  109. 0109rewrite PA4
  110. 0110rewrite PA4
  111. 0111rewrite PA4
  112. 0112rewrite PA4
  113. 0113rewrite PA4
  114. 0114rewrite PA4
  115. 0115rewrite PA4
  116. 0116rewrite PA4
  117. 0117rewrite PA4
  118. 0118rewrite PA4
  119. 0119rewrite PA3
  120. 0120refl
  121. 0121have hseven : exists pa_b_bpt_seed_seven pa_c_bpt_seed_seven. ((forall pa_i_bpt_seed_seven_repeat. (exists pa_lt_bpt_seed_seven_repeat_bound. pa_lt_bpt_seed_seven_repeat_bound + S pa_i_bpt_seed_seven_repeat = 7) -> (((exists pa_h_bpt_seed_seven_repeat_decoded. pa_h_bpt_seed_seven_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_repeat_decoded. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_repeat_decoded * S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven) + (2)))) /\ (exists pa_u_bpt_seed_seven_product pa_v_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_start. pa_h_bpt_seed_seven_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_start. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_start * S ((S (0)) * pa_v_bpt_seed_seven_product) + (1))) /\ ((((exists pa_h_bpt_seed_seven_product_terminal. pa_h_bpt_seed_seven_product_terminal + S (128) = S ((S (7)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_terminal. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_terminal * S ((S (7)) * pa_v_bpt_seed_seven_product) + (128))) /\ forall pa_i_bpt_seed_seven_product. (exists pa_lt_bpt_seed_seven_product_bound. pa_lt_bpt_seed_seven_product_bound + S pa_i_bpt_seed_seven_product = 7) -> exists pa_p_bpt_seed_seven_product pa_r_bpt_seed_seven_product pa_s_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_factor. pa_h_bpt_seed_seven_product_factor + S (pa_p_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_product_factor. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_product_factor * S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven) + (pa_p_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_partial. pa_h_bpt_seed_seven_product_partial + S (pa_r_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_partial. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_partial * S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_r_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_successor. pa_h_bpt_seed_seven_product_successor + S (pa_s_bpt_seed_seven_product) = S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_successor. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_successor * S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_s_bpt_seed_seven_product))) /\ pa_s_bpt_seed_seven_product = pa_r_bpt_seed_seven_product * pa_p_bpt_seed_seven_product)))))))
  122. 0122specialize pow_successor_compose_from_total 2
  123. 0123specialize pow_successor_compose_from_total 6
  124. 0124specialize pow_successor_compose_from_total 64
  125. 0125specialize pow_successor_compose_from_total 128
  126. 0126apply pow_successor_compose_from_total
  127. 0127exact htotal
  128. 0128exact hsix
  129. 0129symm
  130. 0130rewrite PA6
  131. 0131rewrite PA6
  132. 0132rewrite PA5
  133. 0133rewrite PA4
  134. 0134rewrite PA4
  135. 0135rewrite PA4
  136. 0136rewrite PA4
  137. 0137rewrite PA4
  138. 0138rewrite PA4
  139. 0139rewrite PA4
  140. 0140rewrite PA4
  141. 0141rewrite PA4
  142. 0142rewrite PA4
  143. 0143rewrite PA4
  144. 0144rewrite PA4
  145. 0145rewrite PA4
  146. 0146rewrite PA4
  147. 0147rewrite PA4
  148. 0148rewrite PA4
  149. 0149rewrite PA4
  150. 0150rewrite PA4
  151. 0151rewrite PA4
  152. 0152rewrite PA4
  153. 0153rewrite PA4
  154. 0154rewrite PA4
  155. 0155rewrite PA4
  156. 0156rewrite PA4
  157. 0157rewrite PA4
  158. 0158rewrite PA4
  159. 0159rewrite PA4
  160. 0160rewrite PA4
  161. 0161rewrite PA4
  162. 0162rewrite PA4
  163. 0163rewrite PA4
  164. 0164rewrite PA4
  165. 0165rewrite PA4
  166. 0166rewrite PA4
  167. 0167rewrite PA4
  168. 0168rewrite PA4
  169. 0169rewrite PA4
  170. 0170rewrite PA4
  171. 0171rewrite PA4
  172. 0172rewrite PA4
  173. 0173rewrite PA4
  174. 0174rewrite PA4
  175. 0175rewrite PA4
  176. 0176rewrite PA4
  177. 0177rewrite PA4
  178. 0178rewrite PA4
  179. 0179rewrite PA4
  180. 0180rewrite PA4
  181. 0181rewrite PA4
  182. 0182rewrite PA4
  183. 0183rewrite PA4
  184. 0184rewrite PA4
  185. 0185rewrite PA4
  186. 0186rewrite PA4
  187. 0187rewrite PA4
  188. 0188rewrite PA4
  189. 0189rewrite PA4
  190. 0190rewrite PA4
  191. 0191rewrite PA4
  192. 0192rewrite PA4
  193. 0193rewrite PA4
  194. 0194rewrite PA4
  195. 0195rewrite PA4
  196. 0196rewrite PA4
  197. 0197rewrite PA3
  198. 0198rewrite PA4
  199. 0199rewrite PA4
  200. 0200rewrite PA4
  201. 0201rewrite PA4
  202. 0202rewrite PA4
  203. 0203rewrite PA4
  204. 0204rewrite PA4
  205. 0205rewrite PA4
  206. 0206rewrite PA4
  207. 0207rewrite PA4
  208. 0208rewrite PA4
  209. 0209rewrite PA4
  210. 0210rewrite PA4
  211. 0211rewrite PA4
  212. 0212rewrite PA4
  213. 0213rewrite PA4
  214. 0214rewrite PA4
  215. 0215rewrite PA4
  216. 0216rewrite PA4
  217. 0217rewrite PA4
  218. 0218rewrite PA4
  219. 0219rewrite PA4
  220. 0220rewrite PA4
  221. 0221rewrite PA4
  222. 0222rewrite PA4
  223. 0223rewrite PA4
  224. 0224rewrite PA4
  225. 0225rewrite PA4
  226. 0226rewrite PA4
  227. 0227rewrite PA4
  228. 0228rewrite PA4
  229. 0229rewrite PA4
  230. 0230rewrite PA4
  231. 0231rewrite PA4
  232. 0232rewrite PA4
  233. 0233rewrite PA4
  234. 0234rewrite PA4
  235. 0235rewrite PA4
  236. 0236rewrite PA4
  237. 0237rewrite PA4
  238. 0238rewrite PA4
  239. 0239rewrite PA4
  240. 0240rewrite PA4
  241. 0241rewrite PA4
  242. 0242rewrite PA4
  243. 0243rewrite PA4
  244. 0244rewrite PA4
  245. 0245rewrite PA4
  246. 0246rewrite PA4
  247. 0247rewrite PA4
  248. 0248rewrite PA4
  249. 0249rewrite PA4
  250. 0250rewrite PA4
  251. 0251rewrite PA4
  252. 0252rewrite PA4
  253. 0253rewrite PA4
  254. 0254rewrite PA4
  255. 0255rewrite PA4
  256. 0256rewrite PA4
  257. 0257rewrite PA4
  258. 0258rewrite PA4
  259. 0259rewrite PA4
  260. 0260rewrite PA4
  261. 0261rewrite PA4
  262. 0262rewrite PA3
  263. 0263refl
  264. 0264split
  265. 0265exact htwo
  266. 0266exact hseven