power_quotient_successor_pointwise_add

Exact expanded PA statement

forall p n f b c d e z v. ((~(p = 1) /\ forall frm_prime_left_legendre_successor_prime frm_prime_right_legendre_successor_prime. p = frm_prime_left_legendre_successor_prime * frm_prime_right_legendre_successor_prime -> frm_prime_left_legendre_successor_prime = 1 \/ frm_prime_right_legendre_successor_prime = 1)) -> ((((exists blsr_le_gap_legendre_successor_pointwise_valuation_exponent_bound. blsr_le_gap_legendre_successor_pointwise_valuation_exponent_bound + (f) = (S n)) /\ (exists bpvi_result_legendre_successor_pointwise_valuation_selected. ((exists bpvi_b_legendre_successor_pointwise_valuation_selected_power bpvi_c_legendre_successor_pointwise_valuation_selected_power. ((forall bpvi_i_legendre_successor_pointwise_valuation_selected_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_valuation_selected_power. bpvi_repeat_gap_legendre_successor_pointwise_valuation_selected_power + S bpvi_i_legendre_successor_pointwise_valuation_selected_power = f) -> (((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_repeat. bpvi_h_legendre_successor_pointwise_valuation_selected_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_repeat. bpvi_b_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_valuation_selected_power bpvi_v_legendre_successor_pointwise_valuation_selected_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_start. bpvi_h_legendre_successor_pointwise_valuation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_start. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_terminal. bpvi_h_legendre_successor_pointwise_valuation_selected_power_terminal + S (bpvi_result_legendre_successor_pointwise_valuation_selected) = S ((S (f)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_terminal. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_terminal * S ((S (f)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (bpvi_result_legendre_successor_pointwise_valuation_selected))) /\ forall bpvi_j_legendre_successor_pointwise_valuation_selected_power. (exists bpvi_product_gap_legendre_successor_pointwise_valuation_selected_power. bpvi_product_gap_legendre_successor_pointwise_valuation_selected_power + S bpvi_j_legendre_successor_pointwise_valuation_selected_power = f) -> exists bpvi_factor_legendre_successor_pointwise_valuation_selected_power bpvi_partial_legendre_successor_pointwise_valuation_selected_power bpvi_successor_legendre_successor_pointwise_valuation_selected_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_factor. bpvi_h_legendre_successor_pointwise_valuation_selected_power_factor + S (bpvi_factor_legendre_successor_pointwise_valuation_selected_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_factor. bpvi_b_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power) + (bpvi_factor_legendre_successor_pointwise_valuation_selected_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_partial. bpvi_h_legendre_successor_pointwise_valuation_selected_power_partial + S (bpvi_partial_legendre_successor_pointwise_valuation_selected_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_partial. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (bpvi_partial_legendre_successor_pointwise_valuation_selected_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_successor. bpvi_h_legendre_successor_pointwise_valuation_selected_power_successor + S (bpvi_successor_legendre_successor_pointwise_valuation_selected_power) = S ((S (S bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_successor. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (bpvi_successor_legendre_successor_pointwise_valuation_selected_power))) /\ bpvi_successor_legendre_successor_pointwise_valuation_selected_power = bpvi_partial_legendre_successor_pointwise_valuation_selected_power * bpvi_factor_legendre_successor_pointwise_valuation_selected_power)))))))) /\ exists bpvi_divisor_factor_legendre_successor_pointwise_valuation_selected. S n = bpvi_result_legendre_successor_pointwise_valuation_selected * bpvi_divisor_factor_legendre_successor_pointwise_valuation_selected))) /\ forall blsr_candidate_legendre_successor_pointwise_valuation. (exists blsr_le_gap_legendre_successor_pointwise_valuation_candidate_bound. blsr_le_gap_legendre_successor_pointwise_valuation_candidate_bound + (blsr_candidate_legendre_successor_pointwise_valuation) = (S n)) -> (exists bpvi_result_legendre_successor_pointwise_valuation_candidate. ((exists bpvi_b_legendre_successor_pointwise_valuation_candidate_power bpvi_c_legendre_successor_pointwise_valuation_candidate_power. ((forall bpvi_i_legendre_successor_pointwise_valuation_candidate_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_valuation_candidate_power. bpvi_repeat_gap_legendre_successor_pointwise_valuation_candidate_power + S bpvi_i_legendre_successor_pointwise_valuation_candidate_power = blsr_candidate_legendre_successor_pointwise_valuation) -> (((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_repeat. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_repeat. bpvi_b_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_valuation_candidate_power bpvi_v_legendre_successor_pointwise_valuation_candidate_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_start. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_start. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_terminal. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_terminal + S (bpvi_result_legendre_successor_pointwise_valuation_candidate) = S ((S (blsr_candidate_legendre_successor_pointwise_valuation)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_terminal. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_terminal * S ((S (blsr_candidate_legendre_successor_pointwise_valuation)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_result_legendre_successor_pointwise_valuation_candidate))) /\ forall bpvi_j_legendre_successor_pointwise_valuation_candidate_power. (exists bpvi_product_gap_legendre_successor_pointwise_valuation_candidate_power. bpvi_product_gap_legendre_successor_pointwise_valuation_candidate_power + S bpvi_j_legendre_successor_pointwise_valuation_candidate_power = blsr_candidate_legendre_successor_pointwise_valuation) -> exists bpvi_factor_legendre_successor_pointwise_valuation_candidate_power bpvi_partial_legendre_successor_pointwise_valuation_candidate_power bpvi_successor_legendre_successor_pointwise_valuation_candidate_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_factor. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_factor + S (bpvi_factor_legendre_successor_pointwise_valuation_candidate_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_factor. bpvi_b_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_factor_legendre_successor_pointwise_valuation_candidate_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_partial. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_partial + S (bpvi_partial_legendre_successor_pointwise_valuation_candidate_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_partial. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_partial_legendre_successor_pointwise_valuation_candidate_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_successor. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_successor + S (bpvi_successor_legendre_successor_pointwise_valuation_candidate_power) = S ((S (S bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_successor. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_successor_legendre_successor_pointwise_valuation_candidate_power))) /\ bpvi_successor_legendre_successor_pointwise_valuation_candidate_power = bpvi_partial_legendre_successor_pointwise_valuation_candidate_power * bpvi_factor_legendre_successor_pointwise_valuation_candidate_power)))))))) /\ exists bpvi_divisor_factor_legendre_successor_pointwise_valuation_candidate. S n = bpvi_result_legendre_successor_pointwise_valuation_candidate * bpvi_divisor_factor_legendre_successor_pointwise_valuation_candidate)) -> (exists blsr_le_gap_legendre_successor_pointwise_valuation_maximal. blsr_le_gap_legendre_successor_pointwise_valuation_maximal + (blsr_candidate_legendre_successor_pointwise_valuation) = (f)))) -> (forall bls_index_legendre_successor_pointwise_old. (exists bls_gap_legendre_successor_pointwise_old_bound. bls_gap_legendre_successor_pointwise_old_bound + S (bls_index_legendre_successor_pointwise_old) = (S n)) -> exists bls_power_legendre_successor_pointwise_old bls_quotient_legendre_successor_pointwise_old bls_remainder_legendre_successor_pointwise_old. ((exists bpvi_b_bls_legendre_successor_pointwise_old_power bpvi_c_bls_legendre_successor_pointwise_old_power. ((forall bpvi_i_bls_legendre_successor_pointwise_old_power. (exists bpvi_repeat_gap_bls_legendre_successor_pointwise_old_power. bpvi_repeat_gap_bls_legendre_successor_pointwise_old_power + S bpvi_i_bls_legendre_successor_pointwise_old_power = S bls_index_legendre_successor_pointwise_old) -> (((exists bpvi_h_bls_legendre_successor_pointwise_old_power_repeat. bpvi_h_bls_legendre_successor_pointwise_old_power_repeat + S (p) = S ((S (bpvi_i_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_repeat. bpvi_b_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_repeat * S ((S (bpvi_i_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power) + (p)))) /\ (exists bpvi_u_bls_legendre_successor_pointwise_old_power bpvi_v_bls_legendre_successor_pointwise_old_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_start. bpvi_h_bls_legendre_successor_pointwise_old_power_start + S (1) = S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_start. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_start * S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (1))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_terminal. bpvi_h_bls_legendre_successor_pointwise_old_power_terminal + S (bls_power_legendre_successor_pointwise_old) = S ((S (S bls_index_legendre_successor_pointwise_old)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_terminal. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_terminal * S ((S (S bls_index_legendre_successor_pointwise_old)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (bls_power_legendre_successor_pointwise_old))) /\ forall bpvi_j_bls_legendre_successor_pointwise_old_power. (exists bpvi_product_gap_bls_legendre_successor_pointwise_old_power. bpvi_product_gap_bls_legendre_successor_pointwise_old_power + S bpvi_j_bls_legendre_successor_pointwise_old_power = S bls_index_legendre_successor_pointwise_old) -> exists bpvi_factor_bls_legendre_successor_pointwise_old_power bpvi_partial_bls_legendre_successor_pointwise_old_power bpvi_successor_bls_legendre_successor_pointwise_old_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_factor. bpvi_h_bls_legendre_successor_pointwise_old_power_factor + S (bpvi_factor_bls_legendre_successor_pointwise_old_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_factor. bpvi_b_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_factor * S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power) + (bpvi_factor_bls_legendre_successor_pointwise_old_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_partial. bpvi_h_bls_legendre_successor_pointwise_old_power_partial + S (bpvi_partial_bls_legendre_successor_pointwise_old_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_partial. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_partial * S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (bpvi_partial_bls_legendre_successor_pointwise_old_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_successor. bpvi_h_bls_legendre_successor_pointwise_old_power_successor + S (bpvi_successor_bls_legendre_successor_pointwise_old_power) = S ((S (S bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_successor. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_successor * S ((S (S bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (bpvi_successor_bls_legendre_successor_pointwise_old_power))) /\ bpvi_successor_bls_legendre_successor_pointwise_old_power = bpvi_partial_bls_legendre_successor_pointwise_old_power * bpvi_factor_bls_legendre_successor_pointwise_old_power)))))))) /\ ((((exists ff_h_bls_legendre_successor_pointwise_old_quotient_entry. ff_h_bls_legendre_successor_pointwise_old_quotient_entry + S (bls_quotient_legendre_successor_pointwise_old) = S ((S (bls_index_legendre_successor_pointwise_old)) * c)) /\ exists ff_q_bls_legendre_successor_pointwise_old_quotient_entry. b = ff_q_bls_legendre_successor_pointwise_old_quotient_entry * S ((S (bls_index_legendre_successor_pointwise_old)) * c) + (bls_quotient_legendre_successor_pointwise_old))) /\ ((n = bls_power_legendre_successor_pointwise_old * bls_quotient_legendre_successor_pointwise_old + bls_remainder_legendre_successor_pointwise_old /\ exists bls_remainder_gap_legendre_successor_pointwise_old_division. bls_remainder_gap_legendre_successor_pointwise_old_division + S (bls_remainder_legendre_successor_pointwise_old) = bls_power_legendre_successor_pointwise_old))))) -> (forall bls_index_legendre_successor_pointwise_new. (exists bls_gap_legendre_successor_pointwise_new_bound. bls_gap_legendre_successor_pointwise_new_bound + S (bls_index_legendre_successor_pointwise_new) = (S n)) -> exists bls_power_legendre_successor_pointwise_new bls_quotient_legendre_successor_pointwise_new bls_remainder_legendre_successor_pointwise_new. ((exists bpvi_b_bls_legendre_successor_pointwise_new_power bpvi_c_bls_legendre_successor_pointwise_new_power. ((forall bpvi_i_bls_legendre_successor_pointwise_new_power. (exists bpvi_repeat_gap_bls_legendre_successor_pointwise_new_power. bpvi_repeat_gap_bls_legendre_successor_pointwise_new_power + S bpvi_i_bls_legendre_successor_pointwise_new_power = S bls_index_legendre_successor_pointwise_new) -> (((exists bpvi_h_bls_legendre_successor_pointwise_new_power_repeat. bpvi_h_bls_legendre_successor_pointwise_new_power_repeat + S (p) = S ((S (bpvi_i_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_repeat. bpvi_b_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_repeat * S ((S (bpvi_i_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power) + (p)))) /\ (exists bpvi_u_bls_legendre_successor_pointwise_new_power bpvi_v_bls_legendre_successor_pointwise_new_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_start. bpvi_h_bls_legendre_successor_pointwise_new_power_start + S (1) = S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_start. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_start * S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (1))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_terminal. bpvi_h_bls_legendre_successor_pointwise_new_power_terminal + S (bls_power_legendre_successor_pointwise_new) = S ((S (S bls_index_legendre_successor_pointwise_new)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_terminal. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_terminal * S ((S (S bls_index_legendre_successor_pointwise_new)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (bls_power_legendre_successor_pointwise_new))) /\ forall bpvi_j_bls_legendre_successor_pointwise_new_power. (exists bpvi_product_gap_bls_legendre_successor_pointwise_new_power. bpvi_product_gap_bls_legendre_successor_pointwise_new_power + S bpvi_j_bls_legendre_successor_pointwise_new_power = S bls_index_legendre_successor_pointwise_new) -> exists bpvi_factor_bls_legendre_successor_pointwise_new_power bpvi_partial_bls_legendre_successor_pointwise_new_power bpvi_successor_bls_legendre_successor_pointwise_new_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_factor. bpvi_h_bls_legendre_successor_pointwise_new_power_factor + S (bpvi_factor_bls_legendre_successor_pointwise_new_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_factor. bpvi_b_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_factor * S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power) + (bpvi_factor_bls_legendre_successor_pointwise_new_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_partial. bpvi_h_bls_legendre_successor_pointwise_new_power_partial + S (bpvi_partial_bls_legendre_successor_pointwise_new_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_partial. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_partial * S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (bpvi_partial_bls_legendre_successor_pointwise_new_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_successor. bpvi_h_bls_legendre_successor_pointwise_new_power_successor + S (bpvi_successor_bls_legendre_successor_pointwise_new_power) = S ((S (S bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_successor. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_successor * S ((S (S bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (bpvi_successor_bls_legendre_successor_pointwise_new_power))) /\ bpvi_successor_bls_legendre_successor_pointwise_new_power = bpvi_partial_bls_legendre_successor_pointwise_new_power * bpvi_factor_bls_legendre_successor_pointwise_new_power)))))))) /\ ((((exists ff_h_bls_legendre_successor_pointwise_new_quotient_entry. ff_h_bls_legendre_successor_pointwise_new_quotient_entry + S (bls_quotient_legendre_successor_pointwise_new) = S ((S (bls_index_legendre_successor_pointwise_new)) * e)) /\ exists ff_q_bls_legendre_successor_pointwise_new_quotient_entry. d = ff_q_bls_legendre_successor_pointwise_new_quotient_entry * S ((S (bls_index_legendre_successor_pointwise_new)) * e) + (bls_quotient_legendre_successor_pointwise_new))) /\ ((S n = bls_power_legendre_successor_pointwise_new * bls_quotient_legendre_successor_pointwise_new + bls_remainder_legendre_successor_pointwise_new /\ exists bls_remainder_gap_legendre_successor_pointwise_new_division. bls_remainder_gap_legendre_successor_pointwise_new_division + S (bls_remainder_legendre_successor_pointwise_new) = bls_power_legendre_successor_pointwise_new))))) -> (forall eis_index_legendre_successor_pointwise_threshold. (exists eis_lt_gap_legendre_successor_pointwise_threshold_bound. eis_lt_gap_legendre_successor_pointwise_threshold_bound + S (eis_index_legendre_successor_pointwise_threshold) = S n) -> exists eis_bit_legendre_successor_pointwise_threshold. ((((exists ff_h_eis_legendre_successor_pointwise_threshold_decoded. ff_h_eis_legendre_successor_pointwise_threshold_decoded + S (eis_bit_legendre_successor_pointwise_threshold) = S ((S (eis_index_legendre_successor_pointwise_threshold)) * v)) /\ exists ff_q_eis_legendre_successor_pointwise_threshold_decoded. z = ff_q_eis_legendre_successor_pointwise_threshold_decoded * S ((S (eis_index_legendre_successor_pointwise_threshold)) * v) + (eis_bit_legendre_successor_pointwise_threshold))) /\ (((eis_bit_legendre_successor_pointwise_threshold = 1 /\ (exists eis_le_gap_legendre_successor_pointwise_threshold_choice_inside. eis_le_gap_legendre_successor_pointwise_threshold_choice_inside + (S eis_index_legendre_successor_pointwise_threshold) = f)) \/ (eis_bit_legendre_successor_pointwise_threshold = 0 /\ (exists eis_lt_gap_legendre_successor_pointwise_threshold_choice_outside. eis_lt_gap_legendre_successor_pointwise_threshold_choice_outside + S (f) = S eis_index_legendre_successor_pointwise_threshold)))))) -> forall i a bit s. (exists blsr_lt_gap_legendre_successor_pointwise_index. blsr_lt_gap_legendre_successor_pointwise_index + S (i) = (S n)) -> (((exists ff_h_legendre_successor_pointwise_old_entry. ff_h_legendre_successor_pointwise_old_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_legendre_successor_pointwise_old_entry. b = ff_q_legendre_successor_pointwise_old_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_legendre_successor_pointwise_bit_entry. ff_h_legendre_successor_pointwise_bit_entry + S (bit) = S ((S (i)) * v)) /\ exists ff_q_legendre_successor_pointwise_bit_entry. z = ff_q_legendre_successor_pointwise_bit_entry * S ((S (i)) * v) + (bit))) -> (((exists ff_h_legendre_successor_pointwise_new_entry. ff_h_legendre_successor_pointwise_new_entry + S (s) = S ((S (i)) * e)) /\ exists ff_q_legendre_successor_pointwise_new_entry. d = ff_q_legendre_successor_pointwise_new_entry * S ((S (i)) * e) + (s))) -> s = a + bit