BT00WN

pow_six_ten_block_le_pow_four_thirteen_block_from_total

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

The seed 6^10 <= 4^13 extends through a common block count.

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 x y. (forall bpt_a_hj32_six_block bpt_e_hj32_six_block. exists bpt_x_hj32_six_block. (exists ff_b_bpt_value_hj32_six_block ff_c_bpt_value_hj32_six_block. ((forall ff_i_bpt_value_hj32_six_block_repeat. (exists ff_lt_bpt_value_hj32_six_block_repeat_bound. ff_lt_bpt_value_hj32_six_block_repeat_bound + S ff_i_bpt_value_hj32_six_block_repeat = bpt_e_hj32_six_block) -> (((exists ff_h_bpt_value_hj32_six_block_repeat_decoded. ff_h_bpt_value_hj32_six_block_repeat_decoded + S (bpt_a_hj32_six_block) = S ((S (ff_i_bpt_value_hj32_six_block_repeat)) * ff_c_bpt_value_hj32_six_block)) /\ exists ff_q_bpt_value_hj32_six_block_repeat_decoded. ff_b_bpt_value_hj32_six_block = ff_q_bpt_value_hj32_six_block_repeat_decoded * S ((S (ff_i_bpt_value_hj32_six_block_repeat)) * ff_c_bpt_value_hj32_six_block) + (bpt_a_hj32_six_block)))) /\ (exists ff_u_bpt_value_hj32_six_block_product ff_v_bpt_value_hj32_six_block_product. ((((exists ff_h_bpt_value_hj32_six_block_product_start. ff_h_bpt_value_hj32_six_block_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_six_block_product)) /\ exists ff_q_bpt_value_hj32_six_block_product_start. ff_u_bpt_value_hj32_six_block_product = ff_q_bpt_value_hj32_six_block_product_start * S ((S (0)) * ff_v_bpt_value_hj32_six_block_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_six_block_product_terminal. ff_h_bpt_value_hj32_six_block_product_terminal + S (bpt_x_hj32_six_block) = S ((S (bpt_e_hj32_six_block)) * ff_v_bpt_value_hj32_six_block_product)) /\ exists ff_q_bpt_value_hj32_six_block_product_terminal. ff_u_bpt_value_hj32_six_block_product = ff_q_bpt_value_hj32_six_block_product_terminal * S ((S (bpt_e_hj32_six_block)) * ff_v_bpt_value_hj32_six_block_product) + (bpt_x_hj32_six_block))) /\ forall ff_i_bpt_value_hj32_six_block_product. (exists ff_lt_bpt_value_hj32_six_block_product_bound. ff_lt_bpt_value_hj32_six_block_product_bound + S ff_i_bpt_value_hj32_six_block_product = bpt_e_hj32_six_block) -> exists ff_p_bpt_value_hj32_six_block_product ff_r_bpt_value_hj32_six_block_product ff_s_bpt_value_hj32_six_block_product. ((((exists ff_h_bpt_value_hj32_six_block_product_factor. ff_h_bpt_value_hj32_six_block_product_factor + S (ff_p_bpt_value_hj32_six_block_product) = S ((S (ff_i_bpt_value_hj32_six_block_product)) * ff_c_bpt_value_hj32_six_block)) /\ exists ff_q_bpt_value_hj32_six_block_product_factor. ff_b_bpt_value_hj32_six_block = ff_q_bpt_value_hj32_six_block_product_factor * S ((S (ff_i_bpt_value_hj32_six_block_product)) * ff_c_bpt_value_hj32_six_block) + (ff_p_bpt_value_hj32_six_block_product))) /\ ((((exists ff_h_bpt_value_hj32_six_block_product_partial. ff_h_bpt_value_hj32_six_block_product_partial + S (ff_r_bpt_value_hj32_six_block_product) = S ((S (ff_i_bpt_value_hj32_six_block_product)) * ff_v_bpt_value_hj32_six_block_product)) /\ exists ff_q_bpt_value_hj32_six_block_product_partial. ff_u_bpt_value_hj32_six_block_product = ff_q_bpt_value_hj32_six_block_product_partial * S ((S (ff_i_bpt_value_hj32_six_block_product)) * ff_v_bpt_value_hj32_six_block_product) + (ff_r_bpt_value_hj32_six_block_product))) /\ ((((exists ff_h_bpt_value_hj32_six_block_product_successor. ff_h_bpt_value_hj32_six_block_product_successor + S (ff_s_bpt_value_hj32_six_block_product) = S ((S (S ff_i_bpt_value_hj32_six_block_product)) * ff_v_bpt_value_hj32_six_block_product)) /\ exists ff_q_bpt_value_hj32_six_block_product_successor. ff_u_bpt_value_hj32_six_block_product = ff_q_bpt_value_hj32_six_block_product_successor * S ((S (S ff_i_bpt_value_hj32_six_block_product)) * ff_v_bpt_value_hj32_six_block_product) + (ff_s_bpt_value_hj32_six_block_product))) /\ ff_s_bpt_value_hj32_six_block_product = ff_r_bpt_value_hj32_six_block_product * ff_p_bpt_value_hj32_six_block_product))))))))) -> (exists pa_b_hj32_six_block_left pa_c_hj32_six_block_left. ((forall pa_i_hj32_six_block_left_repeat. (exists pa_lt_hj32_six_block_left_repeat_bound. pa_lt_hj32_six_block_left_repeat_bound + S pa_i_hj32_six_block_left_repeat = 10 * m) -> (((exists pa_h_hj32_six_block_left_repeat_decoded. pa_h_hj32_six_block_left_repeat_decoded + S (6) = S ((S (pa_i_hj32_six_block_left_repeat)) * pa_c_hj32_six_block_left)) /\ exists pa_q_hj32_six_block_left_repeat_decoded. pa_b_hj32_six_block_left = pa_q_hj32_six_block_left_repeat_decoded * S ((S (pa_i_hj32_six_block_left_repeat)) * pa_c_hj32_six_block_left) + (6)))) /\ (exists pa_u_hj32_six_block_left_product pa_v_hj32_six_block_left_product. ((((exists pa_h_hj32_six_block_left_product_start. pa_h_hj32_six_block_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_six_block_left_product)) /\ exists pa_q_hj32_six_block_left_product_start. pa_u_hj32_six_block_left_product = pa_q_hj32_six_block_left_product_start * S ((S (0)) * pa_v_hj32_six_block_left_product) + (1))) /\ ((((exists pa_h_hj32_six_block_left_product_terminal. pa_h_hj32_six_block_left_product_terminal + S (x) = S ((S (10 * m)) * pa_v_hj32_six_block_left_product)) /\ exists pa_q_hj32_six_block_left_product_terminal. pa_u_hj32_six_block_left_product = pa_q_hj32_six_block_left_product_terminal * S ((S (10 * m)) * pa_v_hj32_six_block_left_product) + (x))) /\ forall pa_i_hj32_six_block_left_product. (exists pa_lt_hj32_six_block_left_product_bound. pa_lt_hj32_six_block_left_product_bound + S pa_i_hj32_six_block_left_product = 10 * m) -> exists pa_p_hj32_six_block_left_product pa_r_hj32_six_block_left_product pa_s_hj32_six_block_left_product. ((((exists pa_h_hj32_six_block_left_product_factor. pa_h_hj32_six_block_left_product_factor + S (pa_p_hj32_six_block_left_product) = S ((S (pa_i_hj32_six_block_left_product)) * pa_c_hj32_six_block_left)) /\ exists pa_q_hj32_six_block_left_product_factor. pa_b_hj32_six_block_left = pa_q_hj32_six_block_left_product_factor * S ((S (pa_i_hj32_six_block_left_product)) * pa_c_hj32_six_block_left) + (pa_p_hj32_six_block_left_product))) /\ ((((exists pa_h_hj32_six_block_left_product_partial. pa_h_hj32_six_block_left_product_partial + S (pa_r_hj32_six_block_left_product) = S ((S (pa_i_hj32_six_block_left_product)) * pa_v_hj32_six_block_left_product)) /\ exists pa_q_hj32_six_block_left_product_partial. pa_u_hj32_six_block_left_product = pa_q_hj32_six_block_left_product_partial * S ((S (pa_i_hj32_six_block_left_product)) * pa_v_hj32_six_block_left_product) + (pa_r_hj32_six_block_left_product))) /\ ((((exists pa_h_hj32_six_block_left_product_successor. pa_h_hj32_six_block_left_product_successor + S (pa_s_hj32_six_block_left_product) = S ((S (S pa_i_hj32_six_block_left_product)) * pa_v_hj32_six_block_left_product)) /\ exists pa_q_hj32_six_block_left_product_successor. pa_u_hj32_six_block_left_product = pa_q_hj32_six_block_left_product_successor * S ((S (S pa_i_hj32_six_block_left_product)) * pa_v_hj32_six_block_left_product) + (pa_s_hj32_six_block_left_product))) /\ pa_s_hj32_six_block_left_product = pa_r_hj32_six_block_left_product * pa_p_hj32_six_block_left_product)))))))) -> (exists pa_b_hj32_six_block_right pa_c_hj32_six_block_right. ((forall pa_i_hj32_six_block_right_repeat. (exists pa_lt_hj32_six_block_right_repeat_bound. pa_lt_hj32_six_block_right_repeat_bound + S pa_i_hj32_six_block_right_repeat = 13 * m) -> (((exists pa_h_hj32_six_block_right_repeat_decoded. pa_h_hj32_six_block_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_six_block_right_repeat)) * pa_c_hj32_six_block_right)) /\ exists pa_q_hj32_six_block_right_repeat_decoded. pa_b_hj32_six_block_right = pa_q_hj32_six_block_right_repeat_decoded * S ((S (pa_i_hj32_six_block_right_repeat)) * pa_c_hj32_six_block_right) + (4)))) /\ (exists pa_u_hj32_six_block_right_product pa_v_hj32_six_block_right_product. ((((exists pa_h_hj32_six_block_right_product_start. pa_h_hj32_six_block_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_six_block_right_product)) /\ exists pa_q_hj32_six_block_right_product_start. pa_u_hj32_six_block_right_product = pa_q_hj32_six_block_right_product_start * S ((S (0)) * pa_v_hj32_six_block_right_product) + (1))) /\ ((((exists pa_h_hj32_six_block_right_product_terminal. pa_h_hj32_six_block_right_product_terminal + S (y) = S ((S (13 * m)) * pa_v_hj32_six_block_right_product)) /\ exists pa_q_hj32_six_block_right_product_terminal. pa_u_hj32_six_block_right_product = pa_q_hj32_six_block_right_product_terminal * S ((S (13 * m)) * pa_v_hj32_six_block_right_product) + (y))) /\ forall pa_i_hj32_six_block_right_product. (exists pa_lt_hj32_six_block_right_product_bound. pa_lt_hj32_six_block_right_product_bound + S pa_i_hj32_six_block_right_product = 13 * m) -> exists pa_p_hj32_six_block_right_product pa_r_hj32_six_block_right_product pa_s_hj32_six_block_right_product. ((((exists pa_h_hj32_six_block_right_product_factor. pa_h_hj32_six_block_right_product_factor + S (pa_p_hj32_six_block_right_product) = S ((S (pa_i_hj32_six_block_right_product)) * pa_c_hj32_six_block_right)) /\ exists pa_q_hj32_six_block_right_product_factor. pa_b_hj32_six_block_right = pa_q_hj32_six_block_right_product_factor * S ((S (pa_i_hj32_six_block_right_product)) * pa_c_hj32_six_block_right) + (pa_p_hj32_six_block_right_product))) /\ ((((exists pa_h_hj32_six_block_right_product_partial. pa_h_hj32_six_block_right_product_partial + S (pa_r_hj32_six_block_right_product) = S ((S (pa_i_hj32_six_block_right_product)) * pa_v_hj32_six_block_right_product)) /\ exists pa_q_hj32_six_block_right_product_partial. pa_u_hj32_six_block_right_product = pa_q_hj32_six_block_right_product_partial * S ((S (pa_i_hj32_six_block_right_product)) * pa_v_hj32_six_block_right_product) + (pa_r_hj32_six_block_right_product))) /\ ((((exists pa_h_hj32_six_block_right_product_successor. pa_h_hj32_six_block_right_product_successor + S (pa_s_hj32_six_block_right_product) = S ((S (S pa_i_hj32_six_block_right_product)) * pa_v_hj32_six_block_right_product)) /\ exists pa_q_hj32_six_block_right_product_successor. pa_u_hj32_six_block_right_product = pa_q_hj32_six_block_right_product_successor * S ((S (S pa_i_hj32_six_block_right_product)) * pa_v_hj32_six_block_right_product) + (pa_s_hj32_six_block_right_product))) /\ pa_s_hj32_six_block_right_product = pa_r_hj32_six_block_right_product * pa_p_hj32_six_block_right_product)))))))) -> (exists bqb_le_gap_hj32_six_block_result. bqb_le_gap_hj32_six_block_result + (x) = (y))

