BT00WL

pow_eleven_double_block_le_pow_four_even_from_total

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

An even 11-to-2 block exponent converts exactly to base four.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall m k x y. (forall bpt_a_hj32_eleven_even bpt_e_hj32_eleven_even. exists bpt_x_hj32_eleven_even. (exists ff_b_bpt_value_hj32_eleven_even ff_c_bpt_value_hj32_eleven_even. ((forall ff_i_bpt_value_hj32_eleven_even_repeat. (exists ff_lt_bpt_value_hj32_eleven_even_repeat_bound. ff_lt_bpt_value_hj32_eleven_even_repeat_bound + S ff_i_bpt_value_hj32_eleven_even_repeat = bpt_e_hj32_eleven_even) -> (((exists ff_h_bpt_value_hj32_eleven_even_repeat_decoded. ff_h_bpt_value_hj32_eleven_even_repeat_decoded + S (bpt_a_hj32_eleven_even) = S ((S (ff_i_bpt_value_hj32_eleven_even_repeat)) * ff_c_bpt_value_hj32_eleven_even)) /\ exists ff_q_bpt_value_hj32_eleven_even_repeat_decoded. ff_b_bpt_value_hj32_eleven_even = ff_q_bpt_value_hj32_eleven_even_repeat_decoded * S ((S (ff_i_bpt_value_hj32_eleven_even_repeat)) * ff_c_bpt_value_hj32_eleven_even) + (bpt_a_hj32_eleven_even)))) /\ (exists ff_u_bpt_value_hj32_eleven_even_product ff_v_bpt_value_hj32_eleven_even_product. ((((exists ff_h_bpt_value_hj32_eleven_even_product_start. ff_h_bpt_value_hj32_eleven_even_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_eleven_even_product)) /\ exists ff_q_bpt_value_hj32_eleven_even_product_start. ff_u_bpt_value_hj32_eleven_even_product = ff_q_bpt_value_hj32_eleven_even_product_start * S ((S (0)) * ff_v_bpt_value_hj32_eleven_even_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_eleven_even_product_terminal. ff_h_bpt_value_hj32_eleven_even_product_terminal + S (bpt_x_hj32_eleven_even) = S ((S (bpt_e_hj32_eleven_even)) * ff_v_bpt_value_hj32_eleven_even_product)) /\ exists ff_q_bpt_value_hj32_eleven_even_product_terminal. ff_u_bpt_value_hj32_eleven_even_product = ff_q_bpt_value_hj32_eleven_even_product_terminal * S ((S (bpt_e_hj32_eleven_even)) * ff_v_bpt_value_hj32_eleven_even_product) + (bpt_x_hj32_eleven_even))) /\ forall ff_i_bpt_value_hj32_eleven_even_product. (exists ff_lt_bpt_value_hj32_eleven_even_product_bound. ff_lt_bpt_value_hj32_eleven_even_product_bound + S ff_i_bpt_value_hj32_eleven_even_product = bpt_e_hj32_eleven_even) -> exists ff_p_bpt_value_hj32_eleven_even_product ff_r_bpt_value_hj32_eleven_even_product ff_s_bpt_value_hj32_eleven_even_product. ((((exists ff_h_bpt_value_hj32_eleven_even_product_factor. ff_h_bpt_value_hj32_eleven_even_product_factor + S (ff_p_bpt_value_hj32_eleven_even_product) = S ((S (ff_i_bpt_value_hj32_eleven_even_product)) * ff_c_bpt_value_hj32_eleven_even)) /\ exists ff_q_bpt_value_hj32_eleven_even_product_factor. ff_b_bpt_value_hj32_eleven_even = ff_q_bpt_value_hj32_eleven_even_product_factor * S ((S (ff_i_bpt_value_hj32_eleven_even_product)) * ff_c_bpt_value_hj32_eleven_even) + (ff_p_bpt_value_hj32_eleven_even_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_even_product_partial. ff_h_bpt_value_hj32_eleven_even_product_partial + S (ff_r_bpt_value_hj32_eleven_even_product) = S ((S (ff_i_bpt_value_hj32_eleven_even_product)) * ff_v_bpt_value_hj32_eleven_even_product)) /\ exists ff_q_bpt_value_hj32_eleven_even_product_partial. ff_u_bpt_value_hj32_eleven_even_product = ff_q_bpt_value_hj32_eleven_even_product_partial * S ((S (ff_i_bpt_value_hj32_eleven_even_product)) * ff_v_bpt_value_hj32_eleven_even_product) + (ff_r_bpt_value_hj32_eleven_even_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_even_product_successor. ff_h_bpt_value_hj32_eleven_even_product_successor + S (ff_s_bpt_value_hj32_eleven_even_product) = S ((S (S ff_i_bpt_value_hj32_eleven_even_product)) * ff_v_bpt_value_hj32_eleven_even_product)) /\ exists ff_q_bpt_value_hj32_eleven_even_product_successor. ff_u_bpt_value_hj32_eleven_even_product = ff_q_bpt_value_hj32_eleven_even_product_successor * S ((S (S ff_i_bpt_value_hj32_eleven_even_product)) * ff_v_bpt_value_hj32_eleven_even_product) + (ff_s_bpt_value_hj32_eleven_even_product))) /\ ff_s_bpt_value_hj32_eleven_even_product = ff_r_bpt_value_hj32_eleven_even_product * ff_p_bpt_value_hj32_eleven_even_product))))))))) -> 7 * m = 2 * k -> (exists pa_b_hj32_eleven_even_left pa_c_hj32_eleven_even_left. ((forall pa_i_hj32_eleven_even_left_repeat. (exists pa_lt_hj32_eleven_even_left_repeat_bound. pa_lt_hj32_eleven_even_left_repeat_bound + S pa_i_hj32_eleven_even_left_repeat = 2 * m) -> (((exists pa_h_hj32_eleven_even_left_repeat_decoded. pa_h_hj32_eleven_even_left_repeat_decoded + S (11) = S ((S (pa_i_hj32_eleven_even_left_repeat)) * pa_c_hj32_eleven_even_left)) /\ exists pa_q_hj32_eleven_even_left_repeat_decoded. pa_b_hj32_eleven_even_left = pa_q_hj32_eleven_even_left_repeat_decoded * S ((S (pa_i_hj32_eleven_even_left_repeat)) * pa_c_hj32_eleven_even_left) + (11)))) /\ (exists pa_u_hj32_eleven_even_left_product pa_v_hj32_eleven_even_left_product. ((((exists pa_h_hj32_eleven_even_left_product_start. pa_h_hj32_eleven_even_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_even_left_product)) /\ exists pa_q_hj32_eleven_even_left_product_start. pa_u_hj32_eleven_even_left_product = pa_q_hj32_eleven_even_left_product_start * S ((S (0)) * pa_v_hj32_eleven_even_left_product) + (1))) /\ ((((exists pa_h_hj32_eleven_even_left_product_terminal. pa_h_hj32_eleven_even_left_product_terminal + S (x) = S ((S (2 * m)) * pa_v_hj32_eleven_even_left_product)) /\ exists pa_q_hj32_eleven_even_left_product_terminal. pa_u_hj32_eleven_even_left_product = pa_q_hj32_eleven_even_left_product_terminal * S ((S (2 * m)) * pa_v_hj32_eleven_even_left_product) + (x))) /\ forall pa_i_hj32_eleven_even_left_product. (exists pa_lt_hj32_eleven_even_left_product_bound. pa_lt_hj32_eleven_even_left_product_bound + S pa_i_hj32_eleven_even_left_product = 2 * m) -> exists pa_p_hj32_eleven_even_left_product pa_r_hj32_eleven_even_left_product pa_s_hj32_eleven_even_left_product. ((((exists pa_h_hj32_eleven_even_left_product_factor. pa_h_hj32_eleven_even_left_product_factor + S (pa_p_hj32_eleven_even_left_product) = S ((S (pa_i_hj32_eleven_even_left_product)) * pa_c_hj32_eleven_even_left)) /\ exists pa_q_hj32_eleven_even_left_product_factor. pa_b_hj32_eleven_even_left = pa_q_hj32_eleven_even_left_product_factor * S ((S (pa_i_hj32_eleven_even_left_product)) * pa_c_hj32_eleven_even_left) + (pa_p_hj32_eleven_even_left_product))) /\ ((((exists pa_h_hj32_eleven_even_left_product_partial. pa_h_hj32_eleven_even_left_product_partial + S (pa_r_hj32_eleven_even_left_product) = S ((S (pa_i_hj32_eleven_even_left_product)) * pa_v_hj32_eleven_even_left_product)) /\ exists pa_q_hj32_eleven_even_left_product_partial. pa_u_hj32_eleven_even_left_product = pa_q_hj32_eleven_even_left_product_partial * S ((S (pa_i_hj32_eleven_even_left_product)) * pa_v_hj32_eleven_even_left_product) + (pa_r_hj32_eleven_even_left_product))) /\ ((((exists pa_h_hj32_eleven_even_left_product_successor. pa_h_hj32_eleven_even_left_product_successor + S (pa_s_hj32_eleven_even_left_product) = S ((S (S pa_i_hj32_eleven_even_left_product)) * pa_v_hj32_eleven_even_left_product)) /\ exists pa_q_hj32_eleven_even_left_product_successor. pa_u_hj32_eleven_even_left_product = pa_q_hj32_eleven_even_left_product_successor * S ((S (S pa_i_hj32_eleven_even_left_product)) * pa_v_hj32_eleven_even_left_product) + (pa_s_hj32_eleven_even_left_product))) /\ pa_s_hj32_eleven_even_left_product = pa_r_hj32_eleven_even_left_product * pa_p_hj32_eleven_even_left_product)))))))) -> (exists pa_b_hj32_eleven_even_right pa_c_hj32_eleven_even_right. ((forall pa_i_hj32_eleven_even_right_repeat. (exists pa_lt_hj32_eleven_even_right_repeat_bound. pa_lt_hj32_eleven_even_right_repeat_bound + S pa_i_hj32_eleven_even_right_repeat = k) -> (((exists pa_h_hj32_eleven_even_right_repeat_decoded. pa_h_hj32_eleven_even_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_eleven_even_right_repeat)) * pa_c_hj32_eleven_even_right)) /\ exists pa_q_hj32_eleven_even_right_repeat_decoded. pa_b_hj32_eleven_even_right = pa_q_hj32_eleven_even_right_repeat_decoded * S ((S (pa_i_hj32_eleven_even_right_repeat)) * pa_c_hj32_eleven_even_right) + (4)))) /\ (exists pa_u_hj32_eleven_even_right_product pa_v_hj32_eleven_even_right_product. ((((exists pa_h_hj32_eleven_even_right_product_start. pa_h_hj32_eleven_even_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_even_right_product)) /\ exists pa_q_hj32_eleven_even_right_product_start. pa_u_hj32_eleven_even_right_product = pa_q_hj32_eleven_even_right_product_start * S ((S (0)) * pa_v_hj32_eleven_even_right_product) + (1))) /\ ((((exists pa_h_hj32_eleven_even_right_product_terminal. pa_h_hj32_eleven_even_right_product_terminal + S (y) = S ((S (k)) * pa_v_hj32_eleven_even_right_product)) /\ exists pa_q_hj32_eleven_even_right_product_terminal. pa_u_hj32_eleven_even_right_product = pa_q_hj32_eleven_even_right_product_terminal * S ((S (k)) * pa_v_hj32_eleven_even_right_product) + (y))) /\ forall pa_i_hj32_eleven_even_right_product. (exists pa_lt_hj32_eleven_even_right_product_bound. pa_lt_hj32_eleven_even_right_product_bound + S pa_i_hj32_eleven_even_right_product = k) -> exists pa_p_hj32_eleven_even_right_product pa_r_hj32_eleven_even_right_product pa_s_hj32_eleven_even_right_product. ((((exists pa_h_hj32_eleven_even_right_product_factor. pa_h_hj32_eleven_even_right_product_factor + S (pa_p_hj32_eleven_even_right_product) = S ((S (pa_i_hj32_eleven_even_right_product)) * pa_c_hj32_eleven_even_right)) /\ exists pa_q_hj32_eleven_even_right_product_factor. pa_b_hj32_eleven_even_right = pa_q_hj32_eleven_even_right_product_factor * S ((S (pa_i_hj32_eleven_even_right_product)) * pa_c_hj32_eleven_even_right) + (pa_p_hj32_eleven_even_right_product))) /\ ((((exists pa_h_hj32_eleven_even_right_product_partial. pa_h_hj32_eleven_even_right_product_partial + S (pa_r_hj32_eleven_even_right_product) = S ((S (pa_i_hj32_eleven_even_right_product)) * pa_v_hj32_eleven_even_right_product)) /\ exists pa_q_hj32_eleven_even_right_product_partial. pa_u_hj32_eleven_even_right_product = pa_q_hj32_eleven_even_right_product_partial * S ((S (pa_i_hj32_eleven_even_right_product)) * pa_v_hj32_eleven_even_right_product) + (pa_r_hj32_eleven_even_right_product))) /\ ((((exists pa_h_hj32_eleven_even_right_product_successor. pa_h_hj32_eleven_even_right_product_successor + S (pa_s_hj32_eleven_even_right_product) = S ((S (S pa_i_hj32_eleven_even_right_product)) * pa_v_hj32_eleven_even_right_product)) /\ exists pa_q_hj32_eleven_even_right_product_successor. pa_u_hj32_eleven_even_right_product = pa_q_hj32_eleven_even_right_product_successor * S ((S (S pa_i_hj32_eleven_even_right_product)) * pa_v_hj32_eleven_even_right_product) + (pa_s_hj32_eleven_even_right_product))) /\ pa_s_hj32_eleven_even_right_product = pa_r_hj32_eleven_even_right_product * pa_p_hj32_eleven_even_right_product)))))))) -> (exists bqb_le_gap_hj32_eleven_even_result. bqb_le_gap_hj32_eleven_even_result + (x) = (y))

