BT00ST

legendre_sum_zero_extended_prefix

Alpha body-checked · checked-use disabled

An old Legendre sum has a successor-length quotient code ending in zero.

Exact expanded PA statement

forall p n e. ((~(p = 1) /\ forall frm_prime_left_blrr_tail_prime frm_prime_right_blrr_tail_prime. p = frm_prime_left_blrr_tail_prime * frm_prime_right_blrr_tail_prime -> frm_prime_left_blrr_tail_prime = 1 \/ frm_prime_right_blrr_tail_prime = 1)) -> (exists bls_code_blrr_extend_old bls_scale_blrr_extend_old. ((forall bls_index_blrr_extend_old_prefix. (exists bls_gap_blrr_extend_old_prefix_bound. bls_gap_blrr_extend_old_prefix_bound + S (bls_index_blrr_extend_old_prefix) = (n)) -> exists bls_power_blrr_extend_old_prefix bls_quotient_blrr_extend_old_prefix bls_remainder_blrr_extend_old_prefix. ((exists bpvi_b_bls_blrr_extend_old_prefix_power bpvi_c_bls_blrr_extend_old_prefix_power. ((forall bpvi_i_bls_blrr_extend_old_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_old_prefix_power. bpvi_repeat_gap_bls_blrr_extend_old_prefix_power + S bpvi_i_bls_blrr_extend_old_prefix_power = S bls_index_blrr_extend_old_prefix) -> (((exists bpvi_h_bls_blrr_extend_old_prefix_power_repeat. bpvi_h_bls_blrr_extend_old_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_repeat. bpvi_b_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_old_prefix_power bpvi_v_bls_blrr_extend_old_prefix_power. ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_start. bpvi_h_bls_blrr_extend_old_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_start. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_terminal. bpvi_h_bls_blrr_extend_old_prefix_power_terminal + S (bls_power_blrr_extend_old_prefix) = S ((S (S bls_index_blrr_extend_old_prefix)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_terminal. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_terminal * S ((S (S bls_index_blrr_extend_old_prefix)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (bls_power_blrr_extend_old_prefix))) /\ forall bpvi_j_bls_blrr_extend_old_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_old_prefix_power. bpvi_product_gap_bls_blrr_extend_old_prefix_power + S bpvi_j_bls_blrr_extend_old_prefix_power = S bls_index_blrr_extend_old_prefix) -> exists bpvi_factor_bls_blrr_extend_old_prefix_power bpvi_partial_bls_blrr_extend_old_prefix_power bpvi_successor_bls_blrr_extend_old_prefix_power. ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_factor. bpvi_h_bls_blrr_extend_old_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_old_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_factor. bpvi_b_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power) + (bpvi_factor_bls_blrr_extend_old_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_partial. bpvi_h_bls_blrr_extend_old_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_old_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_partial. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (bpvi_partial_bls_blrr_extend_old_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_successor. bpvi_h_bls_blrr_extend_old_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_old_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_successor. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (bpvi_successor_bls_blrr_extend_old_prefix_power))) /\ bpvi_successor_bls_blrr_extend_old_prefix_power = bpvi_partial_bls_blrr_extend_old_prefix_power * bpvi_factor_bls_blrr_extend_old_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_old_prefix_quotient_entry. ff_h_bls_blrr_extend_old_prefix_quotient_entry + S (bls_quotient_blrr_extend_old_prefix) = S ((S (bls_index_blrr_extend_old_prefix)) * bls_scale_blrr_extend_old)) /\ exists ff_q_bls_blrr_extend_old_prefix_quotient_entry. bls_code_blrr_extend_old = ff_q_bls_blrr_extend_old_prefix_quotient_entry * S ((S (bls_index_blrr_extend_old_prefix)) * bls_scale_blrr_extend_old) + (bls_quotient_blrr_extend_old_prefix))) /\ ((n = bls_power_blrr_extend_old_prefix * bls_quotient_blrr_extend_old_prefix + bls_remainder_blrr_extend_old_prefix /\ exists bls_remainder_gap_blrr_extend_old_prefix_division. bls_remainder_gap_blrr_extend_old_prefix_division + S (bls_remainder_blrr_extend_old_prefix) = bls_power_blrr_extend_old_prefix))))) /\ (exists ff_u_bls_blrr_extend_old_sum ff_v_bls_blrr_extend_old_sum. ((((exists ff_h_bls_blrr_extend_old_sum_start. ff_h_bls_blrr_extend_old_sum_start + S (0) = S ((S (0)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_start. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_start * S ((S (0)) * ff_v_bls_blrr_extend_old_sum) + (0))) /\ ((((exists ff_h_bls_blrr_extend_old_sum_terminal. ff_h_bls_blrr_extend_old_sum_terminal + S (e) = S ((S (n)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_terminal. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_terminal * S ((S (n)) * ff_v_bls_blrr_extend_old_sum) + (e))) /\ forall ff_i_bls_blrr_extend_old_sum. (exists ff_lt_bls_blrr_extend_old_sum_bound. ff_lt_bls_blrr_extend_old_sum_bound + S ff_i_bls_blrr_extend_old_sum = n) -> exists ff_a_bls_blrr_extend_old_sum ff_r_bls_blrr_extend_old_sum ff_s_bls_blrr_extend_old_sum. ((((exists ff_h_bls_blrr_extend_old_sum_summand. ff_h_bls_blrr_extend_old_sum_summand + S (ff_a_bls_blrr_extend_old_sum) = S ((S (ff_i_bls_blrr_extend_old_sum)) * bls_scale_blrr_extend_old)) /\ exists ff_q_bls_blrr_extend_old_sum_summand. bls_code_blrr_extend_old = ff_q_bls_blrr_extend_old_sum_summand * S ((S (ff_i_bls_blrr_extend_old_sum)) * bls_scale_blrr_extend_old) + (ff_a_bls_blrr_extend_old_sum))) /\ ((((exists ff_h_bls_blrr_extend_old_sum_partial. ff_h_bls_blrr_extend_old_sum_partial + S (ff_r_bls_blrr_extend_old_sum) = S ((S (ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_partial. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_partial * S ((S (ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum) + (ff_r_bls_blrr_extend_old_sum))) /\ ((((exists ff_h_bls_blrr_extend_old_sum_successor. ff_h_bls_blrr_extend_old_sum_successor + S (ff_s_bls_blrr_extend_old_sum) = S ((S (S ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_successor. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_successor * S ((S (S ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum) + (ff_s_bls_blrr_extend_old_sum))) /\ ff_s_bls_blrr_extend_old_sum = ff_r_bls_blrr_extend_old_sum + ff_a_bls_blrr_extend_old_sum)))))))) -> (exists b c. ((forall bls_index_blrr_extend_prefix. (exists bls_gap_blrr_extend_prefix_bound. bls_gap_blrr_extend_prefix_bound + S (bls_index_blrr_extend_prefix) = (S n)) -> exists bls_power_blrr_extend_prefix bls_quotient_blrr_extend_prefix bls_remainder_blrr_extend_prefix. ((exists bpvi_b_bls_blrr_extend_prefix_power bpvi_c_bls_blrr_extend_prefix_power. ((forall bpvi_i_bls_blrr_extend_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_prefix_power. bpvi_repeat_gap_bls_blrr_extend_prefix_power + S bpvi_i_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> (((exists bpvi_h_bls_blrr_extend_prefix_power_repeat. bpvi_h_bls_blrr_extend_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_repeat. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_prefix_power bpvi_v_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_start. bpvi_h_bls_blrr_extend_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_start. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_terminal. bpvi_h_bls_blrr_extend_prefix_power_terminal + S (bls_power_blrr_extend_prefix) = S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_terminal. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_terminal * S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power) + (bls_power_blrr_extend_prefix))) /\ forall bpvi_j_bls_blrr_extend_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_prefix_power. bpvi_product_gap_bls_blrr_extend_prefix_power + S bpvi_j_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> exists bpvi_factor_bls_blrr_extend_prefix_power bpvi_partial_bls_blrr_extend_prefix_power bpvi_successor_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_factor. bpvi_h_bls_blrr_extend_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_factor. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (bpvi_factor_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_partial. bpvi_h_bls_blrr_extend_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_partial. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_partial_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_successor. bpvi_h_bls_blrr_extend_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_successor. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_successor_bls_blrr_extend_prefix_power))) /\ bpvi_successor_bls_blrr_extend_prefix_power = bpvi_partial_bls_blrr_extend_prefix_power * bpvi_factor_bls_blrr_extend_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_prefix_quotient_entry. ff_h_bls_blrr_extend_prefix_quotient_entry + S (bls_quotient_blrr_extend_prefix) = S ((S (bls_index_blrr_extend_prefix)) * c)) /\ exists ff_q_bls_blrr_extend_prefix_quotient_entry. b = ff_q_bls_blrr_extend_prefix_quotient_entry * S ((S (bls_index_blrr_extend_prefix)) * c) + (bls_quotient_blrr_extend_prefix))) /\ ((n = bls_power_blrr_extend_prefix * bls_quotient_blrr_extend_prefix + bls_remainder_blrr_extend_prefix /\ exists bls_remainder_gap_blrr_extend_prefix_division. bls_remainder_gap_blrr_extend_prefix_division + S (bls_remainder_blrr_extend_prefix) = bls_power_blrr_extend_prefix))))) /\ (exists fs_u_blrr_extend_sum fs_v_blrr_extend_sum. ((((exists fs_h_blrr_extend_sum_body_start. fs_h_blrr_extend_sum_body_start + S (0) = S ((S (0)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_start. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_start * S ((S (0)) * fs_v_blrr_extend_sum) + (0))) /\ ((((exists fs_h_blrr_extend_sum_body_terminal. fs_h_blrr_extend_sum_body_terminal + S (e) = S ((S (S n)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_terminal. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_terminal * S ((S (S n)) * fs_v_blrr_extend_sum) + (e))) /\ forall fs_i_blrr_extend_sum_body_steps. (exists fs_lt_blrr_extend_sum_body_steps_bound. fs_lt_blrr_extend_sum_body_steps_bound + S fs_i_blrr_extend_sum_body_steps = S n) -> exists fs_a_blrr_extend_sum_body_steps fs_r_blrr_extend_sum_body_steps fs_s_blrr_extend_sum_body_steps. ((((exists fs_h_blrr_extend_sum_body_steps_summand. fs_h_blrr_extend_sum_body_steps_summand + S (fs_a_blrr_extend_sum_body_steps) = S ((S (fs_i_blrr_extend_sum_body_steps)) * c)) /\ exists fs_q_blrr_extend_sum_body_steps_summand. b = fs_q_blrr_extend_sum_body_steps_summand * S ((S (fs_i_blrr_extend_sum_body_steps)) * c) + (fs_a_blrr_extend_sum_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_body_steps_partial. fs_h_blrr_extend_sum_body_steps_partial + S (fs_r_blrr_extend_sum_body_steps) = S ((S (fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_steps_partial. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_steps_partial * S ((S (fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum) + (fs_r_blrr_extend_sum_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_body_steps_successor. fs_h_blrr_extend_sum_body_steps_successor + S (fs_s_blrr_extend_sum_body_steps) = S ((S (S fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_steps_successor. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_steps_successor * S ((S (S fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum) + (fs_s_blrr_extend_sum_body_steps))) /\ fs_s_blrr_extend_sum_body_steps = fs_r_blrr_extend_sum_body_steps + fs_a_blrr_extend_sum_body_steps))))))))

Structural proof guide

An old Legendre sum has a successor-length quotient code ending in zero.

Direct prerequisites: prime_power_quotient_prefix_exists, prime_power_quotient_prefix_last_zero, beta_sum_exists, beta_sum_succ_last_zero, le_succ, legendre_sum_functional. The authored body proceeds by case analysis (3), intermediate claims (7), equality transport (2).

Proof neighborhood

Direct dependencies

BT00S0 prime_power_quotient_prefix_exists BT00SS prime_power_quotient_prefix_last_zero BT008A beta_sum_exists BT00SR beta_sum_succ_last_zero BT0018 le_succ BT00S3 legendre_sum_functional

Direct dependents

BT00SV prime_legendre_sum_succ

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro n
  3. 0003intro e
  4. 0004intro hp
  5. 0005intro hlegendre
  6. 0006have hprefix : exists b c. (forall bls_index_blrr_extend_prefix. (exists bls_gap_blrr_extend_prefix_bound. bls_gap_blrr_extend_prefix_bound + S (bls_index_blrr_extend_prefix) = (S n)) -> exists bls_power_blrr_extend_prefix bls_quotient_blrr_extend_prefix bls_remainder_blrr_extend_prefix. ((exists bpvi_b_bls_blrr_extend_prefix_power bpvi_c_bls_blrr_extend_prefix_power. ((forall bpvi_i_bls_blrr_extend_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_prefix_power. bpvi_repeat_gap_bls_blrr_extend_prefix_power + S bpvi_i_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> (((exists bpvi_h_bls_blrr_extend_prefix_power_repeat. bpvi_h_bls_blrr_extend_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_repeat. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_prefix_power bpvi_v_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_start. bpvi_h_bls_blrr_extend_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_start. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_terminal. bpvi_h_bls_blrr_extend_prefix_power_terminal + S (bls_power_blrr_extend_prefix) = S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_terminal. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_terminal * S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power) + (bls_power_blrr_extend_prefix))) /\ forall bpvi_j_bls_blrr_extend_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_prefix_power. bpvi_product_gap_bls_blrr_extend_prefix_power + S bpvi_j_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> exists bpvi_factor_bls_blrr_extend_prefix_power bpvi_partial_bls_blrr_extend_prefix_power bpvi_successor_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_factor. bpvi_h_bls_blrr_extend_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_factor. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (bpvi_factor_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_partial. bpvi_h_bls_blrr_extend_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_partial. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_partial_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_successor. bpvi_h_bls_blrr_extend_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_successor. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_successor_bls_blrr_extend_prefix_power))) /\ bpvi_successor_bls_blrr_extend_prefix_power = bpvi_partial_bls_blrr_extend_prefix_power * bpvi_factor_bls_blrr_extend_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_prefix_quotient_entry. ff_h_bls_blrr_extend_prefix_quotient_entry + S (bls_quotient_blrr_extend_prefix) = S ((S (bls_index_blrr_extend_prefix)) * c)) /\ exists ff_q_bls_blrr_extend_prefix_quotient_entry. b = ff_q_bls_blrr_extend_prefix_quotient_entry * S ((S (bls_index_blrr_extend_prefix)) * c) + (bls_quotient_blrr_extend_prefix))) /\ ((n = bls_power_blrr_extend_prefix * bls_quotient_blrr_extend_prefix + bls_remainder_blrr_extend_prefix /\ exists bls_remainder_gap_blrr_extend_prefix_division. bls_remainder_gap_blrr_extend_prefix_division + S (bls_remainder_blrr_extend_prefix) = bls_power_blrr_extend_prefix)))))
  7. 0007specialize prime_power_quotient_prefix_exists p
  8. 0008specialize prime_power_quotient_prefix_exists n
  9. 0009specialize prime_power_quotient_prefix_exists (S n)
  10. 0010apply prime_power_quotient_prefix_exists
  11. 0011exact hp
  12. 0012cases hprefix
  13. 0013cases hprefix_witness
  14. 0014have hzero : ((exists fs_h_blrr_extend_last_zero. fs_h_blrr_extend_last_zero + S (0) = S ((S (n)) * x1)) /\ exists fs_q_blrr_extend_last_zero. x = fs_q_blrr_extend_last_zero * S ((S (n)) * x1) + (0))
  15. 0015specialize prime_power_quotient_prefix_last_zero p
  16. 0016specialize prime_power_quotient_prefix_last_zero n
  17. 0017specialize prime_power_quotient_prefix_last_zero x
  18. 0018specialize prime_power_quotient_prefix_last_zero x1
  19. 0019apply prime_power_quotient_prefix_last_zero
  20. 0020exact hp
  21. 0021exact hprefix_witness_witness
  22. 0022have hsuccessor_sum : exists q. exists fs_u_blrr_extend_sum_exists fs_v_blrr_extend_sum_exists. ((((exists fs_h_blrr_extend_sum_exists_body_start. fs_h_blrr_extend_sum_exists_body_start + S (0) = S ((S (0)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_start. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_start * S ((S (0)) * fs_v_blrr_extend_sum_exists) + (0))) /\ ((((exists fs_h_blrr_extend_sum_exists_body_terminal. fs_h_blrr_extend_sum_exists_body_terminal + S (q) = S ((S (S n)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_terminal. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_terminal * S ((S (S n)) * fs_v_blrr_extend_sum_exists) + (q))) /\ forall fs_i_blrr_extend_sum_exists_body_steps. (exists fs_lt_blrr_extend_sum_exists_body_steps_bound. fs_lt_blrr_extend_sum_exists_body_steps_bound + S fs_i_blrr_extend_sum_exists_body_steps = S n) -> exists fs_a_blrr_extend_sum_exists_body_steps fs_r_blrr_extend_sum_exists_body_steps fs_s_blrr_extend_sum_exists_body_steps. ((((exists fs_h_blrr_extend_sum_exists_body_steps_summand. fs_h_blrr_extend_sum_exists_body_steps_summand + S (fs_a_blrr_extend_sum_exists_body_steps) = S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * x1)) /\ exists fs_q_blrr_extend_sum_exists_body_steps_summand. x = fs_q_blrr_extend_sum_exists_body_steps_summand * S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * x1) + (fs_a_blrr_extend_sum_exists_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_exists_body_steps_partial. fs_h_blrr_extend_sum_exists_body_steps_partial + S (fs_r_blrr_extend_sum_exists_body_steps) = S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_steps_partial. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_steps_partial * S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists) + (fs_r_blrr_extend_sum_exists_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_exists_body_steps_successor. fs_h_blrr_extend_sum_exists_body_steps_successor + S (fs_s_blrr_extend_sum_exists_body_steps) = S ((S (S fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_steps_successor. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_steps_successor * S ((S (S fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists) + (fs_s_blrr_extend_sum_exists_body_steps))) /\ fs_s_blrr_extend_sum_exists_body_steps = fs_r_blrr_extend_sum_exists_body_steps + fs_a_blrr_extend_sum_exists_body_steps)))))
  23. 0023specialize beta_sum_exists x
  24. 0024specialize beta_sum_exists x1
  25. 0025specialize beta_sum_exists (S n)
  26. 0026exact beta_sum_exists
  27. 0027cases hsuccessor_sum
  28. 0028have hpredecessor_sum : exists ff_u_blrr_extend_predecessor_sum ff_v_blrr_extend_predecessor_sum. ((((exists ff_h_blrr_extend_predecessor_sum_start. ff_h_blrr_extend_predecessor_sum_start + S (0) = S ((S (0)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_start. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_start * S ((S (0)) * ff_v_blrr_extend_predecessor_sum) + (0))) /\ ((((exists ff_h_blrr_extend_predecessor_sum_terminal. ff_h_blrr_extend_predecessor_sum_terminal + S (x2) = S ((S (n)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_terminal. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_terminal * S ((S (n)) * ff_v_blrr_extend_predecessor_sum) + (x2))) /\ forall ff_i_blrr_extend_predecessor_sum. (exists ff_lt_blrr_extend_predecessor_sum_bound. ff_lt_blrr_extend_predecessor_sum_bound + S ff_i_blrr_extend_predecessor_sum = n) -> exists ff_a_blrr_extend_predecessor_sum ff_r_blrr_extend_predecessor_sum ff_s_blrr_extend_predecessor_sum. ((((exists ff_h_blrr_extend_predecessor_sum_summand. ff_h_blrr_extend_predecessor_sum_summand + S (ff_a_blrr_extend_predecessor_sum) = S ((S (ff_i_blrr_extend_predecessor_sum)) * x1)) /\ exists ff_q_blrr_extend_predecessor_sum_summand. x = ff_q_blrr_extend_predecessor_sum_summand * S ((S (ff_i_blrr_extend_predecessor_sum)) * x1) + (ff_a_blrr_extend_predecessor_sum))) /\ ((((exists ff_h_blrr_extend_predecessor_sum_partial. ff_h_blrr_extend_predecessor_sum_partial + S (ff_r_blrr_extend_predecessor_sum) = S ((S (ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_partial. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_partial * S ((S (ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum) + (ff_r_blrr_extend_predecessor_sum))) /\ ((((exists ff_h_blrr_extend_predecessor_sum_successor. ff_h_blrr_extend_predecessor_sum_successor + S (ff_s_blrr_extend_predecessor_sum) = S ((S (S ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_successor. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_successor * S ((S (S ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum) + (ff_s_blrr_extend_predecessor_sum))) /\ ff_s_blrr_extend_predecessor_sum = ff_r_blrr_extend_predecessor_sum + ff_a_blrr_extend_predecessor_sum)))))
  29. 0029specialize beta_sum_succ_last_zero x
  30. 0030specialize beta_sum_succ_last_zero x1
  31. 0031specialize beta_sum_succ_last_zero n
  32. 0032specialize beta_sum_succ_last_zero x2
  33. 0033apply beta_sum_succ_last_zero
  34. 0034exact hsuccessor_sum_witness
  35. 0035exact hzero
  36. 0036have hrestricted : forall bls_index_blrr_extend_restricted. (exists bls_gap_blrr_extend_restricted_bound. bls_gap_blrr_extend_restricted_bound + S (bls_index_blrr_extend_restricted) = (n)) -> exists bls_power_blrr_extend_restricted bls_quotient_blrr_extend_restricted bls_remainder_blrr_extend_restricted. ((exists bpvi_b_bls_blrr_extend_restricted_power bpvi_c_bls_blrr_extend_restricted_power. ((forall bpvi_i_bls_blrr_extend_restricted_power. (exists bpvi_repeat_gap_bls_blrr_extend_restricted_power. bpvi_repeat_gap_bls_blrr_extend_restricted_power + S bpvi_i_bls_blrr_extend_restricted_power = S bls_index_blrr_extend_restricted) -> (((exists bpvi_h_bls_blrr_extend_restricted_power_repeat. bpvi_h_bls_blrr_extend_restricted_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_repeat. bpvi_b_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_repeat * S ((S (bpvi_i_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_restricted_power bpvi_v_bls_blrr_extend_restricted_power. ((((exists bpvi_h_bls_blrr_extend_restricted_power_start. bpvi_h_bls_blrr_extend_restricted_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_start. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_restricted_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_restricted_power_terminal. bpvi_h_bls_blrr_extend_restricted_power_terminal + S (bls_power_blrr_extend_restricted) = S ((S (S bls_index_blrr_extend_restricted)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_terminal. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_terminal * S ((S (S bls_index_blrr_extend_restricted)) * bpvi_v_bls_blrr_extend_restricted_power) + (bls_power_blrr_extend_restricted))) /\ forall bpvi_j_bls_blrr_extend_restricted_power. (exists bpvi_product_gap_bls_blrr_extend_restricted_power. bpvi_product_gap_bls_blrr_extend_restricted_power + S bpvi_j_bls_blrr_extend_restricted_power = S bls_index_blrr_extend_restricted) -> exists bpvi_factor_bls_blrr_extend_restricted_power bpvi_partial_bls_blrr_extend_restricted_power bpvi_successor_bls_blrr_extend_restricted_power. ((((exists bpvi_h_bls_blrr_extend_restricted_power_factor. bpvi_h_bls_blrr_extend_restricted_power_factor + S (bpvi_factor_bls_blrr_extend_restricted_power) = S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_factor. bpvi_b_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_factor * S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power) + (bpvi_factor_bls_blrr_extend_restricted_power))) /\ ((((exists bpvi_h_bls_blrr_extend_restricted_power_partial. bpvi_h_bls_blrr_extend_restricted_power_partial + S (bpvi_partial_bls_blrr_extend_restricted_power) = S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_partial. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_partial * S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power) + (bpvi_partial_bls_blrr_extend_restricted_power))) /\ ((((exists bpvi_h_bls_blrr_extend_restricted_power_successor. bpvi_h_bls_blrr_extend_restricted_power_successor + S (bpvi_successor_bls_blrr_extend_restricted_power) = S ((S (S bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_successor. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_successor * S ((S (S bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power) + (bpvi_successor_bls_blrr_extend_restricted_power))) /\ bpvi_successor_bls_blrr_extend_restricted_power = bpvi_partial_bls_blrr_extend_restricted_power * bpvi_factor_bls_blrr_extend_restricted_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_restricted_quotient_entry. ff_h_bls_blrr_extend_restricted_quotient_entry + S (bls_quotient_blrr_extend_restricted) = S ((S (bls_index_blrr_extend_restricted)) * x1)) /\ exists ff_q_bls_blrr_extend_restricted_quotient_entry. x = ff_q_bls_blrr_extend_restricted_quotient_entry * S ((S (bls_index_blrr_extend_restricted)) * x1) + (bls_quotient_blrr_extend_restricted))) /\ ((n = bls_power_blrr_extend_restricted * bls_quotient_blrr_extend_restricted + bls_remainder_blrr_extend_restricted /\ exists bls_remainder_gap_blrr_extend_restricted_division. bls_remainder_gap_blrr_extend_restricted_division + S (bls_remainder_blrr_extend_restricted) = bls_power_blrr_extend_restricted))))
  37. 0037intro i
  38. 0038intro hi
  39. 0039specialize hprefix_witness_witness i
  40. 0040apply hprefix_witness_witness
  41. 0041specialize le_succ (S i)
  42. 0042specialize le_succ n
  43. 0043apply le_succ
  44. 0044exact hi
  45. 0045have hcompeting : exists bls_code_blrr_extend_competing bls_scale_blrr_extend_competing. ((forall bls_index_blrr_extend_competing_prefix. (exists bls_gap_blrr_extend_competing_prefix_bound. bls_gap_blrr_extend_competing_prefix_bound + S (bls_index_blrr_extend_competing_prefix) = (n)) -> exists bls_power_blrr_extend_competing_prefix bls_quotient_blrr_extend_competing_prefix bls_remainder_blrr_extend_competing_prefix. ((exists bpvi_b_bls_blrr_extend_competing_prefix_power bpvi_c_bls_blrr_extend_competing_prefix_power. ((forall bpvi_i_bls_blrr_extend_competing_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_competing_prefix_power. bpvi_repeat_gap_bls_blrr_extend_competing_prefix_power + S bpvi_i_bls_blrr_extend_competing_prefix_power = S bls_index_blrr_extend_competing_prefix) -> (((exists bpvi_h_bls_blrr_extend_competing_prefix_power_repeat. bpvi_h_bls_blrr_extend_competing_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_repeat. bpvi_b_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_competing_prefix_power bpvi_v_bls_blrr_extend_competing_prefix_power. ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_start. bpvi_h_bls_blrr_extend_competing_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_start. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_terminal. bpvi_h_bls_blrr_extend_competing_prefix_power_terminal + S (bls_power_blrr_extend_competing_prefix) = S ((S (S bls_index_blrr_extend_competing_prefix)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_terminal. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_terminal * S ((S (S bls_index_blrr_extend_competing_prefix)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (bls_power_blrr_extend_competing_prefix))) /\ forall bpvi_j_bls_blrr_extend_competing_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_competing_prefix_power. bpvi_product_gap_bls_blrr_extend_competing_prefix_power + S bpvi_j_bls_blrr_extend_competing_prefix_power = S bls_index_blrr_extend_competing_prefix) -> exists bpvi_factor_bls_blrr_extend_competing_prefix_power bpvi_partial_bls_blrr_extend_competing_prefix_power bpvi_successor_bls_blrr_extend_competing_prefix_power. ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_factor. bpvi_h_bls_blrr_extend_competing_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_competing_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_factor. bpvi_b_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power) + (bpvi_factor_bls_blrr_extend_competing_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_partial. bpvi_h_bls_blrr_extend_competing_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_competing_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_partial. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (bpvi_partial_bls_blrr_extend_competing_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_successor. bpvi_h_bls_blrr_extend_competing_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_competing_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_successor. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (bpvi_successor_bls_blrr_extend_competing_prefix_power))) /\ bpvi_successor_bls_blrr_extend_competing_prefix_power = bpvi_partial_bls_blrr_extend_competing_prefix_power * bpvi_factor_bls_blrr_extend_competing_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_competing_prefix_quotient_entry. ff_h_bls_blrr_extend_competing_prefix_quotient_entry + S (bls_quotient_blrr_extend_competing_prefix) = S ((S (bls_index_blrr_extend_competing_prefix)) * bls_scale_blrr_extend_competing)) /\ exists ff_q_bls_blrr_extend_competing_prefix_quotient_entry. bls_code_blrr_extend_competing = ff_q_bls_blrr_extend_competing_prefix_quotient_entry * S ((S (bls_index_blrr_extend_competing_prefix)) * bls_scale_blrr_extend_competing) + (bls_quotient_blrr_extend_competing_prefix))) /\ ((n = bls_power_blrr_extend_competing_prefix * bls_quotient_blrr_extend_competing_prefix + bls_remainder_blrr_extend_competing_prefix /\ exists bls_remainder_gap_blrr_extend_competing_prefix_division. bls_remainder_gap_blrr_extend_competing_prefix_division + S (bls_remainder_blrr_extend_competing_prefix) = bls_power_blrr_extend_competing_prefix))))) /\ (exists ff_u_bls_blrr_extend_competing_sum ff_v_bls_blrr_extend_competing_sum. ((((exists ff_h_bls_blrr_extend_competing_sum_start. ff_h_bls_blrr_extend_competing_sum_start + S (0) = S ((S (0)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_start. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_start * S ((S (0)) * ff_v_bls_blrr_extend_competing_sum) + (0))) /\ ((((exists ff_h_bls_blrr_extend_competing_sum_terminal. ff_h_bls_blrr_extend_competing_sum_terminal + S (x2) = S ((S (n)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_terminal. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_terminal * S ((S (n)) * ff_v_bls_blrr_extend_competing_sum) + (x2))) /\ forall ff_i_bls_blrr_extend_competing_sum. (exists ff_lt_bls_blrr_extend_competing_sum_bound. ff_lt_bls_blrr_extend_competing_sum_bound + S ff_i_bls_blrr_extend_competing_sum = n) -> exists ff_a_bls_blrr_extend_competing_sum ff_r_bls_blrr_extend_competing_sum ff_s_bls_blrr_extend_competing_sum. ((((exists ff_h_bls_blrr_extend_competing_sum_summand. ff_h_bls_blrr_extend_competing_sum_summand + S (ff_a_bls_blrr_extend_competing_sum) = S ((S (ff_i_bls_blrr_extend_competing_sum)) * bls_scale_blrr_extend_competing)) /\ exists ff_q_bls_blrr_extend_competing_sum_summand. bls_code_blrr_extend_competing = ff_q_bls_blrr_extend_competing_sum_summand * S ((S (ff_i_bls_blrr_extend_competing_sum)) * bls_scale_blrr_extend_competing) + (ff_a_bls_blrr_extend_competing_sum))) /\ ((((exists ff_h_bls_blrr_extend_competing_sum_partial. ff_h_bls_blrr_extend_competing_sum_partial + S (ff_r_bls_blrr_extend_competing_sum) = S ((S (ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_partial. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_partial * S ((S (ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum) + (ff_r_bls_blrr_extend_competing_sum))) /\ ((((exists ff_h_bls_blrr_extend_competing_sum_successor. ff_h_bls_blrr_extend_competing_sum_successor + S (ff_s_bls_blrr_extend_competing_sum) = S ((S (S ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_successor. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_successor * S ((S (S ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum) + (ff_s_bls_blrr_extend_competing_sum))) /\ ff_s_bls_blrr_extend_competing_sum = ff_r_bls_blrr_extend_competing_sum + ff_a_bls_blrr_extend_competing_sum)))))))
  46. 0046exists x
  47. 0047exists x1
  48. 0048split
  49. 0049exact hrestricted
  50. 0050exact hpredecessor_sum
  51. 0051have heq : e = x2
  52. 0052specialize legendre_sum_functional p
  53. 0053specialize legendre_sum_functional n
  54. 0054specialize legendre_sum_functional e
  55. 0055specialize legendre_sum_functional x2
  56. 0056apply legendre_sum_functional
  57. 0057exact hlegendre
  58. 0058exact hcompeting
  59. 0059exists x
  60. 0060exists x1
  61. 0061split
  62. 0062exact hprefix_witness_witness
  63. 0063rewrite heq
  64. 0064rewrite heq
  65. 0065exact hsuccessor_sum_witness