Structural proof guide

The seed 6^10 <= 4^13 extends through a common block count.

Direct prerequisites: pow_block_bound_from_total, pow_six_ten_le_pow_four_thirteen_from_total. The authored body proceeds by case analysis (2), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT00W3 pow_block_bound_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total

Direct dependents

BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_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

41 script commands · 8 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 block bound from totalpow six ten le pow four thirteen 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–6

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

  1. L1
    intro m
  2. L2
    intro x
  3. L3
    intro y
  4. L4
    intro htotal
  5. L5
    intro hx
  6. L6
    intro hy
02Establish sb_p6_tenL7–10

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

  1. L7
    have sb_p6_ten : ∃ hj32_local_value_sb_p6_ten. Pow(6,10,hj32_local_value_sb_p6_ten)Definitions: Pow
  2. L8
    specialize htotal 6
  3. L9
    specialize htotal 10
  4. L10
    exact htotal
03Separate the logical casesL11–11

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

  1. L11
    cases sb_p6_ten
04Establish sb_p4_thirteenL12–15

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

  1. L12
    have sb_p4_thirteen : ∃ hj32_local_value_sb_p4_thirteen. Pow(4,13,hj32_local_value_sb_p4_thirteen)Definitions: Pow
  2. L13
    specialize htotal 4
  3. L14
    specialize htotal 13
  4. L15
    exact htotal
