BT00SX · Bertrand theorem

bertrand_j_six_step_transport_from_total

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

J(s) implies J(s+6) through the shared 2^12 = 4^6 factor.

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. ∀ j. ∀ g. ∀ jn. ∀ gn. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → Pow(s + 7,12,j) → Pow(4,s + 5,g) → Le(j,g) → Pow(s + 13,12,jn) → Pow(4,s + 11,gn) → Le(jn,gn)

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

7 occurrences

In local proof propositions

PD0001 Le PD0020 Pow

8 occurrences

Exact expanded native-PA statement
forall s j g jn gn. (forall bpt_a_hjt_j bpt_e_hjt_j. exists bpt_x_hjt_j. (exists ff_b_bpt_value_hjt_j ff_c_bpt_value_hjt_j. ((forall ff_i_bpt_value_hjt_j_repeat. (exists ff_lt_bpt_value_hjt_j_repeat_bound. ff_lt_bpt_value_hjt_j_repeat_bound + S ff_i_bpt_value_hjt_j_repeat = bpt_e_hjt_j) -> (((exists ff_h_bpt_value_hjt_j_repeat_decoded. ff_h_bpt_value_hjt_j_repeat_decoded + S (bpt_a_hjt_j) = S ((S (ff_i_bpt_value_hjt_j_repeat)) * ff_c_bpt_value_hjt_j)) /\ exists ff_q_bpt_value_hjt_j_repeat_decoded. ff_b_bpt_value_hjt_j = ff_q_bpt_value_hjt_j_repeat_decoded * S ((S (ff_i_bpt_value_hjt_j_repeat)) * ff_c_bpt_value_hjt_j) + (bpt_a_hjt_j)))) /\ (exists ff_u_bpt_value_hjt_j_product ff_v_bpt_value_hjt_j_product. ((((exists ff_h_bpt_value_hjt_j_product_start. ff_h_bpt_value_hjt_j_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_start. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_start * S ((S (0)) * ff_v_bpt_value_hjt_j_product) + (1))) /\ ((((exists ff_h_bpt_value_hjt_j_product_terminal. ff_h_bpt_value_hjt_j_product_terminal + S (bpt_x_hjt_j) = S ((S (bpt_e_hjt_j)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_terminal. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_terminal * S ((S (bpt_e_hjt_j)) * ff_v_bpt_value_hjt_j_product) + (bpt_x_hjt_j))) /\ forall ff_i_bpt_value_hjt_j_product. (exists ff_lt_bpt_value_hjt_j_product_bound. ff_lt_bpt_value_hjt_j_product_bound + S ff_i_bpt_value_hjt_j_product = bpt_e_hjt_j) -> exists ff_p_bpt_value_hjt_j_product ff_r_bpt_value_hjt_j_product ff_s_bpt_value_hjt_j_product. ((((exists ff_h_bpt_value_hjt_j_product_factor. ff_h_bpt_value_hjt_j_product_factor + S (ff_p_bpt_value_hjt_j_product) = S ((S (ff_i_bpt_value_hjt_j_product)) * ff_c_bpt_value_hjt_j)) /\ exists ff_q_bpt_value_hjt_j_product_factor. ff_b_bpt_value_hjt_j = ff_q_bpt_value_hjt_j_product_factor * S ((S (ff_i_bpt_value_hjt_j_product)) * ff_c_bpt_value_hjt_j) + (ff_p_bpt_value_hjt_j_product))) /\ ((((exists ff_h_bpt_value_hjt_j_product_partial. ff_h_bpt_value_hjt_j_product_partial + S (ff_r_bpt_value_hjt_j_product) = S ((S (ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_partial. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_partial * S ((S (ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product) + (ff_r_bpt_value_hjt_j_product))) /\ ((((exists ff_h_bpt_value_hjt_j_product_successor. ff_h_bpt_value_hjt_j_product_successor + S (ff_s_bpt_value_hjt_j_product) = S ((S (S ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product)) /\ exists ff_q_bpt_value_hjt_j_product_successor. ff_u_bpt_value_hjt_j_product = ff_q_bpt_value_hjt_j_product_successor * S ((S (S ff_i_bpt_value_hjt_j_product)) * ff_v_bpt_value_hjt_j_product) + (ff_s_bpt_value_hjt_j_product))) /\ ff_s_bpt_value_hjt_j_product = ff_r_bpt_value_hjt_j_product * ff_p_bpt_value_hjt_j_product))))))))) -> (exists pa_b_hjt_j_now pa_c_hjt_j_now. ((forall pa_i_hjt_j_now_repeat. (exists pa_lt_hjt_j_now_repeat_bound. pa_lt_hjt_j_now_repeat_bound + S pa_i_hjt_j_now_repeat = 12) -> (((exists pa_h_hjt_j_now_repeat_decoded. pa_h_hjt_j_now_repeat_decoded + S (s + 7) = S ((S (pa_i_hjt_j_now_repeat)) * pa_c_hjt_j_now)) /\ exists pa_q_hjt_j_now_repeat_decoded. pa_b_hjt_j_now = pa_q_hjt_j_now_repeat_decoded * S ((S (pa_i_hjt_j_now_repeat)) * pa_c_hjt_j_now) + (s + 7)))) /\ (exists pa_u_hjt_j_now_product pa_v_hjt_j_now_product. ((((exists pa_h_hjt_j_now_product_start. pa_h_hjt_j_now_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_start. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_start * S ((S (0)) * pa_v_hjt_j_now_product) + (1))) /\ ((((exists pa_h_hjt_j_now_product_terminal. pa_h_hjt_j_now_product_terminal + S (j) = S ((S (12)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_terminal. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_terminal * S ((S (12)) * pa_v_hjt_j_now_product) + (j))) /\ forall pa_i_hjt_j_now_product. (exists pa_lt_hjt_j_now_product_bound. pa_lt_hjt_j_now_product_bound + S pa_i_hjt_j_now_product = 12) -> exists pa_p_hjt_j_now_product pa_r_hjt_j_now_product pa_s_hjt_j_now_product. ((((exists pa_h_hjt_j_now_product_factor. pa_h_hjt_j_now_product_factor + S (pa_p_hjt_j_now_product) = S ((S (pa_i_hjt_j_now_product)) * pa_c_hjt_j_now)) /\ exists pa_q_hjt_j_now_product_factor. pa_b_hjt_j_now = pa_q_hjt_j_now_product_factor * S ((S (pa_i_hjt_j_now_product)) * pa_c_hjt_j_now) + (pa_p_hjt_j_now_product))) /\ ((((exists pa_h_hjt_j_now_product_partial. pa_h_hjt_j_now_product_partial + S (pa_r_hjt_j_now_product) = S ((S (pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_partial. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_partial * S ((S (pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product) + (pa_r_hjt_j_now_product))) /\ ((((exists pa_h_hjt_j_now_product_successor. pa_h_hjt_j_now_product_successor + S (pa_s_hjt_j_now_product) = S ((S (S pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product)) /\ exists pa_q_hjt_j_now_product_successor. pa_u_hjt_j_now_product = pa_q_hjt_j_now_product_successor * S ((S (S pa_i_hjt_j_now_product)) * pa_v_hjt_j_now_product) + (pa_s_hjt_j_now_product))) /\ pa_s_hjt_j_now_product = pa_r_hjt_j_now_product * pa_p_hjt_j_now_product)))))))) -> (exists pa_b_hjt_j_now_bound pa_c_hjt_j_now_bound. ((forall pa_i_hjt_j_now_bound_repeat. (exists pa_lt_hjt_j_now_bound_repeat_bound. pa_lt_hjt_j_now_bound_repeat_bound + S pa_i_hjt_j_now_bound_repeat = s + 5) -> (((exists pa_h_hjt_j_now_bound_repeat_decoded. pa_h_hjt_j_now_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_j_now_bound_repeat)) * pa_c_hjt_j_now_bound)) /\ exists pa_q_hjt_j_now_bound_repeat_decoded. pa_b_hjt_j_now_bound = pa_q_hjt_j_now_bound_repeat_decoded * S ((S (pa_i_hjt_j_now_bound_repeat)) * pa_c_hjt_j_now_bound) + (4)))) /\ (exists pa_u_hjt_j_now_bound_product pa_v_hjt_j_now_bound_product. ((((exists pa_h_hjt_j_now_bound_product_start. pa_h_hjt_j_now_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_start. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_start * S ((S (0)) * pa_v_hjt_j_now_bound_product) + (1))) /\ ((((exists pa_h_hjt_j_now_bound_product_terminal. pa_h_hjt_j_now_bound_product_terminal + S (g) = S ((S (s + 5)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_terminal. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_terminal * S ((S (s + 5)) * pa_v_hjt_j_now_bound_product) + (g))) /\ forall pa_i_hjt_j_now_bound_product. (exists pa_lt_hjt_j_now_bound_product_bound. pa_lt_hjt_j_now_bound_product_bound + S pa_i_hjt_j_now_bound_product = s + 5) -> exists pa_p_hjt_j_now_bound_product pa_r_hjt_j_now_bound_product pa_s_hjt_j_now_bound_product. ((((exists pa_h_hjt_j_now_bound_product_factor. pa_h_hjt_j_now_bound_product_factor + S (pa_p_hjt_j_now_bound_product) = S ((S (pa_i_hjt_j_now_bound_product)) * pa_c_hjt_j_now_bound)) /\ exists pa_q_hjt_j_now_bound_product_factor. pa_b_hjt_j_now_bound = pa_q_hjt_j_now_bound_product_factor * S ((S (pa_i_hjt_j_now_bound_product)) * pa_c_hjt_j_now_bound) + (pa_p_hjt_j_now_bound_product))) /\ ((((exists pa_h_hjt_j_now_bound_product_partial. pa_h_hjt_j_now_bound_product_partial + S (pa_r_hjt_j_now_bound_product) = S ((S (pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_partial. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_partial * S ((S (pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product) + (pa_r_hjt_j_now_bound_product))) /\ ((((exists pa_h_hjt_j_now_bound_product_successor. pa_h_hjt_j_now_bound_product_successor + S (pa_s_hjt_j_now_bound_product) = S ((S (S pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product)) /\ exists pa_q_hjt_j_now_bound_product_successor. pa_u_hjt_j_now_bound_product = pa_q_hjt_j_now_bound_product_successor * S ((S (S pa_i_hjt_j_now_bound_product)) * pa_v_hjt_j_now_bound_product) + (pa_s_hjt_j_now_bound_product))) /\ pa_s_hjt_j_now_bound_product = pa_r_hjt_j_now_bound_product * pa_p_hjt_j_now_bound_product)))))))) -> (exists bqb_le_gap_hjt_j_now_result. bqb_le_gap_hjt_j_now_result + (j) = (g)) -> (exists pa_b_hjt_j_next pa_c_hjt_j_next. ((forall pa_i_hjt_j_next_repeat. (exists pa_lt_hjt_j_next_repeat_bound. pa_lt_hjt_j_next_repeat_bound + S pa_i_hjt_j_next_repeat = 12) -> (((exists pa_h_hjt_j_next_repeat_decoded. pa_h_hjt_j_next_repeat_decoded + S (s + 13) = S ((S (pa_i_hjt_j_next_repeat)) * pa_c_hjt_j_next)) /\ exists pa_q_hjt_j_next_repeat_decoded. pa_b_hjt_j_next = pa_q_hjt_j_next_repeat_decoded * S ((S (pa_i_hjt_j_next_repeat)) * pa_c_hjt_j_next) + (s + 13)))) /\ (exists pa_u_hjt_j_next_product pa_v_hjt_j_next_product. ((((exists pa_h_hjt_j_next_product_start. pa_h_hjt_j_next_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_start. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_start * S ((S (0)) * pa_v_hjt_j_next_product) + (1))) /\ ((((exists pa_h_hjt_j_next_product_terminal. pa_h_hjt_j_next_product_terminal + S (jn) = S ((S (12)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_terminal. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_terminal * S ((S (12)) * pa_v_hjt_j_next_product) + (jn))) /\ forall pa_i_hjt_j_next_product. (exists pa_lt_hjt_j_next_product_bound. pa_lt_hjt_j_next_product_bound + S pa_i_hjt_j_next_product = 12) -> exists pa_p_hjt_j_next_product pa_r_hjt_j_next_product pa_s_hjt_j_next_product. ((((exists pa_h_hjt_j_next_product_factor. pa_h_hjt_j_next_product_factor + S (pa_p_hjt_j_next_product) = S ((S (pa_i_hjt_j_next_product)) * pa_c_hjt_j_next)) /\ exists pa_q_hjt_j_next_product_factor. pa_b_hjt_j_next = pa_q_hjt_j_next_product_factor * S ((S (pa_i_hjt_j_next_product)) * pa_c_hjt_j_next) + (pa_p_hjt_j_next_product))) /\ ((((exists pa_h_hjt_j_next_product_partial. pa_h_hjt_j_next_product_partial + S (pa_r_hjt_j_next_product) = S ((S (pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_partial. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_partial * S ((S (pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product) + (pa_r_hjt_j_next_product))) /\ ((((exists pa_h_hjt_j_next_product_successor. pa_h_hjt_j_next_product_successor + S (pa_s_hjt_j_next_product) = S ((S (S pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product)) /\ exists pa_q_hjt_j_next_product_successor. pa_u_hjt_j_next_product = pa_q_hjt_j_next_product_successor * S ((S (S pa_i_hjt_j_next_product)) * pa_v_hjt_j_next_product) + (pa_s_hjt_j_next_product))) /\ pa_s_hjt_j_next_product = pa_r_hjt_j_next_product * pa_p_hjt_j_next_product)))))))) -> (exists pa_b_hjt_j_next_bound pa_c_hjt_j_next_bound. ((forall pa_i_hjt_j_next_bound_repeat. (exists pa_lt_hjt_j_next_bound_repeat_bound. pa_lt_hjt_j_next_bound_repeat_bound + S pa_i_hjt_j_next_bound_repeat = s + 11) -> (((exists pa_h_hjt_j_next_bound_repeat_decoded. pa_h_hjt_j_next_bound_repeat_decoded + S (4) = S ((S (pa_i_hjt_j_next_bound_repeat)) * pa_c_hjt_j_next_bound)) /\ exists pa_q_hjt_j_next_bound_repeat_decoded. pa_b_hjt_j_next_bound = pa_q_hjt_j_next_bound_repeat_decoded * S ((S (pa_i_hjt_j_next_bound_repeat)) * pa_c_hjt_j_next_bound) + (4)))) /\ (exists pa_u_hjt_j_next_bound_product pa_v_hjt_j_next_bound_product. ((((exists pa_h_hjt_j_next_bound_product_start. pa_h_hjt_j_next_bound_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_start. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_start * S ((S (0)) * pa_v_hjt_j_next_bound_product) + (1))) /\ ((((exists pa_h_hjt_j_next_bound_product_terminal. pa_h_hjt_j_next_bound_product_terminal + S (gn) = S ((S (s + 11)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_terminal. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_terminal * S ((S (s + 11)) * pa_v_hjt_j_next_bound_product) + (gn))) /\ forall pa_i_hjt_j_next_bound_product. (exists pa_lt_hjt_j_next_bound_product_bound. pa_lt_hjt_j_next_bound_product_bound + S pa_i_hjt_j_next_bound_product = s + 11) -> exists pa_p_hjt_j_next_bound_product pa_r_hjt_j_next_bound_product pa_s_hjt_j_next_bound_product. ((((exists pa_h_hjt_j_next_bound_product_factor. pa_h_hjt_j_next_bound_product_factor + S (pa_p_hjt_j_next_bound_product) = S ((S (pa_i_hjt_j_next_bound_product)) * pa_c_hjt_j_next_bound)) /\ exists pa_q_hjt_j_next_bound_product_factor. pa_b_hjt_j_next_bound = pa_q_hjt_j_next_bound_product_factor * S ((S (pa_i_hjt_j_next_bound_product)) * pa_c_hjt_j_next_bound) + (pa_p_hjt_j_next_bound_product))) /\ ((((exists pa_h_hjt_j_next_bound_product_partial. pa_h_hjt_j_next_bound_product_partial + S (pa_r_hjt_j_next_bound_product) = S ((S (pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_partial. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_partial * S ((S (pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product) + (pa_r_hjt_j_next_bound_product))) /\ ((((exists pa_h_hjt_j_next_bound_product_successor. pa_h_hjt_j_next_bound_product_successor + S (pa_s_hjt_j_next_bound_product) = S ((S (S pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product)) /\ exists pa_q_hjt_j_next_bound_product_successor. pa_u_hjt_j_next_bound_product = pa_q_hjt_j_next_bound_product_successor * S ((S (S pa_i_hjt_j_next_bound_product)) * pa_v_hjt_j_next_bound_product) + (pa_s_hjt_j_next_bound_product))) /\ pa_s_hjt_j_next_bound_product = pa_r_hjt_j_next_bound_product * pa_p_hjt_j_next_bound_product)))))))) -> (exists bqb_le_gap_hjt_j_next_result. bqb_le_gap_hjt_j_next_result + (jn) = (gn))

Proof neighborhood

Direct theorem prerequisites

BT00QU two_mul_eq_add_self BT00PY pow_base_monotone BT00QV pow_mul_base BT00SO pow_two_seed_bundle_from_total BT00SM pow_mul_exp_from_total BT009X pow_add BT00PV mul_le_mul BT000E le_refl BT000F le_trans BT0003 add_assoc BT0002 add_comm

Direct theorem dependents

BT00SY bertrand_hj_six_step_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

113 script commands · 30 reading checkpoints · 11 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 (10)
pow base monotonepow mul basepow two seed bundle from totalpow mul exp from totalpow addmul le mulle reflle transadd assocadd comm
01Fix variables and assumptionsL1–10

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

  1. L1
    intro s
  2. L2
    intro j
  3. L3
    intro g
  4. L4
    intro jn
  5. L5
    intro gn
  6. L6
    intro htotal
  7. L7
    intro hj
  8. L8
    intro hg
  9. L9
    intro hjg
  10. L10
    intro hjn
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hgn
03Establish hbaseL12–12

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

  1. L12
    have hbase : Le(s + 13,2 · (s + 7))Definitions: Le(s + 13,2 · (s + 7))Original native command in the exact edition
04Construct an explicit witnessL13–13

Supply the displayed value, then prove that it has the required property.

  1. L13
    exists S s
05Calculate and transport equalitiesL14–14

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L14
    simp [two_mul_eq_add_self, add_assoc, add_comm]
06Establish hdoubleL15–18

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

  1. L15
    have hdouble : ∃ jd. Pow(2 · (s + 7),12,jd)Definitions: Pow(2 · (s + 7),12,jd)Original native command in the exact edition
  2. L16
    specialize htotal (2 * (s + 7))
  3. L17
    specialize htotal 12
  4. L18
    exact htotal
07Separate the logical casesL19–19

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

  1. L19
    cases hdouble
08Establish hjdoubleL20–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.

  1. L20
    have hjdouble : Le(jn,x)Definitions: Le(jn,x)Original native command in the exact edition
  2. L21
    specialize pow_base_monotone (s + 13)
  3. L22
    specialize pow_base_monotone (2 * (s + 7))
  4. L23
    specialize pow_base_monotone 12
  5. L24
    specialize pow_base_monotone jn
  6. L25
    specialize pow_base_monotone x
  7. L26
    apply pow_base_monotone
  8. L27
    exact hbase
  9. L28
    exact hjn
  10. L29
    exact hdouble_witness
09Establish htwoL30–33

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

  1. L30
    have htwo : ∃ jt. Pow(2,12,jt)Definitions: Pow(2,12,jt)Original native command in the exact edition
  2. L31
    specialize htotal 2
  3. L32
    specialize htotal 12
  4. L33
    exact htotal
10Separate the logical casesL34–34

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

  1. L34
    cases htwo
11Establish hfourL35–38

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

  1. L35
    have hfour : ∃ jf. Pow(4,6,jf)Definitions: Pow(4,6,jf)Original native command in the exact edition
  2. L36
    specialize htotal 4
  3. L37
    specialize htotal 6
  4. L38
    exact htotal
12Separate the logical casesL39–39

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

  1. L39
    cases hfour
13Establish hseedsL40–42

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

  1. L40
    have hseeds : Pow(2,2,4) ∧ Pow(2,7,128)Definitions: Pow(2,2,4)Pow(2,7,128)Original native command in the exact edition
  2. L41
    apply pow_two_seed_bundle_from_total
  3. L42
    exact htotal
14Separate the logical casesL43–43

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

  1. L43
    cases hseeds
15Establish htwo_fourL44–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul exp from total.

  1. L44
    have htwo_four : x1 = x2
  2. L45
    specialize pow_mul_exp_from_total 2
  3. L46
    specialize pow_mul_exp_from_total 2
  4. L47
    specialize pow_mul_exp_from_total 6
  5. L48
    specialize pow_mul_exp_from_total 12
  6. L49
    specialize pow_mul_exp_from_total 4
  7. L50
    specialize pow_mul_exp_from_total x2
  8. L51
    specialize pow_mul_exp_from_total x1
  9. L52
    symm
  10. L53
    apply pow_mul_exp_from_total
16Use earlier factsL54–54

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

  1. L54
    exact htotal
17Calculate and transport equalitiesL55–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L55
    norm_num
18Use earlier factsL56–58

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

  1. L56
    exact hseeds_left
  2. L57
    exact hfour_witness
  3. L58
    exact htwo_witness
19Establish hdouble_factorL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow mul base.

  1. L59
    have hdouble_factor : x = x1 * j
  2. L60
    specialize pow_mul_base 2
  3. L61
    specialize pow_mul_base (s + 7)
  4. L62
    specialize pow_mul_base 12
  5. L63
    specialize pow_mul_base x1
  6. L64
    specialize pow_mul_base j
  7. L65
    specialize pow_mul_base x
  8. L66
    apply pow_mul_base
  9. L67
    exact htwo_witness
  10. L68
    exact hj
20Use earlier factsL69–69

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

  1. L69
    exact hdouble_witness
21Establish hsumL70–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L70
    have hsum : s + 11 = 6 + (s + 5)
  2. L71
    trans s + (6 + 5)
  3. L72
    congr
  4. L73
    refl
  5. L74
    norm_num
  6. L75
    trans (s + 6) + 5
  7. L76
    symm
  8. L77
    apply add_assoc
  9. L78
    trans (6 + s) + 5
  10. L79
    congr
22Use earlier factsL80–80

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

  1. L80
    apply add_comm
23Calculate and transport equalitiesL81–81

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L81
    refl
24Use earlier factsL82–82

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

  1. L82
    apply add_assoc
25Establish hbound_factorL83–92

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow add.

  1. L83
    have hbound_factor : gn = x2 * g
  2. L84
    specialize pow_add 4
  3. L85
    specialize pow_add 6
  4. L86
    specialize pow_add (s + 5)
  5. L87
    specialize pow_add (s + 11)
  6. L88
    specialize pow_add x2
  7. L89
    specialize pow_add g
  8. L90
    specialize pow_add gn
  9. L91
    apply pow_add
  10. L92
    exact hsum
26Use earlier factsL93–95

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

  1. L93
    exact hfour_witness
  2. L94
    exact hg
  3. L95
    exact hgn
27Establish hproductsL96–105

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.

  1. L96
    have hproducts : Le(x1 · j,x2 · g)Definitions: Le(x1 · j,x2 · g)Original native command in the exact edition
  2. L97
    rewrite htwo_four
  3. L98
    specialize mul_le_mul x2
  4. L99
    specialize mul_le_mul x2
  5. L100
    specialize mul_le_mul j
  6. L101
    specialize mul_le_mul g
  7. L102
    apply mul_le_mul
  8. L103
    specialize le_refl x2
  9. L104
    exact le_refl
  10. L105
    exact hjg
28Use earlier factsL106–110

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

  1. L106
    specialize le_trans jn
  2. L107
    specialize le_trans x
  3. L108
    specialize le_trans gn
  4. L109
    apply le_trans
  5. L110
    exact hjdouble
29Calculate and transport equalitiesL111–112

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L111
    rewrite hdouble_factor
  2. L112
    rewrite hbound_factor
30Use earlier factsL113–113

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

  1. L113
    exact hproducts

Library-wide reading audit

Original defined command ledger · 113 lines
  1. 0001intro s
  2. 0002intro j
  3. 0003intro g
  4. 0004intro jn
  5. 0005intro gn
  6. 0006intro htotal
  7. 0007intro hj
  8. 0008intro hg
  9. 0009intro hjg
  10. 0010intro hjn
  11. 0011intro hgn
  12. 0012have hbase : Le(s + 13,2 · (s + 7))
    Exact native replay linehave hbase : exists bqb_le_gap_hjt_j_base. bqb_le_gap_hjt_j_base + (s + 13) = (2 * (s + 7))
  13. 0013exists S s
  14. 0014simp [two_mul_eq_add_self, add_assoc, add_comm]
  15. 0015have hdouble : ∃ jd. Pow(2 · (s + 7),12,jd)
    Exact native replay linehave hdouble : exists jd. (exists pa_b_hjt_j_double pa_c_hjt_j_double. ((forall pa_i_hjt_j_double_repeat. (exists pa_lt_hjt_j_double_repeat_bound. pa_lt_hjt_j_double_repeat_bound + S pa_i_hjt_j_double_repeat = 12) -> (((exists pa_h_hjt_j_double_repeat_decoded. pa_h_hjt_j_double_repeat_decoded + S (2 * (s + 7)) = S ((S (pa_i_hjt_j_double_repeat)) * pa_c_hjt_j_double)) /\ exists pa_q_hjt_j_double_repeat_decoded. pa_b_hjt_j_double = pa_q_hjt_j_double_repeat_decoded * S ((S (pa_i_hjt_j_double_repeat)) * pa_c_hjt_j_double) + (2 * (s + 7))))) /\ (exists pa_u_hjt_j_double_product pa_v_hjt_j_double_product. ((((exists pa_h_hjt_j_double_product_start. pa_h_hjt_j_double_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_start. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_start * S ((S (0)) * pa_v_hjt_j_double_product) + (1))) /\ ((((exists pa_h_hjt_j_double_product_terminal. pa_h_hjt_j_double_product_terminal + S (jd) = S ((S (12)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_terminal. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_terminal * S ((S (12)) * pa_v_hjt_j_double_product) + (jd))) /\ forall pa_i_hjt_j_double_product. (exists pa_lt_hjt_j_double_product_bound. pa_lt_hjt_j_double_product_bound + S pa_i_hjt_j_double_product = 12) -> exists pa_p_hjt_j_double_product pa_r_hjt_j_double_product pa_s_hjt_j_double_product. ((((exists pa_h_hjt_j_double_product_factor. pa_h_hjt_j_double_product_factor + S (pa_p_hjt_j_double_product) = S ((S (pa_i_hjt_j_double_product)) * pa_c_hjt_j_double)) /\ exists pa_q_hjt_j_double_product_factor. pa_b_hjt_j_double = pa_q_hjt_j_double_product_factor * S ((S (pa_i_hjt_j_double_product)) * pa_c_hjt_j_double) + (pa_p_hjt_j_double_product))) /\ ((((exists pa_h_hjt_j_double_product_partial. pa_h_hjt_j_double_product_partial + S (pa_r_hjt_j_double_product) = S ((S (pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_partial. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_partial * S ((S (pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product) + (pa_r_hjt_j_double_product))) /\ ((((exists pa_h_hjt_j_double_product_successor. pa_h_hjt_j_double_product_successor + S (pa_s_hjt_j_double_product) = S ((S (S pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product)) /\ exists pa_q_hjt_j_double_product_successor. pa_u_hjt_j_double_product = pa_q_hjt_j_double_product_successor * S ((S (S pa_i_hjt_j_double_product)) * pa_v_hjt_j_double_product) + (pa_s_hjt_j_double_product))) /\ pa_s_hjt_j_double_product = pa_r_hjt_j_double_product * pa_p_hjt_j_double_product))))))))
  16. 0016specialize htotal (2 * (s + 7))
  17. 0017specialize htotal 12
  18. 0018exact htotal
  19. 0019cases hdouble
  20. 0020have hjdouble : Le(jn,x)
    Exact native replay linehave hjdouble : exists bqb_le_gap_hjt_j_next_double. bqb_le_gap_hjt_j_next_double + (jn) = (x)
  21. 0021specialize pow_base_monotone (s + 13)
  22. 0022specialize pow_base_monotone (2 * (s + 7))
  23. 0023specialize pow_base_monotone 12
  24. 0024specialize pow_base_monotone jn
  25. 0025specialize pow_base_monotone x
  26. 0026apply pow_base_monotone
  27. 0027exact hbase
  28. 0028exact hjn
  29. 0029exact hdouble_witness
  30. 0030have htwo : ∃ jt. Pow(2,12,jt)
    Exact native replay linehave htwo : exists jt. (exists pa_b_hjt_j_two_factor pa_c_hjt_j_two_factor. ((forall pa_i_hjt_j_two_factor_repeat. (exists pa_lt_hjt_j_two_factor_repeat_bound. pa_lt_hjt_j_two_factor_repeat_bound + S pa_i_hjt_j_two_factor_repeat = 12) -> (((exists pa_h_hjt_j_two_factor_repeat_decoded. pa_h_hjt_j_two_factor_repeat_decoded + S (2) = S ((S (pa_i_hjt_j_two_factor_repeat)) * pa_c_hjt_j_two_factor)) /\ exists pa_q_hjt_j_two_factor_repeat_decoded. pa_b_hjt_j_two_factor = pa_q_hjt_j_two_factor_repeat_decoded * S ((S (pa_i_hjt_j_two_factor_repeat)) * pa_c_hjt_j_two_factor) + (2)))) /\ (exists pa_u_hjt_j_two_factor_product pa_v_hjt_j_two_factor_product. ((((exists pa_h_hjt_j_two_factor_product_start. pa_h_hjt_j_two_factor_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_start. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_start * S ((S (0)) * pa_v_hjt_j_two_factor_product) + (1))) /\ ((((exists pa_h_hjt_j_two_factor_product_terminal. pa_h_hjt_j_two_factor_product_terminal + S (jt) = S ((S (12)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_terminal. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_terminal * S ((S (12)) * pa_v_hjt_j_two_factor_product) + (jt))) /\ forall pa_i_hjt_j_two_factor_product. (exists pa_lt_hjt_j_two_factor_product_bound. pa_lt_hjt_j_two_factor_product_bound + S pa_i_hjt_j_two_factor_product = 12) -> exists pa_p_hjt_j_two_factor_product pa_r_hjt_j_two_factor_product pa_s_hjt_j_two_factor_product. ((((exists pa_h_hjt_j_two_factor_product_factor. pa_h_hjt_j_two_factor_product_factor + S (pa_p_hjt_j_two_factor_product) = S ((S (pa_i_hjt_j_two_factor_product)) * pa_c_hjt_j_two_factor)) /\ exists pa_q_hjt_j_two_factor_product_factor. pa_b_hjt_j_two_factor = pa_q_hjt_j_two_factor_product_factor * S ((S (pa_i_hjt_j_two_factor_product)) * pa_c_hjt_j_two_factor) + (pa_p_hjt_j_two_factor_product))) /\ ((((exists pa_h_hjt_j_two_factor_product_partial. pa_h_hjt_j_two_factor_product_partial + S (pa_r_hjt_j_two_factor_product) = S ((S (pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_partial. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_partial * S ((S (pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product) + (pa_r_hjt_j_two_factor_product))) /\ ((((exists pa_h_hjt_j_two_factor_product_successor. pa_h_hjt_j_two_factor_product_successor + S (pa_s_hjt_j_two_factor_product) = S ((S (S pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product)) /\ exists pa_q_hjt_j_two_factor_product_successor. pa_u_hjt_j_two_factor_product = pa_q_hjt_j_two_factor_product_successor * S ((S (S pa_i_hjt_j_two_factor_product)) * pa_v_hjt_j_two_factor_product) + (pa_s_hjt_j_two_factor_product))) /\ pa_s_hjt_j_two_factor_product = pa_r_hjt_j_two_factor_product * pa_p_hjt_j_two_factor_product))))))))
  31. 0031specialize htotal 2
  32. 0032specialize htotal 12
  33. 0033exact htotal
  34. 0034cases htwo
  35. 0035have hfour : ∃ jf. Pow(4,6,jf)
    Exact native replay linehave hfour : exists jf. (exists pa_b_hjt_j_four_factor pa_c_hjt_j_four_factor. ((forall pa_i_hjt_j_four_factor_repeat. (exists pa_lt_hjt_j_four_factor_repeat_bound. pa_lt_hjt_j_four_factor_repeat_bound + S pa_i_hjt_j_four_factor_repeat = 6) -> (((exists pa_h_hjt_j_four_factor_repeat_decoded. pa_h_hjt_j_four_factor_repeat_decoded + S (4) = S ((S (pa_i_hjt_j_four_factor_repeat)) * pa_c_hjt_j_four_factor)) /\ exists pa_q_hjt_j_four_factor_repeat_decoded. pa_b_hjt_j_four_factor = pa_q_hjt_j_four_factor_repeat_decoded * S ((S (pa_i_hjt_j_four_factor_repeat)) * pa_c_hjt_j_four_factor) + (4)))) /\ (exists pa_u_hjt_j_four_factor_product pa_v_hjt_j_four_factor_product. ((((exists pa_h_hjt_j_four_factor_product_start. pa_h_hjt_j_four_factor_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_start. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_start * S ((S (0)) * pa_v_hjt_j_four_factor_product) + (1))) /\ ((((exists pa_h_hjt_j_four_factor_product_terminal. pa_h_hjt_j_four_factor_product_terminal + S (jf) = S ((S (6)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_terminal. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_terminal * S ((S (6)) * pa_v_hjt_j_four_factor_product) + (jf))) /\ forall pa_i_hjt_j_four_factor_product. (exists pa_lt_hjt_j_four_factor_product_bound. pa_lt_hjt_j_four_factor_product_bound + S pa_i_hjt_j_four_factor_product = 6) -> exists pa_p_hjt_j_four_factor_product pa_r_hjt_j_four_factor_product pa_s_hjt_j_four_factor_product. ((((exists pa_h_hjt_j_four_factor_product_factor. pa_h_hjt_j_four_factor_product_factor + S (pa_p_hjt_j_four_factor_product) = S ((S (pa_i_hjt_j_four_factor_product)) * pa_c_hjt_j_four_factor)) /\ exists pa_q_hjt_j_four_factor_product_factor. pa_b_hjt_j_four_factor = pa_q_hjt_j_four_factor_product_factor * S ((S (pa_i_hjt_j_four_factor_product)) * pa_c_hjt_j_four_factor) + (pa_p_hjt_j_four_factor_product))) /\ ((((exists pa_h_hjt_j_four_factor_product_partial. pa_h_hjt_j_four_factor_product_partial + S (pa_r_hjt_j_four_factor_product) = S ((S (pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_partial. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_partial * S ((S (pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product) + (pa_r_hjt_j_four_factor_product))) /\ ((((exists pa_h_hjt_j_four_factor_product_successor. pa_h_hjt_j_four_factor_product_successor + S (pa_s_hjt_j_four_factor_product) = S ((S (S pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product)) /\ exists pa_q_hjt_j_four_factor_product_successor. pa_u_hjt_j_four_factor_product = pa_q_hjt_j_four_factor_product_successor * S ((S (S pa_i_hjt_j_four_factor_product)) * pa_v_hjt_j_four_factor_product) + (pa_s_hjt_j_four_factor_product))) /\ pa_s_hjt_j_four_factor_product = pa_r_hjt_j_four_factor_product * pa_p_hjt_j_four_factor_product))))))))
  36. 0036specialize htotal 4
  37. 0037specialize htotal 6
  38. 0038exact htotal
  39. 0039cases hfour
  40. 0040have hseeds : Pow(2,2,4) ∧ Pow(2,7,128)
    Exact native replay linehave hseeds : (exists pa_b_hjt_j_seed_two pa_c_hjt_j_seed_two. ((forall pa_i_hjt_j_seed_two_repeat. (exists pa_lt_hjt_j_seed_two_repeat_bound. pa_lt_hjt_j_seed_two_repeat_bound + S pa_i_hjt_j_seed_two_repeat = 2) -> (((exists pa_h_hjt_j_seed_two_repeat_decoded. pa_h_hjt_j_seed_two_repeat_decoded + S (2) = S ((S (pa_i_hjt_j_seed_two_repeat)) * pa_c_hjt_j_seed_two)) /\ exists pa_q_hjt_j_seed_two_repeat_decoded. pa_b_hjt_j_seed_two = pa_q_hjt_j_seed_two_repeat_decoded * S ((S (pa_i_hjt_j_seed_two_repeat)) * pa_c_hjt_j_seed_two) + (2)))) /\ (exists pa_u_hjt_j_seed_two_product pa_v_hjt_j_seed_two_product. ((((exists pa_h_hjt_j_seed_two_product_start. pa_h_hjt_j_seed_two_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_start. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_start * S ((S (0)) * pa_v_hjt_j_seed_two_product) + (1))) /\ ((((exists pa_h_hjt_j_seed_two_product_terminal. pa_h_hjt_j_seed_two_product_terminal + S (4) = S ((S (2)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_terminal. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_terminal * S ((S (2)) * pa_v_hjt_j_seed_two_product) + (4))) /\ forall pa_i_hjt_j_seed_two_product. (exists pa_lt_hjt_j_seed_two_product_bound. pa_lt_hjt_j_seed_two_product_bound + S pa_i_hjt_j_seed_two_product = 2) -> exists pa_p_hjt_j_seed_two_product pa_r_hjt_j_seed_two_product pa_s_hjt_j_seed_two_product. ((((exists pa_h_hjt_j_seed_two_product_factor. pa_h_hjt_j_seed_two_product_factor + S (pa_p_hjt_j_seed_two_product) = S ((S (pa_i_hjt_j_seed_two_product)) * pa_c_hjt_j_seed_two)) /\ exists pa_q_hjt_j_seed_two_product_factor. pa_b_hjt_j_seed_two = pa_q_hjt_j_seed_two_product_factor * S ((S (pa_i_hjt_j_seed_two_product)) * pa_c_hjt_j_seed_two) + (pa_p_hjt_j_seed_two_product))) /\ ((((exists pa_h_hjt_j_seed_two_product_partial. pa_h_hjt_j_seed_two_product_partial + S (pa_r_hjt_j_seed_two_product) = S ((S (pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_partial. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_partial * S ((S (pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product) + (pa_r_hjt_j_seed_two_product))) /\ ((((exists pa_h_hjt_j_seed_two_product_successor. pa_h_hjt_j_seed_two_product_successor + S (pa_s_hjt_j_seed_two_product) = S ((S (S pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product)) /\ exists pa_q_hjt_j_seed_two_product_successor. pa_u_hjt_j_seed_two_product = pa_q_hjt_j_seed_two_product_successor * S ((S (S pa_i_hjt_j_seed_two_product)) * pa_v_hjt_j_seed_two_product) + (pa_s_hjt_j_seed_two_product))) /\ pa_s_hjt_j_seed_two_product = pa_r_hjt_j_seed_two_product * pa_p_hjt_j_seed_two_product)))))))) /\ (exists pa_b_hjt_j_seed_seven pa_c_hjt_j_seed_seven. ((forall pa_i_hjt_j_seed_seven_repeat. (exists pa_lt_hjt_j_seed_seven_repeat_bound. pa_lt_hjt_j_seed_seven_repeat_bound + S pa_i_hjt_j_seed_seven_repeat = 7) -> (((exists pa_h_hjt_j_seed_seven_repeat_decoded. pa_h_hjt_j_seed_seven_repeat_decoded + S (2) = S ((S (pa_i_hjt_j_seed_seven_repeat)) * pa_c_hjt_j_seed_seven)) /\ exists pa_q_hjt_j_seed_seven_repeat_decoded. pa_b_hjt_j_seed_seven = pa_q_hjt_j_seed_seven_repeat_decoded * S ((S (pa_i_hjt_j_seed_seven_repeat)) * pa_c_hjt_j_seed_seven) + (2)))) /\ (exists pa_u_hjt_j_seed_seven_product pa_v_hjt_j_seed_seven_product. ((((exists pa_h_hjt_j_seed_seven_product_start. pa_h_hjt_j_seed_seven_product_start + S (1) = S ((S (0)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_start. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_start * S ((S (0)) * pa_v_hjt_j_seed_seven_product) + (1))) /\ ((((exists pa_h_hjt_j_seed_seven_product_terminal. pa_h_hjt_j_seed_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_terminal. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_terminal * S ((S (7)) * pa_v_hjt_j_seed_seven_product) + (128))) /\ forall pa_i_hjt_j_seed_seven_product. (exists pa_lt_hjt_j_seed_seven_product_bound. pa_lt_hjt_j_seed_seven_product_bound + S pa_i_hjt_j_seed_seven_product = 7) -> exists pa_p_hjt_j_seed_seven_product pa_r_hjt_j_seed_seven_product pa_s_hjt_j_seed_seven_product. ((((exists pa_h_hjt_j_seed_seven_product_factor. pa_h_hjt_j_seed_seven_product_factor + S (pa_p_hjt_j_seed_seven_product) = S ((S (pa_i_hjt_j_seed_seven_product)) * pa_c_hjt_j_seed_seven)) /\ exists pa_q_hjt_j_seed_seven_product_factor. pa_b_hjt_j_seed_seven = pa_q_hjt_j_seed_seven_product_factor * S ((S (pa_i_hjt_j_seed_seven_product)) * pa_c_hjt_j_seed_seven) + (pa_p_hjt_j_seed_seven_product))) /\ ((((exists pa_h_hjt_j_seed_seven_product_partial. pa_h_hjt_j_seed_seven_product_partial + S (pa_r_hjt_j_seed_seven_product) = S ((S (pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_partial. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_partial * S ((S (pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product) + (pa_r_hjt_j_seed_seven_product))) /\ ((((exists pa_h_hjt_j_seed_seven_product_successor. pa_h_hjt_j_seed_seven_product_successor + S (pa_s_hjt_j_seed_seven_product) = S ((S (S pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product)) /\ exists pa_q_hjt_j_seed_seven_product_successor. pa_u_hjt_j_seed_seven_product = pa_q_hjt_j_seed_seven_product_successor * S ((S (S pa_i_hjt_j_seed_seven_product)) * pa_v_hjt_j_seed_seven_product) + (pa_s_hjt_j_seed_seven_product))) /\ pa_s_hjt_j_seed_seven_product = pa_r_hjt_j_seed_seven_product * pa_p_hjt_j_seed_seven_product))))))))
  41. 0041apply pow_two_seed_bundle_from_total
  42. 0042exact htotal
  43. 0043cases hseeds
  44. 0044have htwo_four : x1 = x2
  45. 0045specialize pow_mul_exp_from_total 2
  46. 0046specialize pow_mul_exp_from_total 2
  47. 0047specialize pow_mul_exp_from_total 6
  48. 0048specialize pow_mul_exp_from_total 12
  49. 0049specialize pow_mul_exp_from_total 4
  50. 0050specialize pow_mul_exp_from_total x2
  51. 0051specialize pow_mul_exp_from_total x1
  52. 0052symm
  53. 0053apply pow_mul_exp_from_total
  54. 0054exact htotal
  55. 0055norm_num
  56. 0056exact hseeds_left
  57. 0057exact hfour_witness
  58. 0058exact htwo_witness
  59. 0059have hdouble_factor : x = x1 * j
  60. 0060specialize pow_mul_base 2
  61. 0061specialize pow_mul_base (s + 7)
  62. 0062specialize pow_mul_base 12
  63. 0063specialize pow_mul_base x1
  64. 0064specialize pow_mul_base j
  65. 0065specialize pow_mul_base x
  66. 0066apply pow_mul_base
  67. 0067exact htwo_witness
  68. 0068exact hj
  69. 0069exact hdouble_witness
  70. 0070have hsum : s + 11 = 6 + (s + 5)
  71. 0071trans s + (6 + 5)
  72. 0072congr
  73. 0073refl
  74. 0074norm_num
  75. 0075trans (s + 6) + 5
  76. 0076symm
  77. 0077apply add_assoc
  78. 0078trans (6 + s) + 5
  79. 0079congr
  80. 0080apply add_comm
  81. 0081refl
  82. 0082apply add_assoc
  83. 0083have hbound_factor : gn = x2 * g
  84. 0084specialize pow_add 4
  85. 0085specialize pow_add 6
  86. 0086specialize pow_add (s + 5)
  87. 0087specialize pow_add (s + 11)
  88. 0088specialize pow_add x2
  89. 0089specialize pow_add g
  90. 0090specialize pow_add gn
  91. 0091apply pow_add
  92. 0092exact hsum
  93. 0093exact hfour_witness
  94. 0094exact hg
  95. 0095exact hgn
  96. 0096have hproducts : Le(x1 · j,x2 · g)
    Exact native replay linehave hproducts : exists bqb_le_gap_hjt_j_products. bqb_le_gap_hjt_j_products + (x1 * j) = (x2 * g)
  97. 0097rewrite htwo_four
  98. 0098specialize mul_le_mul x2
  99. 0099specialize mul_le_mul x2
  100. 0100specialize mul_le_mul j
  101. 0101specialize mul_le_mul g
  102. 0102apply mul_le_mul
  103. 0103specialize le_refl x2
  104. 0104exact le_refl
  105. 0105exact hjg
  106. 0106specialize le_trans jn
  107. 0107specialize le_trans x
  108. 0108specialize le_trans gn
  109. 0109apply le_trans
  110. 0110exact hjdouble
  111. 0111rewrite hdouble_factor
  112. 0112rewrite hbound_factor
  113. 0113exact hproducts