BT00U1

pow_four_four_exact

Alpha body-checked · checked-use disabled

A relational fourth power of four is the fourfold product.

Exact expanded PA statement

forall p. (exists pa_b_bpf4e_source pa_c_bpf4e_source. ((forall pa_i_bpf4e_source_repeat. (exists pa_lt_bpf4e_source_repeat_bound. pa_lt_bpf4e_source_repeat_bound + S pa_i_bpf4e_source_repeat = 4) -> (((exists pa_h_bpf4e_source_repeat_decoded. pa_h_bpf4e_source_repeat_decoded + S (4) = S ((S (pa_i_bpf4e_source_repeat)) * pa_c_bpf4e_source)) /\ exists pa_q_bpf4e_source_repeat_decoded. pa_b_bpf4e_source = pa_q_bpf4e_source_repeat_decoded * S ((S (pa_i_bpf4e_source_repeat)) * pa_c_bpf4e_source) + (4)))) /\ (exists pa_u_bpf4e_source_product pa_v_bpf4e_source_product. ((((exists pa_h_bpf4e_source_product_start. pa_h_bpf4e_source_product_start + S (1) = S ((S (0)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_start. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_start * S ((S (0)) * pa_v_bpf4e_source_product) + (1))) /\ ((((exists pa_h_bpf4e_source_product_terminal. pa_h_bpf4e_source_product_terminal + S (p) = S ((S (4)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_terminal. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_terminal * S ((S (4)) * pa_v_bpf4e_source_product) + (p))) /\ forall pa_i_bpf4e_source_product. (exists pa_lt_bpf4e_source_product_bound. pa_lt_bpf4e_source_product_bound + S pa_i_bpf4e_source_product = 4) -> exists pa_p_bpf4e_source_product pa_r_bpf4e_source_product pa_s_bpf4e_source_product. ((((exists pa_h_bpf4e_source_product_factor. pa_h_bpf4e_source_product_factor + S (pa_p_bpf4e_source_product) = S ((S (pa_i_bpf4e_source_product)) * pa_c_bpf4e_source)) /\ exists pa_q_bpf4e_source_product_factor. pa_b_bpf4e_source = pa_q_bpf4e_source_product_factor * S ((S (pa_i_bpf4e_source_product)) * pa_c_bpf4e_source) + (pa_p_bpf4e_source_product))) /\ ((((exists pa_h_bpf4e_source_product_partial. pa_h_bpf4e_source_product_partial + S (pa_r_bpf4e_source_product) = S ((S (pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_partial. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_partial * S ((S (pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product) + (pa_r_bpf4e_source_product))) /\ ((((exists pa_h_bpf4e_source_product_successor. pa_h_bpf4e_source_product_successor + S (pa_s_bpf4e_source_product) = S ((S (S pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_successor. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_successor * S ((S (S pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product) + (pa_s_bpf4e_source_product))) /\ pa_s_bpf4e_source_product = pa_r_bpf4e_source_product * pa_p_bpf4e_source_product)))))))) -> p = ((4 * 4) * 4) * 4

Structural proof guide

A relational fourth power of four is the fourfold product.

Direct prerequisites: pow_successor_decompose, pow_two. The authored body proceeds by case analysis (4), intermediate claims (3), equality transport (3).

Proof neighborhood

Direct dependencies

BT0083 pow_successor_decompose BT009W pow_two

Direct dependents

BT00U3 four_pow_central_seed_package

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro hpower
  3. 0003have hthree : exists r. (exists pa_b_bpf4e_three pa_c_bpf4e_three. ((forall pa_i_bpf4e_three_repeat. (exists pa_lt_bpf4e_three_repeat_bound. pa_lt_bpf4e_three_repeat_bound + S pa_i_bpf4e_three_repeat = 3) -> (((exists pa_h_bpf4e_three_repeat_decoded. pa_h_bpf4e_three_repeat_decoded + S (4) = S ((S (pa_i_bpf4e_three_repeat)) * pa_c_bpf4e_three)) /\ exists pa_q_bpf4e_three_repeat_decoded. pa_b_bpf4e_three = pa_q_bpf4e_three_repeat_decoded * S ((S (pa_i_bpf4e_three_repeat)) * pa_c_bpf4e_three) + (4)))) /\ (exists pa_u_bpf4e_three_product pa_v_bpf4e_three_product. ((((exists pa_h_bpf4e_three_product_start. pa_h_bpf4e_three_product_start + S (1) = S ((S (0)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_start. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_start * S ((S (0)) * pa_v_bpf4e_three_product) + (1))) /\ ((((exists pa_h_bpf4e_three_product_terminal. pa_h_bpf4e_three_product_terminal + S (r) = S ((S (3)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_terminal. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_terminal * S ((S (3)) * pa_v_bpf4e_three_product) + (r))) /\ forall pa_i_bpf4e_three_product. (exists pa_lt_bpf4e_three_product_bound. pa_lt_bpf4e_three_product_bound + S pa_i_bpf4e_three_product = 3) -> exists pa_p_bpf4e_three_product pa_r_bpf4e_three_product pa_s_bpf4e_three_product. ((((exists pa_h_bpf4e_three_product_factor. pa_h_bpf4e_three_product_factor + S (pa_p_bpf4e_three_product) = S ((S (pa_i_bpf4e_three_product)) * pa_c_bpf4e_three)) /\ exists pa_q_bpf4e_three_product_factor. pa_b_bpf4e_three = pa_q_bpf4e_three_product_factor * S ((S (pa_i_bpf4e_three_product)) * pa_c_bpf4e_three) + (pa_p_bpf4e_three_product))) /\ ((((exists pa_h_bpf4e_three_product_partial. pa_h_bpf4e_three_product_partial + S (pa_r_bpf4e_three_product) = S ((S (pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_partial. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_partial * S ((S (pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product) + (pa_r_bpf4e_three_product))) /\ ((((exists pa_h_bpf4e_three_product_successor. pa_h_bpf4e_three_product_successor + S (pa_s_bpf4e_three_product) = S ((S (S pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_successor. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_successor * S ((S (S pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product) + (pa_s_bpf4e_three_product))) /\ pa_s_bpf4e_three_product = pa_r_bpf4e_three_product * pa_p_bpf4e_three_product)))))))) /\ p = r * 4
  4. 0004apply pow_successor_decompose
  5. 0005refl
  6. 0006exact hpower
  7. 0007cases hthree
  8. 0008cases hthree_witness
  9. 0009have htwo : exists r. (exists pa_b_bpf4e_two pa_c_bpf4e_two. ((forall pa_i_bpf4e_two_repeat. (exists pa_lt_bpf4e_two_repeat_bound. pa_lt_bpf4e_two_repeat_bound + S pa_i_bpf4e_two_repeat = 2) -> (((exists pa_h_bpf4e_two_repeat_decoded. pa_h_bpf4e_two_repeat_decoded + S (4) = S ((S (pa_i_bpf4e_two_repeat)) * pa_c_bpf4e_two)) /\ exists pa_q_bpf4e_two_repeat_decoded. pa_b_bpf4e_two = pa_q_bpf4e_two_repeat_decoded * S ((S (pa_i_bpf4e_two_repeat)) * pa_c_bpf4e_two) + (4)))) /\ (exists pa_u_bpf4e_two_product pa_v_bpf4e_two_product. ((((exists pa_h_bpf4e_two_product_start. pa_h_bpf4e_two_product_start + S (1) = S ((S (0)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_start. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_start * S ((S (0)) * pa_v_bpf4e_two_product) + (1))) /\ ((((exists pa_h_bpf4e_two_product_terminal. pa_h_bpf4e_two_product_terminal + S (r) = S ((S (2)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_terminal. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_terminal * S ((S (2)) * pa_v_bpf4e_two_product) + (r))) /\ forall pa_i_bpf4e_two_product. (exists pa_lt_bpf4e_two_product_bound. pa_lt_bpf4e_two_product_bound + S pa_i_bpf4e_two_product = 2) -> exists pa_p_bpf4e_two_product pa_r_bpf4e_two_product pa_s_bpf4e_two_product. ((((exists pa_h_bpf4e_two_product_factor. pa_h_bpf4e_two_product_factor + S (pa_p_bpf4e_two_product) = S ((S (pa_i_bpf4e_two_product)) * pa_c_bpf4e_two)) /\ exists pa_q_bpf4e_two_product_factor. pa_b_bpf4e_two = pa_q_bpf4e_two_product_factor * S ((S (pa_i_bpf4e_two_product)) * pa_c_bpf4e_two) + (pa_p_bpf4e_two_product))) /\ ((((exists pa_h_bpf4e_two_product_partial. pa_h_bpf4e_two_product_partial + S (pa_r_bpf4e_two_product) = S ((S (pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_partial. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_partial * S ((S (pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product) + (pa_r_bpf4e_two_product))) /\ ((((exists pa_h_bpf4e_two_product_successor. pa_h_bpf4e_two_product_successor + S (pa_s_bpf4e_two_product) = S ((S (S pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_successor. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_successor * S ((S (S pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product) + (pa_s_bpf4e_two_product))) /\ pa_s_bpf4e_two_product = pa_r_bpf4e_two_product * pa_p_bpf4e_two_product)))))))) /\ x = r * 4
  10. 0010apply pow_successor_decompose
  11. 0011refl
  12. 0012exact hthree_witness_left
  13. 0013cases htwo
  14. 0014cases htwo_witness
  15. 0015have htwo_value : x1 = 4 * 4
  16. 0016apply pow_two
  17. 0017refl
  18. 0018exact htwo_witness_left
  19. 0019rewrite hthree_witness_right
  20. 0020rewrite htwo_witness_right
  21. 0021rewrite htwo_value
  22. 0022refl