Structural proof guide

An even 11-to-2 block exponent converts exactly to base four.

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

Proof neighborhood

Direct dependencies

BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total BT00WI pow_two_double_eq_pow_four_from_total

Direct dependents

BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

37 script commands · 6 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
pow eleven double block le pow two seven block from totalpow two double eq pow four from total

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro m
  2. L2
    intro k
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro htotal
  6. L6
    intro hparity
  7. L7
    intro hx
  8. L8
    intro hy
02Establish ee_p2L9–12

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have ee_p2 : ∃ hj32_local_value_ee_p2. Pow(2,7 · m,hj32_local_value_ee_p2)Definitions: Pow
  2. L10
    specialize htotal 2
  3. L11
    specialize htotal 7 * m
  4. L12
    exact htotal
03Separate the logical casesL13–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases ee_p2
04Establish ee_blockL14–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow eleven double block le pow two seven block from total.

  1. L14
    have ee_block : exists bqb_le_gap_hj32_ee_block. bqb_le_gap_hj32_ee_block + (x) = (x1)
  2. L15
    specialize pow_eleven_double_block_le_pow_two_seven_block_from_total m
  3. L16
    specialize pow_eleven_double_block_le_pow_two_seven_block_from_total x
  4. L17
    specialize pow_eleven_double_block_le_pow_two_seven_block_from_total x1
  5. L18
    apply pow_eleven_double_block_le_pow_two_seven_block_from_total
  6. L19
    exact htotal
  7. L20
    exact hx
  8. L21
    exact ee_p2_witness
