BT00X3 · Bertrand theorem

bertrand_hj_envelope_thirty_two

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

All roots s>=32 satisfy both H and J after discharging power totality once.

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

∀ s. ∀ e. ∀ h. ∀ u. ∀ j. ∀ g. Lt(31,s) → CeilDivSix(s · s,e) → Pow(s + 1,2 · s + 2,h) → Pow(4,e,u) → Pow(s + 7,12,j) → Pow(4,s + 5,g) → Le(h,u) ∧ Le(j,g)

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 PD0002 Lt PD0020 Pow PD0052 CeilDivSix

8 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow PD0052 CeilDivSix

14 occurrences

Exact expanded native-PA statement
forall s e h u j g. (exists bqb_le_gap_hjas_envelope_lower. bqb_le_gap_hjas_envelope_lower + (32) = (s)) -> (((exists bcs_lower_gap_hjas_envelope_ceiling. bcs_lower_gap_hjas_envelope_ceiling + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_hjas_envelope_ceiling. bcs_upper_gap_hjas_envelope_ceiling + S (6 * (e)) = (s * s) + 6)) -> (exists pa_b_hjas_envelope_h pa_c_hjas_envelope_h. ((forall pa_i_hjas_envelope_h_repeat. (exists pa_lt_hjas_envelope_h_repeat_bound. pa_lt_hjas_envelope_h_repeat_bound + S pa_i_hjas_envelope_h_repeat = 2 * s + 2) -> (((exists pa_h_hjas_envelope_h_repeat_decoded. pa_h_hjas_envelope_h_repeat_decoded + S (s + 1) = S ((S (pa_i_hjas_envelope_h_repeat)) * pa_c_hjas_envelope_h)) /\ exists pa_q_hjas_envelope_h_repeat_decoded. pa_b_hjas_envelope_h = pa_q_hjas_envelope_h_repeat_decoded * S ((S (pa_i_hjas_envelope_h_repeat)) * pa_c_hjas_envelope_h) + (s + 1)))) /\ (exists pa_u_hjas_envelope_h_product pa_v_hjas_envelope_h_product. ((((exists pa_h_hjas_envelope_h_product_start. pa_h_hjas_envelope_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_envelope_h_product)) /\ exists pa_q_hjas_envelope_h_product_start. pa_u_hjas_envelope_h_product = pa_q_hjas_envelope_h_product_start * S ((S (0)) * pa_v_hjas_envelope_h_product) + (1))) /\ ((((exists pa_h_hjas_envelope_h_product_terminal. pa_h_hjas_envelope_h_product_terminal + S (h) = S ((S (2 * s + 2)) * pa_v_hjas_envelope_h_product)) /\ exists pa_q_hjas_envelope_h_product_terminal. pa_u_hjas_envelope_h_product = pa_q_hjas_envelope_h_product_terminal * S ((S (2 * s + 2)) * pa_v_hjas_envelope_h_product) + (h))) /\ forall pa_i_hjas_envelope_h_product. (exists pa_lt_hjas_envelope_h_product_bound. pa_lt_hjas_envelope_h_product_bound + S pa_i_hjas_envelope_h_product = 2 * s + 2) -> exists pa_p_hjas_envelope_h_product pa_r_hjas_envelope_h_product pa_s_hjas_envelope_h_product. ((((exists pa_h_hjas_envelope_h_product_factor. pa_h_hjas_envelope_h_product_factor + S (pa_p_hjas_envelope_h_product) = S ((S (pa_i_hjas_envelope_h_product)) * pa_c_hjas_envelope_h)) /\ exists pa_q_hjas_envelope_h_product_factor. pa_b_hjas_envelope_h = pa_q_hjas_envelope_h_product_factor * S ((S (pa_i_hjas_envelope_h_product)) * pa_c_hjas_envelope_h) + (pa_p_hjas_envelope_h_product))) /\ ((((exists pa_h_hjas_envelope_h_product_partial. pa_h_hjas_envelope_h_product_partial + S (pa_r_hjas_envelope_h_product) = S ((S (pa_i_hjas_envelope_h_product)) * pa_v_hjas_envelope_h_product)) /\ exists pa_q_hjas_envelope_h_product_partial. pa_u_hjas_envelope_h_product = pa_q_hjas_envelope_h_product_partial * S ((S (pa_i_hjas_envelope_h_product)) * pa_v_hjas_envelope_h_product) + (pa_r_hjas_envelope_h_product))) /\ ((((exists pa_h_hjas_envelope_h_product_successor. pa_h_hjas_envelope_h_product_successor + S (pa_s_hjas_envelope_h_product) = S ((S (S pa_i_hjas_envelope_h_product)) * pa_v_hjas_envelope_h_product)) /\ exists pa_q_hjas_envelope_h_product_successor. pa_u_hjas_envelope_h_product = pa_q_hjas_envelope_h_product_successor * S ((S (S pa_i_hjas_envelope_h_product)) * pa_v_hjas_envelope_h_product) + (pa_s_hjas_envelope_h_product))) /\ pa_s_hjas_envelope_h_product = pa_r_hjas_envelope_h_product * pa_p_hjas_envelope_h_product)))))))) -> (exists pa_b_hjas_envelope_h_bound pa_c_hjas_envelope_h_bound. ((forall pa_i_hjas_envelope_h_bound_repeat. (exists pa_lt_hjas_envelope_h_bound_repeat_bound. pa_lt_hjas_envelope_h_bound_repeat_bound + S pa_i_hjas_envelope_h_bound_repeat = e) -> (((exists pa_h_hjas_envelope_h_bound_repeat_decoded. pa_h_hjas_envelope_h_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_envelope_h_bound_repeat)) * pa_c_hjas_envelope_h_bound)) /\ exists pa_q_hjas_envelope_h_bound_repeat_decoded. pa_b_hjas_envelope_h_bound = pa_q_hjas_envelope_h_bound_repeat_decoded * S ((S (pa_i_hjas_envelope_h_bound_repeat)) * pa_c_hjas_envelope_h_bound) + (4)))) /\ (exists pa_u_hjas_envelope_h_bound_product pa_v_hjas_envelope_h_bound_product. ((((exists pa_h_hjas_envelope_h_bound_product_start. pa_h_hjas_envelope_h_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_envelope_h_bound_product)) /\ exists pa_q_hjas_envelope_h_bound_product_start. pa_u_hjas_envelope_h_bound_product = pa_q_hjas_envelope_h_bound_product_start * S ((S (0)) * pa_v_hjas_envelope_h_bound_product) + (1))) /\ ((((exists pa_h_hjas_envelope_h_bound_product_terminal. pa_h_hjas_envelope_h_bound_product_terminal + S (u) = S ((S (e)) * pa_v_hjas_envelope_h_bound_product)) /\ exists pa_q_hjas_envelope_h_bound_product_terminal. pa_u_hjas_envelope_h_bound_product = pa_q_hjas_envelope_h_bound_product_terminal * S ((S (e)) * pa_v_hjas_envelope_h_bound_product) + (u))) /\ forall pa_i_hjas_envelope_h_bound_product. (exists pa_lt_hjas_envelope_h_bound_product_bound. pa_lt_hjas_envelope_h_bound_product_bound + S pa_i_hjas_envelope_h_bound_product = e) -> exists pa_p_hjas_envelope_h_bound_product pa_r_hjas_envelope_h_bound_product pa_s_hjas_envelope_h_bound_product. ((((exists pa_h_hjas_envelope_h_bound_product_factor. pa_h_hjas_envelope_h_bound_product_factor + S (pa_p_hjas_envelope_h_bound_product) = S ((S (pa_i_hjas_envelope_h_bound_product)) * pa_c_hjas_envelope_h_bound)) /\ exists pa_q_hjas_envelope_h_bound_product_factor. pa_b_hjas_envelope_h_bound = pa_q_hjas_envelope_h_bound_product_factor * S ((S (pa_i_hjas_envelope_h_bound_product)) * pa_c_hjas_envelope_h_bound) + (pa_p_hjas_envelope_h_bound_product))) /\ ((((exists pa_h_hjas_envelope_h_bound_product_partial. pa_h_hjas_envelope_h_bound_product_partial + S (pa_r_hjas_envelope_h_bound_product) = S ((S (pa_i_hjas_envelope_h_bound_product)) * pa_v_hjas_envelope_h_bound_product)) /\ exists pa_q_hjas_envelope_h_bound_product_partial. pa_u_hjas_envelope_h_bound_product = pa_q_hjas_envelope_h_bound_product_partial * S ((S (pa_i_hjas_envelope_h_bound_product)) * pa_v_hjas_envelope_h_bound_product) + (pa_r_hjas_envelope_h_bound_product))) /\ ((((exists pa_h_hjas_envelope_h_bound_product_successor. pa_h_hjas_envelope_h_bound_product_successor + S (pa_s_hjas_envelope_h_bound_product) = S ((S (S pa_i_hjas_envelope_h_bound_product)) * pa_v_hjas_envelope_h_bound_product)) /\ exists pa_q_hjas_envelope_h_bound_product_successor. pa_u_hjas_envelope_h_bound_product = pa_q_hjas_envelope_h_bound_product_successor * S ((S (S pa_i_hjas_envelope_h_bound_product)) * pa_v_hjas_envelope_h_bound_product) + (pa_s_hjas_envelope_h_bound_product))) /\ pa_s_hjas_envelope_h_bound_product = pa_r_hjas_envelope_h_bound_product * pa_p_hjas_envelope_h_bound_product)))))))) -> (exists pa_b_hjas_envelope_j pa_c_hjas_envelope_j. ((forall pa_i_hjas_envelope_j_repeat. (exists pa_lt_hjas_envelope_j_repeat_bound. pa_lt_hjas_envelope_j_repeat_bound + S pa_i_hjas_envelope_j_repeat = 12) -> (((exists pa_h_hjas_envelope_j_repeat_decoded. pa_h_hjas_envelope_j_repeat_decoded + S (s + 7) = S ((S (pa_i_hjas_envelope_j_repeat)) * pa_c_hjas_envelope_j)) /\ exists pa_q_hjas_envelope_j_repeat_decoded. pa_b_hjas_envelope_j = pa_q_hjas_envelope_j_repeat_decoded * S ((S (pa_i_hjas_envelope_j_repeat)) * pa_c_hjas_envelope_j) + (s + 7)))) /\ (exists pa_u_hjas_envelope_j_product pa_v_hjas_envelope_j_product. ((((exists pa_h_hjas_envelope_j_product_start. pa_h_hjas_envelope_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_envelope_j_product)) /\ exists pa_q_hjas_envelope_j_product_start. pa_u_hjas_envelope_j_product = pa_q_hjas_envelope_j_product_start * S ((S (0)) * pa_v_hjas_envelope_j_product) + (1))) /\ ((((exists pa_h_hjas_envelope_j_product_terminal. pa_h_hjas_envelope_j_product_terminal + S (j) = S ((S (12)) * pa_v_hjas_envelope_j_product)) /\ exists pa_q_hjas_envelope_j_product_terminal. pa_u_hjas_envelope_j_product = pa_q_hjas_envelope_j_product_terminal * S ((S (12)) * pa_v_hjas_envelope_j_product) + (j))) /\ forall pa_i_hjas_envelope_j_product. (exists pa_lt_hjas_envelope_j_product_bound. pa_lt_hjas_envelope_j_product_bound + S pa_i_hjas_envelope_j_product = 12) -> exists pa_p_hjas_envelope_j_product pa_r_hjas_envelope_j_product pa_s_hjas_envelope_j_product. ((((exists pa_h_hjas_envelope_j_product_factor. pa_h_hjas_envelope_j_product_factor + S (pa_p_hjas_envelope_j_product) = S ((S (pa_i_hjas_envelope_j_product)) * pa_c_hjas_envelope_j)) /\ exists pa_q_hjas_envelope_j_product_factor. pa_b_hjas_envelope_j = pa_q_hjas_envelope_j_product_factor * S ((S (pa_i_hjas_envelope_j_product)) * pa_c_hjas_envelope_j) + (pa_p_hjas_envelope_j_product))) /\ ((((exists pa_h_hjas_envelope_j_product_partial. pa_h_hjas_envelope_j_product_partial + S (pa_r_hjas_envelope_j_product) = S ((S (pa_i_hjas_envelope_j_product)) * pa_v_hjas_envelope_j_product)) /\ exists pa_q_hjas_envelope_j_product_partial. pa_u_hjas_envelope_j_product = pa_q_hjas_envelope_j_product_partial * S ((S (pa_i_hjas_envelope_j_product)) * pa_v_hjas_envelope_j_product) + (pa_r_hjas_envelope_j_product))) /\ ((((exists pa_h_hjas_envelope_j_product_successor. pa_h_hjas_envelope_j_product_successor + S (pa_s_hjas_envelope_j_product) = S ((S (S pa_i_hjas_envelope_j_product)) * pa_v_hjas_envelope_j_product)) /\ exists pa_q_hjas_envelope_j_product_successor. pa_u_hjas_envelope_j_product = pa_q_hjas_envelope_j_product_successor * S ((S (S pa_i_hjas_envelope_j_product)) * pa_v_hjas_envelope_j_product) + (pa_s_hjas_envelope_j_product))) /\ pa_s_hjas_envelope_j_product = pa_r_hjas_envelope_j_product * pa_p_hjas_envelope_j_product)))))))) -> (exists pa_b_hjas_envelope_j_bound pa_c_hjas_envelope_j_bound. ((forall pa_i_hjas_envelope_j_bound_repeat. (exists pa_lt_hjas_envelope_j_bound_repeat_bound. pa_lt_hjas_envelope_j_bound_repeat_bound + S pa_i_hjas_envelope_j_bound_repeat = s + 5) -> (((exists pa_h_hjas_envelope_j_bound_repeat_decoded. pa_h_hjas_envelope_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_envelope_j_bound_repeat)) * pa_c_hjas_envelope_j_bound)) /\ exists pa_q_hjas_envelope_j_bound_repeat_decoded. pa_b_hjas_envelope_j_bound = pa_q_hjas_envelope_j_bound_repeat_decoded * S ((S (pa_i_hjas_envelope_j_bound_repeat)) * pa_c_hjas_envelope_j_bound) + (4)))) /\ (exists pa_u_hjas_envelope_j_bound_product pa_v_hjas_envelope_j_bound_product. ((((exists pa_h_hjas_envelope_j_bound_product_start. pa_h_hjas_envelope_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_envelope_j_bound_product)) /\ exists pa_q_hjas_envelope_j_bound_product_start. pa_u_hjas_envelope_j_bound_product = pa_q_hjas_envelope_j_bound_product_start * S ((S (0)) * pa_v_hjas_envelope_j_bound_product) + (1))) /\ ((((exists pa_h_hjas_envelope_j_bound_product_terminal. pa_h_hjas_envelope_j_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hjas_envelope_j_bound_product)) /\ exists pa_q_hjas_envelope_j_bound_product_terminal. pa_u_hjas_envelope_j_bound_product = pa_q_hjas_envelope_j_bound_product_terminal * S ((S (s + 5)) * pa_v_hjas_envelope_j_bound_product) + (g))) /\ forall pa_i_hjas_envelope_j_bound_product. (exists pa_lt_hjas_envelope_j_bound_product_bound. pa_lt_hjas_envelope_j_bound_product_bound + S pa_i_hjas_envelope_j_bound_product = s + 5) -> exists pa_p_hjas_envelope_j_bound_product pa_r_hjas_envelope_j_bound_product pa_s_hjas_envelope_j_bound_product. ((((exists pa_h_hjas_envelope_j_bound_product_factor. pa_h_hjas_envelope_j_bound_product_factor + S (pa_p_hjas_envelope_j_bound_product) = S ((S (pa_i_hjas_envelope_j_bound_product)) * pa_c_hjas_envelope_j_bound)) /\ exists pa_q_hjas_envelope_j_bound_product_factor. pa_b_hjas_envelope_j_bound = pa_q_hjas_envelope_j_bound_product_factor * S ((S (pa_i_hjas_envelope_j_bound_product)) * pa_c_hjas_envelope_j_bound) + (pa_p_hjas_envelope_j_bound_product))) /\ ((((exists pa_h_hjas_envelope_j_bound_product_partial. pa_h_hjas_envelope_j_bound_product_partial + S (pa_r_hjas_envelope_j_bound_product) = S ((S (pa_i_hjas_envelope_j_bound_product)) * pa_v_hjas_envelope_j_bound_product)) /\ exists pa_q_hjas_envelope_j_bound_product_partial. pa_u_hjas_envelope_j_bound_product = pa_q_hjas_envelope_j_bound_product_partial * S ((S (pa_i_hjas_envelope_j_bound_product)) * pa_v_hjas_envelope_j_bound_product) + (pa_r_hjas_envelope_j_bound_product))) /\ ((((exists pa_h_hjas_envelope_j_bound_product_successor. pa_h_hjas_envelope_j_bound_product_successor + S (pa_s_hjas_envelope_j_bound_product) = S ((S (S pa_i_hjas_envelope_j_bound_product)) * pa_v_hjas_envelope_j_bound_product)) /\ exists pa_q_hjas_envelope_j_bound_product_successor. pa_u_hjas_envelope_j_bound_product = pa_q_hjas_envelope_j_bound_product_successor * S ((S (S pa_i_hjas_envelope_j_bound_product)) * pa_v_hjas_envelope_j_bound_product) + (pa_s_hjas_envelope_j_bound_product))) /\ pa_s_hjas_envelope_j_bound_product = pa_r_hjas_envelope_j_bound_product * pa_p_hjas_envelope_j_bound_product)))))))) -> (((exists bqb_le_gap_hjas_envelope_h_result. bqb_le_gap_hjas_envelope_h_result + (h) = (u)) /\ (exists bqb_le_gap_hjas_envelope_j_result. bqb_le_gap_hjas_envelope_j_result + (j) = (g))))

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT00X1 six_block_window_decomposition_above_thirty_two BT00X2 bertrand_hj_six_block_iterate_from_total

