EL000E

euclidean_log_trace_bound

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every genuine BitLen witness constructively bounds an actual complete Euclidean beta history by twice its length.

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 first-order arithmetic statement

forall a b l. ((((b) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_elb_length ff_lower_bl_elb_length ff_upper_bl_elb_length. (((l) = S ff_exponent_bl_elb_length) /\ ((exists ff_positive_bl_elb_length. ff_positive_bl_elb_length + 1 = (b)) /\ ((exists pa_b_bl_elb_length_lower pa_c_bl_elb_length_lower. ((forall pa_i_bl_elb_length_lower_repeat. (exists pa_lt_bl_elb_length_lower_repeat_bound. pa_lt_bl_elb_length_lower_repeat_bound + S pa_i_bl_elb_length_lower_repeat = ff_exponent_bl_elb_length) -> (((exists pa_h_bl_elb_length_lower_repeat_decoded. pa_h_bl_elb_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_repeat_decoded. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_repeat_decoded * S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower) + (2)))) /\ (exists pa_u_bl_elb_length_lower_product pa_v_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_start. pa_h_bl_elb_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_start. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_start * S ((S (0)) * pa_v_bl_elb_length_lower_product) + (1))) /\ ((((exists pa_h_bl_elb_length_lower_product_terminal. pa_h_bl_elb_length_lower_product_terminal + S (ff_lower_bl_elb_length) = S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_terminal. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_terminal * S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product) + (ff_lower_bl_elb_length))) /\ forall pa_i_bl_elb_length_lower_product. (exists pa_lt_bl_elb_length_lower_product_bound. pa_lt_bl_elb_length_lower_product_bound + S pa_i_bl_elb_length_lower_product = ff_exponent_bl_elb_length) -> exists pa_p_bl_elb_length_lower_product pa_r_bl_elb_length_lower_product pa_s_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_factor. pa_h_bl_elb_length_lower_product_factor + S (pa_p_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_product_factor. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_product_factor * S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower) + (pa_p_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_partial. pa_h_bl_elb_length_lower_product_partial + S (pa_r_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_partial. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_partial * S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_r_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_successor. pa_h_bl_elb_length_lower_product_successor + S (pa_s_bl_elb_length_lower_product) = S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_successor. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_successor * S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_s_bl_elb_length_lower_product))) /\ pa_s_bl_elb_length_lower_product = pa_r_bl_elb_length_lower_product * pa_p_bl_elb_length_lower_product)))))))) /\ ((exists pa_b_bl_elb_length_upper pa_c_bl_elb_length_upper. ((forall pa_i_bl_elb_length_upper_repeat. (exists pa_lt_bl_elb_length_upper_repeat_bound. pa_lt_bl_elb_length_upper_repeat_bound + S pa_i_bl_elb_length_upper_repeat = l) -> (((exists pa_h_bl_elb_length_upper_repeat_decoded. pa_h_bl_elb_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_repeat_decoded. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_repeat_decoded * S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper) + (2)))) /\ (exists pa_u_bl_elb_length_upper_product pa_v_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_start. pa_h_bl_elb_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_start. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_start * S ((S (0)) * pa_v_bl_elb_length_upper_product) + (1))) /\ ((((exists pa_h_bl_elb_length_upper_product_terminal. pa_h_bl_elb_length_upper_product_terminal + S (ff_upper_bl_elb_length) = S ((S (l)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_terminal. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_terminal * S ((S (l)) * pa_v_bl_elb_length_upper_product) + (ff_upper_bl_elb_length))) /\ forall pa_i_bl_elb_length_upper_product. (exists pa_lt_bl_elb_length_upper_product_bound. pa_lt_bl_elb_length_upper_product_bound + S pa_i_bl_elb_length_upper_product = l) -> exists pa_p_bl_elb_length_upper_product pa_r_bl_elb_length_upper_product pa_s_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_factor. pa_h_bl_elb_length_upper_product_factor + S (pa_p_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_product_factor. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_product_factor * S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper) + (pa_p_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_partial. pa_h_bl_elb_length_upper_product_partial + S (pa_r_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_partial. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_partial * S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_r_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_successor. pa_h_bl_elb_length_upper_product_successor + S (pa_s_bl_elb_length_upper_product) = S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_successor. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_successor * S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_s_bl_elb_length_upper_product))) /\ pa_s_bl_elb_length_upper_product = pa_r_bl_elb_length_upper_product * pa_p_bl_elb_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_elb_length. ff_lower_gap_bl_elb_length + (ff_lower_bl_elb_length) = (b)) /\ (exists ff_upper_gap_bl_elb_length. ff_upper_gap_bl_elb_length + S (b) = (ff_upper_bl_elb_length))))))))) -> (exists elb_list_length_budget elb_history_length_budget elb_scale_length_budget elb_steps_length_budget. ((exists cf_gcd_elb_length_budget_budget. ((((exists ff_h_cf_elb_length_budget_budget_initial_state. ff_h_cf_elb_length_budget_budget_initial_state + S (((cf_gcd_elb_length_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_initial_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_initial_state * S ((S (0)) * elb_scale_length_budget) + (((cf_gcd_elb_length_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_budget_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_length_budget_budget_terminal_state. ff_h_cf_elb_length_budget_budget_terminal_state + S (((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) * S ((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) + ((((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))))) = S ((S (elb_steps_length_budget)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_terminal_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_terminal_state * S ((S (elb_steps_length_budget)) * elb_scale_length_budget) + (((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) * S ((a) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget)))) + ((((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))) + (((b) + (elb_list_length_budget)) * S ((b) + (elb_list_length_budget)) + ((elb_list_length_budget) + (elb_list_length_budget))))))) /\ forall cf_index_elb_length_budget_budget. (exists ff_lt_cf_elb_length_budget_budget_index. ff_lt_cf_elb_length_budget_budget_index + S cf_index_elb_length_budget_budget = elb_steps_length_budget) -> exists cf_old_a_elb_length_budget_budget cf_old_b_elb_length_budget_budget cf_tail_elb_length_budget_budget cf_new_a_elb_length_budget_budget cf_new_b_elb_length_budget_budget cf_head_elb_length_budget_budget cf_quotient_elb_length_budget_budget. ((((exists ff_h_cf_elb_length_budget_budget_previous_state. ff_h_cf_elb_length_budget_budget_previous_state + S (((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) * S ((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) + ((((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))))) = S ((S (cf_index_elb_length_budget_budget)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_previous_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_previous_state * S ((S (cf_index_elb_length_budget_budget)) * elb_scale_length_budget) + (((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) * S ((cf_old_a_elb_length_budget_budget) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)))) + ((((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))) + (((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) * S ((cf_old_b_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget)) + ((cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget))))))) /\ ((((exists ff_h_cf_elb_length_budget_budget_following_state. ff_h_cf_elb_length_budget_budget_following_state + S (((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) * S ((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) + ((((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))))) = S ((S (S cf_index_elb_length_budget_budget)) * elb_scale_length_budget)) /\ exists ff_q_cf_elb_length_budget_budget_following_state. elb_history_length_budget = ff_q_cf_elb_length_budget_budget_following_state * S ((S (S cf_index_elb_length_budget_budget)) * elb_scale_length_budget) + (((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) * S ((cf_new_a_elb_length_budget_budget) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)))) + ((((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))) + (((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) * S ((cf_new_b_elb_length_budget_budget) + (cf_head_elb_length_budget_budget)) + ((cf_head_elb_length_budget_budget) + (cf_head_elb_length_budget_budget))))))) /\ (cf_new_b_elb_length_budget_budget = cf_old_a_elb_length_budget_budget /\ (cf_new_a_elb_length_budget_budget = cf_new_b_elb_length_budget_budget * cf_quotient_elb_length_budget_budget + cf_old_b_elb_length_budget_budget /\ ((exists ff_lt_cf_elb_length_budget_budget_remainder. ff_lt_cf_elb_length_budget_budget_remainder + S cf_old_b_elb_length_budget_budget = cf_new_b_elb_length_budget_budget) /\ (cf_head_elb_length_budget_budget = S ((cf_quotient_elb_length_budget_budget + cf_tail_elb_length_budget_budget) * S (cf_quotient_elb_length_budget_budget + cf_tail_elb_length_budget_budget) + (cf_tail_elb_length_budget_budget + cf_tail_elb_length_budget_budget))))))))))) /\ exists elb_gap_length_budget. elb_gap_length_budget + elb_steps_length_budget = ((l + l))))

Constructive proof overview

Generated structural guide

Every genuine BitLen witness constructively bounds an actual complete Euclidean beta history by twice its length.

The unchanged tactic script uses 2 declared prerequisites and contains 22 exact native proof lines.

Alpha v34 checked-use · first admitted v23 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

EL000D euclidean_log_binary_length_upper_power EL000C euclidean_log_trace_below_power

Direct dependents

EL000F euclidean_log_execution_strong

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

22 script commands · 7 reading checkpoints · 3 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)
euclidean log binary length upper powereuclidean log trace below power

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–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro l
  4. L4
    intro hlength
02Use earlier factsL5–6

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

  1. L5
    specialize euclidean_log_binary_length_upper_power b
  2. L6
    specialize euclidean_log_binary_length_upper_power l
03Establish hupperL7–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log binary length upper power.

  1. L7
    have hupper : ∃ p. PowTwo(l,p) ∧ Lt(b,p)Definitions: PowTwoLt
  2. L8
    apply euclidean_log_binary_length_upper_power
  3. L9
    exact hlength
04Separate the logical casesL10–11

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

  1. L10
    cases hupper
  2. L11
    cases hupper_witness
05Use earlier factsL12–13

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

  1. L12
    specialize euclidean_log_trace_below_power l
  2. L13
    specialize euclidean_log_trace_below_power x
06Establish hdivisorL14–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean log trace below power.

  1. L14
    have hdivisor : ∀ b. Lt(b,x) → ∀ y. EuclideanBoundedTrace(y,b,l + l)Definitions: EuclideanBoundedTraceLt
  2. L15
    apply euclidean_log_trace_below_power
  3. L16
    exact hupper_witness_left
  4. L17
    specialize hdivisor b
07Establish hallL18–22

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

  1. L18
    have hall : ∀ z. EuclideanBoundedTrace(z,b,l + l)Definitions: EuclideanBoundedTrace
  2. L19
    apply hdivisor
  3. L20
    exact hupper_witness_right
  4. L21
    specialize hall a
  5. L22
    exact hall

Library-wide reading audit

Original exact command ledger · 22 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro l
  4. 0004intro hlength
  5. 0005specialize euclidean_log_binary_length_upper_power b
  6. 0006specialize euclidean_log_binary_length_upper_power l
  7. 0007have hupper : exists p. ((exists pa_b_bl_elb_length_upper pa_c_bl_elb_length_upper. ((forall pa_i_bl_elb_length_upper_repeat. (exists pa_lt_bl_elb_length_upper_repeat_bound. pa_lt_bl_elb_length_upper_repeat_bound + S pa_i_bl_elb_length_upper_repeat = l) -> (((exists pa_h_bl_elb_length_upper_repeat_decoded. pa_h_bl_elb_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_repeat_decoded. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_repeat_decoded * S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper) + (2)))) /\ (exists pa_u_bl_elb_length_upper_product pa_v_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_start. pa_h_bl_elb_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_start. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_start * S ((S (0)) * pa_v_bl_elb_length_upper_product) + (1))) /\ ((((exists pa_h_bl_elb_length_upper_product_terminal. pa_h_bl_elb_length_upper_product_terminal + S (p) = S ((S (l)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_terminal. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_terminal * S ((S (l)) * pa_v_bl_elb_length_upper_product) + (p))) /\ forall pa_i_bl_elb_length_upper_product. (exists pa_lt_bl_elb_length_upper_product_bound. pa_lt_bl_elb_length_upper_product_bound + S pa_i_bl_elb_length_upper_product = l) -> exists pa_p_bl_elb_length_upper_product pa_r_bl_elb_length_upper_product pa_s_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_factor. pa_h_bl_elb_length_upper_product_factor + S (pa_p_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_product_factor. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_product_factor * S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper) + (pa_p_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_partial. pa_h_bl_elb_length_upper_product_partial + S (pa_r_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_partial. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_partial * S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_r_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_successor. pa_h_bl_elb_length_upper_product_successor + S (pa_s_bl_elb_length_upper_product) = S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_successor. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_successor * S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_s_bl_elb_length_upper_product))) /\ pa_s_bl_elb_length_upper_product = pa_r_bl_elb_length_upper_product * pa_p_bl_elb_length_upper_product)))))))) /\ (exists ff_lt_elb_length_upper. ff_lt_elb_length_upper + S b = p))
  8. 0008apply euclidean_log_binary_length_upper_power
  9. 0009exact hlength
  10. 0010cases hupper
  11. 0011cases hupper_witness
  12. 0012specialize euclidean_log_trace_below_power l
  13. 0013specialize euclidean_log_trace_below_power x
  14. 0014have hdivisor : forall b. (exists gap. gap + S b = x) -> forall a. (exists elb_list_length_divisor elb_history_length_divisor elb_scale_length_divisor elb_steps_length_divisor. ((exists cf_gcd_elb_length_divisor_budget. ((((exists ff_h_cf_elb_length_divisor_budget_initial_state. ff_h_cf_elb_length_divisor_budget_initial_state + S (((cf_gcd_elb_length_divisor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_divisor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_length_divisor)) /\ exists ff_q_cf_elb_length_divisor_budget_initial_state. elb_history_length_divisor = ff_q_cf_elb_length_divisor_budget_initial_state * S ((S (0)) * elb_scale_length_divisor) + (((cf_gcd_elb_length_divisor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_divisor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_length_divisor_budget_terminal_state. ff_h_cf_elb_length_divisor_budget_terminal_state + S (((a) + (((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor)))) * S ((a) + (((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor)))) + ((((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor))) + (((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor))))) = S ((S (elb_steps_length_divisor)) * elb_scale_length_divisor)) /\ exists ff_q_cf_elb_length_divisor_budget_terminal_state. elb_history_length_divisor = ff_q_cf_elb_length_divisor_budget_terminal_state * S ((S (elb_steps_length_divisor)) * elb_scale_length_divisor) + (((a) + (((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor)))) * S ((a) + (((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor)))) + ((((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor))) + (((b) + (elb_list_length_divisor)) * S ((b) + (elb_list_length_divisor)) + ((elb_list_length_divisor) + (elb_list_length_divisor))))))) /\ forall cf_index_elb_length_divisor_budget. (exists ff_lt_cf_elb_length_divisor_budget_index. ff_lt_cf_elb_length_divisor_budget_index + S cf_index_elb_length_divisor_budget = elb_steps_length_divisor) -> exists cf_old_a_elb_length_divisor_budget cf_old_b_elb_length_divisor_budget cf_tail_elb_length_divisor_budget cf_new_a_elb_length_divisor_budget cf_new_b_elb_length_divisor_budget cf_head_elb_length_divisor_budget cf_quotient_elb_length_divisor_budget. ((((exists ff_h_cf_elb_length_divisor_budget_previous_state. ff_h_cf_elb_length_divisor_budget_previous_state + S (((cf_old_a_elb_length_divisor_budget) + (((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)))) * S ((cf_old_a_elb_length_divisor_budget) + (((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)))) + ((((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget))) + (((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget))))) = S ((S (cf_index_elb_length_divisor_budget)) * elb_scale_length_divisor)) /\ exists ff_q_cf_elb_length_divisor_budget_previous_state. elb_history_length_divisor = ff_q_cf_elb_length_divisor_budget_previous_state * S ((S (cf_index_elb_length_divisor_budget)) * elb_scale_length_divisor) + (((cf_old_a_elb_length_divisor_budget) + (((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)))) * S ((cf_old_a_elb_length_divisor_budget) + (((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)))) + ((((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget))) + (((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) * S ((cf_old_b_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget)) + ((cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget))))))) /\ ((((exists ff_h_cf_elb_length_divisor_budget_following_state. ff_h_cf_elb_length_divisor_budget_following_state + S (((cf_new_a_elb_length_divisor_budget) + (((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)))) * S ((cf_new_a_elb_length_divisor_budget) + (((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)))) + ((((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget))) + (((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget))))) = S ((S (S cf_index_elb_length_divisor_budget)) * elb_scale_length_divisor)) /\ exists ff_q_cf_elb_length_divisor_budget_following_state. elb_history_length_divisor = ff_q_cf_elb_length_divisor_budget_following_state * S ((S (S cf_index_elb_length_divisor_budget)) * elb_scale_length_divisor) + (((cf_new_a_elb_length_divisor_budget) + (((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)))) * S ((cf_new_a_elb_length_divisor_budget) + (((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)))) + ((((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget))) + (((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) * S ((cf_new_b_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget)) + ((cf_head_elb_length_divisor_budget) + (cf_head_elb_length_divisor_budget))))))) /\ (cf_new_b_elb_length_divisor_budget = cf_old_a_elb_length_divisor_budget /\ (cf_new_a_elb_length_divisor_budget = cf_new_b_elb_length_divisor_budget * cf_quotient_elb_length_divisor_budget + cf_old_b_elb_length_divisor_budget /\ ((exists ff_lt_cf_elb_length_divisor_budget_remainder. ff_lt_cf_elb_length_divisor_budget_remainder + S cf_old_b_elb_length_divisor_budget = cf_new_b_elb_length_divisor_budget) /\ (cf_head_elb_length_divisor_budget = S ((cf_quotient_elb_length_divisor_budget + cf_tail_elb_length_divisor_budget) * S (cf_quotient_elb_length_divisor_budget + cf_tail_elb_length_divisor_budget) + (cf_tail_elb_length_divisor_budget + cf_tail_elb_length_divisor_budget))))))))))) /\ exists elb_gap_length_divisor. elb_gap_length_divisor + elb_steps_length_divisor = ((l + l))))
  15. 0015apply euclidean_log_trace_below_power
  16. 0016exact hupper_witness_left
  17. 0017specialize hdivisor b
  18. 0018have hall : forall z. (exists elb_list_length_all elb_history_length_all elb_scale_length_all elb_steps_length_all. ((exists cf_gcd_elb_length_all_budget. ((((exists ff_h_cf_elb_length_all_budget_initial_state. ff_h_cf_elb_length_all_budget_initial_state + S (((cf_gcd_elb_length_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_length_all)) /\ exists ff_q_cf_elb_length_all_budget_initial_state. elb_history_length_all = ff_q_cf_elb_length_all_budget_initial_state * S ((S (0)) * elb_scale_length_all) + (((cf_gcd_elb_length_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_length_all_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_length_all_budget_terminal_state. ff_h_cf_elb_length_all_budget_terminal_state + S (((z) + (((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all)))) * S ((z) + (((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all)))) + ((((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all))) + (((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all))))) = S ((S (elb_steps_length_all)) * elb_scale_length_all)) /\ exists ff_q_cf_elb_length_all_budget_terminal_state. elb_history_length_all = ff_q_cf_elb_length_all_budget_terminal_state * S ((S (elb_steps_length_all)) * elb_scale_length_all) + (((z) + (((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all)))) * S ((z) + (((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all)))) + ((((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all))) + (((b) + (elb_list_length_all)) * S ((b) + (elb_list_length_all)) + ((elb_list_length_all) + (elb_list_length_all))))))) /\ forall cf_index_elb_length_all_budget. (exists ff_lt_cf_elb_length_all_budget_index. ff_lt_cf_elb_length_all_budget_index + S cf_index_elb_length_all_budget = elb_steps_length_all) -> exists cf_old_a_elb_length_all_budget cf_old_b_elb_length_all_budget cf_tail_elb_length_all_budget cf_new_a_elb_length_all_budget cf_new_b_elb_length_all_budget cf_head_elb_length_all_budget cf_quotient_elb_length_all_budget. ((((exists ff_h_cf_elb_length_all_budget_previous_state. ff_h_cf_elb_length_all_budget_previous_state + S (((cf_old_a_elb_length_all_budget) + (((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget)))) * S ((cf_old_a_elb_length_all_budget) + (((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget)))) + ((((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget))) + (((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget))))) = S ((S (cf_index_elb_length_all_budget)) * elb_scale_length_all)) /\ exists ff_q_cf_elb_length_all_budget_previous_state. elb_history_length_all = ff_q_cf_elb_length_all_budget_previous_state * S ((S (cf_index_elb_length_all_budget)) * elb_scale_length_all) + (((cf_old_a_elb_length_all_budget) + (((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget)))) * S ((cf_old_a_elb_length_all_budget) + (((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget)))) + ((((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget))) + (((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) * S ((cf_old_b_elb_length_all_budget) + (cf_tail_elb_length_all_budget)) + ((cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget))))))) /\ ((((exists ff_h_cf_elb_length_all_budget_following_state. ff_h_cf_elb_length_all_budget_following_state + S (((cf_new_a_elb_length_all_budget) + (((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget)))) * S ((cf_new_a_elb_length_all_budget) + (((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget)))) + ((((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget))) + (((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget))))) = S ((S (S cf_index_elb_length_all_budget)) * elb_scale_length_all)) /\ exists ff_q_cf_elb_length_all_budget_following_state. elb_history_length_all = ff_q_cf_elb_length_all_budget_following_state * S ((S (S cf_index_elb_length_all_budget)) * elb_scale_length_all) + (((cf_new_a_elb_length_all_budget) + (((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget)))) * S ((cf_new_a_elb_length_all_budget) + (((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget)))) + ((((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget))) + (((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) * S ((cf_new_b_elb_length_all_budget) + (cf_head_elb_length_all_budget)) + ((cf_head_elb_length_all_budget) + (cf_head_elb_length_all_budget))))))) /\ (cf_new_b_elb_length_all_budget = cf_old_a_elb_length_all_budget /\ (cf_new_a_elb_length_all_budget = cf_new_b_elb_length_all_budget * cf_quotient_elb_length_all_budget + cf_old_b_elb_length_all_budget /\ ((exists ff_lt_cf_elb_length_all_budget_remainder. ff_lt_cf_elb_length_all_budget_remainder + S cf_old_b_elb_length_all_budget = cf_new_b_elb_length_all_budget) /\ (cf_head_elb_length_all_budget = S ((cf_quotient_elb_length_all_budget + cf_tail_elb_length_all_budget) * S (cf_quotient_elb_length_all_budget + cf_tail_elb_length_all_budget) + (cf_tail_elb_length_all_budget + cf_tail_elb_length_all_budget))))))))))) /\ exists elb_gap_length_all. elb_gap_length_all + elb_steps_length_all = ((l + l))))
  19. 0019apply hdivisor
  20. 0020exact hupper_witness_right
  21. 0021specialize hall a
  22. 0022exact hall

Separate complete second-wave branches: Full T13 proof · Alpha v27.