05Separate the logical casesL16–16

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

  1. L16
    cases sb_p4_thirteen
06Establish sb_seedL17–23

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

  1. L17
    have sb_seed : exists bqb_le_gap_hj32_sb_seed. bqb_le_gap_hj32_sb_seed + (x1) = (x2)
  2. L18
    specialize pow_six_ten_le_pow_four_thirteen_from_total x1
  3. L19
    specialize pow_six_ten_le_pow_four_thirteen_from_total x2
  4. L20
    apply pow_six_ten_le_pow_four_thirteen_from_total
  5. L21
    exact htotal
  6. L22
    exact sb_p6_ten_witness
  7. L23
    exact sb_p4_thirteen_witness
07Establish sb_boundL24–33

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

  1. L24
    have sb_bound : exists bqb_le_gap_hj32_local_block_bound_sb_bound. bqb_le_gap_hj32_local_block_bound_sb_bound + (x) = (y)
  2. L25
    specialize pow_block_bound_from_total 6
  3. L26
    specialize pow_block_bound_from_total 4
  4. L27
    specialize pow_block_bound_from_total 10
  5. L28
    specialize pow_block_bound_from_total 13
  6. L29
    specialize pow_block_bound_from_total m
  7. L30
    specialize pow_block_bound_from_total x1
  8. L31
    specialize pow_block_bound_from_total x2
  9. L32
    specialize pow_block_bound_from_total x
  10. L33
    specialize pow_block_bound_from_total y