Direct theorem dependents

BT00X6 bertrand_main_inequality_factorized_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

68 script commands · 11 reading checkpoints · 7 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 existssix block window decomposition above thirty twobertrand hj six block iterate from total
01Fix variables and assumptionsL1–10

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

  1. L1
    intro s
  2. L2
    intro e
  3. L3
    intro h
  4. L4
    intro u
  5. L5
    intro j
  6. L6
    intro g
  7. L7
    intro hlower
  8. L8
    intro hceiling
  9. L9
    intro hh
  10. L10
    intro hu
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hj
  2. L12
    intro hg
03Establish htotalL13–18

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

  1. L13
    have htotal : ∀ bpt_a_hjas_envelope_total. ∀ bpt_e_hjas_envelope_total. ∃ bpt_x_hjas_envelope_total. Pow(bpt_a_hjas_envelope_total,bpt_e_hjas_envelope_total,bpt_x_hjas_envelope_total)Definitions: Pow(bpt_a_hjas_envelope_total,bpt_e_hjas_envelope_total,bpt_x_hjas_envelope_total)Original native command in the exact edition
  2. L14
    intro a
  3. L15
    intro d
  4. L16
    specialize pow_exists a
  5. L17
    specialize pow_exists d
  6. L18
    exact pow_exists
