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 n. exists l b c. ((((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_total_canonical_length ff_lower_bl_bd_total_canonical_length ff_upper_bl_bd_total_canonical_length. (((l) = S ff_exponent_bl_bd_total_canonical_length) /\ ((exists ff_positive_bl_bd_total_canonical_length. ff_positive_bl_bd_total_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_total_canonical_length_lower pa_c_bl_bd_total_canonical_length_lower. ((forall pa_i_bl_bd_total_canonical_length_lower_repeat. (exists pa_lt_bl_bd_total_canonical_length_lower_repeat_bound. pa_lt_bl_bd_total_canonical_length_lower_repeat_bound + S pa_i_bl_bd_total_canonical_length_lower_repeat = ff_exponent_bl_bd_total_canonical_length) -> (((exists pa_h_bl_bd_total_canonical_length_lower_repeat_decoded. pa_h_bl_bd_total_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_canonical_length_lower_repeat)) * pa_c_bl_bd_total_canonical_length_lower)) /\ exists pa_q_bl_bd_total_canonical_length_lower_repeat_decoded. pa_b_bl_bd_total_canonical_length_lower = pa_q_bl_bd_total_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_total_canonical_length_lower_repeat)) * pa_c_bl_bd_total_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_total_canonical_length_lower_product pa_v_bl_bd_total_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_canonical_length_lower_product_start. pa_h_bl_bd_total_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_start. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_total_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_total_canonical_length_lower_product_terminal. pa_h_bl_bd_total_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_total_canonical_length) = S ((S (ff_exponent_bl_bd_total_canonical_length)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_terminal. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_total_canonical_length)) * pa_v_bl_bd_total_canonical_length_lower_product) + (ff_lower_bl_bd_total_canonical_length))) /\ forall pa_i_bl_bd_total_canonical_length_lower_product. (exists pa_lt_bl_bd_total_canonical_length_lower_product_bound. pa_lt_bl_bd_total_canonical_length_lower_product_bound + S pa_i_bl_bd_total_canonical_length_lower_product = ff_exponent_bl_bd_total_canonical_length) -> exists pa_p_bl_bd_total_canonical_length_lower_product pa_r_bl_bd_total_canonical_length_lower_product pa_s_bl_bd_total_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_canonical_length_lower_product_factor. pa_h_bl_bd_total_canonical_length_lower_product_factor + S (pa_p_bl_bd_total_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_c_bl_bd_total_canonical_length_lower)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_factor. pa_b_bl_bd_total_canonical_length_lower = pa_q_bl_bd_total_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_c_bl_bd_total_canonical_length_lower) + (pa_p_bl_bd_total_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_lower_product_partial. pa_h_bl_bd_total_canonical_length_lower_product_partial + S (pa_r_bl_bd_total_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_partial. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product) + (pa_r_bl_bd_total_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_lower_product_successor. pa_h_bl_bd_total_canonical_length_lower_product_successor + S (pa_s_bl_bd_total_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_successor. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product) + (pa_s_bl_bd_total_canonical_length_lower_product))) /\ pa_s_bl_bd_total_canonical_length_lower_product = pa_r_bl_bd_total_canonical_length_lower_product * pa_p_bl_bd_total_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_total_canonical_length_upper pa_c_bl_bd_total_canonical_length_upper. ((forall pa_i_bl_bd_total_canonical_length_upper_repeat. (exists pa_lt_bl_bd_total_canonical_length_upper_repeat_bound. pa_lt_bl_bd_total_canonical_length_upper_repeat_bound + S pa_i_bl_bd_total_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_total_canonical_length_upper_repeat_decoded. pa_h_bl_bd_total_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_canonical_length_upper_repeat)) * pa_c_bl_bd_total_canonical_length_upper)) /\ exists pa_q_bl_bd_total_canonical_length_upper_repeat_decoded. pa_b_bl_bd_total_canonical_length_upper = pa_q_bl_bd_total_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_total_canonical_length_upper_repeat)) * pa_c_bl_bd_total_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_total_canonical_length_upper_product pa_v_bl_bd_total_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_canonical_length_upper_product_start. pa_h_bl_bd_total_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_start. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_total_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_total_canonical_length_upper_product_terminal. pa_h_bl_bd_total_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_total_canonical_length) = S ((S (l)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_terminal. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_total_canonical_length_upper_product) + (ff_upper_bl_bd_total_canonical_length))) /\ forall pa_i_bl_bd_total_canonical_length_upper_product. (exists pa_lt_bl_bd_total_canonical_length_upper_product_bound. pa_lt_bl_bd_total_canonical_length_upper_product_bound + S pa_i_bl_bd_total_canonical_length_upper_product = l) -> exists pa_p_bl_bd_total_canonical_length_upper_product pa_r_bl_bd_total_canonical_length_upper_product pa_s_bl_bd_total_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_canonical_length_upper_product_factor. pa_h_bl_bd_total_canonical_length_upper_product_factor + S (pa_p_bl_bd_total_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_c_bl_bd_total_canonical_length_upper)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_factor. pa_b_bl_bd_total_canonical_length_upper = pa_q_bl_bd_total_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_c_bl_bd_total_canonical_length_upper) + (pa_p_bl_bd_total_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_upper_product_partial. pa_h_bl_bd_total_canonical_length_upper_product_partial + S (pa_r_bl_bd_total_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_partial. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product) + (pa_r_bl_bd_total_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_upper_product_successor. pa_h_bl_bd_total_canonical_length_upper_product_successor + S (pa_s_bl_bd_total_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_successor. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product) + (pa_s_bl_bd_total_canonical_length_upper_product))) /\ pa_s_bl_bd_total_canonical_length_upper_product = pa_r_bl_bd_total_canonical_length_upper_product * pa_p_bl_bd_total_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_total_canonical_length. ff_lower_gap_bl_bd_total_canonical_length + (ff_lower_bl_bd_total_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_total_canonical_length. ff_upper_gap_bl_bd_total_canonical_length + S (n) = (ff_upper_bl_bd_total_canonical_length))))))))) /\ (((forall ff_index_be_bd_total_canonical_code_digits ff_digit_be_bd_total_canonical_code_digits. (exists ff_lt_be_bd_total_canonical_code_digits_bound. ff_lt_be_bd_total_canonical_code_digits_bound + S ff_index_be_bd_total_canonical_code_digits = l) -> (((exists ff_h_be_bd_total_canonical_code_digits_digit. ff_h_be_bd_total_canonical_code_digits_digit + S (ff_digit_be_bd_total_canonical_code_digits) = S ((S (ff_index_be_bd_total_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_total_canonical_code_digits_digit. b = ff_q_be_bd_total_canonical_code_digits_digit * S ((S (ff_index_be_bd_total_canonical_code_digits)) * c) + (ff_digit_be_bd_total_canonical_code_digits))) -> (ff_digit_be_bd_total_canonical_code_digits = 0 \/ ff_digit_be_bd_total_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_total_canonical_code_horner ff_v_ph_bd_total_canonical_code_horner. ((((exists fs_h_ph_bd_total_canonical_code_horner_body_start. fs_h_ph_bd_total_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_start. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_total_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_total_canonical_code_horner_body_terminal. fs_h_ph_bd_total_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_terminal. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_total_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_total_canonical_code_horner_body_steps. (exists ph_bound_bd_total_canonical_code_horner_body_steps. ph_bound_bd_total_canonical_code_horner_body_steps + S ff_i_ph_bd_total_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_total_canonical_code_horner_body_steps ff_previous_ph_bd_total_canonical_code_horner_body_steps ff_current_ph_bd_total_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_total_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_total_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_total_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_total_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_total_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_canonical_code_horner_body_steps_before. fs_h_ph_bd_total_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_total_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_steps_before. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner) + (ff_previous_ph_bd_total_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_canonical_code_horner_body_steps_after. fs_h_ph_bd_total_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_total_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_steps_after. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner) + (ff_current_ph_bd_total_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_total_canonical_code_horner_body_steps = ff_previous_ph_bd_total_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_total_canonical_code_horner_body_steps))))))))))Constructive proof overview
Generated structural guide
Every arbitrary natural exponent has an actual canonical-length beta-coded binary digit prefix with exactly that exponent as its Horner value.
The unchanged tactic script uses 2 declared prerequisites and contains 18 exact native proof lines.
Alpha v34 checked-use · first admitted v23 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
binary_length_exists Alpha theorem; checked-use authorized BD0009 binary_exponent_digit_prefix_at_lengthDirect dependents
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
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 (1)
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n
02Establish hlengthL2–4
03Separate the logical casesL5–5
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L5
cases hlength
04Establish hdigitsL6–10
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary exponent digit prefix at length.
05Separate the logical casesL11–12
06Construct an explicit witnessL13–15
07Separate the logical casesL16–16
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L16
split
Original exact command ledger · 18 lines
- 0001
intro n - 0002
have hlength : exists l. ((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_total_length ff_lower_bl_bd_total_length ff_upper_bl_bd_total_length. (((l) = S ff_exponent_bl_bd_total_length) /\ ((exists ff_positive_bl_bd_total_length. ff_positive_bl_bd_total_length + 1 = (n)) /\ ((exists pa_b_bl_bd_total_length_lower pa_c_bl_bd_total_length_lower. ((forall pa_i_bl_bd_total_length_lower_repeat. (exists pa_lt_bl_bd_total_length_lower_repeat_bound. pa_lt_bl_bd_total_length_lower_repeat_bound + S pa_i_bl_bd_total_length_lower_repeat = ff_exponent_bl_bd_total_length) -> (((exists pa_h_bl_bd_total_length_lower_repeat_decoded. pa_h_bl_bd_total_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_length_lower_repeat)) * pa_c_bl_bd_total_length_lower)) /\ exists pa_q_bl_bd_total_length_lower_repeat_decoded. pa_b_bl_bd_total_length_lower = pa_q_bl_bd_total_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_total_length_lower_repeat)) * pa_c_bl_bd_total_length_lower) + (2)))) /\ (exists pa_u_bl_bd_total_length_lower_product pa_v_bl_bd_total_length_lower_product. ((((exists pa_h_bl_bd_total_length_lower_product_start. pa_h_bl_bd_total_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_start. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_total_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_total_length_lower_product_terminal. pa_h_bl_bd_total_length_lower_product_terminal + S (ff_lower_bl_bd_total_length) = S ((S (ff_exponent_bl_bd_total_length)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_terminal. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_total_length)) * pa_v_bl_bd_total_length_lower_product) + (ff_lower_bl_bd_total_length))) /\ forall pa_i_bl_bd_total_length_lower_product. (exists pa_lt_bl_bd_total_length_lower_product_bound. pa_lt_bl_bd_total_length_lower_product_bound + S pa_i_bl_bd_total_length_lower_product = ff_exponent_bl_bd_total_length) -> exists pa_p_bl_bd_total_length_lower_product pa_r_bl_bd_total_length_lower_product pa_s_bl_bd_total_length_lower_product. ((((exists pa_h_bl_bd_total_length_lower_product_factor. pa_h_bl_bd_total_length_lower_product_factor + S (pa_p_bl_bd_total_length_lower_product) = S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_c_bl_bd_total_length_lower)) /\ exists pa_q_bl_bd_total_length_lower_product_factor. pa_b_bl_bd_total_length_lower = pa_q_bl_bd_total_length_lower_product_factor * S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_c_bl_bd_total_length_lower) + (pa_p_bl_bd_total_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_length_lower_product_partial. pa_h_bl_bd_total_length_lower_product_partial + S (pa_r_bl_bd_total_length_lower_product) = S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_partial. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_partial * S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product) + (pa_r_bl_bd_total_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_length_lower_product_successor. pa_h_bl_bd_total_length_lower_product_successor + S (pa_s_bl_bd_total_length_lower_product) = S ((S (S pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_successor. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_successor * S ((S (S pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product) + (pa_s_bl_bd_total_length_lower_product))) /\ pa_s_bl_bd_total_length_lower_product = pa_r_bl_bd_total_length_lower_product * pa_p_bl_bd_total_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_total_length_upper pa_c_bl_bd_total_length_upper. ((forall pa_i_bl_bd_total_length_upper_repeat. (exists pa_lt_bl_bd_total_length_upper_repeat_bound. pa_lt_bl_bd_total_length_upper_repeat_bound + S pa_i_bl_bd_total_length_upper_repeat = l) -> (((exists pa_h_bl_bd_total_length_upper_repeat_decoded. pa_h_bl_bd_total_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_length_upper_repeat)) * pa_c_bl_bd_total_length_upper)) /\ exists pa_q_bl_bd_total_length_upper_repeat_decoded. pa_b_bl_bd_total_length_upper = pa_q_bl_bd_total_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_total_length_upper_repeat)) * pa_c_bl_bd_total_length_upper) + (2)))) /\ (exists pa_u_bl_bd_total_length_upper_product pa_v_bl_bd_total_length_upper_product. ((((exists pa_h_bl_bd_total_length_upper_product_start. pa_h_bl_bd_total_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_start. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_total_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_total_length_upper_product_terminal. pa_h_bl_bd_total_length_upper_product_terminal + S (ff_upper_bl_bd_total_length) = S ((S (l)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_terminal. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_total_length_upper_product) + (ff_upper_bl_bd_total_length))) /\ forall pa_i_bl_bd_total_length_upper_product. (exists pa_lt_bl_bd_total_length_upper_product_bound. pa_lt_bl_bd_total_length_upper_product_bound + S pa_i_bl_bd_total_length_upper_product = l) -> exists pa_p_bl_bd_total_length_upper_product pa_r_bl_bd_total_length_upper_product pa_s_bl_bd_total_length_upper_product. ((((exists pa_h_bl_bd_total_length_upper_product_factor. pa_h_bl_bd_total_length_upper_product_factor + S (pa_p_bl_bd_total_length_upper_product) = S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_c_bl_bd_total_length_upper)) /\ exists pa_q_bl_bd_total_length_upper_product_factor. pa_b_bl_bd_total_length_upper = pa_q_bl_bd_total_length_upper_product_factor * S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_c_bl_bd_total_length_upper) + (pa_p_bl_bd_total_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_length_upper_product_partial. pa_h_bl_bd_total_length_upper_product_partial + S (pa_r_bl_bd_total_length_upper_product) = S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_partial. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_partial * S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product) + (pa_r_bl_bd_total_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_length_upper_product_successor. pa_h_bl_bd_total_length_upper_product_successor + S (pa_s_bl_bd_total_length_upper_product) = S ((S (S pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_successor. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_successor * S ((S (S pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product) + (pa_s_bl_bd_total_length_upper_product))) /\ pa_s_bl_bd_total_length_upper_product = pa_r_bl_bd_total_length_upper_product * pa_p_bl_bd_total_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_total_length. ff_lower_gap_bl_bd_total_length + (ff_lower_bl_bd_total_length) = (n)) /\ (exists ff_upper_gap_bl_bd_total_length. ff_upper_gap_bl_bd_total_length + S (n) = (ff_upper_bl_bd_total_length))))))))) - 0003
specialize binary_length_exists n - 0004
exact binary_length_exists - 0005
cases hlength - 0006
have hdigits : exists b c. (((forall ff_index_be_bd_total_digits_digits ff_digit_be_bd_total_digits_digits. (exists ff_lt_be_bd_total_digits_digits_bound. ff_lt_be_bd_total_digits_digits_bound + S ff_index_be_bd_total_digits_digits = x) -> (((exists ff_h_be_bd_total_digits_digits_digit. ff_h_be_bd_total_digits_digits_digit + S (ff_digit_be_bd_total_digits_digits) = S ((S (ff_index_be_bd_total_digits_digits)) * c)) /\ exists ff_q_be_bd_total_digits_digits_digit. b = ff_q_be_bd_total_digits_digits_digit * S ((S (ff_index_be_bd_total_digits_digits)) * c) + (ff_digit_be_bd_total_digits_digits))) -> (ff_digit_be_bd_total_digits_digits = 0 \/ ff_digit_be_bd_total_digits_digits = 1)) /\ (exists ff_u_ph_bd_total_digits_horner ff_v_ph_bd_total_digits_horner. ((((exists fs_h_ph_bd_total_digits_horner_body_start. fs_h_ph_bd_total_digits_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_start. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_start * S ((S (0)) * ff_v_ph_bd_total_digits_horner) + (0))) /\ ((((exists fs_h_ph_bd_total_digits_horner_body_terminal. fs_h_ph_bd_total_digits_horner_body_terminal + S (n) = S ((S (x)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_terminal. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_terminal * S ((S (x)) * ff_v_ph_bd_total_digits_horner) + (n))) /\ forall ff_i_ph_bd_total_digits_horner_body_steps. (exists ph_bound_bd_total_digits_horner_body_steps. ph_bound_bd_total_digits_horner_body_steps + S ff_i_ph_bd_total_digits_horner_body_steps = x) -> exists ff_coefficient_ph_bd_total_digits_horner_body_steps ff_previous_ph_bd_total_digits_horner_body_steps ff_current_ph_bd_total_digits_horner_body_steps. ((((exists fs_h_ph_bd_total_digits_horner_body_steps_coefficient. fs_h_ph_bd_total_digits_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_total_digits_horner_body_steps) = S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_total_digits_horner_body_steps_coefficient. b = fs_q_ph_bd_total_digits_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * c) + (ff_coefficient_ph_bd_total_digits_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_digits_horner_body_steps_before. fs_h_ph_bd_total_digits_horner_body_steps_before + S (ff_previous_ph_bd_total_digits_horner_body_steps) = S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_steps_before. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_steps_before * S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner) + (ff_previous_ph_bd_total_digits_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_digits_horner_body_steps_after. fs_h_ph_bd_total_digits_horner_body_steps_after + S (ff_current_ph_bd_total_digits_horner_body_steps) = S ((S (S ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_steps_after. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_steps_after * S ((S (S ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner) + (ff_current_ph_bd_total_digits_horner_body_steps))) /\ ff_current_ph_bd_total_digits_horner_body_steps = ff_previous_ph_bd_total_digits_horner_body_steps * 2 + ff_coefficient_ph_bd_total_digits_horner_body_steps)))))))) - 0007
specialize binary_exponent_digit_prefix_at_length n - 0008
specialize binary_exponent_digit_prefix_at_length x - 0009
apply binary_exponent_digit_prefix_at_length - 0010
exact hlength_witness - 0011
cases hdigits - 0012
cases hdigits_witness - 0013
exists x - 0014
exists x1 - 0015
exists x2 - 0016
split - 0017
exact hlength_witness - 0018
exact hdigits_witness_witness
Separate complete second-wave branches: Full T13 proof · Alpha v27.