BT00WM · Bertrand theorem

pow_eleven_double_block_le_pow_four_odd_from_total

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

An odd 11-to-2 block exponent converts to the next base-four power.

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 + 1 → Pow(11,2 · m,x) → Pow(4,k + 1,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

4 occurrences

Exact expanded native-PA statement
forall m k x y. (forall bpt_a_hj32_eleven_odd bpt_e_hj32_eleven_odd. exists bpt_x_hj32_eleven_odd. (exists ff_b_bpt_value_hj32_eleven_odd ff_c_bpt_value_hj32_eleven_odd. ((forall ff_i_bpt_value_hj32_eleven_odd_repeat. (exists ff_lt_bpt_value_hj32_eleven_odd_repeat_bound. ff_lt_bpt_value_hj32_eleven_odd_repeat_bound + S ff_i_bpt_value_hj32_eleven_odd_repeat = bpt_e_hj32_eleven_odd) -> (((exists ff_h_bpt_value_hj32_eleven_odd_repeat_decoded. ff_h_bpt_value_hj32_eleven_odd_repeat_decoded + S (bpt_a_hj32_eleven_odd) = S ((S (ff_i_bpt_value_hj32_eleven_odd_repeat)) * ff_c_bpt_value_hj32_eleven_odd)) /\ exists ff_q_bpt_value_hj32_eleven_odd_repeat_decoded. ff_b_bpt_value_hj32_eleven_odd = ff_q_bpt_value_hj32_eleven_odd_repeat_decoded * S ((S (ff_i_bpt_value_hj32_eleven_odd_repeat)) * ff_c_bpt_value_hj32_eleven_odd) + (bpt_a_hj32_eleven_odd)))) /\ (exists ff_u_bpt_value_hj32_eleven_odd_product ff_v_bpt_value_hj32_eleven_odd_product. ((((exists ff_h_bpt_value_hj32_eleven_odd_product_start. ff_h_bpt_value_hj32_eleven_odd_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_start. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_start * S ((S (0)) * ff_v_bpt_value_hj32_eleven_odd_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_eleven_odd_product_terminal. ff_h_bpt_value_hj32_eleven_odd_product_terminal + S (bpt_x_hj32_eleven_odd) = S ((S (bpt_e_hj32_eleven_odd)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_terminal. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_terminal * S ((S (bpt_e_hj32_eleven_odd)) * ff_v_bpt_value_hj32_eleven_odd_product) + (bpt_x_hj32_eleven_odd))) /\ forall ff_i_bpt_value_hj32_eleven_odd_product. (exists ff_lt_bpt_value_hj32_eleven_odd_product_bound. ff_lt_bpt_value_hj32_eleven_odd_product_bound + S ff_i_bpt_value_hj32_eleven_odd_product = bpt_e_hj32_eleven_odd) -> exists ff_p_bpt_value_hj32_eleven_odd_product ff_r_bpt_value_hj32_eleven_odd_product ff_s_bpt_value_hj32_eleven_odd_product. ((((exists ff_h_bpt_value_hj32_eleven_odd_product_factor. ff_h_bpt_value_hj32_eleven_odd_product_factor + S (ff_p_bpt_value_hj32_eleven_odd_product) = S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_c_bpt_value_hj32_eleven_odd)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_factor. ff_b_bpt_value_hj32_eleven_odd = ff_q_bpt_value_hj32_eleven_odd_product_factor * S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_c_bpt_value_hj32_eleven_odd) + (ff_p_bpt_value_hj32_eleven_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_odd_product_partial. ff_h_bpt_value_hj32_eleven_odd_product_partial + S (ff_r_bpt_value_hj32_eleven_odd_product) = S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_partial. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_partial * S ((S (ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product) + (ff_r_bpt_value_hj32_eleven_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_eleven_odd_product_successor. ff_h_bpt_value_hj32_eleven_odd_product_successor + S (ff_s_bpt_value_hj32_eleven_odd_product) = S ((S (S ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product)) /\ exists ff_q_bpt_value_hj32_eleven_odd_product_successor. ff_u_bpt_value_hj32_eleven_odd_product = ff_q_bpt_value_hj32_eleven_odd_product_successor * S ((S (S ff_i_bpt_value_hj32_eleven_odd_product)) * ff_v_bpt_value_hj32_eleven_odd_product) + (ff_s_bpt_value_hj32_eleven_odd_product))) /\ ff_s_bpt_value_hj32_eleven_odd_product = ff_r_bpt_value_hj32_eleven_odd_product * ff_p_bpt_value_hj32_eleven_odd_product))))))))) -> 7 * m = 2 * k + 1 -> (exists pa_b_hj32_eleven_odd_left pa_c_hj32_eleven_odd_left. ((forall pa_i_hj32_eleven_odd_left_repeat. (exists pa_lt_hj32_eleven_odd_left_repeat_bound. pa_lt_hj32_eleven_odd_left_repeat_bound + S pa_i_hj32_eleven_odd_left_repeat = 2 * m) -> (((exists pa_h_hj32_eleven_odd_left_repeat_decoded. pa_h_hj32_eleven_odd_left_repeat_decoded + S (11) = S ((S (pa_i_hj32_eleven_odd_left_repeat)) * pa_c_hj32_eleven_odd_left)) /\ exists pa_q_hj32_eleven_odd_left_repeat_decoded. pa_b_hj32_eleven_odd_left = pa_q_hj32_eleven_odd_left_repeat_decoded * S ((S (pa_i_hj32_eleven_odd_left_repeat)) * pa_c_hj32_eleven_odd_left) + (11)))) /\ (exists pa_u_hj32_eleven_odd_left_product pa_v_hj32_eleven_odd_left_product. ((((exists pa_h_hj32_eleven_odd_left_product_start. pa_h_hj32_eleven_odd_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_start. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_start * S ((S (0)) * pa_v_hj32_eleven_odd_left_product) + (1))) /\ ((((exists pa_h_hj32_eleven_odd_left_product_terminal. pa_h_hj32_eleven_odd_left_product_terminal + S (x) = S ((S (2 * m)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_terminal. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_terminal * S ((S (2 * m)) * pa_v_hj32_eleven_odd_left_product) + (x))) /\ forall pa_i_hj32_eleven_odd_left_product. (exists pa_lt_hj32_eleven_odd_left_product_bound. pa_lt_hj32_eleven_odd_left_product_bound + S pa_i_hj32_eleven_odd_left_product = 2 * m) -> exists pa_p_hj32_eleven_odd_left_product pa_r_hj32_eleven_odd_left_product pa_s_hj32_eleven_odd_left_product. ((((exists pa_h_hj32_eleven_odd_left_product_factor. pa_h_hj32_eleven_odd_left_product_factor + S (pa_p_hj32_eleven_odd_left_product) = S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_c_hj32_eleven_odd_left)) /\ exists pa_q_hj32_eleven_odd_left_product_factor. pa_b_hj32_eleven_odd_left = pa_q_hj32_eleven_odd_left_product_factor * S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_c_hj32_eleven_odd_left) + (pa_p_hj32_eleven_odd_left_product))) /\ ((((exists pa_h_hj32_eleven_odd_left_product_partial. pa_h_hj32_eleven_odd_left_product_partial + S (pa_r_hj32_eleven_odd_left_product) = S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_partial. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_partial * S ((S (pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product) + (pa_r_hj32_eleven_odd_left_product))) /\ ((((exists pa_h_hj32_eleven_odd_left_product_successor. pa_h_hj32_eleven_odd_left_product_successor + S (pa_s_hj32_eleven_odd_left_product) = S ((S (S pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product)) /\ exists pa_q_hj32_eleven_odd_left_product_successor. pa_u_hj32_eleven_odd_left_product = pa_q_hj32_eleven_odd_left_product_successor * S ((S (S pa_i_hj32_eleven_odd_left_product)) * pa_v_hj32_eleven_odd_left_product) + (pa_s_hj32_eleven_odd_left_product))) /\ pa_s_hj32_eleven_odd_left_product = pa_r_hj32_eleven_odd_left_product * pa_p_hj32_eleven_odd_left_product)))))))) -> (exists pa_b_hj32_eleven_odd_right pa_c_hj32_eleven_odd_right. ((forall pa_i_hj32_eleven_odd_right_repeat. (exists pa_lt_hj32_eleven_odd_right_repeat_bound. pa_lt_hj32_eleven_odd_right_repeat_bound + S pa_i_hj32_eleven_odd_right_repeat = k + 1) -> (((exists pa_h_hj32_eleven_odd_right_repeat_decoded. pa_h_hj32_eleven_odd_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_eleven_odd_right_repeat)) * pa_c_hj32_eleven_odd_right)) /\ exists pa_q_hj32_eleven_odd_right_repeat_decoded. pa_b_hj32_eleven_odd_right = pa_q_hj32_eleven_odd_right_repeat_decoded * S ((S (pa_i_hj32_eleven_odd_right_repeat)) * pa_c_hj32_eleven_odd_right) + (4)))) /\ (exists pa_u_hj32_eleven_odd_right_product pa_v_hj32_eleven_odd_right_product. ((((exists pa_h_hj32_eleven_odd_right_product_start. pa_h_hj32_eleven_odd_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_start. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_start * S ((S (0)) * pa_v_hj32_eleven_odd_right_product) + (1))) /\ ((((exists pa_h_hj32_eleven_odd_right_product_terminal. pa_h_hj32_eleven_odd_right_product_terminal + S (y) = S ((S (k + 1)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_terminal. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_terminal * S ((S (k + 1)) * pa_v_hj32_eleven_odd_right_product) + (y))) /\ forall pa_i_hj32_eleven_odd_right_product. (exists pa_lt_hj32_eleven_odd_right_product_bound. pa_lt_hj32_eleven_odd_right_product_bound + S pa_i_hj32_eleven_odd_right_product = k + 1) -> exists pa_p_hj32_eleven_odd_right_product pa_r_hj32_eleven_odd_right_product pa_s_hj32_eleven_odd_right_product. ((((exists pa_h_hj32_eleven_odd_right_product_factor. pa_h_hj32_eleven_odd_right_product_factor + S (pa_p_hj32_eleven_odd_right_product) = S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_c_hj32_eleven_odd_right)) /\ exists pa_q_hj32_eleven_odd_right_product_factor. pa_b_hj32_eleven_odd_right = pa_q_hj32_eleven_odd_right_product_factor * S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_c_hj32_eleven_odd_right) + (pa_p_hj32_eleven_odd_right_product))) /\ ((((exists pa_h_hj32_eleven_odd_right_product_partial. pa_h_hj32_eleven_odd_right_product_partial + S (pa_r_hj32_eleven_odd_right_product) = S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_partial. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_partial * S ((S (pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product) + (pa_r_hj32_eleven_odd_right_product))) /\ ((((exists pa_h_hj32_eleven_odd_right_product_successor. pa_h_hj32_eleven_odd_right_product_successor + S (pa_s_hj32_eleven_odd_right_product) = S ((S (S pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product)) /\ exists pa_q_hj32_eleven_odd_right_product_successor. pa_u_hj32_eleven_odd_right_product = pa_q_hj32_eleven_odd_right_product_successor * S ((S (S pa_i_hj32_eleven_odd_right_product)) * pa_v_hj32_eleven_odd_right_product) + (pa_s_hj32_eleven_odd_right_product))) /\ pa_s_hj32_eleven_odd_right_product = pa_r_hj32_eleven_odd_right_product * pa_p_hj32_eleven_odd_right_product)))))))) -> (exists bqb_le_gap_hj32_eleven_odd_result. bqb_le_gap_hj32_eleven_odd_result + (x) = (y))

Proof neighborhood

Direct theorem prerequisites

BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT000F le_trans

Direct theorem dependents

BT00WP bertrand_h_root_32_from_total BT00WT bertrand_h_root_36_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

41 script commands · 7 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 (3)
pow eleven double block le pow two seven block from totalpow two successor double le pow four successor from totalle trans
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 eo_p2L9–12

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

  1. L9
    have eo_p2 : ∃ hj32_local_value_eo_p2. Pow(2,7 · m,hj32_local_value_eo_p2)Definitions: Pow(2,7 · m,hj32_local_value_eo_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 eo_p2
04Establish eo_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 eo_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 eo_p2_witness
05Establish eo_parity_powerL22–27

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

  1. L22
    have eo_parity_power : Pow(2,2 · k + 1,x1)Definitions: Pow(2,2 · k + 1,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 eo_p2_witness
06Establish eo_boundL28–37

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

  1. L28
    have eo_bound : Le(x1,y)Definitions: Le(x1,y)Original native command in the exact edition
  2. L29
    specialize pow_two_successor_double_le_pow_four_successor_from_total k
  3. L30
    specialize pow_two_successor_double_le_pow_four_successor_from_total x1
  4. L31
    specialize pow_two_successor_double_le_pow_four_successor_from_total y
  5. L32
    apply pow_two_successor_double_le_pow_four_successor_from_total
  6. L33
    exact htotal
  7. L34
    exact eo_parity_power
  8. L35
    exact hy
  9. L36
    specialize le_trans x
  10. L37
    specialize le_trans x1
07Use earlier factsL38–41

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L38
    specialize le_trans y
  2. L39
    apply le_trans
  3. L40
    exact eo_block
  4. L41
    exact eo_bound

Library-wide reading audit

Original defined command ledger · 41 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 eo_p2 : ∃ hj32_local_value_eo_p2. Pow(2,7 · m,hj32_local_value_eo_p2)
    Exact native replay linehave eo_p2 : exists hj32_local_value_eo_p2. (exists pa_b_hj32_local_total_eo_p2 pa_c_hj32_local_total_eo_p2. ((forall pa_i_hj32_local_total_eo_p2_repeat. (exists pa_lt_hj32_local_total_eo_p2_repeat_bound. pa_lt_hj32_local_total_eo_p2_repeat_bound + S pa_i_hj32_local_total_eo_p2_repeat = 7 * m) -> (((exists pa_h_hj32_local_total_eo_p2_repeat_decoded. pa_h_hj32_local_total_eo_p2_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_eo_p2_repeat)) * pa_c_hj32_local_total_eo_p2)) /\ exists pa_q_hj32_local_total_eo_p2_repeat_decoded. pa_b_hj32_local_total_eo_p2 = pa_q_hj32_local_total_eo_p2_repeat_decoded * S ((S (pa_i_hj32_local_total_eo_p2_repeat)) * pa_c_hj32_local_total_eo_p2) + (2)))) /\ (exists pa_u_hj32_local_total_eo_p2_product pa_v_hj32_local_total_eo_p2_product. ((((exists pa_h_hj32_local_total_eo_p2_product_start. pa_h_hj32_local_total_eo_p2_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_start. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_start * S ((S (0)) * pa_v_hj32_local_total_eo_p2_product) + (1))) /\ ((((exists pa_h_hj32_local_total_eo_p2_product_terminal. pa_h_hj32_local_total_eo_p2_product_terminal + S (hj32_local_value_eo_p2) = S ((S (7 * m)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_terminal. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_terminal * S ((S (7 * m)) * pa_v_hj32_local_total_eo_p2_product) + (hj32_local_value_eo_p2))) /\ forall pa_i_hj32_local_total_eo_p2_product. (exists pa_lt_hj32_local_total_eo_p2_product_bound. pa_lt_hj32_local_total_eo_p2_product_bound + S pa_i_hj32_local_total_eo_p2_product = 7 * m) -> exists pa_p_hj32_local_total_eo_p2_product pa_r_hj32_local_total_eo_p2_product pa_s_hj32_local_total_eo_p2_product. ((((exists pa_h_hj32_local_total_eo_p2_product_factor. pa_h_hj32_local_total_eo_p2_product_factor + S (pa_p_hj32_local_total_eo_p2_product) = S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_c_hj32_local_total_eo_p2)) /\ exists pa_q_hj32_local_total_eo_p2_product_factor. pa_b_hj32_local_total_eo_p2 = pa_q_hj32_local_total_eo_p2_product_factor * S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_c_hj32_local_total_eo_p2) + (pa_p_hj32_local_total_eo_p2_product))) /\ ((((exists pa_h_hj32_local_total_eo_p2_product_partial. pa_h_hj32_local_total_eo_p2_product_partial + S (pa_r_hj32_local_total_eo_p2_product) = S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_partial. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_partial * S ((S (pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product) + (pa_r_hj32_local_total_eo_p2_product))) /\ ((((exists pa_h_hj32_local_total_eo_p2_product_successor. pa_h_hj32_local_total_eo_p2_product_successor + S (pa_s_hj32_local_total_eo_p2_product) = S ((S (S pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product)) /\ exists pa_q_hj32_local_total_eo_p2_product_successor. pa_u_hj32_local_total_eo_p2_product = pa_q_hj32_local_total_eo_p2_product_successor * S ((S (S pa_i_hj32_local_total_eo_p2_product)) * pa_v_hj32_local_total_eo_p2_product) + (pa_s_hj32_local_total_eo_p2_product))) /\ pa_s_hj32_local_total_eo_p2_product = pa_r_hj32_local_total_eo_p2_product * pa_p_hj32_local_total_eo_p2_product))))))))
  10. 0010specialize htotal 2
  11. 0011specialize htotal 7 * m
  12. 0012exact htotal
  13. 0013cases eo_p2
  14. 0014have eo_block : Le(x,x1)
    Exact native replay linehave eo_block : exists bqb_le_gap_hj32_eo_block. bqb_le_gap_hj32_eo_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 eo_p2_witness
  22. 0022have eo_parity_power : Pow(2,2 · k + 1,x1)
    Exact native replay linehave eo_parity_power : exists pa_b_hj32_eo_parity_power pa_c_hj32_eo_parity_power. ((forall pa_i_hj32_eo_parity_power_repeat. (exists pa_lt_hj32_eo_parity_power_repeat_bound. pa_lt_hj32_eo_parity_power_repeat_bound + S pa_i_hj32_eo_parity_power_repeat = 2 * k + 1) -> (((exists pa_h_hj32_eo_parity_power_repeat_decoded. pa_h_hj32_eo_parity_power_repeat_decoded + S (2) = S ((S (pa_i_hj32_eo_parity_power_repeat)) * pa_c_hj32_eo_parity_power)) /\ exists pa_q_hj32_eo_parity_power_repeat_decoded. pa_b_hj32_eo_parity_power = pa_q_hj32_eo_parity_power_repeat_decoded * S ((S (pa_i_hj32_eo_parity_power_repeat)) * pa_c_hj32_eo_parity_power) + (2)))) /\ (exists pa_u_hj32_eo_parity_power_product pa_v_hj32_eo_parity_power_product. ((((exists pa_h_hj32_eo_parity_power_product_start. pa_h_hj32_eo_parity_power_product_start + S (1) = S ((S (0)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_start. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_start * S ((S (0)) * pa_v_hj32_eo_parity_power_product) + (1))) /\ ((((exists pa_h_hj32_eo_parity_power_product_terminal. pa_h_hj32_eo_parity_power_product_terminal + S (x1) = S ((S (2 * k + 1)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_terminal. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_terminal * S ((S (2 * k + 1)) * pa_v_hj32_eo_parity_power_product) + (x1))) /\ forall pa_i_hj32_eo_parity_power_product. (exists pa_lt_hj32_eo_parity_power_product_bound. pa_lt_hj32_eo_parity_power_product_bound + S pa_i_hj32_eo_parity_power_product = 2 * k + 1) -> exists pa_p_hj32_eo_parity_power_product pa_r_hj32_eo_parity_power_product pa_s_hj32_eo_parity_power_product. ((((exists pa_h_hj32_eo_parity_power_product_factor. pa_h_hj32_eo_parity_power_product_factor + S (pa_p_hj32_eo_parity_power_product) = S ((S (pa_i_hj32_eo_parity_power_product)) * pa_c_hj32_eo_parity_power)) /\ exists pa_q_hj32_eo_parity_power_product_factor. pa_b_hj32_eo_parity_power = pa_q_hj32_eo_parity_power_product_factor * S ((S (pa_i_hj32_eo_parity_power_product)) * pa_c_hj32_eo_parity_power) + (pa_p_hj32_eo_parity_power_product))) /\ ((((exists pa_h_hj32_eo_parity_power_product_partial. pa_h_hj32_eo_parity_power_product_partial + S (pa_r_hj32_eo_parity_power_product) = S ((S (pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_partial. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_partial * S ((S (pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product) + (pa_r_hj32_eo_parity_power_product))) /\ ((((exists pa_h_hj32_eo_parity_power_product_successor. pa_h_hj32_eo_parity_power_product_successor + S (pa_s_hj32_eo_parity_power_product) = S ((S (S pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product)) /\ exists pa_q_hj32_eo_parity_power_product_successor. pa_u_hj32_eo_parity_power_product = pa_q_hj32_eo_parity_power_product_successor * S ((S (S pa_i_hj32_eo_parity_power_product)) * pa_v_hj32_eo_parity_power_product) + (pa_s_hj32_eo_parity_power_product))) /\ pa_s_hj32_eo_parity_power_product = pa_r_hj32_eo_parity_power_product * pa_p_hj32_eo_parity_power_product)))))))
  23. 0023rewrite <- hparity
  24. 0024rewrite <- hparity
  25. 0025rewrite <- hparity
  26. 0026rewrite <- hparity
  27. 0027exact eo_p2_witness
  28. 0028have eo_bound : Le(x1,y)
    Exact native replay linehave eo_bound : exists bqb_le_gap_hj32_eo_bound. bqb_le_gap_hj32_eo_bound + (x1) = (y)
  29. 0029specialize pow_two_successor_double_le_pow_four_successor_from_total k
  30. 0030specialize pow_two_successor_double_le_pow_four_successor_from_total x1
  31. 0031specialize pow_two_successor_double_le_pow_four_successor_from_total y
  32. 0032apply pow_two_successor_double_le_pow_four_successor_from_total
  33. 0033exact htotal
  34. 0034exact eo_parity_power
  35. 0035exact hy
  36. 0036specialize le_trans x
  37. 0037specialize le_trans x1
  38. 0038specialize le_trans y
  39. 0039apply le_trans
  40. 0040exact eo_block
  41. 0041exact eo_bound