04Establish hdecompositionL19–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply six block window decomposition above thirty two.

  1. L19
    have hdecomposition : ∃ b. ∃ k. Lt(31,b) ∧ Le(b,37) ∧ s = b + 6 · kDefinitions: Lt(31,b)Le(b,37)Original native command in the exact edition
  2. L20
    specialize six_block_window_decomposition_above_thirty_two s
  3. L21
    apply six_block_window_decomposition_above_thirty_two
  4. L22
    exact hlower
05Separate the logical casesL23–26

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

  1. L23
    cases hdecomposition
  2. L24
    cases hdecomposition_witness
  3. L25
    cases hdecomposition_witness_witness
  4. L26
    cases hdecomposition_witness_witness_left
06Establish hfamilyL27–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand hj six block iterate from total.

  1. L27
    have hfamily : ∀ kk. ∀ ee. ∀ hh. ∀ uu. ∀ jj. ∀ gg. CeilDivSix((x + 6 · kk) · (x + 6 · kk),ee) → Pow(x + 6 · kk + 1,2 · (x + 6 · kk) + 2,hh) → Pow(4,ee,uu) → Pow(x + 6 · kk + 7,12,jj) → Pow(4,x + 6 · kk + 5,gg) → Le(hh,uu) ∧ Le(jj,gg)Definitions: CeilDivSix((x + 6 · kk) · (x + 6 · kk),ee)Pow(x + 6 · kk + 1,2 · (x + 6 · kk) + 2,hh)Pow(4,ee,uu)Pow(x + 6 · kk + 7,12,jj)Pow(4,x + 6 · kk + 5,gg)Le(hh,uu)Le(jj,gg)Original native command in the exact edition
  2. L28
    specialize bertrand_hj_six_block_iterate_from_total x
  3. L29
    apply bertrand_hj_six_block_iterate_from_total
  4. L30
    exact htotal
  5. L31
    exact hdecomposition_witness_witness_left_left
  6. L32
    exact hdecomposition_witness_witness_left_right