05Establish ee_parity_powerL22–27

Establish this local claim before using it. It is not an additional assumption.

  1. L22
    have ee_parity_power : Pow(2,2 · k,x1)Definitions: Pow
  2. L23
    rewrite <- hparity
  3. L24
    rewrite <- hparity
  4. L25
    rewrite <- hparity
  5. L26
    rewrite <- hparity
  6. L27
    exact ee_p2_witness
06Establish ee_eqL28–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two double eq pow four from total.

  1. L28
    have ee_eq : x1 = y
  2. L29
    specialize pow_two_double_eq_pow_four_from_total k
  3. L30
    specialize pow_two_double_eq_pow_four_from_total x1
  4. L31
    specialize pow_two_double_eq_pow_four_from_total y
  5. L32
    apply pow_two_double_eq_pow_four_from_total
  6. L33
    exact htotal
  7. L34
    exact ee_parity_power
  8. L35
    exact hy
  9. L36
    rewrite ee_eq at ee_block
  10. L37
    exact ee_block

Library-wide reading audit

Original exact command ledger · 37 lines
  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 ee_p2 : exists hj32_local_value_ee_p2. (exists pa_b_hj32_local_total_ee_p2 pa_c_hj32_local_total_ee_p2. ((forall pa_i_hj32_local_total_ee_p2_repeat. (exists pa_lt_hj32_local_total_ee_p2_repeat_bound. pa_lt_hj32_local_total_ee_p2_repeat_bound + S pa_i_hj32_local_total_ee_p2_repeat = 7 * m) -> (((exists pa_h_hj32_local_total_ee_p2_repeat_decoded. pa_h_hj32_local_total_ee_p2_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_ee_p2_repeat)) * pa_c_hj32_local_total_ee_p2)) /\ exists pa_q_hj32_local_total_ee_p2_repeat_decoded. pa_b_hj32_local_total_ee_p2 = pa_q_hj32_local_total_ee_p2_repeat_decoded * S ((S (pa_i_hj32_local_total_ee_p2_repeat)) * pa_c_hj32_local_total_ee_p2) + (2)))) /\ (exists pa_u_hj32_local_total_ee_p2_product pa_v_hj32_local_total_ee_p2_product. ((((exists pa_h_hj32_local_total_ee_p2_product_start. pa_h_hj32_local_total_ee_p2_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_ee_p2_product)) /\ exists pa_q_hj32_local_total_ee_p2_product_start. pa_u_hj32_local_total_ee_p2_product = pa_q_hj32_local_total_ee_p2_product_start * S ((S (0)) * pa_v_hj32_local_total_ee_p2_product) + (1))) /\ ((((exists pa_h_hj32_local_total_ee_p2_product_terminal. pa_h_hj32_local_total_ee_p2_product_terminal + S (hj32_local_value_ee_p2) = S ((S (7 * m)) * pa_v_hj32_local_total_ee_p2_product)) /\ exists pa_q_hj32_local_total_ee_p2_product_terminal. pa_u_hj32_local_total_ee_p2_product = pa_q_hj32_local_total_ee_p2_product_terminal * S ((S (7 * m)) * pa_v_hj32_local_total_ee_p2_product) + (hj32_local_value_ee_p2))) /\ forall pa_i_hj32_local_total_ee_p2_product. (exists pa_lt_hj32_local_total_ee_p2_product_bound. pa_lt_hj32_local_total_ee_p2_product_bound + S pa_i_hj32_local_total_ee_p2_product = 7 * m) -> exists pa_p_hj32_local_total_ee_p2_product pa_r_hj32_local_total_ee_p2_product pa_s_hj32_local_total_ee_p2_product. ((((exists pa_h_hj32_local_total_ee_p2_product_factor. pa_h_hj32_local_total_ee_p2_product_factor + S (pa_p_hj32_local_total_ee_p2_product) = S ((S (pa_i_hj32_local_total_ee_p2_product)) * pa_c_hj32_local_total_ee_p2)) /\ exists pa_q_hj32_local_total_ee_p2_product_factor. pa_b_hj32_local_total_ee_p2 = pa_q_hj32_local_total_ee_p2_product_factor * S ((S (pa_i_hj32_local_total_ee_p2_product)) * pa_c_hj32_local_total_ee_p2) + (pa_p_hj32_local_total_ee_p2_product))) /\ ((((exists pa_h_hj32_local_total_ee_p2_product_partial. pa_h_hj32_local_total_ee_p2_product_partial + S (pa_r_hj32_local_total_ee_p2_product) = S ((S (pa_i_hj32_local_total_ee_p2_product)) * pa_v_hj32_local_total_ee_p2_product)) /\ exists pa_q_hj32_local_total_ee_p2_product_partial. pa_u_hj32_local_total_ee_p2_product = pa_q_hj32_local_total_ee_p2_product_partial * S ((S (pa_i_hj32_local_total_ee_p2_product)) * pa_v_hj32_local_total_ee_p2_product) + (pa_r_hj32_local_total_ee_p2_product))) /\ ((((exists pa_h_hj32_local_total_ee_p2_product_successor. pa_h_hj32_local_total_ee_p2_product_successor + S (pa_s_hj32_local_total_ee_p2_product) = S ((S (S pa_i_hj32_local_total_ee_p2_product)) * pa_v_hj32_local_total_ee_p2_product)) /\ exists pa_q_hj32_local_total_ee_p2_product_successor. pa_u_hj32_local_total_ee_p2_product = pa_q_hj32_local_total_ee_p2_product_successor * S ((S (S pa_i_hj32_local_total_ee_p2_product)) * pa_v_hj32_local_total_ee_p2_product) + (pa_s_hj32_local_total_ee_p2_product))) /\ pa_s_hj32_local_total_ee_p2_product = pa_r_hj32_local_total_ee_p2_product * pa_p_hj32_local_total_ee_p2_product))))))))
  10. 0010specialize htotal 2
  11. 0011specialize htotal 7 * m
  12. 0012exact htotal
  13. 0013cases ee_p2
  14. 0014have ee_block : exists bqb_le_gap_hj32_ee_block. bqb_le_gap_hj32_ee_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 ee_p2_witness
  22. 0022have ee_parity_power : exists pa_b_hj32_ee_parity_power pa_c_hj32_ee_parity_power. ((forall pa_i_hj32_ee_parity_power_repeat. (exists pa_lt_hj32_ee_parity_power_repeat_bound. pa_lt_hj32_ee_parity_power_repeat_bound + S pa_i_hj32_ee_parity_power_repeat = 2 * k) -> (((exists pa_h_hj32_ee_parity_power_repeat_decoded. pa_h_hj32_ee_parity_power_repeat_decoded + S (2) = S ((S (pa_i_hj32_ee_parity_power_repeat)) * pa_c_hj32_ee_parity_power)) /\ exists pa_q_hj32_ee_parity_power_repeat_decoded. pa_b_hj32_ee_parity_power = pa_q_hj32_ee_parity_power_repeat_decoded * S ((S (pa_i_hj32_ee_parity_power_repeat)) * pa_c_hj32_ee_parity_power) + (2)))) /\ (exists pa_u_hj32_ee_parity_power_product pa_v_hj32_ee_parity_power_product. ((((exists pa_h_hj32_ee_parity_power_product_start. pa_h_hj32_ee_parity_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_ee_parity_power_product)) /\ exists pa_q_hj32_ee_parity_power_product_start. pa_u_hj32_ee_parity_power_product = pa_q_hj32_ee_parity_power_product_start * S ((S (0)) * pa_v_hj32_ee_parity_power_product) + (1))) /\ ((((exists pa_h_hj32_ee_parity_power_product_terminal. pa_h_hj32_ee_parity_power_product_terminal + S (x1) = S ((S (2 * k)) * pa_v_hj32_ee_parity_power_product)) /\ exists pa_q_hj32_ee_parity_power_product_terminal. pa_u_hj32_ee_parity_power_product = pa_q_hj32_ee_parity_power_product_terminal * S ((S (2 * k)) * pa_v_hj32_ee_parity_power_product) + (x1))) /\ forall pa_i_hj32_ee_parity_power_product. (exists pa_lt_hj32_ee_parity_power_product_bound. pa_lt_hj32_ee_parity_power_product_bound + S pa_i_hj32_ee_parity_power_product = 2 * k) -> exists pa_p_hj32_ee_parity_power_product pa_r_hj32_ee_parity_power_product pa_s_hj32_ee_parity_power_product. ((((exists pa_h_hj32_ee_parity_power_product_factor. pa_h_hj32_ee_parity_power_product_factor + S (pa_p_hj32_ee_parity_power_product) = S ((S (pa_i_hj32_ee_parity_power_product)) * pa_c_hj32_ee_parity_power)) /\ exists pa_q_hj32_ee_parity_power_product_factor. pa_b_hj32_ee_parity_power = pa_q_hj32_ee_parity_power_product_factor * S ((S (pa_i_hj32_ee_parity_power_product)) * pa_c_hj32_ee_parity_power) + (pa_p_hj32_ee_parity_power_product))) /\ ((((exists pa_h_hj32_ee_parity_power_product_partial. pa_h_hj32_ee_parity_power_product_partial + S (pa_r_hj32_ee_parity_power_product) = S ((S (pa_i_hj32_ee_parity_power_product)) * pa_v_hj32_ee_parity_power_product)) /\ exists pa_q_hj32_ee_parity_power_product_partial. pa_u_hj32_ee_parity_power_product = pa_q_hj32_ee_parity_power_product_partial * S ((S (pa_i_hj32_ee_parity_power_product)) * pa_v_hj32_ee_parity_power_product) + (pa_r_hj32_ee_parity_power_product))) /\ ((((exists pa_h_hj32_ee_parity_power_product_successor. pa_h_hj32_ee_parity_power_product_successor + S (pa_s_hj32_ee_parity_power_product) = S ((S (S pa_i_hj32_ee_parity_power_product)) * pa_v_hj32_ee_parity_power_product)) /\ exists pa_q_hj32_ee_parity_power_product_successor. pa_u_hj32_ee_parity_power_product = pa_q_hj32_ee_parity_power_product_successor * S ((S (S pa_i_hj32_ee_parity_power_product)) * pa_v_hj32_ee_parity_power_product) + (pa_s_hj32_ee_parity_power_product))) /\ pa_s_hj32_ee_parity_power_product = pa_r_hj32_ee_parity_power_product * pa_p_hj32_ee_parity_power_product)))))))
  23. 0023rewrite <- hparity
  24. 0024rewrite <- hparity
  25. 0025rewrite <- hparity
  26. 0026rewrite <- hparity
  27. 0027exact ee_p2_witness
  28. 0028have ee_eq : x1 = y
  29. 0029specialize pow_two_double_eq_pow_four_from_total k
  30. 0030specialize pow_two_double_eq_pow_four_from_total x1
  31. 0031specialize pow_two_double_eq_pow_four_from_total y
  32. 0032apply pow_two_double_eq_pow_four_from_total
  33. 0033exact htotal
  34. 0034exact ee_parity_power
  35. 0035exact hy
  36. 0036rewrite ee_eq at ee_block
  37. 0037exact ee_block