08Use earlier factsL34–41

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

  1. L34
    apply pow_block_bound_from_total
  2. L35
    exact htotal
  3. L36
    exact sb_p6_ten_witness
  4. L37
    exact sb_p4_thirteen_witness
  5. L38
    exact sb_seed
  6. L39
    exact hx
  7. L40
    exact hy
  8. L41
    exact sb_bound

Library-wide reading audit

Original exact command ledger · 41 lines
  1. 0001intro m
  2. 0002intro x
  3. 0003intro y
  4. 0004intro htotal
  5. 0005intro hx
  6. 0006intro hy
  7. 0007have sb_p6_ten : exists hj32_local_value_sb_p6_ten. (exists pa_b_hj32_local_total_sb_p6_ten pa_c_hj32_local_total_sb_p6_ten. ((forall pa_i_hj32_local_total_sb_p6_ten_repeat. (exists pa_lt_hj32_local_total_sb_p6_ten_repeat_bound. pa_lt_hj32_local_total_sb_p6_ten_repeat_bound + S pa_i_hj32_local_total_sb_p6_ten_repeat = 10) -> (((exists pa_h_hj32_local_total_sb_p6_ten_repeat_decoded. pa_h_hj32_local_total_sb_p6_ten_repeat_decoded + S (6) = S ((S (pa_i_hj32_local_total_sb_p6_ten_repeat)) * pa_c_hj32_local_total_sb_p6_ten)) /\ exists pa_q_hj32_local_total_sb_p6_ten_repeat_decoded. pa_b_hj32_local_total_sb_p6_ten = pa_q_hj32_local_total_sb_p6_ten_repeat_decoded * S ((S (pa_i_hj32_local_total_sb_p6_ten_repeat)) * pa_c_hj32_local_total_sb_p6_ten) + (6)))) /\ (exists pa_u_hj32_local_total_sb_p6_ten_product pa_v_hj32_local_total_sb_p6_ten_product. ((((exists pa_h_hj32_local_total_sb_p6_ten_product_start. pa_h_hj32_local_total_sb_p6_ten_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_sb_p6_ten_product)) /\ exists pa_q_hj32_local_total_sb_p6_ten_product_start. pa_u_hj32_local_total_sb_p6_ten_product = pa_q_hj32_local_total_sb_p6_ten_product_start * S ((S (0)) * pa_v_hj32_local_total_sb_p6_ten_product) + (1))) /\ ((((exists pa_h_hj32_local_total_sb_p6_ten_product_terminal. pa_h_hj32_local_total_sb_p6_ten_product_terminal + S (hj32_local_value_sb_p6_ten) = S ((S (10)) * pa_v_hj32_local_total_sb_p6_ten_product)) /\ exists pa_q_hj32_local_total_sb_p6_ten_product_terminal. pa_u_hj32_local_total_sb_p6_ten_product = pa_q_hj32_local_total_sb_p6_ten_product_terminal * S ((S (10)) * pa_v_hj32_local_total_sb_p6_ten_product) + (hj32_local_value_sb_p6_ten))) /\ forall pa_i_hj32_local_total_sb_p6_ten_product. (exists pa_lt_hj32_local_total_sb_p6_ten_product_bound. pa_lt_hj32_local_total_sb_p6_ten_product_bound + S pa_i_hj32_local_total_sb_p6_ten_product = 10) -> exists pa_p_hj32_local_total_sb_p6_ten_product pa_r_hj32_local_total_sb_p6_ten_product pa_s_hj32_local_total_sb_p6_ten_product. ((((exists pa_h_hj32_local_total_sb_p6_ten_product_factor. pa_h_hj32_local_total_sb_p6_ten_product_factor + S (pa_p_hj32_local_total_sb_p6_ten_product) = S ((S (pa_i_hj32_local_total_sb_p6_ten_product)) * pa_c_hj32_local_total_sb_p6_ten)) /\ exists pa_q_hj32_local_total_sb_p6_ten_product_factor. pa_b_hj32_local_total_sb_p6_ten = pa_q_hj32_local_total_sb_p6_ten_product_factor * S ((S (pa_i_hj32_local_total_sb_p6_ten_product)) * pa_c_hj32_local_total_sb_p6_ten) + (pa_p_hj32_local_total_sb_p6_ten_product))) /\ ((((exists pa_h_hj32_local_total_sb_p6_ten_product_partial. pa_h_hj32_local_total_sb_p6_ten_product_partial + S (pa_r_hj32_local_total_sb_p6_ten_product) = S ((S (pa_i_hj32_local_total_sb_p6_ten_product)) * pa_v_hj32_local_total_sb_p6_ten_product)) /\ exists pa_q_hj32_local_total_sb_p6_ten_product_partial. pa_u_hj32_local_total_sb_p6_ten_product = pa_q_hj32_local_total_sb_p6_ten_product_partial * S ((S (pa_i_hj32_local_total_sb_p6_ten_product)) * pa_v_hj32_local_total_sb_p6_ten_product) + (pa_r_hj32_local_total_sb_p6_ten_product))) /\ ((((exists pa_h_hj32_local_total_sb_p6_ten_product_successor. pa_h_hj32_local_total_sb_p6_ten_product_successor + S (pa_s_hj32_local_total_sb_p6_ten_product) = S ((S (S pa_i_hj32_local_total_sb_p6_ten_product)) * pa_v_hj32_local_total_sb_p6_ten_product)) /\ exists pa_q_hj32_local_total_sb_p6_ten_product_successor. pa_u_hj32_local_total_sb_p6_ten_product = pa_q_hj32_local_total_sb_p6_ten_product_successor * S ((S (S pa_i_hj32_local_total_sb_p6_ten_product)) * pa_v_hj32_local_total_sb_p6_ten_product) + (pa_s_hj32_local_total_sb_p6_ten_product))) /\ pa_s_hj32_local_total_sb_p6_ten_product = pa_r_hj32_local_total_sb_p6_ten_product * pa_p_hj32_local_total_sb_p6_ten_product))))))))
  8. 0008specialize htotal 6
  9. 0009specialize htotal 10
  10. 0010exact htotal
  11. 0011cases sb_p6_ten
  12. 0012have sb_p4_thirteen : exists hj32_local_value_sb_p4_thirteen. (exists pa_b_hj32_local_total_sb_p4_thirteen pa_c_hj32_local_total_sb_p4_thirteen. ((forall pa_i_hj32_local_total_sb_p4_thirteen_repeat. (exists pa_lt_hj32_local_total_sb_p4_thirteen_repeat_bound. pa_lt_hj32_local_total_sb_p4_thirteen_repeat_bound + S pa_i_hj32_local_total_sb_p4_thirteen_repeat = 13) -> (((exists pa_h_hj32_local_total_sb_p4_thirteen_repeat_decoded. pa_h_hj32_local_total_sb_p4_thirteen_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_sb_p4_thirteen_repeat)) * pa_c_hj32_local_total_sb_p4_thirteen)) /\ exists pa_q_hj32_local_total_sb_p4_thirteen_repeat_decoded. pa_b_hj32_local_total_sb_p4_thirteen = pa_q_hj32_local_total_sb_p4_thirteen_repeat_decoded * S ((S (pa_i_hj32_local_total_sb_p4_thirteen_repeat)) * pa_c_hj32_local_total_sb_p4_thirteen) + (4)))) /\ (exists pa_u_hj32_local_total_sb_p4_thirteen_product pa_v_hj32_local_total_sb_p4_thirteen_product. ((((exists pa_h_hj32_local_total_sb_p4_thirteen_product_start. pa_h_hj32_local_total_sb_p4_thirteen_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_sb_p4_thirteen_product)) /\ exists pa_q_hj32_local_total_sb_p4_thirteen_product_start. pa_u_hj32_local_total_sb_p4_thirteen_product = pa_q_hj32_local_total_sb_p4_thirteen_product_start * S ((S (0)) * pa_v_hj32_local_total_sb_p4_thirteen_product) + (1))) /\ ((((exists pa_h_hj32_local_total_sb_p4_thirteen_product_terminal. pa_h_hj32_local_total_sb_p4_thirteen_product_terminal + S (hj32_local_value_sb_p4_thirteen) = S ((S (13)) * pa_v_hj32_local_total_sb_p4_thirteen_product)) /\ exists pa_q_hj32_local_total_sb_p4_thirteen_product_terminal. pa_u_hj32_local_total_sb_p4_thirteen_product = pa_q_hj32_local_total_sb_p4_thirteen_product_terminal * S ((S (13)) * pa_v_hj32_local_total_sb_p4_thirteen_product) + (hj32_local_value_sb_p4_thirteen))) /\ forall pa_i_hj32_local_total_sb_p4_thirteen_product. (exists pa_lt_hj32_local_total_sb_p4_thirteen_product_bound. pa_lt_hj32_local_total_sb_p4_thirteen_product_bound + S pa_i_hj32_local_total_sb_p4_thirteen_product = 13) -> exists pa_p_hj32_local_total_sb_p4_thirteen_product pa_r_hj32_local_total_sb_p4_thirteen_product pa_s_hj32_local_total_sb_p4_thirteen_product. ((((exists pa_h_hj32_local_total_sb_p4_thirteen_product_factor. pa_h_hj32_local_total_sb_p4_thirteen_product_factor + S (pa_p_hj32_local_total_sb_p4_thirteen_product) = S ((S (pa_i_hj32_local_total_sb_p4_thirteen_product)) * pa_c_hj32_local_total_sb_p4_thirteen)) /\ exists pa_q_hj32_local_total_sb_p4_thirteen_product_factor. pa_b_hj32_local_total_sb_p4_thirteen = pa_q_hj32_local_total_sb_p4_thirteen_product_factor * S ((S (pa_i_hj32_local_total_sb_p4_thirteen_product)) * pa_c_hj32_local_total_sb_p4_thirteen) + (pa_p_hj32_local_total_sb_p4_thirteen_product))) /\ ((((exists pa_h_hj32_local_total_sb_p4_thirteen_product_partial. pa_h_hj32_local_total_sb_p4_thirteen_product_partial + S (pa_r_hj32_local_total_sb_p4_thirteen_product) = S ((S (pa_i_hj32_local_total_sb_p4_thirteen_product)) * pa_v_hj32_local_total_sb_p4_thirteen_product)) /\ exists pa_q_hj32_local_total_sb_p4_thirteen_product_partial. pa_u_hj32_local_total_sb_p4_thirteen_product = pa_q_hj32_local_total_sb_p4_thirteen_product_partial * S ((S (pa_i_hj32_local_total_sb_p4_thirteen_product)) * pa_v_hj32_local_total_sb_p4_thirteen_product) + (pa_r_hj32_local_total_sb_p4_thirteen_product))) /\ ((((exists pa_h_hj32_local_total_sb_p4_thirteen_product_successor. pa_h_hj32_local_total_sb_p4_thirteen_product_successor + S (pa_s_hj32_local_total_sb_p4_thirteen_product) = S ((S (S pa_i_hj32_local_total_sb_p4_thirteen_product)) * pa_v_hj32_local_total_sb_p4_thirteen_product)) /\ exists pa_q_hj32_local_total_sb_p4_thirteen_product_successor. pa_u_hj32_local_total_sb_p4_thirteen_product = pa_q_hj32_local_total_sb_p4_thirteen_product_successor * S ((S (S pa_i_hj32_local_total_sb_p4_thirteen_product)) * pa_v_hj32_local_total_sb_p4_thirteen_product) + (pa_s_hj32_local_total_sb_p4_thirteen_product))) /\ pa_s_hj32_local_total_sb_p4_thirteen_product = pa_r_hj32_local_total_sb_p4_thirteen_product * pa_p_hj32_local_total_sb_p4_thirteen_product))))))))
  13. 0013specialize htotal 4
  14. 0014specialize htotal 13
  15. 0015exact htotal
  16. 0016cases sb_p4_thirteen
  17. 0017have sb_seed : exists bqb_le_gap_hj32_sb_seed. bqb_le_gap_hj32_sb_seed + (x1) = (x2)
  18. 0018specialize pow_six_ten_le_pow_four_thirteen_from_total x1
  19. 0019specialize pow_six_ten_le_pow_four_thirteen_from_total x2
  20. 0020apply pow_six_ten_le_pow_four_thirteen_from_total
  21. 0021exact htotal
  22. 0022exact sb_p6_ten_witness
  23. 0023exact sb_p4_thirteen_witness
  24. 0024have sb_bound : exists bqb_le_gap_hj32_local_block_bound_sb_bound. bqb_le_gap_hj32_local_block_bound_sb_bound + (x) = (y)
  25. 0025specialize pow_block_bound_from_total 6
  26. 0026specialize pow_block_bound_from_total 4
  27. 0027specialize pow_block_bound_from_total 10
  28. 0028specialize pow_block_bound_from_total 13
  29. 0029specialize pow_block_bound_from_total m
  30. 0030specialize pow_block_bound_from_total x1
  31. 0031specialize pow_block_bound_from_total x2
  32. 0032specialize pow_block_bound_from_total x
  33. 0033specialize pow_block_bound_from_total y
  34. 0034apply pow_block_bound_from_total
  35. 0035exact htotal
  36. 0036exact sb_p6_ten_witness
  37. 0037exact sb_p4_thirteen_witness
  38. 0038exact sb_seed
  39. 0039exact hx
  40. 0040exact hy
  41. 0041exact sb_bound