BT00WL · Bertrand theorem

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.

Statement with defined notation

∀ m. ∀ k. ∀ x. ∀ y. (∀ z. ∀ n. ∃ i. Pow(z,n,i)) → 7 · m = 2 · k → Pow(11,2 · m,x) → Pow(4,k,y) → Le(x,y)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0020 Pow

4 occurrences

In local proof propositions

PD0001 Le PD0020 Pow

3 occurrences

Exact expanded native-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))

Proof neighborhood

Direct theorem prerequisites

BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total BT00WI pow_two_double_eq_pow_four_from_total

Direct theorem dependents

BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
pow eleven double block le pow two seven block from totalpow two double eq pow four from total
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,7 · m,hj32_local_value_ee_p2)Original native command in the exact edition
  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 : Le(x,x1)Definitions: Le(x,x1)Original native command in the exact edition
  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,2 · k,x1)Original native command in the exact edition
  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 defined 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 : ∃ hj32_local_value_ee_p2. Pow(2,7 · m,hj32_local_value_ee_p2)
    Exact native replay linehave 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 : Le(x,x1)
    Exact native replay linehave 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 : Pow(2,2 · k,x1)
    Exact native replay linehave 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