prime_exponent_entries_append

Exact expanded first-order arithmetic statement

forall n pb pc eb ec vb vc l p e v. (forall pvs_index_append_old. (exists pvs_gap_append_oldindex. pvs_gap_append_oldindex + S (pvs_index_append_old) = (l)) -> exists pvs_prime_append_old pvs_exponent_append_old pvs_power_append_old. (((((exists ff_h_pvs_append_oldprime. ff_h_pvs_append_oldprime + S (pvs_prime_append_old) = S ((S (pvs_index_append_old)) * pc)) /\ exists ff_q_pvs_append_oldprime. pb = ff_q_pvs_append_oldprime * S ((S (pvs_index_append_old)) * pc) + (pvs_prime_append_old))) /\ (((((exists ff_h_pvs_append_oldexponent. ff_h_pvs_append_oldexponent + S (pvs_exponent_append_old) = S ((S (pvs_index_append_old)) * ec)) /\ exists ff_q_pvs_append_oldexponent. eb = ff_q_pvs_append_oldexponent * S ((S (pvs_index_append_old)) * ec) + (pvs_exponent_append_old))) /\ (((((exists ff_h_pvs_append_oldpower. ff_h_pvs_append_oldpower + S (pvs_power_append_old) = S ((S (pvs_index_append_old)) * vc)) /\ exists ff_q_pvs_append_oldpower. vb = ff_q_pvs_append_oldpower * S ((S (pvs_index_append_old)) * vc) + (pvs_power_append_old))) /\ (((~((pvs_prime_append_old) = 1) /\ forall pvs_left_append_olddomain pvs_right_append_olddomain. (pvs_prime_append_old) = pvs_left_append_olddomain * pvs_right_append_olddomain -> pvs_left_append_olddomain = 1 \/ pvs_right_append_olddomain = 1) /\ (((~(pvs_exponent_append_old = 0)) /\ (((((exists bpd_gap_pvs_append_oldvaluation_selected_bound. bpd_gap_pvs_append_oldvaluation_selected_bound + (pvs_exponent_append_old) = (n)) /\ (exists bpvi_result_pvs_append_oldvaluation_selected. ((exists bpvi_b_pvs_append_oldvaluation_selected_power bpvi_c_pvs_append_oldvaluation_selected_power. ((forall bpvi_i_pvs_append_oldvaluation_selected_power. (exists bpvi_repeat_gap_pvs_append_oldvaluation_selected_power. bpvi_repeat_gap_pvs_append_oldvaluation_selected_power + S bpvi_i_pvs_append_oldvaluation_selected_power = pvs_exponent_append_old) -> (((exists bpvi_h_pvs_append_oldvaluation_selected_power_repeat. bpvi_h_pvs_append_oldvaluation_selected_power_repeat + S (pvs_prime_append_old) = S ((S (bpvi_i_pvs_append_oldvaluation_selected_power)) * bpvi_c_pvs_append_oldvaluation_selected_power)) /\ exists bpvi_q_pvs_append_oldvaluation_selected_power_repeat. bpvi_b_pvs_append_oldvaluation_selected_power = bpvi_q_pvs_append_oldvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_append_oldvaluation_selected_power)) * bpvi_c_pvs_append_oldvaluation_selected_power) + (pvs_prime_append_old)))) /\ (exists bpvi_u_pvs_append_oldvaluation_selected_power bpvi_v_pvs_append_oldvaluation_selected_power. ((((exists bpvi_h_pvs_append_oldvaluation_selected_power_start. bpvi_h_pvs_append_oldvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_append_oldvaluation_selected_power)) /\ exists bpvi_q_pvs_append_oldvaluation_selected_power_start. bpvi_u_pvs_append_oldvaluation_selected_power = bpvi_q_pvs_append_oldvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_append_oldvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_append_oldvaluation_selected_power_terminal. bpvi_h_pvs_append_oldvaluation_selected_power_terminal + S (bpvi_result_pvs_append_oldvaluation_selected) = S ((S (pvs_exponent_append_old)) * bpvi_v_pvs_append_oldvaluation_selected_power)) /\ exists bpvi_q_pvs_append_oldvaluation_selected_power_terminal. bpvi_u_pvs_append_oldvaluation_selected_power = bpvi_q_pvs_append_oldvaluation_selected_power_terminal * S ((S (pvs_exponent_append_old)) * bpvi_v_pvs_append_oldvaluation_selected_power) + (bpvi_result_pvs_append_oldvaluation_selected))) /\ forall bpvi_j_pvs_append_oldvaluation_selected_power. (exists bpvi_product_gap_pvs_append_oldvaluation_selected_power. bpvi_product_gap_pvs_append_oldvaluation_selected_power + S bpvi_j_pvs_append_oldvaluation_selected_power = pvs_exponent_append_old) -> exists bpvi_factor_pvs_append_oldvaluation_selected_power bpvi_partial_pvs_append_oldvaluation_selected_power bpvi_successor_pvs_append_oldvaluation_selected_power. ((((exists bpvi_h_pvs_append_oldvaluation_selected_power_factor. bpvi_h_pvs_append_oldvaluation_selected_power_factor + S (bpvi_factor_pvs_append_oldvaluation_selected_power) = S ((S (bpvi_j_pvs_append_oldvaluation_selected_power)) * bpvi_c_pvs_append_oldvaluation_selected_power)) /\ exists bpvi_q_pvs_append_oldvaluation_selected_power_factor. bpvi_b_pvs_append_oldvaluation_selected_power = bpvi_q_pvs_append_oldvaluation_selected_power_factor * S ((S (bpvi_j_pvs_append_oldvaluation_selected_power)) * bpvi_c_pvs_append_oldvaluation_selected_power) + (bpvi_factor_pvs_append_oldvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_append_oldvaluation_selected_power_partial. bpvi_h_pvs_append_oldvaluation_selected_power_partial + S (bpvi_partial_pvs_append_oldvaluation_selected_power) = S ((S (bpvi_j_pvs_append_oldvaluation_selected_power)) * bpvi_v_pvs_append_oldvaluation_selected_power)) /\ exists bpvi_q_pvs_append_oldvaluation_selected_power_partial. bpvi_u_pvs_append_oldvaluation_selected_power = bpvi_q_pvs_append_oldvaluation_selected_power_partial * S ((S (bpvi_j_pvs_append_oldvaluation_selected_power)) * bpvi_v_pvs_append_oldvaluation_selected_power) + (bpvi_partial_pvs_append_oldvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_append_oldvaluation_selected_power_successor. bpvi_h_pvs_append_oldvaluation_selected_power_successor + S (bpvi_successor_pvs_append_oldvaluation_selected_power) = S ((S (S bpvi_j_pvs_append_oldvaluation_selected_power)) * bpvi_v_pvs_append_oldvaluation_selected_power)) /\ exists bpvi_q_pvs_append_oldvaluation_selected_power_successor. bpvi_u_pvs_append_oldvaluation_selected_power = bpvi_q_pvs_append_oldvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_append_oldvaluation_selected_power)) * bpvi_v_pvs_append_oldvaluation_selected_power) + (bpvi_successor_pvs_append_oldvaluation_selected_power))) /\ bpvi_successor_pvs_append_oldvaluation_selected_power = bpvi_partial_pvs_append_oldvaluation_selected_power * bpvi_factor_pvs_append_oldvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_append_oldvaluation_selected. n = bpvi_result_pvs_append_oldvaluation_selected * bpvi_divisor_factor_pvs_append_oldvaluation_selected))) /\ forall bpd_candidate_pvs_append_oldvaluation. (exists bpd_gap_pvs_append_oldvaluation_candidate_bound. bpd_gap_pvs_append_oldvaluation_candidate_bound + (bpd_candidate_pvs_append_oldvaluation) = (n)) -> (exists bpvi_result_pvs_append_oldvaluation_candidate. ((exists bpvi_b_pvs_append_oldvaluation_candidate_power bpvi_c_pvs_append_oldvaluation_candidate_power. ((forall bpvi_i_pvs_append_oldvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_append_oldvaluation_candidate_power. bpvi_repeat_gap_pvs_append_oldvaluation_candidate_power + S bpvi_i_pvs_append_oldvaluation_candidate_power = bpd_candidate_pvs_append_oldvaluation) -> (((exists bpvi_h_pvs_append_oldvaluation_candidate_power_repeat. bpvi_h_pvs_append_oldvaluation_candidate_power_repeat + S (pvs_prime_append_old) = S ((S (bpvi_i_pvs_append_oldvaluation_candidate_power)) * bpvi_c_pvs_append_oldvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_oldvaluation_candidate_power_repeat. bpvi_b_pvs_append_oldvaluation_candidate_power = bpvi_q_pvs_append_oldvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_append_oldvaluation_candidate_power)) * bpvi_c_pvs_append_oldvaluation_candidate_power) + (pvs_prime_append_old)))) /\ (exists bpvi_u_pvs_append_oldvaluation_candidate_power bpvi_v_pvs_append_oldvaluation_candidate_power. ((((exists bpvi_h_pvs_append_oldvaluation_candidate_power_start. bpvi_h_pvs_append_oldvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_append_oldvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_oldvaluation_candidate_power_start. bpvi_u_pvs_append_oldvaluation_candidate_power = bpvi_q_pvs_append_oldvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_append_oldvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_append_oldvaluation_candidate_power_terminal. bpvi_h_pvs_append_oldvaluation_candidate_power_terminal + S (bpvi_result_pvs_append_oldvaluation_candidate) = S ((S (bpd_candidate_pvs_append_oldvaluation)) * bpvi_v_pvs_append_oldvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_oldvaluation_candidate_power_terminal. bpvi_u_pvs_append_oldvaluation_candidate_power = bpvi_q_pvs_append_oldvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_append_oldvaluation)) * bpvi_v_pvs_append_oldvaluation_candidate_power) + (bpvi_result_pvs_append_oldvaluation_candidate))) /\ forall bpvi_j_pvs_append_oldvaluation_candidate_power. (exists bpvi_product_gap_pvs_append_oldvaluation_candidate_power. bpvi_product_gap_pvs_append_oldvaluation_candidate_power + S bpvi_j_pvs_append_oldvaluation_candidate_power = bpd_candidate_pvs_append_oldvaluation) -> exists bpvi_factor_pvs_append_oldvaluation_candidate_power bpvi_partial_pvs_append_oldvaluation_candidate_power bpvi_successor_pvs_append_oldvaluation_candidate_power. ((((exists bpvi_h_pvs_append_oldvaluation_candidate_power_factor. bpvi_h_pvs_append_oldvaluation_candidate_power_factor + S (bpvi_factor_pvs_append_oldvaluation_candidate_power) = S ((S (bpvi_j_pvs_append_oldvaluation_candidate_power)) * bpvi_c_pvs_append_oldvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_oldvaluation_candidate_power_factor. bpvi_b_pvs_append_oldvaluation_candidate_power = bpvi_q_pvs_append_oldvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_append_oldvaluation_candidate_power)) * bpvi_c_pvs_append_oldvaluation_candidate_power) + (bpvi_factor_pvs_append_oldvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_append_oldvaluation_candidate_power_partial. bpvi_h_pvs_append_oldvaluation_candidate_power_partial + S (bpvi_partial_pvs_append_oldvaluation_candidate_power) = S ((S (bpvi_j_pvs_append_oldvaluation_candidate_power)) * bpvi_v_pvs_append_oldvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_oldvaluation_candidate_power_partial. bpvi_u_pvs_append_oldvaluation_candidate_power = bpvi_q_pvs_append_oldvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_append_oldvaluation_candidate_power)) * bpvi_v_pvs_append_oldvaluation_candidate_power) + (bpvi_partial_pvs_append_oldvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_append_oldvaluation_candidate_power_successor. bpvi_h_pvs_append_oldvaluation_candidate_power_successor + S (bpvi_successor_pvs_append_oldvaluation_candidate_power) = S ((S (S bpvi_j_pvs_append_oldvaluation_candidate_power)) * bpvi_v_pvs_append_oldvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_oldvaluation_candidate_power_successor. bpvi_u_pvs_append_oldvaluation_candidate_power = bpvi_q_pvs_append_oldvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_append_oldvaluation_candidate_power)) * bpvi_v_pvs_append_oldvaluation_candidate_power) + (bpvi_successor_pvs_append_oldvaluation_candidate_power))) /\ bpvi_successor_pvs_append_oldvaluation_candidate_power = bpvi_partial_pvs_append_oldvaluation_candidate_power * bpvi_factor_pvs_append_oldvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_append_oldvaluation_candidate. n = bpvi_result_pvs_append_oldvaluation_candidate * bpvi_divisor_factor_pvs_append_oldvaluation_candidate)) -> (exists bpd_gap_pvs_append_oldvaluation_maximal. bpd_gap_pvs_append_oldvaluation_maximal + (bpd_candidate_pvs_append_oldvaluation) = (pvs_exponent_append_old))) /\ (exists pa_b_pvs_append_oldvalue pa_c_pvs_append_oldvalue. ((forall pa_i_pvs_append_oldvalue_repeat. (exists pa_lt_pvs_append_oldvalue_repeat_bound. pa_lt_pvs_append_oldvalue_repeat_bound + S pa_i_pvs_append_oldvalue_repeat = pvs_exponent_append_old) -> (((exists pa_h_pvs_append_oldvalue_repeat_decoded. pa_h_pvs_append_oldvalue_repeat_decoded + S (pvs_prime_append_old) = S ((S (pa_i_pvs_append_oldvalue_repeat)) * pa_c_pvs_append_oldvalue)) /\ exists pa_q_pvs_append_oldvalue_repeat_decoded. pa_b_pvs_append_oldvalue = pa_q_pvs_append_oldvalue_repeat_decoded * S ((S (pa_i_pvs_append_oldvalue_repeat)) * pa_c_pvs_append_oldvalue) + (pvs_prime_append_old)))) /\ (exists pa_u_pvs_append_oldvalue_product pa_v_pvs_append_oldvalue_product. ((((exists pa_h_pvs_append_oldvalue_product_start. pa_h_pvs_append_oldvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_append_oldvalue_product)) /\ exists pa_q_pvs_append_oldvalue_product_start. pa_u_pvs_append_oldvalue_product = pa_q_pvs_append_oldvalue_product_start * S ((S (0)) * pa_v_pvs_append_oldvalue_product) + (1))) /\ ((((exists pa_h_pvs_append_oldvalue_product_terminal. pa_h_pvs_append_oldvalue_product_terminal + S (pvs_power_append_old) = S ((S (pvs_exponent_append_old)) * pa_v_pvs_append_oldvalue_product)) /\ exists pa_q_pvs_append_oldvalue_product_terminal. pa_u_pvs_append_oldvalue_product = pa_q_pvs_append_oldvalue_product_terminal * S ((S (pvs_exponent_append_old)) * pa_v_pvs_append_oldvalue_product) + (pvs_power_append_old))) /\ forall pa_i_pvs_append_oldvalue_product. (exists pa_lt_pvs_append_oldvalue_product_bound. pa_lt_pvs_append_oldvalue_product_bound + S pa_i_pvs_append_oldvalue_product = pvs_exponent_append_old) -> exists pa_p_pvs_append_oldvalue_product pa_r_pvs_append_oldvalue_product pa_s_pvs_append_oldvalue_product. ((((exists pa_h_pvs_append_oldvalue_product_factor. pa_h_pvs_append_oldvalue_product_factor + S (pa_p_pvs_append_oldvalue_product) = S ((S (pa_i_pvs_append_oldvalue_product)) * pa_c_pvs_append_oldvalue)) /\ exists pa_q_pvs_append_oldvalue_product_factor. pa_b_pvs_append_oldvalue = pa_q_pvs_append_oldvalue_product_factor * S ((S (pa_i_pvs_append_oldvalue_product)) * pa_c_pvs_append_oldvalue) + (pa_p_pvs_append_oldvalue_product))) /\ ((((exists pa_h_pvs_append_oldvalue_product_partial. pa_h_pvs_append_oldvalue_product_partial + S (pa_r_pvs_append_oldvalue_product) = S ((S (pa_i_pvs_append_oldvalue_product)) * pa_v_pvs_append_oldvalue_product)) /\ exists pa_q_pvs_append_oldvalue_product_partial. pa_u_pvs_append_oldvalue_product = pa_q_pvs_append_oldvalue_product_partial * S ((S (pa_i_pvs_append_oldvalue_product)) * pa_v_pvs_append_oldvalue_product) + (pa_r_pvs_append_oldvalue_product))) /\ ((((exists pa_h_pvs_append_oldvalue_product_successor. pa_h_pvs_append_oldvalue_product_successor + S (pa_s_pvs_append_oldvalue_product) = S ((S (S pa_i_pvs_append_oldvalue_product)) * pa_v_pvs_append_oldvalue_product)) /\ exists pa_q_pvs_append_oldvalue_product_successor. pa_u_pvs_append_oldvalue_product = pa_q_pvs_append_oldvalue_product_successor * S ((S (S pa_i_pvs_append_oldvalue_product)) * pa_v_pvs_append_oldvalue_product) + (pa_s_pvs_append_oldvalue_product))) /\ pa_s_pvs_append_oldvalue_product = pa_r_pvs_append_oldvalue_product * pa_p_pvs_append_oldvalue_product))))))))))))))))))))) -> (((((exists ff_h_pvs_append_lastprime. ff_h_pvs_append_lastprime + S (p) = S ((S (l)) * pc)) /\ exists ff_q_pvs_append_lastprime. pb = ff_q_pvs_append_lastprime * S ((S (l)) * pc) + (p))) /\ (((((exists ff_h_pvs_append_lastexponent. ff_h_pvs_append_lastexponent + S (e) = S ((S (l)) * ec)) /\ exists ff_q_pvs_append_lastexponent. eb = ff_q_pvs_append_lastexponent * S ((S (l)) * ec) + (e))) /\ (((((exists ff_h_pvs_append_lastpower. ff_h_pvs_append_lastpower + S (v) = S ((S (l)) * vc)) /\ exists ff_q_pvs_append_lastpower. vb = ff_q_pvs_append_lastpower * S ((S (l)) * vc) + (v))) /\ (((~((p) = 1) /\ forall pvs_left_append_lastdomain pvs_right_append_lastdomain. (p) = pvs_left_append_lastdomain * pvs_right_append_lastdomain -> pvs_left_append_lastdomain = 1 \/ pvs_right_append_lastdomain = 1) /\ (((~(e = 0)) /\ (((((exists bpd_gap_pvs_append_lastvaluation_selected_bound. bpd_gap_pvs_append_lastvaluation_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_append_lastvaluation_selected. ((exists bpvi_b_pvs_append_lastvaluation_selected_power bpvi_c_pvs_append_lastvaluation_selected_power. ((forall bpvi_i_pvs_append_lastvaluation_selected_power. (exists bpvi_repeat_gap_pvs_append_lastvaluation_selected_power. bpvi_repeat_gap_pvs_append_lastvaluation_selected_power + S bpvi_i_pvs_append_lastvaluation_selected_power = e) -> (((exists bpvi_h_pvs_append_lastvaluation_selected_power_repeat. bpvi_h_pvs_append_lastvaluation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_append_lastvaluation_selected_power)) * bpvi_c_pvs_append_lastvaluation_selected_power)) /\ exists bpvi_q_pvs_append_lastvaluation_selected_power_repeat. bpvi_b_pvs_append_lastvaluation_selected_power = bpvi_q_pvs_append_lastvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_append_lastvaluation_selected_power)) * bpvi_c_pvs_append_lastvaluation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_append_lastvaluation_selected_power bpvi_v_pvs_append_lastvaluation_selected_power. ((((exists bpvi_h_pvs_append_lastvaluation_selected_power_start. bpvi_h_pvs_append_lastvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_append_lastvaluation_selected_power)) /\ exists bpvi_q_pvs_append_lastvaluation_selected_power_start. bpvi_u_pvs_append_lastvaluation_selected_power = bpvi_q_pvs_append_lastvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_append_lastvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_append_lastvaluation_selected_power_terminal. bpvi_h_pvs_append_lastvaluation_selected_power_terminal + S (bpvi_result_pvs_append_lastvaluation_selected) = S ((S (e)) * bpvi_v_pvs_append_lastvaluation_selected_power)) /\ exists bpvi_q_pvs_append_lastvaluation_selected_power_terminal. bpvi_u_pvs_append_lastvaluation_selected_power = bpvi_q_pvs_append_lastvaluation_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_append_lastvaluation_selected_power) + (bpvi_result_pvs_append_lastvaluation_selected))) /\ forall bpvi_j_pvs_append_lastvaluation_selected_power. (exists bpvi_product_gap_pvs_append_lastvaluation_selected_power. bpvi_product_gap_pvs_append_lastvaluation_selected_power + S bpvi_j_pvs_append_lastvaluation_selected_power = e) -> exists bpvi_factor_pvs_append_lastvaluation_selected_power bpvi_partial_pvs_append_lastvaluation_selected_power bpvi_successor_pvs_append_lastvaluation_selected_power. ((((exists bpvi_h_pvs_append_lastvaluation_selected_power_factor. bpvi_h_pvs_append_lastvaluation_selected_power_factor + S (bpvi_factor_pvs_append_lastvaluation_selected_power) = S ((S (bpvi_j_pvs_append_lastvaluation_selected_power)) * bpvi_c_pvs_append_lastvaluation_selected_power)) /\ exists bpvi_q_pvs_append_lastvaluation_selected_power_factor. bpvi_b_pvs_append_lastvaluation_selected_power = bpvi_q_pvs_append_lastvaluation_selected_power_factor * S ((S (bpvi_j_pvs_append_lastvaluation_selected_power)) * bpvi_c_pvs_append_lastvaluation_selected_power) + (bpvi_factor_pvs_append_lastvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_append_lastvaluation_selected_power_partial. bpvi_h_pvs_append_lastvaluation_selected_power_partial + S (bpvi_partial_pvs_append_lastvaluation_selected_power) = S ((S (bpvi_j_pvs_append_lastvaluation_selected_power)) * bpvi_v_pvs_append_lastvaluation_selected_power)) /\ exists bpvi_q_pvs_append_lastvaluation_selected_power_partial. bpvi_u_pvs_append_lastvaluation_selected_power = bpvi_q_pvs_append_lastvaluation_selected_power_partial * S ((S (bpvi_j_pvs_append_lastvaluation_selected_power)) * bpvi_v_pvs_append_lastvaluation_selected_power) + (bpvi_partial_pvs_append_lastvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_append_lastvaluation_selected_power_successor. bpvi_h_pvs_append_lastvaluation_selected_power_successor + S (bpvi_successor_pvs_append_lastvaluation_selected_power) = S ((S (S bpvi_j_pvs_append_lastvaluation_selected_power)) * bpvi_v_pvs_append_lastvaluation_selected_power)) /\ exists bpvi_q_pvs_append_lastvaluation_selected_power_successor. bpvi_u_pvs_append_lastvaluation_selected_power = bpvi_q_pvs_append_lastvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_append_lastvaluation_selected_power)) * bpvi_v_pvs_append_lastvaluation_selected_power) + (bpvi_successor_pvs_append_lastvaluation_selected_power))) /\ bpvi_successor_pvs_append_lastvaluation_selected_power = bpvi_partial_pvs_append_lastvaluation_selected_power * bpvi_factor_pvs_append_lastvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_append_lastvaluation_selected. n = bpvi_result_pvs_append_lastvaluation_selected * bpvi_divisor_factor_pvs_append_lastvaluation_selected))) /\ forall bpd_candidate_pvs_append_lastvaluation. (exists bpd_gap_pvs_append_lastvaluation_candidate_bound. bpd_gap_pvs_append_lastvaluation_candidate_bound + (bpd_candidate_pvs_append_lastvaluation) = (n)) -> (exists bpvi_result_pvs_append_lastvaluation_candidate. ((exists bpvi_b_pvs_append_lastvaluation_candidate_power bpvi_c_pvs_append_lastvaluation_candidate_power. ((forall bpvi_i_pvs_append_lastvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_append_lastvaluation_candidate_power. bpvi_repeat_gap_pvs_append_lastvaluation_candidate_power + S bpvi_i_pvs_append_lastvaluation_candidate_power = bpd_candidate_pvs_append_lastvaluation) -> (((exists bpvi_h_pvs_append_lastvaluation_candidate_power_repeat. bpvi_h_pvs_append_lastvaluation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_append_lastvaluation_candidate_power)) * bpvi_c_pvs_append_lastvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_lastvaluation_candidate_power_repeat. bpvi_b_pvs_append_lastvaluation_candidate_power = bpvi_q_pvs_append_lastvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_append_lastvaluation_candidate_power)) * bpvi_c_pvs_append_lastvaluation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_append_lastvaluation_candidate_power bpvi_v_pvs_append_lastvaluation_candidate_power. ((((exists bpvi_h_pvs_append_lastvaluation_candidate_power_start. bpvi_h_pvs_append_lastvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_append_lastvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_lastvaluation_candidate_power_start. bpvi_u_pvs_append_lastvaluation_candidate_power = bpvi_q_pvs_append_lastvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_append_lastvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_append_lastvaluation_candidate_power_terminal. bpvi_h_pvs_append_lastvaluation_candidate_power_terminal + S (bpvi_result_pvs_append_lastvaluation_candidate) = S ((S (bpd_candidate_pvs_append_lastvaluation)) * bpvi_v_pvs_append_lastvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_lastvaluation_candidate_power_terminal. bpvi_u_pvs_append_lastvaluation_candidate_power = bpvi_q_pvs_append_lastvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_append_lastvaluation)) * bpvi_v_pvs_append_lastvaluation_candidate_power) + (bpvi_result_pvs_append_lastvaluation_candidate))) /\ forall bpvi_j_pvs_append_lastvaluation_candidate_power. (exists bpvi_product_gap_pvs_append_lastvaluation_candidate_power. bpvi_product_gap_pvs_append_lastvaluation_candidate_power + S bpvi_j_pvs_append_lastvaluation_candidate_power = bpd_candidate_pvs_append_lastvaluation) -> exists bpvi_factor_pvs_append_lastvaluation_candidate_power bpvi_partial_pvs_append_lastvaluation_candidate_power bpvi_successor_pvs_append_lastvaluation_candidate_power. ((((exists bpvi_h_pvs_append_lastvaluation_candidate_power_factor. bpvi_h_pvs_append_lastvaluation_candidate_power_factor + S (bpvi_factor_pvs_append_lastvaluation_candidate_power) = S ((S (bpvi_j_pvs_append_lastvaluation_candidate_power)) * bpvi_c_pvs_append_lastvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_lastvaluation_candidate_power_factor. bpvi_b_pvs_append_lastvaluation_candidate_power = bpvi_q_pvs_append_lastvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_append_lastvaluation_candidate_power)) * bpvi_c_pvs_append_lastvaluation_candidate_power) + (bpvi_factor_pvs_append_lastvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_append_lastvaluation_candidate_power_partial. bpvi_h_pvs_append_lastvaluation_candidate_power_partial + S (bpvi_partial_pvs_append_lastvaluation_candidate_power) = S ((S (bpvi_j_pvs_append_lastvaluation_candidate_power)) * bpvi_v_pvs_append_lastvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_lastvaluation_candidate_power_partial. bpvi_u_pvs_append_lastvaluation_candidate_power = bpvi_q_pvs_append_lastvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_append_lastvaluation_candidate_power)) * bpvi_v_pvs_append_lastvaluation_candidate_power) + (bpvi_partial_pvs_append_lastvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_append_lastvaluation_candidate_power_successor. bpvi_h_pvs_append_lastvaluation_candidate_power_successor + S (bpvi_successor_pvs_append_lastvaluation_candidate_power) = S ((S (S bpvi_j_pvs_append_lastvaluation_candidate_power)) * bpvi_v_pvs_append_lastvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_lastvaluation_candidate_power_successor. bpvi_u_pvs_append_lastvaluation_candidate_power = bpvi_q_pvs_append_lastvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_append_lastvaluation_candidate_power)) * bpvi_v_pvs_append_lastvaluation_candidate_power) + (bpvi_successor_pvs_append_lastvaluation_candidate_power))) /\ bpvi_successor_pvs_append_lastvaluation_candidate_power = bpvi_partial_pvs_append_lastvaluation_candidate_power * bpvi_factor_pvs_append_lastvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_append_lastvaluation_candidate. n = bpvi_result_pvs_append_lastvaluation_candidate * bpvi_divisor_factor_pvs_append_lastvaluation_candidate)) -> (exists bpd_gap_pvs_append_lastvaluation_maximal. bpd_gap_pvs_append_lastvaluation_maximal + (bpd_candidate_pvs_append_lastvaluation) = (e))) /\ (exists pa_b_pvs_append_lastvalue pa_c_pvs_append_lastvalue. ((forall pa_i_pvs_append_lastvalue_repeat. (exists pa_lt_pvs_append_lastvalue_repeat_bound. pa_lt_pvs_append_lastvalue_repeat_bound + S pa_i_pvs_append_lastvalue_repeat = e) -> (((exists pa_h_pvs_append_lastvalue_repeat_decoded. pa_h_pvs_append_lastvalue_repeat_decoded + S (p) = S ((S (pa_i_pvs_append_lastvalue_repeat)) * pa_c_pvs_append_lastvalue)) /\ exists pa_q_pvs_append_lastvalue_repeat_decoded. pa_b_pvs_append_lastvalue = pa_q_pvs_append_lastvalue_repeat_decoded * S ((S (pa_i_pvs_append_lastvalue_repeat)) * pa_c_pvs_append_lastvalue) + (p)))) /\ (exists pa_u_pvs_append_lastvalue_product pa_v_pvs_append_lastvalue_product. ((((exists pa_h_pvs_append_lastvalue_product_start. pa_h_pvs_append_lastvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_append_lastvalue_product)) /\ exists pa_q_pvs_append_lastvalue_product_start. pa_u_pvs_append_lastvalue_product = pa_q_pvs_append_lastvalue_product_start * S ((S (0)) * pa_v_pvs_append_lastvalue_product) + (1))) /\ ((((exists pa_h_pvs_append_lastvalue_product_terminal. pa_h_pvs_append_lastvalue_product_terminal + S (v) = S ((S (e)) * pa_v_pvs_append_lastvalue_product)) /\ exists pa_q_pvs_append_lastvalue_product_terminal. pa_u_pvs_append_lastvalue_product = pa_q_pvs_append_lastvalue_product_terminal * S ((S (e)) * pa_v_pvs_append_lastvalue_product) + (v))) /\ forall pa_i_pvs_append_lastvalue_product. (exists pa_lt_pvs_append_lastvalue_product_bound. pa_lt_pvs_append_lastvalue_product_bound + S pa_i_pvs_append_lastvalue_product = e) -> exists pa_p_pvs_append_lastvalue_product pa_r_pvs_append_lastvalue_product pa_s_pvs_append_lastvalue_product. ((((exists pa_h_pvs_append_lastvalue_product_factor. pa_h_pvs_append_lastvalue_product_factor + S (pa_p_pvs_append_lastvalue_product) = S ((S (pa_i_pvs_append_lastvalue_product)) * pa_c_pvs_append_lastvalue)) /\ exists pa_q_pvs_append_lastvalue_product_factor. pa_b_pvs_append_lastvalue = pa_q_pvs_append_lastvalue_product_factor * S ((S (pa_i_pvs_append_lastvalue_product)) * pa_c_pvs_append_lastvalue) + (pa_p_pvs_append_lastvalue_product))) /\ ((((exists pa_h_pvs_append_lastvalue_product_partial. pa_h_pvs_append_lastvalue_product_partial + S (pa_r_pvs_append_lastvalue_product) = S ((S (pa_i_pvs_append_lastvalue_product)) * pa_v_pvs_append_lastvalue_product)) /\ exists pa_q_pvs_append_lastvalue_product_partial. pa_u_pvs_append_lastvalue_product = pa_q_pvs_append_lastvalue_product_partial * S ((S (pa_i_pvs_append_lastvalue_product)) * pa_v_pvs_append_lastvalue_product) + (pa_r_pvs_append_lastvalue_product))) /\ ((((exists pa_h_pvs_append_lastvalue_product_successor. pa_h_pvs_append_lastvalue_product_successor + S (pa_s_pvs_append_lastvalue_product) = S ((S (S pa_i_pvs_append_lastvalue_product)) * pa_v_pvs_append_lastvalue_product)) /\ exists pa_q_pvs_append_lastvalue_product_successor. pa_u_pvs_append_lastvalue_product = pa_q_pvs_append_lastvalue_product_successor * S ((S (S pa_i_pvs_append_lastvalue_product)) * pa_v_pvs_append_lastvalue_product) + (pa_s_pvs_append_lastvalue_product))) /\ pa_s_pvs_append_lastvalue_product = pa_r_pvs_append_lastvalue_product * pa_p_pvs_append_lastvalue_product)))))))))))))))))))) -> (forall pvs_index_append_next. (exists pvs_gap_append_nextindex. pvs_gap_append_nextindex + S (pvs_index_append_next) = (S l)) -> exists pvs_prime_append_next pvs_exponent_append_next pvs_power_append_next. (((((exists ff_h_pvs_append_nextprime. ff_h_pvs_append_nextprime + S (pvs_prime_append_next) = S ((S (pvs_index_append_next)) * pc)) /\ exists ff_q_pvs_append_nextprime. pb = ff_q_pvs_append_nextprime * S ((S (pvs_index_append_next)) * pc) + (pvs_prime_append_next))) /\ (((((exists ff_h_pvs_append_nextexponent. ff_h_pvs_append_nextexponent + S (pvs_exponent_append_next) = S ((S (pvs_index_append_next)) * ec)) /\ exists ff_q_pvs_append_nextexponent. eb = ff_q_pvs_append_nextexponent * S ((S (pvs_index_append_next)) * ec) + (pvs_exponent_append_next))) /\ (((((exists ff_h_pvs_append_nextpower. ff_h_pvs_append_nextpower + S (pvs_power_append_next) = S ((S (pvs_index_append_next)) * vc)) /\ exists ff_q_pvs_append_nextpower. vb = ff_q_pvs_append_nextpower * S ((S (pvs_index_append_next)) * vc) + (pvs_power_append_next))) /\ (((~((pvs_prime_append_next) = 1) /\ forall pvs_left_append_nextdomain pvs_right_append_nextdomain. (pvs_prime_append_next) = pvs_left_append_nextdomain * pvs_right_append_nextdomain -> pvs_left_append_nextdomain = 1 \/ pvs_right_append_nextdomain = 1) /\ (((~(pvs_exponent_append_next = 0)) /\ (((((exists bpd_gap_pvs_append_nextvaluation_selected_bound. bpd_gap_pvs_append_nextvaluation_selected_bound + (pvs_exponent_append_next) = (n)) /\ (exists bpvi_result_pvs_append_nextvaluation_selected. ((exists bpvi_b_pvs_append_nextvaluation_selected_power bpvi_c_pvs_append_nextvaluation_selected_power. ((forall bpvi_i_pvs_append_nextvaluation_selected_power. (exists bpvi_repeat_gap_pvs_append_nextvaluation_selected_power. bpvi_repeat_gap_pvs_append_nextvaluation_selected_power + S bpvi_i_pvs_append_nextvaluation_selected_power = pvs_exponent_append_next) -> (((exists bpvi_h_pvs_append_nextvaluation_selected_power_repeat. bpvi_h_pvs_append_nextvaluation_selected_power_repeat + S (pvs_prime_append_next) = S ((S (bpvi_i_pvs_append_nextvaluation_selected_power)) * bpvi_c_pvs_append_nextvaluation_selected_power)) /\ exists bpvi_q_pvs_append_nextvaluation_selected_power_repeat. bpvi_b_pvs_append_nextvaluation_selected_power = bpvi_q_pvs_append_nextvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_append_nextvaluation_selected_power)) * bpvi_c_pvs_append_nextvaluation_selected_power) + (pvs_prime_append_next)))) /\ (exists bpvi_u_pvs_append_nextvaluation_selected_power bpvi_v_pvs_append_nextvaluation_selected_power. ((((exists bpvi_h_pvs_append_nextvaluation_selected_power_start. bpvi_h_pvs_append_nextvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_append_nextvaluation_selected_power)) /\ exists bpvi_q_pvs_append_nextvaluation_selected_power_start. bpvi_u_pvs_append_nextvaluation_selected_power = bpvi_q_pvs_append_nextvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_append_nextvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_append_nextvaluation_selected_power_terminal. bpvi_h_pvs_append_nextvaluation_selected_power_terminal + S (bpvi_result_pvs_append_nextvaluation_selected) = S ((S (pvs_exponent_append_next)) * bpvi_v_pvs_append_nextvaluation_selected_power)) /\ exists bpvi_q_pvs_append_nextvaluation_selected_power_terminal. bpvi_u_pvs_append_nextvaluation_selected_power = bpvi_q_pvs_append_nextvaluation_selected_power_terminal * S ((S (pvs_exponent_append_next)) * bpvi_v_pvs_append_nextvaluation_selected_power) + (bpvi_result_pvs_append_nextvaluation_selected))) /\ forall bpvi_j_pvs_append_nextvaluation_selected_power. (exists bpvi_product_gap_pvs_append_nextvaluation_selected_power. bpvi_product_gap_pvs_append_nextvaluation_selected_power + S bpvi_j_pvs_append_nextvaluation_selected_power = pvs_exponent_append_next) -> exists bpvi_factor_pvs_append_nextvaluation_selected_power bpvi_partial_pvs_append_nextvaluation_selected_power bpvi_successor_pvs_append_nextvaluation_selected_power. ((((exists bpvi_h_pvs_append_nextvaluation_selected_power_factor. bpvi_h_pvs_append_nextvaluation_selected_power_factor + S (bpvi_factor_pvs_append_nextvaluation_selected_power) = S ((S (bpvi_j_pvs_append_nextvaluation_selected_power)) * bpvi_c_pvs_append_nextvaluation_selected_power)) /\ exists bpvi_q_pvs_append_nextvaluation_selected_power_factor. bpvi_b_pvs_append_nextvaluation_selected_power = bpvi_q_pvs_append_nextvaluation_selected_power_factor * S ((S (bpvi_j_pvs_append_nextvaluation_selected_power)) * bpvi_c_pvs_append_nextvaluation_selected_power) + (bpvi_factor_pvs_append_nextvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_append_nextvaluation_selected_power_partial. bpvi_h_pvs_append_nextvaluation_selected_power_partial + S (bpvi_partial_pvs_append_nextvaluation_selected_power) = S ((S (bpvi_j_pvs_append_nextvaluation_selected_power)) * bpvi_v_pvs_append_nextvaluation_selected_power)) /\ exists bpvi_q_pvs_append_nextvaluation_selected_power_partial. bpvi_u_pvs_append_nextvaluation_selected_power = bpvi_q_pvs_append_nextvaluation_selected_power_partial * S ((S (bpvi_j_pvs_append_nextvaluation_selected_power)) * bpvi_v_pvs_append_nextvaluation_selected_power) + (bpvi_partial_pvs_append_nextvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_append_nextvaluation_selected_power_successor. bpvi_h_pvs_append_nextvaluation_selected_power_successor + S (bpvi_successor_pvs_append_nextvaluation_selected_power) = S ((S (S bpvi_j_pvs_append_nextvaluation_selected_power)) * bpvi_v_pvs_append_nextvaluation_selected_power)) /\ exists bpvi_q_pvs_append_nextvaluation_selected_power_successor. bpvi_u_pvs_append_nextvaluation_selected_power = bpvi_q_pvs_append_nextvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_append_nextvaluation_selected_power)) * bpvi_v_pvs_append_nextvaluation_selected_power) + (bpvi_successor_pvs_append_nextvaluation_selected_power))) /\ bpvi_successor_pvs_append_nextvaluation_selected_power = bpvi_partial_pvs_append_nextvaluation_selected_power * bpvi_factor_pvs_append_nextvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_append_nextvaluation_selected. n = bpvi_result_pvs_append_nextvaluation_selected * bpvi_divisor_factor_pvs_append_nextvaluation_selected))) /\ forall bpd_candidate_pvs_append_nextvaluation. (exists bpd_gap_pvs_append_nextvaluation_candidate_bound. bpd_gap_pvs_append_nextvaluation_candidate_bound + (bpd_candidate_pvs_append_nextvaluation) = (n)) -> (exists bpvi_result_pvs_append_nextvaluation_candidate. ((exists bpvi_b_pvs_append_nextvaluation_candidate_power bpvi_c_pvs_append_nextvaluation_candidate_power. ((forall bpvi_i_pvs_append_nextvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_append_nextvaluation_candidate_power. bpvi_repeat_gap_pvs_append_nextvaluation_candidate_power + S bpvi_i_pvs_append_nextvaluation_candidate_power = bpd_candidate_pvs_append_nextvaluation) -> (((exists bpvi_h_pvs_append_nextvaluation_candidate_power_repeat. bpvi_h_pvs_append_nextvaluation_candidate_power_repeat + S (pvs_prime_append_next) = S ((S (bpvi_i_pvs_append_nextvaluation_candidate_power)) * bpvi_c_pvs_append_nextvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_nextvaluation_candidate_power_repeat. bpvi_b_pvs_append_nextvaluation_candidate_power = bpvi_q_pvs_append_nextvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_append_nextvaluation_candidate_power)) * bpvi_c_pvs_append_nextvaluation_candidate_power) + (pvs_prime_append_next)))) /\ (exists bpvi_u_pvs_append_nextvaluation_candidate_power bpvi_v_pvs_append_nextvaluation_candidate_power. ((((exists bpvi_h_pvs_append_nextvaluation_candidate_power_start. bpvi_h_pvs_append_nextvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_append_nextvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_nextvaluation_candidate_power_start. bpvi_u_pvs_append_nextvaluation_candidate_power = bpvi_q_pvs_append_nextvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_append_nextvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_append_nextvaluation_candidate_power_terminal. bpvi_h_pvs_append_nextvaluation_candidate_power_terminal + S (bpvi_result_pvs_append_nextvaluation_candidate) = S ((S (bpd_candidate_pvs_append_nextvaluation)) * bpvi_v_pvs_append_nextvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_nextvaluation_candidate_power_terminal. bpvi_u_pvs_append_nextvaluation_candidate_power = bpvi_q_pvs_append_nextvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_append_nextvaluation)) * bpvi_v_pvs_append_nextvaluation_candidate_power) + (bpvi_result_pvs_append_nextvaluation_candidate))) /\ forall bpvi_j_pvs_append_nextvaluation_candidate_power. (exists bpvi_product_gap_pvs_append_nextvaluation_candidate_power. bpvi_product_gap_pvs_append_nextvaluation_candidate_power + S bpvi_j_pvs_append_nextvaluation_candidate_power = bpd_candidate_pvs_append_nextvaluation) -> exists bpvi_factor_pvs_append_nextvaluation_candidate_power bpvi_partial_pvs_append_nextvaluation_candidate_power bpvi_successor_pvs_append_nextvaluation_candidate_power. ((((exists bpvi_h_pvs_append_nextvaluation_candidate_power_factor. bpvi_h_pvs_append_nextvaluation_candidate_power_factor + S (bpvi_factor_pvs_append_nextvaluation_candidate_power) = S ((S (bpvi_j_pvs_append_nextvaluation_candidate_power)) * bpvi_c_pvs_append_nextvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_nextvaluation_candidate_power_factor. bpvi_b_pvs_append_nextvaluation_candidate_power = bpvi_q_pvs_append_nextvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_append_nextvaluation_candidate_power)) * bpvi_c_pvs_append_nextvaluation_candidate_power) + (bpvi_factor_pvs_append_nextvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_append_nextvaluation_candidate_power_partial. bpvi_h_pvs_append_nextvaluation_candidate_power_partial + S (bpvi_partial_pvs_append_nextvaluation_candidate_power) = S ((S (bpvi_j_pvs_append_nextvaluation_candidate_power)) * bpvi_v_pvs_append_nextvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_nextvaluation_candidate_power_partial. bpvi_u_pvs_append_nextvaluation_candidate_power = bpvi_q_pvs_append_nextvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_append_nextvaluation_candidate_power)) * bpvi_v_pvs_append_nextvaluation_candidate_power) + (bpvi_partial_pvs_append_nextvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_append_nextvaluation_candidate_power_successor. bpvi_h_pvs_append_nextvaluation_candidate_power_successor + S (bpvi_successor_pvs_append_nextvaluation_candidate_power) = S ((S (S bpvi_j_pvs_append_nextvaluation_candidate_power)) * bpvi_v_pvs_append_nextvaluation_candidate_power)) /\ exists bpvi_q_pvs_append_nextvaluation_candidate_power_successor. bpvi_u_pvs_append_nextvaluation_candidate_power = bpvi_q_pvs_append_nextvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_append_nextvaluation_candidate_power)) * bpvi_v_pvs_append_nextvaluation_candidate_power) + (bpvi_successor_pvs_append_nextvaluation_candidate_power))) /\ bpvi_successor_pvs_append_nextvaluation_candidate_power = bpvi_partial_pvs_append_nextvaluation_candidate_power * bpvi_factor_pvs_append_nextvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_append_nextvaluation_candidate. n = bpvi_result_pvs_append_nextvaluation_candidate * bpvi_divisor_factor_pvs_append_nextvaluation_candidate)) -> (exists bpd_gap_pvs_append_nextvaluation_maximal. bpd_gap_pvs_append_nextvaluation_maximal + (bpd_candidate_pvs_append_nextvaluation) = (pvs_exponent_append_next))) /\ (exists pa_b_pvs_append_nextvalue pa_c_pvs_append_nextvalue. ((forall pa_i_pvs_append_nextvalue_repeat. (exists pa_lt_pvs_append_nextvalue_repeat_bound. pa_lt_pvs_append_nextvalue_repeat_bound + S pa_i_pvs_append_nextvalue_repeat = pvs_exponent_append_next) -> (((exists pa_h_pvs_append_nextvalue_repeat_decoded. pa_h_pvs_append_nextvalue_repeat_decoded + S (pvs_prime_append_next) = S ((S (pa_i_pvs_append_nextvalue_repeat)) * pa_c_pvs_append_nextvalue)) /\ exists pa_q_pvs_append_nextvalue_repeat_decoded. pa_b_pvs_append_nextvalue = pa_q_pvs_append_nextvalue_repeat_decoded * S ((S (pa_i_pvs_append_nextvalue_repeat)) * pa_c_pvs_append_nextvalue) + (pvs_prime_append_next)))) /\ (exists pa_u_pvs_append_nextvalue_product pa_v_pvs_append_nextvalue_product. ((((exists pa_h_pvs_append_nextvalue_product_start. pa_h_pvs_append_nextvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_append_nextvalue_product)) /\ exists pa_q_pvs_append_nextvalue_product_start. pa_u_pvs_append_nextvalue_product = pa_q_pvs_append_nextvalue_product_start * S ((S (0)) * pa_v_pvs_append_nextvalue_product) + (1))) /\ ((((exists pa_h_pvs_append_nextvalue_product_terminal. pa_h_pvs_append_nextvalue_product_terminal + S (pvs_power_append_next) = S ((S (pvs_exponent_append_next)) * pa_v_pvs_append_nextvalue_product)) /\ exists pa_q_pvs_append_nextvalue_product_terminal. pa_u_pvs_append_nextvalue_product = pa_q_pvs_append_nextvalue_product_terminal * S ((S (pvs_exponent_append_next)) * pa_v_pvs_append_nextvalue_product) + (pvs_power_append_next))) /\ forall pa_i_pvs_append_nextvalue_product. (exists pa_lt_pvs_append_nextvalue_product_bound. pa_lt_pvs_append_nextvalue_product_bound + S pa_i_pvs_append_nextvalue_product = pvs_exponent_append_next) -> exists pa_p_pvs_append_nextvalue_product pa_r_pvs_append_nextvalue_product pa_s_pvs_append_nextvalue_product. ((((exists pa_h_pvs_append_nextvalue_product_factor. pa_h_pvs_append_nextvalue_product_factor + S (pa_p_pvs_append_nextvalue_product) = S ((S (pa_i_pvs_append_nextvalue_product)) * pa_c_pvs_append_nextvalue)) /\ exists pa_q_pvs_append_nextvalue_product_factor. pa_b_pvs_append_nextvalue = pa_q_pvs_append_nextvalue_product_factor * S ((S (pa_i_pvs_append_nextvalue_product)) * pa_c_pvs_append_nextvalue) + (pa_p_pvs_append_nextvalue_product))) /\ ((((exists pa_h_pvs_append_nextvalue_product_partial. pa_h_pvs_append_nextvalue_product_partial + S (pa_r_pvs_append_nextvalue_product) = S ((S (pa_i_pvs_append_nextvalue_product)) * pa_v_pvs_append_nextvalue_product)) /\ exists pa_q_pvs_append_nextvalue_product_partial. pa_u_pvs_append_nextvalue_product = pa_q_pvs_append_nextvalue_product_partial * S ((S (pa_i_pvs_append_nextvalue_product)) * pa_v_pvs_append_nextvalue_product) + (pa_r_pvs_append_nextvalue_product))) /\ ((((exists pa_h_pvs_append_nextvalue_product_successor. pa_h_pvs_append_nextvalue_product_successor + S (pa_s_pvs_append_nextvalue_product) = S ((S (S pa_i_pvs_append_nextvalue_product)) * pa_v_pvs_append_nextvalue_product)) /\ exists pa_q_pvs_append_nextvalue_product_successor. pa_u_pvs_append_nextvalue_product = pa_q_pvs_append_nextvalue_product_successor * S ((S (S pa_i_pvs_append_nextvalue_product)) * pa_v_pvs_append_nextvalue_product) + (pa_s_pvs_append_nextvalue_product))) /\ pa_s_pvs_append_nextvalue_product = pa_r_pvs_append_nextvalue_product * pa_p_pvs_append_nextvalue_product)))))))))))))))))))))