07Establish hblock_ceilingL33–38

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

  1. L33
    have hblock_ceiling : CeilDivSix((x + 6 · x1) · (x + 6 · x1),e)Definitions: CeilDivSix((x + 6 · x1) · (x + 6 · x1),e)Original native command in the exact edition
  2. L34
    rewrite <- hdecomposition_witness_witness_right
  3. L35
    rewrite <- hdecomposition_witness_witness_right
  4. L36
    rewrite <- hdecomposition_witness_witness_right
  5. L37
    rewrite <- hdecomposition_witness_witness_right
  6. L38
    exact hceiling
08Establish hblock_hL39–46

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

  1. L39
    have hblock_h : Pow(x + 6 · x1 + 1,2 · (x + 6 · x1) + 2,h)Definitions: Pow(x + 6 · x1 + 1,2 · (x + 6 · x1) + 2,h)Original native command in the exact edition
  2. L40
    rewrite <- hdecomposition_witness_witness_right
  3. L41
    rewrite <- hdecomposition_witness_witness_right
  4. L42
    rewrite <- hdecomposition_witness_witness_right
  5. L43
    rewrite <- hdecomposition_witness_witness_right
  6. L44
    rewrite <- hdecomposition_witness_witness_right
  7. L45
    rewrite <- hdecomposition_witness_witness_right
  8. L46
    exact hh
09Establish hblock_jL47–50

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

  1. L47
    have hblock_j : Pow(x + 6 · x1 + 7,12,j)Definitions: Pow(x + 6 · x1 + 7,12,j)Original native command in the exact edition
  2. L48
    rewrite <- hdecomposition_witness_witness_right
  3. L49
    rewrite <- hdecomposition_witness_witness_right
  4. L50
    exact hj
10Establish hblock_gL51–60

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

  1. L51
    have hblock_g : Pow(4,x + 6 · x1 + 5,g)Definitions: Pow(4,x + 6 · x1 + 5,g)Original native command in the exact edition
  2. L52
    rewrite <- hdecomposition_witness_witness_right
  3. L53
    rewrite <- hdecomposition_witness_witness_right
  4. L54
    rewrite <- hdecomposition_witness_witness_right
  5. L55
    rewrite <- hdecomposition_witness_witness_right
  6. L56
    exact hg
  7. L57
    specialize hfamily x1
  8. L58
    specialize hfamily e
  9. L59
    specialize hfamily h
  10. L60
    specialize hfamily u
