prime_exponent_entries_recode

Exact expanded first-order arithmetic statement

forall n pb pc eb ec vb vc l qb qc fb fc wb wc. (forall pvs_index_recode_source. (exists pvs_gap_recode_sourceindex. pvs_gap_recode_sourceindex + S (pvs_index_recode_source) = (l)) -> exists pvs_prime_recode_source pvs_exponent_recode_source pvs_power_recode_source. (((((exists ff_h_pvs_recode_sourceprime. ff_h_pvs_recode_sourceprime + S (pvs_prime_recode_source) = S ((S (pvs_index_recode_source)) * pc)) /\ exists ff_q_pvs_recode_sourceprime. pb = ff_q_pvs_recode_sourceprime * S ((S (pvs_index_recode_source)) * pc) + (pvs_prime_recode_source))) /\ (((((exists ff_h_pvs_recode_sourceexponent. ff_h_pvs_recode_sourceexponent + S (pvs_exponent_recode_source) = S ((S (pvs_index_recode_source)) * ec)) /\ exists ff_q_pvs_recode_sourceexponent. eb = ff_q_pvs_recode_sourceexponent * S ((S (pvs_index_recode_source)) * ec) + (pvs_exponent_recode_source))) /\ (((((exists ff_h_pvs_recode_sourcepower. ff_h_pvs_recode_sourcepower + S (pvs_power_recode_source) = S ((S (pvs_index_recode_source)) * vc)) /\ exists ff_q_pvs_recode_sourcepower. vb = ff_q_pvs_recode_sourcepower * S ((S (pvs_index_recode_source)) * vc) + (pvs_power_recode_source))) /\ (((~((pvs_prime_recode_source) = 1) /\ forall pvs_left_recode_sourcedomain pvs_right_recode_sourcedomain. (pvs_prime_recode_source) = pvs_left_recode_sourcedomain * pvs_right_recode_sourcedomain -> pvs_left_recode_sourcedomain = 1 \/ pvs_right_recode_sourcedomain = 1) /\ (((~(pvs_exponent_recode_source = 0)) /\ (((((exists bpd_gap_pvs_recode_sourcevaluation_selected_bound. bpd_gap_pvs_recode_sourcevaluation_selected_bound + (pvs_exponent_recode_source) = (n)) /\ (exists bpvi_result_pvs_recode_sourcevaluation_selected. ((exists bpvi_b_pvs_recode_sourcevaluation_selected_power bpvi_c_pvs_recode_sourcevaluation_selected_power. ((forall bpvi_i_pvs_recode_sourcevaluation_selected_power. (exists bpvi_repeat_gap_pvs_recode_sourcevaluation_selected_power. bpvi_repeat_gap_pvs_recode_sourcevaluation_selected_power + S bpvi_i_pvs_recode_sourcevaluation_selected_power = pvs_exponent_recode_source) -> (((exists bpvi_h_pvs_recode_sourcevaluation_selected_power_repeat. bpvi_h_pvs_recode_sourcevaluation_selected_power_repeat + S (pvs_prime_recode_source) = S ((S (bpvi_i_pvs_recode_sourcevaluation_selected_power)) * bpvi_c_pvs_recode_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_selected_power_repeat. bpvi_b_pvs_recode_sourcevaluation_selected_power = bpvi_q_pvs_recode_sourcevaluation_selected_power_repeat * S ((S (bpvi_i_pvs_recode_sourcevaluation_selected_power)) * bpvi_c_pvs_recode_sourcevaluation_selected_power) + (pvs_prime_recode_source)))) /\ (exists bpvi_u_pvs_recode_sourcevaluation_selected_power bpvi_v_pvs_recode_sourcevaluation_selected_power. ((((exists bpvi_h_pvs_recode_sourcevaluation_selected_power_start. bpvi_h_pvs_recode_sourcevaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_recode_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_selected_power_start. bpvi_u_pvs_recode_sourcevaluation_selected_power = bpvi_q_pvs_recode_sourcevaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_recode_sourcevaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_recode_sourcevaluation_selected_power_terminal. bpvi_h_pvs_recode_sourcevaluation_selected_power_terminal + S (bpvi_result_pvs_recode_sourcevaluation_selected) = S ((S (pvs_exponent_recode_source)) * bpvi_v_pvs_recode_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_selected_power_terminal. bpvi_u_pvs_recode_sourcevaluation_selected_power = bpvi_q_pvs_recode_sourcevaluation_selected_power_terminal * S ((S (pvs_exponent_recode_source)) * bpvi_v_pvs_recode_sourcevaluation_selected_power) + (bpvi_result_pvs_recode_sourcevaluation_selected))) /\ forall bpvi_j_pvs_recode_sourcevaluation_selected_power. (exists bpvi_product_gap_pvs_recode_sourcevaluation_selected_power. bpvi_product_gap_pvs_recode_sourcevaluation_selected_power + S bpvi_j_pvs_recode_sourcevaluation_selected_power = pvs_exponent_recode_source) -> exists bpvi_factor_pvs_recode_sourcevaluation_selected_power bpvi_partial_pvs_recode_sourcevaluation_selected_power bpvi_successor_pvs_recode_sourcevaluation_selected_power. ((((exists bpvi_h_pvs_recode_sourcevaluation_selected_power_factor. bpvi_h_pvs_recode_sourcevaluation_selected_power_factor + S (bpvi_factor_pvs_recode_sourcevaluation_selected_power) = S ((S (bpvi_j_pvs_recode_sourcevaluation_selected_power)) * bpvi_c_pvs_recode_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_selected_power_factor. bpvi_b_pvs_recode_sourcevaluation_selected_power = bpvi_q_pvs_recode_sourcevaluation_selected_power_factor * S ((S (bpvi_j_pvs_recode_sourcevaluation_selected_power)) * bpvi_c_pvs_recode_sourcevaluation_selected_power) + (bpvi_factor_pvs_recode_sourcevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_recode_sourcevaluation_selected_power_partial. bpvi_h_pvs_recode_sourcevaluation_selected_power_partial + S (bpvi_partial_pvs_recode_sourcevaluation_selected_power) = S ((S (bpvi_j_pvs_recode_sourcevaluation_selected_power)) * bpvi_v_pvs_recode_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_selected_power_partial. bpvi_u_pvs_recode_sourcevaluation_selected_power = bpvi_q_pvs_recode_sourcevaluation_selected_power_partial * S ((S (bpvi_j_pvs_recode_sourcevaluation_selected_power)) * bpvi_v_pvs_recode_sourcevaluation_selected_power) + (bpvi_partial_pvs_recode_sourcevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_recode_sourcevaluation_selected_power_successor. bpvi_h_pvs_recode_sourcevaluation_selected_power_successor + S (bpvi_successor_pvs_recode_sourcevaluation_selected_power) = S ((S (S bpvi_j_pvs_recode_sourcevaluation_selected_power)) * bpvi_v_pvs_recode_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_selected_power_successor. bpvi_u_pvs_recode_sourcevaluation_selected_power = bpvi_q_pvs_recode_sourcevaluation_selected_power_successor * S ((S (S bpvi_j_pvs_recode_sourcevaluation_selected_power)) * bpvi_v_pvs_recode_sourcevaluation_selected_power) + (bpvi_successor_pvs_recode_sourcevaluation_selected_power))) /\ bpvi_successor_pvs_recode_sourcevaluation_selected_power = bpvi_partial_pvs_recode_sourcevaluation_selected_power * bpvi_factor_pvs_recode_sourcevaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_recode_sourcevaluation_selected. n = bpvi_result_pvs_recode_sourcevaluation_selected * bpvi_divisor_factor_pvs_recode_sourcevaluation_selected))) /\ forall bpd_candidate_pvs_recode_sourcevaluation. (exists bpd_gap_pvs_recode_sourcevaluation_candidate_bound. bpd_gap_pvs_recode_sourcevaluation_candidate_bound + (bpd_candidate_pvs_recode_sourcevaluation) = (n)) -> (exists bpvi_result_pvs_recode_sourcevaluation_candidate. ((exists bpvi_b_pvs_recode_sourcevaluation_candidate_power bpvi_c_pvs_recode_sourcevaluation_candidate_power. ((forall bpvi_i_pvs_recode_sourcevaluation_candidate_power. (exists bpvi_repeat_gap_pvs_recode_sourcevaluation_candidate_power. bpvi_repeat_gap_pvs_recode_sourcevaluation_candidate_power + S bpvi_i_pvs_recode_sourcevaluation_candidate_power = bpd_candidate_pvs_recode_sourcevaluation) -> (((exists bpvi_h_pvs_recode_sourcevaluation_candidate_power_repeat. bpvi_h_pvs_recode_sourcevaluation_candidate_power_repeat + S (pvs_prime_recode_source) = S ((S (bpvi_i_pvs_recode_sourcevaluation_candidate_power)) * bpvi_c_pvs_recode_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_candidate_power_repeat. bpvi_b_pvs_recode_sourcevaluation_candidate_power = bpvi_q_pvs_recode_sourcevaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_recode_sourcevaluation_candidate_power)) * bpvi_c_pvs_recode_sourcevaluation_candidate_power) + (pvs_prime_recode_source)))) /\ (exists bpvi_u_pvs_recode_sourcevaluation_candidate_power bpvi_v_pvs_recode_sourcevaluation_candidate_power. ((((exists bpvi_h_pvs_recode_sourcevaluation_candidate_power_start. bpvi_h_pvs_recode_sourcevaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_candidate_power_start. bpvi_u_pvs_recode_sourcevaluation_candidate_power = bpvi_q_pvs_recode_sourcevaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_recode_sourcevaluation_candidate_power_terminal. bpvi_h_pvs_recode_sourcevaluation_candidate_power_terminal + S (bpvi_result_pvs_recode_sourcevaluation_candidate) = S ((S (bpd_candidate_pvs_recode_sourcevaluation)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_candidate_power_terminal. bpvi_u_pvs_recode_sourcevaluation_candidate_power = bpvi_q_pvs_recode_sourcevaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_recode_sourcevaluation)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power) + (bpvi_result_pvs_recode_sourcevaluation_candidate))) /\ forall bpvi_j_pvs_recode_sourcevaluation_candidate_power. (exists bpvi_product_gap_pvs_recode_sourcevaluation_candidate_power. bpvi_product_gap_pvs_recode_sourcevaluation_candidate_power + S bpvi_j_pvs_recode_sourcevaluation_candidate_power = bpd_candidate_pvs_recode_sourcevaluation) -> exists bpvi_factor_pvs_recode_sourcevaluation_candidate_power bpvi_partial_pvs_recode_sourcevaluation_candidate_power bpvi_successor_pvs_recode_sourcevaluation_candidate_power. ((((exists bpvi_h_pvs_recode_sourcevaluation_candidate_power_factor. bpvi_h_pvs_recode_sourcevaluation_candidate_power_factor + S (bpvi_factor_pvs_recode_sourcevaluation_candidate_power) = S ((S (bpvi_j_pvs_recode_sourcevaluation_candidate_power)) * bpvi_c_pvs_recode_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_candidate_power_factor. bpvi_b_pvs_recode_sourcevaluation_candidate_power = bpvi_q_pvs_recode_sourcevaluation_candidate_power_factor * S ((S (bpvi_j_pvs_recode_sourcevaluation_candidate_power)) * bpvi_c_pvs_recode_sourcevaluation_candidate_power) + (bpvi_factor_pvs_recode_sourcevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_recode_sourcevaluation_candidate_power_partial. bpvi_h_pvs_recode_sourcevaluation_candidate_power_partial + S (bpvi_partial_pvs_recode_sourcevaluation_candidate_power) = S ((S (bpvi_j_pvs_recode_sourcevaluation_candidate_power)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_candidate_power_partial. bpvi_u_pvs_recode_sourcevaluation_candidate_power = bpvi_q_pvs_recode_sourcevaluation_candidate_power_partial * S ((S (bpvi_j_pvs_recode_sourcevaluation_candidate_power)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power) + (bpvi_partial_pvs_recode_sourcevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_recode_sourcevaluation_candidate_power_successor. bpvi_h_pvs_recode_sourcevaluation_candidate_power_successor + S (bpvi_successor_pvs_recode_sourcevaluation_candidate_power) = S ((S (S bpvi_j_pvs_recode_sourcevaluation_candidate_power)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_sourcevaluation_candidate_power_successor. bpvi_u_pvs_recode_sourcevaluation_candidate_power = bpvi_q_pvs_recode_sourcevaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_recode_sourcevaluation_candidate_power)) * bpvi_v_pvs_recode_sourcevaluation_candidate_power) + (bpvi_successor_pvs_recode_sourcevaluation_candidate_power))) /\ bpvi_successor_pvs_recode_sourcevaluation_candidate_power = bpvi_partial_pvs_recode_sourcevaluation_candidate_power * bpvi_factor_pvs_recode_sourcevaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_recode_sourcevaluation_candidate. n = bpvi_result_pvs_recode_sourcevaluation_candidate * bpvi_divisor_factor_pvs_recode_sourcevaluation_candidate)) -> (exists bpd_gap_pvs_recode_sourcevaluation_maximal. bpd_gap_pvs_recode_sourcevaluation_maximal + (bpd_candidate_pvs_recode_sourcevaluation) = (pvs_exponent_recode_source))) /\ (exists pa_b_pvs_recode_sourcevalue pa_c_pvs_recode_sourcevalue. ((forall pa_i_pvs_recode_sourcevalue_repeat. (exists pa_lt_pvs_recode_sourcevalue_repeat_bound. pa_lt_pvs_recode_sourcevalue_repeat_bound + S pa_i_pvs_recode_sourcevalue_repeat = pvs_exponent_recode_source) -> (((exists pa_h_pvs_recode_sourcevalue_repeat_decoded. pa_h_pvs_recode_sourcevalue_repeat_decoded + S (pvs_prime_recode_source) = S ((S (pa_i_pvs_recode_sourcevalue_repeat)) * pa_c_pvs_recode_sourcevalue)) /\ exists pa_q_pvs_recode_sourcevalue_repeat_decoded. pa_b_pvs_recode_sourcevalue = pa_q_pvs_recode_sourcevalue_repeat_decoded * S ((S (pa_i_pvs_recode_sourcevalue_repeat)) * pa_c_pvs_recode_sourcevalue) + (pvs_prime_recode_source)))) /\ (exists pa_u_pvs_recode_sourcevalue_product pa_v_pvs_recode_sourcevalue_product. ((((exists pa_h_pvs_recode_sourcevalue_product_start. pa_h_pvs_recode_sourcevalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_recode_sourcevalue_product)) /\ exists pa_q_pvs_recode_sourcevalue_product_start. pa_u_pvs_recode_sourcevalue_product = pa_q_pvs_recode_sourcevalue_product_start * S ((S (0)) * pa_v_pvs_recode_sourcevalue_product) + (1))) /\ ((((exists pa_h_pvs_recode_sourcevalue_product_terminal. pa_h_pvs_recode_sourcevalue_product_terminal + S (pvs_power_recode_source) = S ((S (pvs_exponent_recode_source)) * pa_v_pvs_recode_sourcevalue_product)) /\ exists pa_q_pvs_recode_sourcevalue_product_terminal. pa_u_pvs_recode_sourcevalue_product = pa_q_pvs_recode_sourcevalue_product_terminal * S ((S (pvs_exponent_recode_source)) * pa_v_pvs_recode_sourcevalue_product) + (pvs_power_recode_source))) /\ forall pa_i_pvs_recode_sourcevalue_product. (exists pa_lt_pvs_recode_sourcevalue_product_bound. pa_lt_pvs_recode_sourcevalue_product_bound + S pa_i_pvs_recode_sourcevalue_product = pvs_exponent_recode_source) -> exists pa_p_pvs_recode_sourcevalue_product pa_r_pvs_recode_sourcevalue_product pa_s_pvs_recode_sourcevalue_product. ((((exists pa_h_pvs_recode_sourcevalue_product_factor. pa_h_pvs_recode_sourcevalue_product_factor + S (pa_p_pvs_recode_sourcevalue_product) = S ((S (pa_i_pvs_recode_sourcevalue_product)) * pa_c_pvs_recode_sourcevalue)) /\ exists pa_q_pvs_recode_sourcevalue_product_factor. pa_b_pvs_recode_sourcevalue = pa_q_pvs_recode_sourcevalue_product_factor * S ((S (pa_i_pvs_recode_sourcevalue_product)) * pa_c_pvs_recode_sourcevalue) + (pa_p_pvs_recode_sourcevalue_product))) /\ ((((exists pa_h_pvs_recode_sourcevalue_product_partial. pa_h_pvs_recode_sourcevalue_product_partial + S (pa_r_pvs_recode_sourcevalue_product) = S ((S (pa_i_pvs_recode_sourcevalue_product)) * pa_v_pvs_recode_sourcevalue_product)) /\ exists pa_q_pvs_recode_sourcevalue_product_partial. pa_u_pvs_recode_sourcevalue_product = pa_q_pvs_recode_sourcevalue_product_partial * S ((S (pa_i_pvs_recode_sourcevalue_product)) * pa_v_pvs_recode_sourcevalue_product) + (pa_r_pvs_recode_sourcevalue_product))) /\ ((((exists pa_h_pvs_recode_sourcevalue_product_successor. pa_h_pvs_recode_sourcevalue_product_successor + S (pa_s_pvs_recode_sourcevalue_product) = S ((S (S pa_i_pvs_recode_sourcevalue_product)) * pa_v_pvs_recode_sourcevalue_product)) /\ exists pa_q_pvs_recode_sourcevalue_product_successor. pa_u_pvs_recode_sourcevalue_product = pa_q_pvs_recode_sourcevalue_product_successor * S ((S (S pa_i_pvs_recode_sourcevalue_product)) * pa_v_pvs_recode_sourcevalue_product) + (pa_s_pvs_recode_sourcevalue_product))) /\ pa_s_pvs_recode_sourcevalue_product = pa_r_pvs_recode_sourcevalue_product * pa_p_pvs_recode_sourcevalue_product))))))))))))))))))))) -> (forall pfp_i_pvs_recode_primes pfp_a_pvs_recode_primes. (exists pfp_gap_pvs_recode_primesbound. pfp_gap_pvs_recode_primesbound + S (pfp_i_pvs_recode_primes) = (l)) -> (((exists ff_h_pfp_pvs_recode_primesold. ff_h_pfp_pvs_recode_primesold + S (pfp_a_pvs_recode_primes) = S ((S (pfp_i_pvs_recode_primes)) * pc)) /\ exists ff_q_pfp_pvs_recode_primesold. pb = ff_q_pfp_pvs_recode_primesold * S ((S (pfp_i_pvs_recode_primes)) * pc) + (pfp_a_pvs_recode_primes))) -> (((exists ff_h_pfp_pvs_recode_primesnew. ff_h_pfp_pvs_recode_primesnew + S (pfp_a_pvs_recode_primes) = S ((S (pfp_i_pvs_recode_primes)) * qc)) /\ exists ff_q_pfp_pvs_recode_primesnew. qb = ff_q_pfp_pvs_recode_primesnew * S ((S (pfp_i_pvs_recode_primes)) * qc) + (pfp_a_pvs_recode_primes)))) -> (forall pfp_i_pvs_recode_exponents pfp_a_pvs_recode_exponents. (exists pfp_gap_pvs_recode_exponentsbound. pfp_gap_pvs_recode_exponentsbound + S (pfp_i_pvs_recode_exponents) = (l)) -> (((exists ff_h_pfp_pvs_recode_exponentsold. ff_h_pfp_pvs_recode_exponentsold + S (pfp_a_pvs_recode_exponents) = S ((S (pfp_i_pvs_recode_exponents)) * ec)) /\ exists ff_q_pfp_pvs_recode_exponentsold. eb = ff_q_pfp_pvs_recode_exponentsold * S ((S (pfp_i_pvs_recode_exponents)) * ec) + (pfp_a_pvs_recode_exponents))) -> (((exists ff_h_pfp_pvs_recode_exponentsnew. ff_h_pfp_pvs_recode_exponentsnew + S (pfp_a_pvs_recode_exponents) = S ((S (pfp_i_pvs_recode_exponents)) * fc)) /\ exists ff_q_pfp_pvs_recode_exponentsnew. fb = ff_q_pfp_pvs_recode_exponentsnew * S ((S (pfp_i_pvs_recode_exponents)) * fc) + (pfp_a_pvs_recode_exponents)))) -> (forall pfp_i_pvs_recode_powers pfp_a_pvs_recode_powers. (exists pfp_gap_pvs_recode_powersbound. pfp_gap_pvs_recode_powersbound + S (pfp_i_pvs_recode_powers) = (l)) -> (((exists ff_h_pfp_pvs_recode_powersold. ff_h_pfp_pvs_recode_powersold + S (pfp_a_pvs_recode_powers) = S ((S (pfp_i_pvs_recode_powers)) * vc)) /\ exists ff_q_pfp_pvs_recode_powersold. vb = ff_q_pfp_pvs_recode_powersold * S ((S (pfp_i_pvs_recode_powers)) * vc) + (pfp_a_pvs_recode_powers))) -> (((exists ff_h_pfp_pvs_recode_powersnew. ff_h_pfp_pvs_recode_powersnew + S (pfp_a_pvs_recode_powers) = S ((S (pfp_i_pvs_recode_powers)) * wc)) /\ exists ff_q_pfp_pvs_recode_powersnew. wb = ff_q_pfp_pvs_recode_powersnew * S ((S (pfp_i_pvs_recode_powers)) * wc) + (pfp_a_pvs_recode_powers)))) -> (forall pvs_index_recode_target. (exists pvs_gap_recode_targetindex. pvs_gap_recode_targetindex + S (pvs_index_recode_target) = (l)) -> exists pvs_prime_recode_target pvs_exponent_recode_target pvs_power_recode_target. (((((exists ff_h_pvs_recode_targetprime. ff_h_pvs_recode_targetprime + S (pvs_prime_recode_target) = S ((S (pvs_index_recode_target)) * qc)) /\ exists ff_q_pvs_recode_targetprime. qb = ff_q_pvs_recode_targetprime * S ((S (pvs_index_recode_target)) * qc) + (pvs_prime_recode_target))) /\ (((((exists ff_h_pvs_recode_targetexponent. ff_h_pvs_recode_targetexponent + S (pvs_exponent_recode_target) = S ((S (pvs_index_recode_target)) * fc)) /\ exists ff_q_pvs_recode_targetexponent. fb = ff_q_pvs_recode_targetexponent * S ((S (pvs_index_recode_target)) * fc) + (pvs_exponent_recode_target))) /\ (((((exists ff_h_pvs_recode_targetpower. ff_h_pvs_recode_targetpower + S (pvs_power_recode_target) = S ((S (pvs_index_recode_target)) * wc)) /\ exists ff_q_pvs_recode_targetpower. wb = ff_q_pvs_recode_targetpower * S ((S (pvs_index_recode_target)) * wc) + (pvs_power_recode_target))) /\ (((~((pvs_prime_recode_target) = 1) /\ forall pvs_left_recode_targetdomain pvs_right_recode_targetdomain. (pvs_prime_recode_target) = pvs_left_recode_targetdomain * pvs_right_recode_targetdomain -> pvs_left_recode_targetdomain = 1 \/ pvs_right_recode_targetdomain = 1) /\ (((~(pvs_exponent_recode_target = 0)) /\ (((((exists bpd_gap_pvs_recode_targetvaluation_selected_bound. bpd_gap_pvs_recode_targetvaluation_selected_bound + (pvs_exponent_recode_target) = (n)) /\ (exists bpvi_result_pvs_recode_targetvaluation_selected. ((exists bpvi_b_pvs_recode_targetvaluation_selected_power bpvi_c_pvs_recode_targetvaluation_selected_power. ((forall bpvi_i_pvs_recode_targetvaluation_selected_power. (exists bpvi_repeat_gap_pvs_recode_targetvaluation_selected_power. bpvi_repeat_gap_pvs_recode_targetvaluation_selected_power + S bpvi_i_pvs_recode_targetvaluation_selected_power = pvs_exponent_recode_target) -> (((exists bpvi_h_pvs_recode_targetvaluation_selected_power_repeat. bpvi_h_pvs_recode_targetvaluation_selected_power_repeat + S (pvs_prime_recode_target) = S ((S (bpvi_i_pvs_recode_targetvaluation_selected_power)) * bpvi_c_pvs_recode_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_selected_power_repeat. bpvi_b_pvs_recode_targetvaluation_selected_power = bpvi_q_pvs_recode_targetvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_recode_targetvaluation_selected_power)) * bpvi_c_pvs_recode_targetvaluation_selected_power) + (pvs_prime_recode_target)))) /\ (exists bpvi_u_pvs_recode_targetvaluation_selected_power bpvi_v_pvs_recode_targetvaluation_selected_power. ((((exists bpvi_h_pvs_recode_targetvaluation_selected_power_start. bpvi_h_pvs_recode_targetvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_recode_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_selected_power_start. bpvi_u_pvs_recode_targetvaluation_selected_power = bpvi_q_pvs_recode_targetvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_recode_targetvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_recode_targetvaluation_selected_power_terminal. bpvi_h_pvs_recode_targetvaluation_selected_power_terminal + S (bpvi_result_pvs_recode_targetvaluation_selected) = S ((S (pvs_exponent_recode_target)) * bpvi_v_pvs_recode_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_selected_power_terminal. bpvi_u_pvs_recode_targetvaluation_selected_power = bpvi_q_pvs_recode_targetvaluation_selected_power_terminal * S ((S (pvs_exponent_recode_target)) * bpvi_v_pvs_recode_targetvaluation_selected_power) + (bpvi_result_pvs_recode_targetvaluation_selected))) /\ forall bpvi_j_pvs_recode_targetvaluation_selected_power. (exists bpvi_product_gap_pvs_recode_targetvaluation_selected_power. bpvi_product_gap_pvs_recode_targetvaluation_selected_power + S bpvi_j_pvs_recode_targetvaluation_selected_power = pvs_exponent_recode_target) -> exists bpvi_factor_pvs_recode_targetvaluation_selected_power bpvi_partial_pvs_recode_targetvaluation_selected_power bpvi_successor_pvs_recode_targetvaluation_selected_power. ((((exists bpvi_h_pvs_recode_targetvaluation_selected_power_factor. bpvi_h_pvs_recode_targetvaluation_selected_power_factor + S (bpvi_factor_pvs_recode_targetvaluation_selected_power) = S ((S (bpvi_j_pvs_recode_targetvaluation_selected_power)) * bpvi_c_pvs_recode_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_selected_power_factor. bpvi_b_pvs_recode_targetvaluation_selected_power = bpvi_q_pvs_recode_targetvaluation_selected_power_factor * S ((S (bpvi_j_pvs_recode_targetvaluation_selected_power)) * bpvi_c_pvs_recode_targetvaluation_selected_power) + (bpvi_factor_pvs_recode_targetvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_recode_targetvaluation_selected_power_partial. bpvi_h_pvs_recode_targetvaluation_selected_power_partial + S (bpvi_partial_pvs_recode_targetvaluation_selected_power) = S ((S (bpvi_j_pvs_recode_targetvaluation_selected_power)) * bpvi_v_pvs_recode_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_selected_power_partial. bpvi_u_pvs_recode_targetvaluation_selected_power = bpvi_q_pvs_recode_targetvaluation_selected_power_partial * S ((S (bpvi_j_pvs_recode_targetvaluation_selected_power)) * bpvi_v_pvs_recode_targetvaluation_selected_power) + (bpvi_partial_pvs_recode_targetvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_recode_targetvaluation_selected_power_successor. bpvi_h_pvs_recode_targetvaluation_selected_power_successor + S (bpvi_successor_pvs_recode_targetvaluation_selected_power) = S ((S (S bpvi_j_pvs_recode_targetvaluation_selected_power)) * bpvi_v_pvs_recode_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_selected_power_successor. bpvi_u_pvs_recode_targetvaluation_selected_power = bpvi_q_pvs_recode_targetvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_recode_targetvaluation_selected_power)) * bpvi_v_pvs_recode_targetvaluation_selected_power) + (bpvi_successor_pvs_recode_targetvaluation_selected_power))) /\ bpvi_successor_pvs_recode_targetvaluation_selected_power = bpvi_partial_pvs_recode_targetvaluation_selected_power * bpvi_factor_pvs_recode_targetvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_recode_targetvaluation_selected. n = bpvi_result_pvs_recode_targetvaluation_selected * bpvi_divisor_factor_pvs_recode_targetvaluation_selected))) /\ forall bpd_candidate_pvs_recode_targetvaluation. (exists bpd_gap_pvs_recode_targetvaluation_candidate_bound. bpd_gap_pvs_recode_targetvaluation_candidate_bound + (bpd_candidate_pvs_recode_targetvaluation) = (n)) -> (exists bpvi_result_pvs_recode_targetvaluation_candidate. ((exists bpvi_b_pvs_recode_targetvaluation_candidate_power bpvi_c_pvs_recode_targetvaluation_candidate_power. ((forall bpvi_i_pvs_recode_targetvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_recode_targetvaluation_candidate_power. bpvi_repeat_gap_pvs_recode_targetvaluation_candidate_power + S bpvi_i_pvs_recode_targetvaluation_candidate_power = bpd_candidate_pvs_recode_targetvaluation) -> (((exists bpvi_h_pvs_recode_targetvaluation_candidate_power_repeat. bpvi_h_pvs_recode_targetvaluation_candidate_power_repeat + S (pvs_prime_recode_target) = S ((S (bpvi_i_pvs_recode_targetvaluation_candidate_power)) * bpvi_c_pvs_recode_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_candidate_power_repeat. bpvi_b_pvs_recode_targetvaluation_candidate_power = bpvi_q_pvs_recode_targetvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_recode_targetvaluation_candidate_power)) * bpvi_c_pvs_recode_targetvaluation_candidate_power) + (pvs_prime_recode_target)))) /\ (exists bpvi_u_pvs_recode_targetvaluation_candidate_power bpvi_v_pvs_recode_targetvaluation_candidate_power. ((((exists bpvi_h_pvs_recode_targetvaluation_candidate_power_start. bpvi_h_pvs_recode_targetvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_recode_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_candidate_power_start. bpvi_u_pvs_recode_targetvaluation_candidate_power = bpvi_q_pvs_recode_targetvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_recode_targetvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_recode_targetvaluation_candidate_power_terminal. bpvi_h_pvs_recode_targetvaluation_candidate_power_terminal + S (bpvi_result_pvs_recode_targetvaluation_candidate) = S ((S (bpd_candidate_pvs_recode_targetvaluation)) * bpvi_v_pvs_recode_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_candidate_power_terminal. bpvi_u_pvs_recode_targetvaluation_candidate_power = bpvi_q_pvs_recode_targetvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_recode_targetvaluation)) * bpvi_v_pvs_recode_targetvaluation_candidate_power) + (bpvi_result_pvs_recode_targetvaluation_candidate))) /\ forall bpvi_j_pvs_recode_targetvaluation_candidate_power. (exists bpvi_product_gap_pvs_recode_targetvaluation_candidate_power. bpvi_product_gap_pvs_recode_targetvaluation_candidate_power + S bpvi_j_pvs_recode_targetvaluation_candidate_power = bpd_candidate_pvs_recode_targetvaluation) -> exists bpvi_factor_pvs_recode_targetvaluation_candidate_power bpvi_partial_pvs_recode_targetvaluation_candidate_power bpvi_successor_pvs_recode_targetvaluation_candidate_power. ((((exists bpvi_h_pvs_recode_targetvaluation_candidate_power_factor. bpvi_h_pvs_recode_targetvaluation_candidate_power_factor + S (bpvi_factor_pvs_recode_targetvaluation_candidate_power) = S ((S (bpvi_j_pvs_recode_targetvaluation_candidate_power)) * bpvi_c_pvs_recode_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_candidate_power_factor. bpvi_b_pvs_recode_targetvaluation_candidate_power = bpvi_q_pvs_recode_targetvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_recode_targetvaluation_candidate_power)) * bpvi_c_pvs_recode_targetvaluation_candidate_power) + (bpvi_factor_pvs_recode_targetvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_recode_targetvaluation_candidate_power_partial. bpvi_h_pvs_recode_targetvaluation_candidate_power_partial + S (bpvi_partial_pvs_recode_targetvaluation_candidate_power) = S ((S (bpvi_j_pvs_recode_targetvaluation_candidate_power)) * bpvi_v_pvs_recode_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_candidate_power_partial. bpvi_u_pvs_recode_targetvaluation_candidate_power = bpvi_q_pvs_recode_targetvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_recode_targetvaluation_candidate_power)) * bpvi_v_pvs_recode_targetvaluation_candidate_power) + (bpvi_partial_pvs_recode_targetvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_recode_targetvaluation_candidate_power_successor. bpvi_h_pvs_recode_targetvaluation_candidate_power_successor + S (bpvi_successor_pvs_recode_targetvaluation_candidate_power) = S ((S (S bpvi_j_pvs_recode_targetvaluation_candidate_power)) * bpvi_v_pvs_recode_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_recode_targetvaluation_candidate_power_successor. bpvi_u_pvs_recode_targetvaluation_candidate_power = bpvi_q_pvs_recode_targetvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_recode_targetvaluation_candidate_power)) * bpvi_v_pvs_recode_targetvaluation_candidate_power) + (bpvi_successor_pvs_recode_targetvaluation_candidate_power))) /\ bpvi_successor_pvs_recode_targetvaluation_candidate_power = bpvi_partial_pvs_recode_targetvaluation_candidate_power * bpvi_factor_pvs_recode_targetvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_recode_targetvaluation_candidate. n = bpvi_result_pvs_recode_targetvaluation_candidate * bpvi_divisor_factor_pvs_recode_targetvaluation_candidate)) -> (exists bpd_gap_pvs_recode_targetvaluation_maximal. bpd_gap_pvs_recode_targetvaluation_maximal + (bpd_candidate_pvs_recode_targetvaluation) = (pvs_exponent_recode_target))) /\ (exists pa_b_pvs_recode_targetvalue pa_c_pvs_recode_targetvalue. ((forall pa_i_pvs_recode_targetvalue_repeat. (exists pa_lt_pvs_recode_targetvalue_repeat_bound. pa_lt_pvs_recode_targetvalue_repeat_bound + S pa_i_pvs_recode_targetvalue_repeat = pvs_exponent_recode_target) -> (((exists pa_h_pvs_recode_targetvalue_repeat_decoded. pa_h_pvs_recode_targetvalue_repeat_decoded + S (pvs_prime_recode_target) = S ((S (pa_i_pvs_recode_targetvalue_repeat)) * pa_c_pvs_recode_targetvalue)) /\ exists pa_q_pvs_recode_targetvalue_repeat_decoded. pa_b_pvs_recode_targetvalue = pa_q_pvs_recode_targetvalue_repeat_decoded * S ((S (pa_i_pvs_recode_targetvalue_repeat)) * pa_c_pvs_recode_targetvalue) + (pvs_prime_recode_target)))) /\ (exists pa_u_pvs_recode_targetvalue_product pa_v_pvs_recode_targetvalue_product. ((((exists pa_h_pvs_recode_targetvalue_product_start. pa_h_pvs_recode_targetvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_recode_targetvalue_product)) /\ exists pa_q_pvs_recode_targetvalue_product_start. pa_u_pvs_recode_targetvalue_product = pa_q_pvs_recode_targetvalue_product_start * S ((S (0)) * pa_v_pvs_recode_targetvalue_product) + (1))) /\ ((((exists pa_h_pvs_recode_targetvalue_product_terminal. pa_h_pvs_recode_targetvalue_product_terminal + S (pvs_power_recode_target) = S ((S (pvs_exponent_recode_target)) * pa_v_pvs_recode_targetvalue_product)) /\ exists pa_q_pvs_recode_targetvalue_product_terminal. pa_u_pvs_recode_targetvalue_product = pa_q_pvs_recode_targetvalue_product_terminal * S ((S (pvs_exponent_recode_target)) * pa_v_pvs_recode_targetvalue_product) + (pvs_power_recode_target))) /\ forall pa_i_pvs_recode_targetvalue_product. (exists pa_lt_pvs_recode_targetvalue_product_bound. pa_lt_pvs_recode_targetvalue_product_bound + S pa_i_pvs_recode_targetvalue_product = pvs_exponent_recode_target) -> exists pa_p_pvs_recode_targetvalue_product pa_r_pvs_recode_targetvalue_product pa_s_pvs_recode_targetvalue_product. ((((exists pa_h_pvs_recode_targetvalue_product_factor. pa_h_pvs_recode_targetvalue_product_factor + S (pa_p_pvs_recode_targetvalue_product) = S ((S (pa_i_pvs_recode_targetvalue_product)) * pa_c_pvs_recode_targetvalue)) /\ exists pa_q_pvs_recode_targetvalue_product_factor. pa_b_pvs_recode_targetvalue = pa_q_pvs_recode_targetvalue_product_factor * S ((S (pa_i_pvs_recode_targetvalue_product)) * pa_c_pvs_recode_targetvalue) + (pa_p_pvs_recode_targetvalue_product))) /\ ((((exists pa_h_pvs_recode_targetvalue_product_partial. pa_h_pvs_recode_targetvalue_product_partial + S (pa_r_pvs_recode_targetvalue_product) = S ((S (pa_i_pvs_recode_targetvalue_product)) * pa_v_pvs_recode_targetvalue_product)) /\ exists pa_q_pvs_recode_targetvalue_product_partial. pa_u_pvs_recode_targetvalue_product = pa_q_pvs_recode_targetvalue_product_partial * S ((S (pa_i_pvs_recode_targetvalue_product)) * pa_v_pvs_recode_targetvalue_product) + (pa_r_pvs_recode_targetvalue_product))) /\ ((((exists pa_h_pvs_recode_targetvalue_product_successor. pa_h_pvs_recode_targetvalue_product_successor + S (pa_s_pvs_recode_targetvalue_product) = S ((S (S pa_i_pvs_recode_targetvalue_product)) * pa_v_pvs_recode_targetvalue_product)) /\ exists pa_q_pvs_recode_targetvalue_product_successor. pa_u_pvs_recode_targetvalue_product = pa_q_pvs_recode_targetvalue_product_successor * S ((S (S pa_i_pvs_recode_targetvalue_product)) * pa_v_pvs_recode_targetvalue_product) + (pa_s_pvs_recode_targetvalue_product))) /\ pa_s_pvs_recode_targetvalue_product = pa_r_pvs_recode_targetvalue_product * pa_p_pvs_recode_targetvalue_product)))))))))))))))))))))