11Use earlier factsL61–68

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

  1. L61
    specialize hfamily j
  2. L62
    specialize hfamily g
  3. L63
    apply hfamily
  4. L64
    exact hblock_ceiling
  5. L65
    exact hblock_h
  6. L66
    exact hu
  7. L67
    exact hblock_j
  8. L68
    exact hblock_g

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro s
  2. 0002intro e
  3. 0003intro h
  4. 0004intro u
  5. 0005intro j
  6. 0006intro g
  7. 0007intro hlower
  8. 0008intro hceiling
  9. 0009intro hh
  10. 0010intro hu
  11. 0011intro hj
  12. 0012intro hg
  13. 0013have htotal : ∀ bpt_a_hjas_envelope_total. ∀ bpt_e_hjas_envelope_total. ∃ bpt_x_hjas_envelope_total. Pow(bpt_a_hjas_envelope_total,bpt_e_hjas_envelope_total,bpt_x_hjas_envelope_total)
    Exact native replay linehave htotal : forall bpt_a_hjas_envelope_total bpt_e_hjas_envelope_total. exists bpt_x_hjas_envelope_total. (exists ff_b_bpt_value_hjas_envelope_total ff_c_bpt_value_hjas_envelope_total. ((forall ff_i_bpt_value_hjas_envelope_total_repeat. (exists ff_lt_bpt_value_hjas_envelope_total_repeat_bound. ff_lt_bpt_value_hjas_envelope_total_repeat_bound + S ff_i_bpt_value_hjas_envelope_total_repeat = bpt_e_hjas_envelope_total) -> (((exists ff_h_bpt_value_hjas_envelope_total_repeat_decoded. ff_h_bpt_value_hjas_envelope_total_repeat_decoded + S (bpt_a_hjas_envelope_total) = S ((S (ff_i_bpt_value_hjas_envelope_total_repeat)) * ff_c_bpt_value_hjas_envelope_total)) /\ exists ff_q_bpt_value_hjas_envelope_total_repeat_decoded. ff_b_bpt_value_hjas_envelope_total = ff_q_bpt_value_hjas_envelope_total_repeat_decoded * S ((S (ff_i_bpt_value_hjas_envelope_total_repeat)) * ff_c_bpt_value_hjas_envelope_total) + (bpt_a_hjas_envelope_total)))) /\ (exists ff_u_bpt_value_hjas_envelope_total_product ff_v_bpt_value_hjas_envelope_total_product. ((((exists ff_h_bpt_value_hjas_envelope_total_product_start. ff_h_bpt_value_hjas_envelope_total_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_start. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_start * S ((S (0)) * ff_v_bpt_value_hjas_envelope_total_product) + (1))) /\ ((((exists ff_h_bpt_value_hjas_envelope_total_product_terminal. ff_h_bpt_value_hjas_envelope_total_product_terminal + S (bpt_x_hjas_envelope_total) = S ((S (bpt_e_hjas_envelope_total)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_terminal. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_terminal * S ((S (bpt_e_hjas_envelope_total)) * ff_v_bpt_value_hjas_envelope_total_product) + (bpt_x_hjas_envelope_total))) /\ forall ff_i_bpt_value_hjas_envelope_total_product. (exists ff_lt_bpt_value_hjas_envelope_total_product_bound. ff_lt_bpt_value_hjas_envelope_total_product_bound + S ff_i_bpt_value_hjas_envelope_total_product = bpt_e_hjas_envelope_total) -> exists ff_p_bpt_value_hjas_envelope_total_product ff_r_bpt_value_hjas_envelope_total_product ff_s_bpt_value_hjas_envelope_total_product. ((((exists ff_h_bpt_value_hjas_envelope_total_product_factor. ff_h_bpt_value_hjas_envelope_total_product_factor + S (ff_p_bpt_value_hjas_envelope_total_product) = S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_c_bpt_value_hjas_envelope_total)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_factor. ff_b_bpt_value_hjas_envelope_total = ff_q_bpt_value_hjas_envelope_total_product_factor * S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_c_bpt_value_hjas_envelope_total) + (ff_p_bpt_value_hjas_envelope_total_product))) /\ ((((exists ff_h_bpt_value_hjas_envelope_total_product_partial. ff_h_bpt_value_hjas_envelope_total_product_partial + S (ff_r_bpt_value_hjas_envelope_total_product) = S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_partial. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_partial * S ((S (ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product) + (ff_r_bpt_value_hjas_envelope_total_product))) /\ ((((exists ff_h_bpt_value_hjas_envelope_total_product_successor. ff_h_bpt_value_hjas_envelope_total_product_successor + S (ff_s_bpt_value_hjas_envelope_total_product) = S ((S (S ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product)) /\ exists ff_q_bpt_value_hjas_envelope_total_product_successor. ff_u_bpt_value_hjas_envelope_total_product = ff_q_bpt_value_hjas_envelope_total_product_successor * S ((S (S ff_i_bpt_value_hjas_envelope_total_product)) * ff_v_bpt_value_hjas_envelope_total_product) + (ff_s_bpt_value_hjas_envelope_total_product))) /\ ff_s_bpt_value_hjas_envelope_total_product = ff_r_bpt_value_hjas_envelope_total_product * ff_p_bpt_value_hjas_envelope_total_product))))))))
  14. 0014intro a
  15. 0015intro d
  16. 0016specialize pow_exists a
  17. 0017specialize pow_exists d
  18. 0018exact pow_exists
  19. 0019have hdecomposition : ∃ b. ∃ k. Lt(31,b) ∧ Le(b,37) ∧ s = b + 6 · k
    Exact native replay linehave hdecomposition : exists b k. (((exists bqb_le_gap_hjas_decomposition_base_lower. bqb_le_gap_hjas_decomposition_base_lower + (32) = (b)) /\ (exists bqb_le_gap_hjas_decomposition_base_upper. bqb_le_gap_hjas_decomposition_base_upper + (b) = (37))) /\ s = b + 6 * k)
  20. 0020specialize six_block_window_decomposition_above_thirty_two s
  21. 0021apply six_block_window_decomposition_above_thirty_two
  22. 0022exact hlower
  23. 0023cases hdecomposition
  24. 0024cases hdecomposition_witness
  25. 0025cases hdecomposition_witness_witness
  26. 0026cases hdecomposition_witness_witness_left
  27. 0027have hfamily : ∀ kk. ∀ ee. ∀ hh. ∀ uu. ∀ jj. ∀ gg. CeilDivSix((x + 6 · kk) · (x + 6 · kk),ee) → Pow(x + 6 · kk + 1,2 · (x + 6 · kk) + 2,hh) → Pow(4,ee,uu) → Pow(x + 6 · kk + 7,12,jj) → Pow(4,x + 6 · kk + 5,gg) → Le(hh,uu) ∧ Le(jj,gg)
    Exact native replay linehave hfamily : forall kk ee hh uu jj gg. (((exists bcs_lower_gap_hjas_family_ceiling. bcs_lower_gap_hjas_family_ceiling + ((x + 6 * kk) * (x + 6 * kk)) = 6 * (ee)) /\ exists bcs_upper_gap_hjas_family_ceiling. bcs_upper_gap_hjas_family_ceiling + S (6 * (ee)) = ((x + 6 * kk) * (x + 6 * kk)) + 6)) -> (exists pa_b_hjas_family_h pa_c_hjas_family_h. ((forall pa_i_hjas_family_h_repeat. (exists pa_lt_hjas_family_h_repeat_bound. pa_lt_hjas_family_h_repeat_bound + S pa_i_hjas_family_h_repeat = 2 * (x + 6 * kk) + 2) -> (((exists pa_h_hjas_family_h_repeat_decoded. pa_h_hjas_family_h_repeat_decoded + S ((x + 6 * kk) + 1) = S ((S (pa_i_hjas_family_h_repeat)) * pa_c_hjas_family_h)) /\ exists pa_q_hjas_family_h_repeat_decoded. pa_b_hjas_family_h = pa_q_hjas_family_h_repeat_decoded * S ((S (pa_i_hjas_family_h_repeat)) * pa_c_hjas_family_h) + ((x + 6 * kk) + 1)))) /\ (exists pa_u_hjas_family_h_product pa_v_hjas_family_h_product. ((((exists pa_h_hjas_family_h_product_start. pa_h_hjas_family_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_start. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_start * S ((S (0)) * pa_v_hjas_family_h_product) + (1))) /\ ((((exists pa_h_hjas_family_h_product_terminal. pa_h_hjas_family_h_product_terminal + S (hh) = S ((S (2 * (x + 6 * kk) + 2)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_terminal. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_terminal * S ((S (2 * (x + 6 * kk) + 2)) * pa_v_hjas_family_h_product) + (hh))) /\ forall pa_i_hjas_family_h_product. (exists pa_lt_hjas_family_h_product_bound. pa_lt_hjas_family_h_product_bound + S pa_i_hjas_family_h_product = 2 * (x + 6 * kk) + 2) -> exists pa_p_hjas_family_h_product pa_r_hjas_family_h_product pa_s_hjas_family_h_product. ((((exists pa_h_hjas_family_h_product_factor. pa_h_hjas_family_h_product_factor + S (pa_p_hjas_family_h_product) = S ((S (pa_i_hjas_family_h_product)) * pa_c_hjas_family_h)) /\ exists pa_q_hjas_family_h_product_factor. pa_b_hjas_family_h = pa_q_hjas_family_h_product_factor * S ((S (pa_i_hjas_family_h_product)) * pa_c_hjas_family_h) + (pa_p_hjas_family_h_product))) /\ ((((exists pa_h_hjas_family_h_product_partial. pa_h_hjas_family_h_product_partial + S (pa_r_hjas_family_h_product) = S ((S (pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_partial. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_partial * S ((S (pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product) + (pa_r_hjas_family_h_product))) /\ ((((exists pa_h_hjas_family_h_product_successor. pa_h_hjas_family_h_product_successor + S (pa_s_hjas_family_h_product) = S ((S (S pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product)) /\ exists pa_q_hjas_family_h_product_successor. pa_u_hjas_family_h_product = pa_q_hjas_family_h_product_successor * S ((S (S pa_i_hjas_family_h_product)) * pa_v_hjas_family_h_product) + (pa_s_hjas_family_h_product))) /\ pa_s_hjas_family_h_product = pa_r_hjas_family_h_product * pa_p_hjas_family_h_product)))))))) -> (exists pa_b_hjas_family_h_bound pa_c_hjas_family_h_bound. ((forall pa_i_hjas_family_h_bound_repeat. (exists pa_lt_hjas_family_h_bound_repeat_bound. pa_lt_hjas_family_h_bound_repeat_bound + S pa_i_hjas_family_h_bound_repeat = ee) -> (((exists pa_h_hjas_family_h_bound_repeat_decoded. pa_h_hjas_family_h_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_family_h_bound_repeat)) * pa_c_hjas_family_h_bound)) /\ exists pa_q_hjas_family_h_bound_repeat_decoded. pa_b_hjas_family_h_bound = pa_q_hjas_family_h_bound_repeat_decoded * S ((S (pa_i_hjas_family_h_bound_repeat)) * pa_c_hjas_family_h_bound) + (4)))) /\ (exists pa_u_hjas_family_h_bound_product pa_v_hjas_family_h_bound_product. ((((exists pa_h_hjas_family_h_bound_product_start. pa_h_hjas_family_h_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_start. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_start * S ((S (0)) * pa_v_hjas_family_h_bound_product) + (1))) /\ ((((exists pa_h_hjas_family_h_bound_product_terminal. pa_h_hjas_family_h_bound_product_terminal + S (uu) = S ((S (ee)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_terminal. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_terminal * S ((S (ee)) * pa_v_hjas_family_h_bound_product) + (uu))) /\ forall pa_i_hjas_family_h_bound_product. (exists pa_lt_hjas_family_h_bound_product_bound. pa_lt_hjas_family_h_bound_product_bound + S pa_i_hjas_family_h_bound_product = ee) -> exists pa_p_hjas_family_h_bound_product pa_r_hjas_family_h_bound_product pa_s_hjas_family_h_bound_product. ((((exists pa_h_hjas_family_h_bound_product_factor. pa_h_hjas_family_h_bound_product_factor + S (pa_p_hjas_family_h_bound_product) = S ((S (pa_i_hjas_family_h_bound_product)) * pa_c_hjas_family_h_bound)) /\ exists pa_q_hjas_family_h_bound_product_factor. pa_b_hjas_family_h_bound = pa_q_hjas_family_h_bound_product_factor * S ((S (pa_i_hjas_family_h_bound_product)) * pa_c_hjas_family_h_bound) + (pa_p_hjas_family_h_bound_product))) /\ ((((exists pa_h_hjas_family_h_bound_product_partial. pa_h_hjas_family_h_bound_product_partial + S (pa_r_hjas_family_h_bound_product) = S ((S (pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_partial. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_partial * S ((S (pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product) + (pa_r_hjas_family_h_bound_product))) /\ ((((exists pa_h_hjas_family_h_bound_product_successor. pa_h_hjas_family_h_bound_product_successor + S (pa_s_hjas_family_h_bound_product) = S ((S (S pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product)) /\ exists pa_q_hjas_family_h_bound_product_successor. pa_u_hjas_family_h_bound_product = pa_q_hjas_family_h_bound_product_successor * S ((S (S pa_i_hjas_family_h_bound_product)) * pa_v_hjas_family_h_bound_product) + (pa_s_hjas_family_h_bound_product))) /\ pa_s_hjas_family_h_bound_product = pa_r_hjas_family_h_bound_product * pa_p_hjas_family_h_bound_product)))))))) -> (exists pa_b_hjas_family_j pa_c_hjas_family_j. ((forall pa_i_hjas_family_j_repeat. (exists pa_lt_hjas_family_j_repeat_bound. pa_lt_hjas_family_j_repeat_bound + S pa_i_hjas_family_j_repeat = 12) -> (((exists pa_h_hjas_family_j_repeat_decoded. pa_h_hjas_family_j_repeat_decoded + S ((x + 6 * kk) + 7) = S ((S (pa_i_hjas_family_j_repeat)) * pa_c_hjas_family_j)) /\ exists pa_q_hjas_family_j_repeat_decoded. pa_b_hjas_family_j = pa_q_hjas_family_j_repeat_decoded * S ((S (pa_i_hjas_family_j_repeat)) * pa_c_hjas_family_j) + ((x + 6 * kk) + 7)))) /\ (exists pa_u_hjas_family_j_product pa_v_hjas_family_j_product. ((((exists pa_h_hjas_family_j_product_start. pa_h_hjas_family_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_start. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_start * S ((S (0)) * pa_v_hjas_family_j_product) + (1))) /\ ((((exists pa_h_hjas_family_j_product_terminal. pa_h_hjas_family_j_product_terminal + S (jj) = S ((S (12)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_terminal. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_terminal * S ((S (12)) * pa_v_hjas_family_j_product) + (jj))) /\ forall pa_i_hjas_family_j_product. (exists pa_lt_hjas_family_j_product_bound. pa_lt_hjas_family_j_product_bound + S pa_i_hjas_family_j_product = 12) -> exists pa_p_hjas_family_j_product pa_r_hjas_family_j_product pa_s_hjas_family_j_product. ((((exists pa_h_hjas_family_j_product_factor. pa_h_hjas_family_j_product_factor + S (pa_p_hjas_family_j_product) = S ((S (pa_i_hjas_family_j_product)) * pa_c_hjas_family_j)) /\ exists pa_q_hjas_family_j_product_factor. pa_b_hjas_family_j = pa_q_hjas_family_j_product_factor * S ((S (pa_i_hjas_family_j_product)) * pa_c_hjas_family_j) + (pa_p_hjas_family_j_product))) /\ ((((exists pa_h_hjas_family_j_product_partial. pa_h_hjas_family_j_product_partial + S (pa_r_hjas_family_j_product) = S ((S (pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_partial. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_partial * S ((S (pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product) + (pa_r_hjas_family_j_product))) /\ ((((exists pa_h_hjas_family_j_product_successor. pa_h_hjas_family_j_product_successor + S (pa_s_hjas_family_j_product) = S ((S (S pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product)) /\ exists pa_q_hjas_family_j_product_successor. pa_u_hjas_family_j_product = pa_q_hjas_family_j_product_successor * S ((S (S pa_i_hjas_family_j_product)) * pa_v_hjas_family_j_product) + (pa_s_hjas_family_j_product))) /\ pa_s_hjas_family_j_product = pa_r_hjas_family_j_product * pa_p_hjas_family_j_product)))))))) -> (exists pa_b_hjas_family_j_bound pa_c_hjas_family_j_bound. ((forall pa_i_hjas_family_j_bound_repeat. (exists pa_lt_hjas_family_j_bound_repeat_bound. pa_lt_hjas_family_j_bound_repeat_bound + S pa_i_hjas_family_j_bound_repeat = (x + 6 * kk) + 5) -> (((exists pa_h_hjas_family_j_bound_repeat_decoded. pa_h_hjas_family_j_bound_repeat_decoded + S (4) = S ((S (pa_i_hjas_family_j_bound_repeat)) * pa_c_hjas_family_j_bound)) /\ exists pa_q_hjas_family_j_bound_repeat_decoded. pa_b_hjas_family_j_bound = pa_q_hjas_family_j_bound_repeat_decoded * S ((S (pa_i_hjas_family_j_bound_repeat)) * pa_c_hjas_family_j_bound) + (4)))) /\ (exists pa_u_hjas_family_j_bound_product pa_v_hjas_family_j_bound_product. ((((exists pa_h_hjas_family_j_bound_product_start. pa_h_hjas_family_j_bound_product_start + S (1) = S ((S (0)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_start. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_start * S ((S (0)) * pa_v_hjas_family_j_bound_product) + (1))) /\ ((((exists pa_h_hjas_family_j_bound_product_terminal. pa_h_hjas_family_j_bound_product_terminal + S (gg) = S ((S ((x + 6 * kk) + 5)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_terminal. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_terminal * S ((S ((x + 6 * kk) + 5)) * pa_v_hjas_family_j_bound_product) + (gg))) /\ forall pa_i_hjas_family_j_bound_product. (exists pa_lt_hjas_family_j_bound_product_bound. pa_lt_hjas_family_j_bound_product_bound + S pa_i_hjas_family_j_bound_product = (x + 6 * kk) + 5) -> exists pa_p_hjas_family_j_bound_product pa_r_hjas_family_j_bound_product pa_s_hjas_family_j_bound_product. ((((exists pa_h_hjas_family_j_bound_product_factor. pa_h_hjas_family_j_bound_product_factor + S (pa_p_hjas_family_j_bound_product) = S ((S (pa_i_hjas_family_j_bound_product)) * pa_c_hjas_family_j_bound)) /\ exists pa_q_hjas_family_j_bound_product_factor. pa_b_hjas_family_j_bound = pa_q_hjas_family_j_bound_product_factor * S ((S (pa_i_hjas_family_j_bound_product)) * pa_c_hjas_family_j_bound) + (pa_p_hjas_family_j_bound_product))) /\ ((((exists pa_h_hjas_family_j_bound_product_partial. pa_h_hjas_family_j_bound_product_partial + S (pa_r_hjas_family_j_bound_product) = S ((S (pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_partial. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_partial * S ((S (pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product) + (pa_r_hjas_family_j_bound_product))) /\ ((((exists pa_h_hjas_family_j_bound_product_successor. pa_h_hjas_family_j_bound_product_successor + S (pa_s_hjas_family_j_bound_product) = S ((S (S pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product)) /\ exists pa_q_hjas_family_j_bound_product_successor. pa_u_hjas_family_j_bound_product = pa_q_hjas_family_j_bound_product_successor * S ((S (S pa_i_hjas_family_j_bound_product)) * pa_v_hjas_family_j_bound_product) + (pa_s_hjas_family_j_bound_product))) /\ pa_s_hjas_family_j_bound_product = pa_r_hjas_family_j_bound_product * pa_p_hjas_family_j_bound_product)))))))) -> (((exists bqb_le_gap_hjas_family_h_result. bqb_le_gap_hjas_family_h_result + (hh) = (uu)) /\ (exists bqb_le_gap_hjas_family_j_result. bqb_le_gap_hjas_family_j_result + (jj) = (gg))))
  28. 0028specialize bertrand_hj_six_block_iterate_from_total x
  29. 0029apply bertrand_hj_six_block_iterate_from_total
  30. 0030exact htotal
  31. 0031exact hdecomposition_witness_witness_left_left
  32. 0032exact hdecomposition_witness_witness_left_right
  33. 0033have hblock_ceiling : CeilDivSix((x + 6 · x1) · (x + 6 · x1),e)
    Exact native replay linehave hblock_ceiling : ((exists bcs_lower_gap_hjas_block_ceiling. bcs_lower_gap_hjas_block_ceiling + ((x + 6 * x1) * (x + 6 * x1)) = 6 * (e)) /\ exists bcs_upper_gap_hjas_block_ceiling. bcs_upper_gap_hjas_block_ceiling + S (6 * (e)) = ((x + 6 * x1) * (x + 6 * x1)) + 6)
  34. 0034rewrite <- hdecomposition_witness_witness_right
  35. 0035rewrite <- hdecomposition_witness_witness_right
  36. 0036rewrite <- hdecomposition_witness_witness_right
  37. 0037rewrite <- hdecomposition_witness_witness_right
  38. 0038exact hceiling
  39. 0039have hblock_h : Pow(x + 6 · x1 + 1,2 · (x + 6 · x1) + 2,h)
    Exact native replay linehave hblock_h : exists pa_b_hjas_block_h pa_c_hjas_block_h. ((forall pa_i_hjas_block_h_repeat. (exists pa_lt_hjas_block_h_repeat_bound. pa_lt_hjas_block_h_repeat_bound + S pa_i_hjas_block_h_repeat = 2 * (x + 6 * x1) + 2) -> (((exists pa_h_hjas_block_h_repeat_decoded. pa_h_hjas_block_h_repeat_decoded + S ((x + 6 * x1) + 1) = S ((S (pa_i_hjas_block_h_repeat)) * pa_c_hjas_block_h)) /\ exists pa_q_hjas_block_h_repeat_decoded. pa_b_hjas_block_h = pa_q_hjas_block_h_repeat_decoded * S ((S (pa_i_hjas_block_h_repeat)) * pa_c_hjas_block_h) + ((x + 6 * x1) + 1)))) /\ (exists pa_u_hjas_block_h_product pa_v_hjas_block_h_product. ((((exists pa_h_hjas_block_h_product_start. pa_h_hjas_block_h_product_start + S (1) = S ((S (0)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_start. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_start * S ((S (0)) * pa_v_hjas_block_h_product) + (1))) /\ ((((exists pa_h_hjas_block_h_product_terminal. pa_h_hjas_block_h_product_terminal + S (h) = S ((S (2 * (x + 6 * x1) + 2)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_terminal. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_terminal * S ((S (2 * (x + 6 * x1) + 2)) * pa_v_hjas_block_h_product) + (h))) /\ forall pa_i_hjas_block_h_product. (exists pa_lt_hjas_block_h_product_bound. pa_lt_hjas_block_h_product_bound + S pa_i_hjas_block_h_product = 2 * (x + 6 * x1) + 2) -> exists pa_p_hjas_block_h_product pa_r_hjas_block_h_product pa_s_hjas_block_h_product. ((((exists pa_h_hjas_block_h_product_factor. pa_h_hjas_block_h_product_factor + S (pa_p_hjas_block_h_product) = S ((S (pa_i_hjas_block_h_product)) * pa_c_hjas_block_h)) /\ exists pa_q_hjas_block_h_product_factor. pa_b_hjas_block_h = pa_q_hjas_block_h_product_factor * S ((S (pa_i_hjas_block_h_product)) * pa_c_hjas_block_h) + (pa_p_hjas_block_h_product))) /\ ((((exists pa_h_hjas_block_h_product_partial. pa_h_hjas_block_h_product_partial + S (pa_r_hjas_block_h_product) = S ((S (pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_partial. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_partial * S ((S (pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product) + (pa_r_hjas_block_h_product))) /\ ((((exists pa_h_hjas_block_h_product_successor. pa_h_hjas_block_h_product_successor + S (pa_s_hjas_block_h_product) = S ((S (S pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product)) /\ exists pa_q_hjas_block_h_product_successor. pa_u_hjas_block_h_product = pa_q_hjas_block_h_product_successor * S ((S (S pa_i_hjas_block_h_product)) * pa_v_hjas_block_h_product) + (pa_s_hjas_block_h_product))) /\ pa_s_hjas_block_h_product = pa_r_hjas_block_h_product * pa_p_hjas_block_h_product)))))))
  40. 0040rewrite <- hdecomposition_witness_witness_right
  41. 0041rewrite <- hdecomposition_witness_witness_right
  42. 0042rewrite <- hdecomposition_witness_witness_right
  43. 0043rewrite <- hdecomposition_witness_witness_right
  44. 0044rewrite <- hdecomposition_witness_witness_right
  45. 0045rewrite <- hdecomposition_witness_witness_right
  46. 0046exact hh
  47. 0047have hblock_j : Pow(x + 6 · x1 + 7,12,j)
    Exact native replay linehave hblock_j : exists pa_b_hjas_block_j pa_c_hjas_block_j. ((forall pa_i_hjas_block_j_repeat. (exists pa_lt_hjas_block_j_repeat_bound. pa_lt_hjas_block_j_repeat_bound + S pa_i_hjas_block_j_repeat = 12) -> (((exists pa_h_hjas_block_j_repeat_decoded. pa_h_hjas_block_j_repeat_decoded + S ((x + 6 * x1) + 7) = S ((S (pa_i_hjas_block_j_repeat)) * pa_c_hjas_block_j)) /\ exists pa_q_hjas_block_j_repeat_decoded. pa_b_hjas_block_j = pa_q_hjas_block_j_repeat_decoded * S ((S (pa_i_hjas_block_j_repeat)) * pa_c_hjas_block_j) + ((x + 6 * x1) + 7)))) /\ (exists pa_u_hjas_block_j_product pa_v_hjas_block_j_product. ((((exists pa_h_hjas_block_j_product_start. pa_h_hjas_block_j_product_start + S (1) = S ((S (0)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_start. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_start * S ((S (0)) * pa_v_hjas_block_j_product) + (1))) /\ ((((exists pa_h_hjas_block_j_product_terminal. pa_h_hjas_block_j_product_terminal + S (j) = S ((S (12)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_terminal. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_terminal * S ((S (12)) * pa_v_hjas_block_j_product) + (j))) /\ forall pa_i_hjas_block_j_product. (exists pa_lt_hjas_block_j_product_bound. pa_lt_hjas_block_j_product_bound + S pa_i_hjas_block_j_product = 12) -> exists pa_p_hjas_block_j_product pa_r_hjas_block_j_product pa_s_hjas_block_j_product. ((((exists pa_h_hjas_block_j_product_factor. pa_h_hjas_block_j_product_factor + S (pa_p_hjas_block_j_product) = S ((S (pa_i_hjas_block_j_product)) * pa_c_hjas_block_j)) /\ exists pa_q_hjas_block_j_product_factor. pa_b_hjas_block_j = pa_q_hjas_block_j_product_factor * S ((S (pa_i_hjas_block_j_product)) * pa_c_hjas_block_j) + (pa_p_hjas_block_j_product))) /\ ((((exists pa_h_hjas_block_j_product_partial. pa_h_hjas_block_j_product_partial + S (pa_r_hjas_block_j_product) = S ((S (pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_partial. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_partial * S ((S (pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product) + (pa_r_hjas_block_j_product))) /\ ((((exists pa_h_hjas_block_j_product_successor. pa_h_hjas_block_j_product_successor + S (pa_s_hjas_block_j_product) = S ((S (S pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product)) /\ exists pa_q_hjas_block_j_product_successor. pa_u_hjas_block_j_product = pa_q_hjas_block_j_product_successor * S ((S (S pa_i_hjas_block_j_product)) * pa_v_hjas_block_j_product) + (pa_s_hjas_block_j_product))) /\ pa_s_hjas_block_j_product = pa_r_hjas_block_j_product * pa_p_hjas_block_j_product)))))))
  48. 0048rewrite <- hdecomposition_witness_witness_right
  49. 0049rewrite <- hdecomposition_witness_witness_right
  50. 0050exact hj
  51. 0051have hblock_g : Pow(4,x + 6 · x1 + 5,g)
    Exact native replay linehave hblock_g : exists pa_b_hjas_block_g pa_c_hjas_block_g. ((forall pa_i_hjas_block_g_repeat. (exists pa_lt_hjas_block_g_repeat_bound. pa_lt_hjas_block_g_repeat_bound + S pa_i_hjas_block_g_repeat = (x + 6 * x1) + 5) -> (((exists pa_h_hjas_block_g_repeat_decoded. pa_h_hjas_block_g_repeat_decoded + S (4) = S ((S (pa_i_hjas_block_g_repeat)) * pa_c_hjas_block_g)) /\ exists pa_q_hjas_block_g_repeat_decoded. pa_b_hjas_block_g = pa_q_hjas_block_g_repeat_decoded * S ((S (pa_i_hjas_block_g_repeat)) * pa_c_hjas_block_g) + (4)))) /\ (exists pa_u_hjas_block_g_product pa_v_hjas_block_g_product. ((((exists pa_h_hjas_block_g_product_start. pa_h_hjas_block_g_product_start + S (1) = S ((S (0)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_start. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_start * S ((S (0)) * pa_v_hjas_block_g_product) + (1))) /\ ((((exists pa_h_hjas_block_g_product_terminal. pa_h_hjas_block_g_product_terminal + S (g) = S ((S ((x + 6 * x1) + 5)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_terminal. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_terminal * S ((S ((x + 6 * x1) + 5)) * pa_v_hjas_block_g_product) + (g))) /\ forall pa_i_hjas_block_g_product. (exists pa_lt_hjas_block_g_product_bound. pa_lt_hjas_block_g_product_bound + S pa_i_hjas_block_g_product = (x + 6 * x1) + 5) -> exists pa_p_hjas_block_g_product pa_r_hjas_block_g_product pa_s_hjas_block_g_product. ((((exists pa_h_hjas_block_g_product_factor. pa_h_hjas_block_g_product_factor + S (pa_p_hjas_block_g_product) = S ((S (pa_i_hjas_block_g_product)) * pa_c_hjas_block_g)) /\ exists pa_q_hjas_block_g_product_factor. pa_b_hjas_block_g = pa_q_hjas_block_g_product_factor * S ((S (pa_i_hjas_block_g_product)) * pa_c_hjas_block_g) + (pa_p_hjas_block_g_product))) /\ ((((exists pa_h_hjas_block_g_product_partial. pa_h_hjas_block_g_product_partial + S (pa_r_hjas_block_g_product) = S ((S (pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_partial. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_partial * S ((S (pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product) + (pa_r_hjas_block_g_product))) /\ ((((exists pa_h_hjas_block_g_product_successor. pa_h_hjas_block_g_product_successor + S (pa_s_hjas_block_g_product) = S ((S (S pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product)) /\ exists pa_q_hjas_block_g_product_successor. pa_u_hjas_block_g_product = pa_q_hjas_block_g_product_successor * S ((S (S pa_i_hjas_block_g_product)) * pa_v_hjas_block_g_product) + (pa_s_hjas_block_g_product))) /\ pa_s_hjas_block_g_product = pa_r_hjas_block_g_product * pa_p_hjas_block_g_product)))))))
  52. 0052rewrite <- hdecomposition_witness_witness_right
  53. 0053rewrite <- hdecomposition_witness_witness_right
  54. 0054rewrite <- hdecomposition_witness_witness_right
  55. 0055rewrite <- hdecomposition_witness_witness_right
  56. 0056exact hg
  57. 0057specialize hfamily x1
  58. 0058specialize hfamily e
  59. 0059specialize hfamily h
  60. 0060specialize hfamily u
  61. 0061specialize hfamily j
  62. 0062specialize hfamily g
  63. 0063apply hfamily
  64. 0064exact hblock_ceiling
  65. 0065exact hblock_h
  66. 0066exact hu
  67. 0067exact hblock_j
  68. 0068exact hblock_g