perfect_power_profile_nonunit_decode

Exact expanded first-order arithmetic statement

forall n w. (((((n) = 1) /\ ((((w) = 0) /\ (forall ppf_unit_degree_profile_decodeunit. ~(ppf_unit_degree_profile_decodeunit = 0) -> (exists pa_b_pvs_profile_decodeunitidentity pa_c_pvs_profile_decodeunitidentity. ((forall pa_i_pvs_profile_decodeunitidentity_repeat. (exists pa_lt_pvs_profile_decodeunitidentity_repeat_bound. pa_lt_pvs_profile_decodeunitidentity_repeat_bound + S pa_i_pvs_profile_decodeunitidentity_repeat = ppf_unit_degree_profile_decodeunit) -> (((exists pa_h_pvs_profile_decodeunitidentity_repeat_decoded. pa_h_pvs_profile_decodeunitidentity_repeat_decoded + S (1) = S ((S (pa_i_pvs_profile_decodeunitidentity_repeat)) * pa_c_pvs_profile_decodeunitidentity)) /\ exists pa_q_pvs_profile_decodeunitidentity_repeat_decoded. pa_b_pvs_profile_decodeunitidentity = pa_q_pvs_profile_decodeunitidentity_repeat_decoded * S ((S (pa_i_pvs_profile_decodeunitidentity_repeat)) * pa_c_pvs_profile_decodeunitidentity) + (1)))) /\ (exists pa_u_pvs_profile_decodeunitidentity_product pa_v_pvs_profile_decodeunitidentity_product. ((((exists pa_h_pvs_profile_decodeunitidentity_product_start. pa_h_pvs_profile_decodeunitidentity_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_decodeunitidentity_product)) /\ exists pa_q_pvs_profile_decodeunitidentity_product_start. pa_u_pvs_profile_decodeunitidentity_product = pa_q_pvs_profile_decodeunitidentity_product_start * S ((S (0)) * pa_v_pvs_profile_decodeunitidentity_product) + (1))) /\ ((((exists pa_h_pvs_profile_decodeunitidentity_product_terminal. pa_h_pvs_profile_decodeunitidentity_product_terminal + S (1) = S ((S (ppf_unit_degree_profile_decodeunit)) * pa_v_pvs_profile_decodeunitidentity_product)) /\ exists pa_q_pvs_profile_decodeunitidentity_product_terminal. pa_u_pvs_profile_decodeunitidentity_product = pa_q_pvs_profile_decodeunitidentity_product_terminal * S ((S (ppf_unit_degree_profile_decodeunit)) * pa_v_pvs_profile_decodeunitidentity_product) + (1))) /\ forall pa_i_pvs_profile_decodeunitidentity_product. (exists pa_lt_pvs_profile_decodeunitidentity_product_bound. pa_lt_pvs_profile_decodeunitidentity_product_bound + S pa_i_pvs_profile_decodeunitidentity_product = ppf_unit_degree_profile_decodeunit) -> exists pa_p_pvs_profile_decodeunitidentity_product pa_r_pvs_profile_decodeunitidentity_product pa_s_pvs_profile_decodeunitidentity_product. ((((exists pa_h_pvs_profile_decodeunitidentity_product_factor. pa_h_pvs_profile_decodeunitidentity_product_factor + S (pa_p_pvs_profile_decodeunitidentity_product) = S ((S (pa_i_pvs_profile_decodeunitidentity_product)) * pa_c_pvs_profile_decodeunitidentity)) /\ exists pa_q_pvs_profile_decodeunitidentity_product_factor. pa_b_pvs_profile_decodeunitidentity = pa_q_pvs_profile_decodeunitidentity_product_factor * S ((S (pa_i_pvs_profile_decodeunitidentity_product)) * pa_c_pvs_profile_decodeunitidentity) + (pa_p_pvs_profile_decodeunitidentity_product))) /\ ((((exists pa_h_pvs_profile_decodeunitidentity_product_partial. pa_h_pvs_profile_decodeunitidentity_product_partial + S (pa_r_pvs_profile_decodeunitidentity_product) = S ((S (pa_i_pvs_profile_decodeunitidentity_product)) * pa_v_pvs_profile_decodeunitidentity_product)) /\ exists pa_q_pvs_profile_decodeunitidentity_product_partial. pa_u_pvs_profile_decodeunitidentity_product = pa_q_pvs_profile_decodeunitidentity_product_partial * S ((S (pa_i_pvs_profile_decodeunitidentity_product)) * pa_v_pvs_profile_decodeunitidentity_product) + (pa_r_pvs_profile_decodeunitidentity_product))) /\ ((((exists pa_h_pvs_profile_decodeunitidentity_product_successor. pa_h_pvs_profile_decodeunitidentity_product_successor + S (pa_s_pvs_profile_decodeunitidentity_product) = S ((S (S pa_i_pvs_profile_decodeunitidentity_product)) * pa_v_pvs_profile_decodeunitidentity_product)) /\ exists pa_q_pvs_profile_decodeunitidentity_product_successor. pa_u_pvs_profile_decodeunitidentity_product = pa_q_pvs_profile_decodeunitidentity_product_successor * S ((S (S pa_i_pvs_profile_decodeunitidentity_product)) * pa_v_pvs_profile_decodeunitidentity_product) + (pa_s_pvs_profile_decodeunitidentity_product))) /\ pa_s_pvs_profile_decodeunitidentity_product = pa_r_pvs_profile_decodeunitidentity_product * pa_p_pvs_profile_decodeunitidentity_product))))))))))))) \/ (exists ppf_pb_profile_decode ppf_pc_profile_decode ppf_eb_profile_decode ppf_ec_profile_decode ppf_vb_profile_decode ppf_vc_profile_decode ppf_length_profile_decode ppf_gcd_profile_decode ppf_rb_profile_decode ppf_rc_profile_decode. (((~((n) = 1)) /\ (((exists ppf_code_0_profile_decodedatacode ppf_code_1_profile_decodedatacode ppf_code_2_profile_decodedatacode ppf_code_3_profile_decodedatacode ppf_code_4_profile_decodedatacode ppf_code_5_profile_decodedatacode ppf_code_6_profile_decodedatacode ppf_code_7_profile_decodedatacode. ((((w) = ((ppf_pb_profile_decode) + (ppf_code_0_profile_decodedatacode)) * S ((ppf_pb_profile_decode) + (ppf_code_0_profile_decodedatacode)) + ((ppf_code_0_profile_decodedatacode) + (ppf_code_0_profile_decodedatacode))) /\ ((((ppf_code_0_profile_decodedatacode) = ((ppf_pc_profile_decode) + (ppf_code_1_profile_decodedatacode)) * S ((ppf_pc_profile_decode) + (ppf_code_1_profile_decodedatacode)) + ((ppf_code_1_profile_decodedatacode) + (ppf_code_1_profile_decodedatacode))) /\ ((((ppf_code_1_profile_decodedatacode) = ((ppf_eb_profile_decode) + (ppf_code_2_profile_decodedatacode)) * S ((ppf_eb_profile_decode) + (ppf_code_2_profile_decodedatacode)) + ((ppf_code_2_profile_decodedatacode) + (ppf_code_2_profile_decodedatacode))) /\ ((((ppf_code_2_profile_decodedatacode) = ((ppf_ec_profile_decode) + (ppf_code_3_profile_decodedatacode)) * S ((ppf_ec_profile_decode) + (ppf_code_3_profile_decodedatacode)) + ((ppf_code_3_profile_decodedatacode) + (ppf_code_3_profile_decodedatacode))) /\ ((((ppf_code_3_profile_decodedatacode) = ((ppf_vb_profile_decode) + (ppf_code_4_profile_decodedatacode)) * S ((ppf_vb_profile_decode) + (ppf_code_4_profile_decodedatacode)) + ((ppf_code_4_profile_decodedatacode) + (ppf_code_4_profile_decodedatacode))) /\ ((((ppf_code_4_profile_decodedatacode) = ((ppf_vc_profile_decode) + (ppf_code_5_profile_decodedatacode)) * S ((ppf_vc_profile_decode) + (ppf_code_5_profile_decodedatacode)) + ((ppf_code_5_profile_decodedatacode) + (ppf_code_5_profile_decodedatacode))) /\ ((((ppf_code_5_profile_decodedatacode) = ((ppf_length_profile_decode) + (ppf_code_6_profile_decodedatacode)) * S ((ppf_length_profile_decode) + (ppf_code_6_profile_decodedatacode)) + ((ppf_code_6_profile_decodedatacode) + (ppf_code_6_profile_decodedatacode))) /\ ((((ppf_code_6_profile_decodedatacode) = ((ppf_gcd_profile_decode) + (ppf_code_7_profile_decodedatacode)) * S ((ppf_gcd_profile_decode) + (ppf_code_7_profile_decodedatacode)) + ((ppf_code_7_profile_decodedatacode) + (ppf_code_7_profile_decodedatacode))) /\ ((ppf_code_7_profile_decodedatacode) = ((ppf_rb_profile_decode) + (ppf_rc_profile_decode)) * S ((ppf_rb_profile_decode) + (ppf_rc_profile_decode)) + ((ppf_rc_profile_decode) + (ppf_rc_profile_decode)))))))))))))))))))) /\ (((((~((n) = 0)) /\ (((forall pfp_i_pvs_profile_decodedatasupportdistinct pfp_j_pvs_profile_decodedatasupportdistinct pfp_a_pvs_profile_decodedatasupportdistinct. (exists pfp_gap_pvs_profile_decodedatasupportdistinctfirst. pfp_gap_pvs_profile_decodedatasupportdistinctfirst + S (pfp_i_pvs_profile_decodedatasupportdistinct) = (ppf_length_profile_decode)) -> (exists pfp_gap_pvs_profile_decodedatasupportdistinctsecond. pfp_gap_pvs_profile_decodedatasupportdistinctsecond + S (pfp_j_pvs_profile_decodedatasupportdistinct) = (ppf_length_profile_decode)) -> (((exists ff_h_pfp_pvs_profile_decodedatasupportdistinctleft. ff_h_pfp_pvs_profile_decodedatasupportdistinctleft + S (pfp_a_pvs_profile_decodedatasupportdistinct) = S ((S (pfp_i_pvs_profile_decodedatasupportdistinct)) * ppf_pc_profile_decode)) /\ exists ff_q_pfp_pvs_profile_decodedatasupportdistinctleft. ppf_pb_profile_decode = ff_q_pfp_pvs_profile_decodedatasupportdistinctleft * S ((S (pfp_i_pvs_profile_decodedatasupportdistinct)) * ppf_pc_profile_decode) + (pfp_a_pvs_profile_decodedatasupportdistinct))) -> (((exists ff_h_pfp_pvs_profile_decodedatasupportdistinctright. ff_h_pfp_pvs_profile_decodedatasupportdistinctright + S (pfp_a_pvs_profile_decodedatasupportdistinct) = S ((S (pfp_j_pvs_profile_decodedatasupportdistinct)) * ppf_pc_profile_decode)) /\ exists ff_q_pfp_pvs_profile_decodedatasupportdistinctright. ppf_pb_profile_decode = ff_q_pfp_pvs_profile_decodedatasupportdistinctright * S ((S (pfp_j_pvs_profile_decodedatasupportdistinct)) * ppf_pc_profile_decode) + (pfp_a_pvs_profile_decodedatasupportdistinct))) -> pfp_i_pvs_profile_decodedatasupportdistinct = pfp_j_pvs_profile_decodedatasupportdistinct) /\ (((forall pvs_index_profile_decodedatasupportentries. (exists pvs_gap_profile_decodedatasupportentriesindex. pvs_gap_profile_decodedatasupportentriesindex + S (pvs_index_profile_decodedatasupportentries) = (ppf_length_profile_decode)) -> exists pvs_prime_profile_decodedatasupportentries pvs_exponent_profile_decodedatasupportentries pvs_power_profile_decodedatasupportentries. (((((exists ff_h_pvs_profile_decodedatasupportentriesprime. ff_h_pvs_profile_decodedatasupportentriesprime + S (pvs_prime_profile_decodedatasupportentries) = S ((S (pvs_index_profile_decodedatasupportentries)) * ppf_pc_profile_decode)) /\ exists ff_q_pvs_profile_decodedatasupportentriesprime. ppf_pb_profile_decode = ff_q_pvs_profile_decodedatasupportentriesprime * S ((S (pvs_index_profile_decodedatasupportentries)) * ppf_pc_profile_decode) + (pvs_prime_profile_decodedatasupportentries))) /\ (((((exists ff_h_pvs_profile_decodedatasupportentriesexponent. ff_h_pvs_profile_decodedatasupportentriesexponent + S (pvs_exponent_profile_decodedatasupportentries) = S ((S (pvs_index_profile_decodedatasupportentries)) * ppf_ec_profile_decode)) /\ exists ff_q_pvs_profile_decodedatasupportentriesexponent. ppf_eb_profile_decode = ff_q_pvs_profile_decodedatasupportentriesexponent * S ((S (pvs_index_profile_decodedatasupportentries)) * ppf_ec_profile_decode) + (pvs_exponent_profile_decodedatasupportentries))) /\ (((((exists ff_h_pvs_profile_decodedatasupportentriespower. ff_h_pvs_profile_decodedatasupportentriespower + S (pvs_power_profile_decodedatasupportentries) = S ((S (pvs_index_profile_decodedatasupportentries)) * ppf_vc_profile_decode)) /\ exists ff_q_pvs_profile_decodedatasupportentriespower. ppf_vb_profile_decode = ff_q_pvs_profile_decodedatasupportentriespower * S ((S (pvs_index_profile_decodedatasupportentries)) * ppf_vc_profile_decode) + (pvs_power_profile_decodedatasupportentries))) /\ (((~((pvs_prime_profile_decodedatasupportentries) = 1) /\ forall pvs_left_profile_decodedatasupportentriesdomain pvs_right_profile_decodedatasupportentriesdomain. (pvs_prime_profile_decodedatasupportentries) = pvs_left_profile_decodedatasupportentriesdomain * pvs_right_profile_decodedatasupportentriesdomain -> pvs_left_profile_decodedatasupportentriesdomain = 1 \/ pvs_right_profile_decodedatasupportentriesdomain = 1) /\ (((~(pvs_exponent_profile_decodedatasupportentries = 0)) /\ (((((exists bpd_gap_pvs_profile_decodedatasupportentriesvaluation_selected_bound. bpd_gap_pvs_profile_decodedatasupportentriesvaluation_selected_bound + (pvs_exponent_profile_decodedatasupportentries) = (n)) /\ (exists bpvi_result_pvs_profile_decodedatasupportentriesvaluation_selected. ((exists bpvi_b_pvs_profile_decodedatasupportentriesvaluation_selected_power bpvi_c_pvs_profile_decodedatasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_profile_decodedatasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_profile_decodedatasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_profile_decodedatasupportentriesvaluation_selected_power + S bpvi_i_pvs_profile_decodedatasupportentriesvaluation_selected_power = pvs_exponent_profile_decodedatasupportentries) -> (((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_repeat + S (pvs_prime_profile_decodedatasupportentries) = S ((S (bpvi_i_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_profile_decodedatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_selected_power) + (pvs_prime_profile_decodedatasupportentries)))) /\ (exists bpvi_u_pvs_profile_decodedatasupportentriesvaluation_selected_power bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_start. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_start. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_profile_decodedatasupportentriesvaluation_selected) = S ((S (pvs_exponent_profile_decodedatasupportentries)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_profile_decodedatasupportentries)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power) + (bpvi_result_pvs_profile_decodedatasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_profile_decodedatasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_profile_decodedatasupportentriesvaluation_selected_power + S bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power = pvs_exponent_profile_decodedatasupportentries) -> exists bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_selected_power bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_selected_power bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_profile_decodedatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_profile_decodedatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_selected_power = bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_selected_power * bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_decodedatasupportentriesvaluation_selected. n = bpvi_result_pvs_profile_decodedatasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_profile_decodedatasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_profile_decodedatasupportentriesvaluation. (exists bpd_gap_pvs_profile_decodedatasupportentriesvaluation_candidate_bound. bpd_gap_pvs_profile_decodedatasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_profile_decodedatasupportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_profile_decodedatasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_profile_decodedatasupportentriesvaluation_candidate_power bpvi_c_pvs_profile_decodedatasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_profile_decodedatasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_profile_decodedatasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_profile_decodedatasupportentriesvaluation_candidate_power + S bpvi_i_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_decodedatasupportentriesvaluation) -> (((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_profile_decodedatasupportentries) = S ((S (bpvi_i_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_candidate_power) + (pvs_prime_profile_decodedatasupportentries)))) /\ (exists bpvi_u_pvs_profile_decodedatasupportentriesvaluation_candidate_power bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_profile_decodedatasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_profile_decodedatasupportentriesvaluation)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_profile_decodedatasupportentriesvaluation)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_profile_decodedatasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_profile_decodedatasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_profile_decodedatasupportentriesvaluation_candidate_power + S bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_decodedatasupportentriesvaluation) -> exists bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_candidate_power bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_candidate_power bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decodedatasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_profile_decodedatasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decodedatasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_profile_decodedatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decodedatasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_profile_decodedatasupportentriesvaluation_candidate_power = bpvi_partial_pvs_profile_decodedatasupportentriesvaluation_candidate_power * bpvi_factor_pvs_profile_decodedatasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_decodedatasupportentriesvaluation_candidate. n = bpvi_result_pvs_profile_decodedatasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_profile_decodedatasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_profile_decodedatasupportentriesvaluation_maximal. bpd_gap_pvs_profile_decodedatasupportentriesvaluation_maximal + (bpd_candidate_pvs_profile_decodedatasupportentriesvaluation) = (pvs_exponent_profile_decodedatasupportentries))) /\ (exists pa_b_pvs_profile_decodedatasupportentriesvalue pa_c_pvs_profile_decodedatasupportentriesvalue. ((forall pa_i_pvs_profile_decodedatasupportentriesvalue_repeat. (exists pa_lt_pvs_profile_decodedatasupportentriesvalue_repeat_bound. pa_lt_pvs_profile_decodedatasupportentriesvalue_repeat_bound + S pa_i_pvs_profile_decodedatasupportentriesvalue_repeat = pvs_exponent_profile_decodedatasupportentries) -> (((exists pa_h_pvs_profile_decodedatasupportentriesvalue_repeat_decoded. pa_h_pvs_profile_decodedatasupportentriesvalue_repeat_decoded + S (pvs_prime_profile_decodedatasupportentries) = S ((S (pa_i_pvs_profile_decodedatasupportentriesvalue_repeat)) * pa_c_pvs_profile_decodedatasupportentriesvalue)) /\ exists pa_q_pvs_profile_decodedatasupportentriesvalue_repeat_decoded. pa_b_pvs_profile_decodedatasupportentriesvalue = pa_q_pvs_profile_decodedatasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_profile_decodedatasupportentriesvalue_repeat)) * pa_c_pvs_profile_decodedatasupportentriesvalue) + (pvs_prime_profile_decodedatasupportentries)))) /\ (exists pa_u_pvs_profile_decodedatasupportentriesvalue_product pa_v_pvs_profile_decodedatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_decodedatasupportentriesvalue_product_start. pa_h_pvs_profile_decodedatasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decodedatasupportentriesvalue_product_start. pa_u_pvs_profile_decodedatasupportentriesvalue_product = pa_q_pvs_profile_decodedatasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_profile_decodedatasupportentriesvalue_product_terminal. pa_h_pvs_profile_decodedatasupportentriesvalue_product_terminal + S (pvs_power_profile_decodedatasupportentries) = S ((S (pvs_exponent_profile_decodedatasupportentries)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decodedatasupportentriesvalue_product_terminal. pa_u_pvs_profile_decodedatasupportentriesvalue_product = pa_q_pvs_profile_decodedatasupportentriesvalue_product_terminal * S ((S (pvs_exponent_profile_decodedatasupportentries)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product) + (pvs_power_profile_decodedatasupportentries))) /\ forall pa_i_pvs_profile_decodedatasupportentriesvalue_product. (exists pa_lt_pvs_profile_decodedatasupportentriesvalue_product_bound. pa_lt_pvs_profile_decodedatasupportentriesvalue_product_bound + S pa_i_pvs_profile_decodedatasupportentriesvalue_product = pvs_exponent_profile_decodedatasupportentries) -> exists pa_p_pvs_profile_decodedatasupportentriesvalue_product pa_r_pvs_profile_decodedatasupportentriesvalue_product pa_s_pvs_profile_decodedatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_decodedatasupportentriesvalue_product_factor. pa_h_pvs_profile_decodedatasupportentriesvalue_product_factor + S (pa_p_pvs_profile_decodedatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_decodedatasupportentriesvalue_product)) * pa_c_pvs_profile_decodedatasupportentriesvalue)) /\ exists pa_q_pvs_profile_decodedatasupportentriesvalue_product_factor. pa_b_pvs_profile_decodedatasupportentriesvalue = pa_q_pvs_profile_decodedatasupportentriesvalue_product_factor * S ((S (pa_i_pvs_profile_decodedatasupportentriesvalue_product)) * pa_c_pvs_profile_decodedatasupportentriesvalue) + (pa_p_pvs_profile_decodedatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_decodedatasupportentriesvalue_product_partial. pa_h_pvs_profile_decodedatasupportentriesvalue_product_partial + S (pa_r_pvs_profile_decodedatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_decodedatasupportentriesvalue_product)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decodedatasupportentriesvalue_product_partial. pa_u_pvs_profile_decodedatasupportentriesvalue_product = pa_q_pvs_profile_decodedatasupportentriesvalue_product_partial * S ((S (pa_i_pvs_profile_decodedatasupportentriesvalue_product)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product) + (pa_r_pvs_profile_decodedatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_decodedatasupportentriesvalue_product_successor. pa_h_pvs_profile_decodedatasupportentriesvalue_product_successor + S (pa_s_pvs_profile_decodedatasupportentriesvalue_product) = S ((S (S pa_i_pvs_profile_decodedatasupportentriesvalue_product)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decodedatasupportentriesvalue_product_successor. pa_u_pvs_profile_decodedatasupportentriesvalue_product = pa_q_pvs_profile_decodedatasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_profile_decodedatasupportentriesvalue_product)) * pa_v_pvs_profile_decodedatasupportentriesvalue_product) + (pa_s_pvs_profile_decodedatasupportentriesvalue_product))) /\ pa_s_pvs_profile_decodedatasupportentriesvalue_product = pa_r_pvs_profile_decodedatasupportentriesvalue_product * pa_p_pvs_profile_decodedatasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_profile_decodedatasupportcover. (~((pvs_divisor_profile_decodedatasupportcover) = 1) /\ forall pvs_left_profile_decodedatasupportcoverprime pvs_right_profile_decodedatasupportcoverprime. (pvs_divisor_profile_decodedatasupportcover) = pvs_left_profile_decodedatasupportcoverprime * pvs_right_profile_decodedatasupportcoverprime -> pvs_left_profile_decodedatasupportcoverprime = 1 \/ pvs_right_profile_decodedatasupportcoverprime = 1) -> (exists pvs_factor_profile_decodedatasupportcoverdivides. (n) = (pvs_divisor_profile_decodedatasupportcover) * pvs_factor_profile_decodedatasupportcoverdivides) -> exists pvs_position_profile_decodedatasupportcover. (exists pvs_gap_profile_decodedatasupportcoverbound. pvs_gap_profile_decodedatasupportcoverbound + S (pvs_position_profile_decodedatasupportcover) = (ppf_length_profile_decode)) /\ (((exists ff_h_pvs_profile_decodedatasupportcoverentry. ff_h_pvs_profile_decodedatasupportcoverentry + S (pvs_divisor_profile_decodedatasupportcover) = S ((S (pvs_position_profile_decodedatasupportcover)) * ppf_pc_profile_decode)) /\ exists ff_q_pvs_profile_decodedatasupportcoverentry. ppf_pb_profile_decode = ff_q_pvs_profile_decodedatasupportcoverentry * S ((S (pvs_position_profile_decodedatasupportcover)) * ppf_pc_profile_decode) + (pvs_divisor_profile_decodedatasupportcover)))) /\ (exists ff_u_pvs_profile_decodedatasupportproduct ff_v_pvs_profile_decodedatasupportproduct. ((((exists ff_h_pvs_profile_decodedatasupportproduct_start. ff_h_pvs_profile_decodedatasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_profile_decodedatasupportproduct)) /\ exists ff_q_pvs_profile_decodedatasupportproduct_start. ff_u_pvs_profile_decodedatasupportproduct = ff_q_pvs_profile_decodedatasupportproduct_start * S ((S (0)) * ff_v_pvs_profile_decodedatasupportproduct) + (1))) /\ ((((exists ff_h_pvs_profile_decodedatasupportproduct_terminal. ff_h_pvs_profile_decodedatasupportproduct_terminal + S (n) = S ((S (ppf_length_profile_decode)) * ff_v_pvs_profile_decodedatasupportproduct)) /\ exists ff_q_pvs_profile_decodedatasupportproduct_terminal. ff_u_pvs_profile_decodedatasupportproduct = ff_q_pvs_profile_decodedatasupportproduct_terminal * S ((S (ppf_length_profile_decode)) * ff_v_pvs_profile_decodedatasupportproduct) + (n))) /\ forall ff_i_pvs_profile_decodedatasupportproduct. (exists ff_lt_pvs_profile_decodedatasupportproduct_bound. ff_lt_pvs_profile_decodedatasupportproduct_bound + S ff_i_pvs_profile_decodedatasupportproduct = ppf_length_profile_decode) -> exists ff_p_pvs_profile_decodedatasupportproduct ff_r_pvs_profile_decodedatasupportproduct ff_s_pvs_profile_decodedatasupportproduct. ((((exists ff_h_pvs_profile_decodedatasupportproduct_factor. ff_h_pvs_profile_decodedatasupportproduct_factor + S (ff_p_pvs_profile_decodedatasupportproduct) = S ((S (ff_i_pvs_profile_decodedatasupportproduct)) * ppf_vc_profile_decode)) /\ exists ff_q_pvs_profile_decodedatasupportproduct_factor. ppf_vb_profile_decode = ff_q_pvs_profile_decodedatasupportproduct_factor * S ((S (ff_i_pvs_profile_decodedatasupportproduct)) * ppf_vc_profile_decode) + (ff_p_pvs_profile_decodedatasupportproduct))) /\ ((((exists ff_h_pvs_profile_decodedatasupportproduct_partial. ff_h_pvs_profile_decodedatasupportproduct_partial + S (ff_r_pvs_profile_decodedatasupportproduct) = S ((S (ff_i_pvs_profile_decodedatasupportproduct)) * ff_v_pvs_profile_decodedatasupportproduct)) /\ exists ff_q_pvs_profile_decodedatasupportproduct_partial. ff_u_pvs_profile_decodedatasupportproduct = ff_q_pvs_profile_decodedatasupportproduct_partial * S ((S (ff_i_pvs_profile_decodedatasupportproduct)) * ff_v_pvs_profile_decodedatasupportproduct) + (ff_r_pvs_profile_decodedatasupportproduct))) /\ ((((exists ff_h_pvs_profile_decodedatasupportproduct_successor. ff_h_pvs_profile_decodedatasupportproduct_successor + S (ff_s_pvs_profile_decodedatasupportproduct) = S ((S (S ff_i_pvs_profile_decodedatasupportproduct)) * ff_v_pvs_profile_decodedatasupportproduct)) /\ exists ff_q_pvs_profile_decodedatasupportproduct_successor. ff_u_pvs_profile_decodedatasupportproduct = ff_q_pvs_profile_decodedatasupportproduct_successor * S ((S (S ff_i_pvs_profile_decodedatasupportproduct)) * ff_v_pvs_profile_decodedatasupportproduct) + (ff_s_pvs_profile_decodedatasupportproduct))) /\ ff_s_pvs_profile_decodedatasupportproduct = ff_r_pvs_profile_decodedatasupportproduct * ff_p_pvs_profile_decodedatasupportproduct)))))))))))))) /\ (((((forall ppf_index_profile_decodedatagcdcommon ppf_entry_profile_decodedatagcdcommon. (exists pvs_gap_profile_decodedatagcdcommonbound. pvs_gap_profile_decodedatagcdcommonbound + S (ppf_index_profile_decodedatagcdcommon) = (ppf_length_profile_decode)) -> (((exists ff_h_pvs_profile_decodedatagcdcommonentry. ff_h_pvs_profile_decodedatagcdcommonentry + S (ppf_entry_profile_decodedatagcdcommon) = S ((S (ppf_index_profile_decodedatagcdcommon)) * ppf_ec_profile_decode)) /\ exists ff_q_pvs_profile_decodedatagcdcommonentry. ppf_eb_profile_decode = ff_q_pvs_profile_decodedatagcdcommonentry * S ((S (ppf_index_profile_decodedatagcdcommon)) * ppf_ec_profile_decode) + (ppf_entry_profile_decodedatagcdcommon))) -> (exists pvs_factor_profile_decodedatagcdcommondivisor. (ppf_entry_profile_decodedatagcdcommon) = (ppf_gcd_profile_decode) * pvs_factor_profile_decodedatagcdcommondivisor)) /\ (forall ppf_common_profile_decodedatagcd. (forall ppf_index_profile_decodedatagcdother ppf_entry_profile_decodedatagcdother. (exists pvs_gap_profile_decodedatagcdotherbound. pvs_gap_profile_decodedatagcdotherbound + S (ppf_index_profile_decodedatagcdother) = (ppf_length_profile_decode)) -> (((exists ff_h_pvs_profile_decodedatagcdotherentry. ff_h_pvs_profile_decodedatagcdotherentry + S (ppf_entry_profile_decodedatagcdother) = S ((S (ppf_index_profile_decodedatagcdother)) * ppf_ec_profile_decode)) /\ exists ff_q_pvs_profile_decodedatagcdotherentry. ppf_eb_profile_decode = ff_q_pvs_profile_decodedatagcdotherentry * S ((S (ppf_index_profile_decodedatagcdother)) * ppf_ec_profile_decode) + (ppf_entry_profile_decodedatagcdother))) -> (exists pvs_factor_profile_decodedatagcdotherdivisor. (ppf_entry_profile_decodedatagcdother) = (ppf_common_profile_decodedatagcd) * pvs_factor_profile_decodedatagcdotherdivisor)) -> (exists pvs_factor_profile_decodedatagcdgreatest. (ppf_gcd_profile_decode) = (ppf_common_profile_decodedatagcd) * pvs_factor_profile_decodedatagcdgreatest)))) /\ (((~((ppf_gcd_profile_decode) = 0)) /\ (forall ppf_table_degree_profile_decodedataroots. ~(ppf_table_degree_profile_decodedataroots = 0) -> (exists pvs_factor_profile_decodedatarootsdivisor. (ppf_gcd_profile_decode) = (ppf_table_degree_profile_decodedataroots) * pvs_factor_profile_decodedatarootsdivisor) -> exists ppf_table_root_profile_decodedataroots. (((exists ff_h_pvs_profile_decodedatarootsentry. ff_h_pvs_profile_decodedatarootsentry + S (ppf_table_root_profile_decodedataroots) = S ((S (ppf_table_degree_profile_decodedataroots)) * ppf_rc_profile_decode)) /\ exists ff_q_pvs_profile_decodedatarootsentry. ppf_rb_profile_decode = ff_q_pvs_profile_decodedatarootsentry * S ((S (ppf_table_degree_profile_decodedataroots)) * ppf_rc_profile_decode) + (ppf_table_root_profile_decodedataroots))) /\ (exists pa_b_pvs_profile_decodedatarootspower pa_c_pvs_profile_decodedatarootspower. ((forall pa_i_pvs_profile_decodedatarootspower_repeat. (exists pa_lt_pvs_profile_decodedatarootspower_repeat_bound. pa_lt_pvs_profile_decodedatarootspower_repeat_bound + S pa_i_pvs_profile_decodedatarootspower_repeat = ppf_table_degree_profile_decodedataroots) -> (((exists pa_h_pvs_profile_decodedatarootspower_repeat_decoded. pa_h_pvs_profile_decodedatarootspower_repeat_decoded + S (ppf_table_root_profile_decodedataroots) = S ((S (pa_i_pvs_profile_decodedatarootspower_repeat)) * pa_c_pvs_profile_decodedatarootspower)) /\ exists pa_q_pvs_profile_decodedatarootspower_repeat_decoded. pa_b_pvs_profile_decodedatarootspower = pa_q_pvs_profile_decodedatarootspower_repeat_decoded * S ((S (pa_i_pvs_profile_decodedatarootspower_repeat)) * pa_c_pvs_profile_decodedatarootspower) + (ppf_table_root_profile_decodedataroots)))) /\ (exists pa_u_pvs_profile_decodedatarootspower_product pa_v_pvs_profile_decodedatarootspower_product. ((((exists pa_h_pvs_profile_decodedatarootspower_product_start. pa_h_pvs_profile_decodedatarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_decodedatarootspower_product)) /\ exists pa_q_pvs_profile_decodedatarootspower_product_start. pa_u_pvs_profile_decodedatarootspower_product = pa_q_pvs_profile_decodedatarootspower_product_start * S ((S (0)) * pa_v_pvs_profile_decodedatarootspower_product) + (1))) /\ ((((exists pa_h_pvs_profile_decodedatarootspower_product_terminal. pa_h_pvs_profile_decodedatarootspower_product_terminal + S (n) = S ((S (ppf_table_degree_profile_decodedataroots)) * pa_v_pvs_profile_decodedatarootspower_product)) /\ exists pa_q_pvs_profile_decodedatarootspower_product_terminal. pa_u_pvs_profile_decodedatarootspower_product = pa_q_pvs_profile_decodedatarootspower_product_terminal * S ((S (ppf_table_degree_profile_decodedataroots)) * pa_v_pvs_profile_decodedatarootspower_product) + (n))) /\ forall pa_i_pvs_profile_decodedatarootspower_product. (exists pa_lt_pvs_profile_decodedatarootspower_product_bound. pa_lt_pvs_profile_decodedatarootspower_product_bound + S pa_i_pvs_profile_decodedatarootspower_product = ppf_table_degree_profile_decodedataroots) -> exists pa_p_pvs_profile_decodedatarootspower_product pa_r_pvs_profile_decodedatarootspower_product pa_s_pvs_profile_decodedatarootspower_product. ((((exists pa_h_pvs_profile_decodedatarootspower_product_factor. pa_h_pvs_profile_decodedatarootspower_product_factor + S (pa_p_pvs_profile_decodedatarootspower_product) = S ((S (pa_i_pvs_profile_decodedatarootspower_product)) * pa_c_pvs_profile_decodedatarootspower)) /\ exists pa_q_pvs_profile_decodedatarootspower_product_factor. pa_b_pvs_profile_decodedatarootspower = pa_q_pvs_profile_decodedatarootspower_product_factor * S ((S (pa_i_pvs_profile_decodedatarootspower_product)) * pa_c_pvs_profile_decodedatarootspower) + (pa_p_pvs_profile_decodedatarootspower_product))) /\ ((((exists pa_h_pvs_profile_decodedatarootspower_product_partial. pa_h_pvs_profile_decodedatarootspower_product_partial + S (pa_r_pvs_profile_decodedatarootspower_product) = S ((S (pa_i_pvs_profile_decodedatarootspower_product)) * pa_v_pvs_profile_decodedatarootspower_product)) /\ exists pa_q_pvs_profile_decodedatarootspower_product_partial. pa_u_pvs_profile_decodedatarootspower_product = pa_q_pvs_profile_decodedatarootspower_product_partial * S ((S (pa_i_pvs_profile_decodedatarootspower_product)) * pa_v_pvs_profile_decodedatarootspower_product) + (pa_r_pvs_profile_decodedatarootspower_product))) /\ ((((exists pa_h_pvs_profile_decodedatarootspower_product_successor. pa_h_pvs_profile_decodedatarootspower_product_successor + S (pa_s_pvs_profile_decodedatarootspower_product) = S ((S (S pa_i_pvs_profile_decodedatarootspower_product)) * pa_v_pvs_profile_decodedatarootspower_product)) /\ exists pa_q_pvs_profile_decodedatarootspower_product_successor. pa_u_pvs_profile_decodedatarootspower_product = pa_q_pvs_profile_decodedatarootspower_product_successor * S ((S (S pa_i_pvs_profile_decodedatarootspower_product)) * pa_v_pvs_profile_decodedatarootspower_product) + (pa_s_pvs_profile_decodedatarootspower_product))) /\ pa_s_pvs_profile_decodedatarootspower_product = pa_r_pvs_profile_decodedatarootspower_product * pa_p_pvs_profile_decodedatarootspower_product))))))))))))))))))))) -> ~(n = 1) -> exists pb pc eb ec vb vc l g rb rc. (((~((n) = 1)) /\ (((exists ppf_code_0_profile_decoded_datacode ppf_code_1_profile_decoded_datacode ppf_code_2_profile_decoded_datacode ppf_code_3_profile_decoded_datacode ppf_code_4_profile_decoded_datacode ppf_code_5_profile_decoded_datacode ppf_code_6_profile_decoded_datacode ppf_code_7_profile_decoded_datacode. ((((w) = ((pb) + (ppf_code_0_profile_decoded_datacode)) * S ((pb) + (ppf_code_0_profile_decoded_datacode)) + ((ppf_code_0_profile_decoded_datacode) + (ppf_code_0_profile_decoded_datacode))) /\ ((((ppf_code_0_profile_decoded_datacode) = ((pc) + (ppf_code_1_profile_decoded_datacode)) * S ((pc) + (ppf_code_1_profile_decoded_datacode)) + ((ppf_code_1_profile_decoded_datacode) + (ppf_code_1_profile_decoded_datacode))) /\ ((((ppf_code_1_profile_decoded_datacode) = ((eb) + (ppf_code_2_profile_decoded_datacode)) * S ((eb) + (ppf_code_2_profile_decoded_datacode)) + ((ppf_code_2_profile_decoded_datacode) + (ppf_code_2_profile_decoded_datacode))) /\ ((((ppf_code_2_profile_decoded_datacode) = ((ec) + (ppf_code_3_profile_decoded_datacode)) * S ((ec) + (ppf_code_3_profile_decoded_datacode)) + ((ppf_code_3_profile_decoded_datacode) + (ppf_code_3_profile_decoded_datacode))) /\ ((((ppf_code_3_profile_decoded_datacode) = ((vb) + (ppf_code_4_profile_decoded_datacode)) * S ((vb) + (ppf_code_4_profile_decoded_datacode)) + ((ppf_code_4_profile_decoded_datacode) + (ppf_code_4_profile_decoded_datacode))) /\ ((((ppf_code_4_profile_decoded_datacode) = ((vc) + (ppf_code_5_profile_decoded_datacode)) * S ((vc) + (ppf_code_5_profile_decoded_datacode)) + ((ppf_code_5_profile_decoded_datacode) + (ppf_code_5_profile_decoded_datacode))) /\ ((((ppf_code_5_profile_decoded_datacode) = ((l) + (ppf_code_6_profile_decoded_datacode)) * S ((l) + (ppf_code_6_profile_decoded_datacode)) + ((ppf_code_6_profile_decoded_datacode) + (ppf_code_6_profile_decoded_datacode))) /\ ((((ppf_code_6_profile_decoded_datacode) = ((g) + (ppf_code_7_profile_decoded_datacode)) * S ((g) + (ppf_code_7_profile_decoded_datacode)) + ((ppf_code_7_profile_decoded_datacode) + (ppf_code_7_profile_decoded_datacode))) /\ ((ppf_code_7_profile_decoded_datacode) = ((rb) + (rc)) * S ((rb) + (rc)) + ((rc) + (rc)))))))))))))))))))) /\ (((((~((n) = 0)) /\ (((forall pfp_i_pvs_profile_decoded_datasupportdistinct pfp_j_pvs_profile_decoded_datasupportdistinct pfp_a_pvs_profile_decoded_datasupportdistinct. (exists pfp_gap_pvs_profile_decoded_datasupportdistinctfirst. pfp_gap_pvs_profile_decoded_datasupportdistinctfirst + S (pfp_i_pvs_profile_decoded_datasupportdistinct) = (l)) -> (exists pfp_gap_pvs_profile_decoded_datasupportdistinctsecond. pfp_gap_pvs_profile_decoded_datasupportdistinctsecond + S (pfp_j_pvs_profile_decoded_datasupportdistinct) = (l)) -> (((exists ff_h_pfp_pvs_profile_decoded_datasupportdistinctleft. ff_h_pfp_pvs_profile_decoded_datasupportdistinctleft + S (pfp_a_pvs_profile_decoded_datasupportdistinct) = S ((S (pfp_i_pvs_profile_decoded_datasupportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_profile_decoded_datasupportdistinctleft. pb = ff_q_pfp_pvs_profile_decoded_datasupportdistinctleft * S ((S (pfp_i_pvs_profile_decoded_datasupportdistinct)) * pc) + (pfp_a_pvs_profile_decoded_datasupportdistinct))) -> (((exists ff_h_pfp_pvs_profile_decoded_datasupportdistinctright. ff_h_pfp_pvs_profile_decoded_datasupportdistinctright + S (pfp_a_pvs_profile_decoded_datasupportdistinct) = S ((S (pfp_j_pvs_profile_decoded_datasupportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_profile_decoded_datasupportdistinctright. pb = ff_q_pfp_pvs_profile_decoded_datasupportdistinctright * S ((S (pfp_j_pvs_profile_decoded_datasupportdistinct)) * pc) + (pfp_a_pvs_profile_decoded_datasupportdistinct))) -> pfp_i_pvs_profile_decoded_datasupportdistinct = pfp_j_pvs_profile_decoded_datasupportdistinct) /\ (((forall pvs_index_profile_decoded_datasupportentries. (exists pvs_gap_profile_decoded_datasupportentriesindex. pvs_gap_profile_decoded_datasupportentriesindex + S (pvs_index_profile_decoded_datasupportentries) = (l)) -> exists pvs_prime_profile_decoded_datasupportentries pvs_exponent_profile_decoded_datasupportentries pvs_power_profile_decoded_datasupportentries. (((((exists ff_h_pvs_profile_decoded_datasupportentriesprime. ff_h_pvs_profile_decoded_datasupportentriesprime + S (pvs_prime_profile_decoded_datasupportentries) = S ((S (pvs_index_profile_decoded_datasupportentries)) * pc)) /\ exists ff_q_pvs_profile_decoded_datasupportentriesprime. pb = ff_q_pvs_profile_decoded_datasupportentriesprime * S ((S (pvs_index_profile_decoded_datasupportentries)) * pc) + (pvs_prime_profile_decoded_datasupportentries))) /\ (((((exists ff_h_pvs_profile_decoded_datasupportentriesexponent. ff_h_pvs_profile_decoded_datasupportentriesexponent + S (pvs_exponent_profile_decoded_datasupportentries) = S ((S (pvs_index_profile_decoded_datasupportentries)) * ec)) /\ exists ff_q_pvs_profile_decoded_datasupportentriesexponent. eb = ff_q_pvs_profile_decoded_datasupportentriesexponent * S ((S (pvs_index_profile_decoded_datasupportentries)) * ec) + (pvs_exponent_profile_decoded_datasupportentries))) /\ (((((exists ff_h_pvs_profile_decoded_datasupportentriespower. ff_h_pvs_profile_decoded_datasupportentriespower + S (pvs_power_profile_decoded_datasupportentries) = S ((S (pvs_index_profile_decoded_datasupportentries)) * vc)) /\ exists ff_q_pvs_profile_decoded_datasupportentriespower. vb = ff_q_pvs_profile_decoded_datasupportentriespower * S ((S (pvs_index_profile_decoded_datasupportentries)) * vc) + (pvs_power_profile_decoded_datasupportentries))) /\ (((~((pvs_prime_profile_decoded_datasupportentries) = 1) /\ forall pvs_left_profile_decoded_datasupportentriesdomain pvs_right_profile_decoded_datasupportentriesdomain. (pvs_prime_profile_decoded_datasupportentries) = pvs_left_profile_decoded_datasupportentriesdomain * pvs_right_profile_decoded_datasupportentriesdomain -> pvs_left_profile_decoded_datasupportentriesdomain = 1 \/ pvs_right_profile_decoded_datasupportentriesdomain = 1) /\ (((~(pvs_exponent_profile_decoded_datasupportentries = 0)) /\ (((((exists bpd_gap_pvs_profile_decoded_datasupportentriesvaluation_selected_bound. bpd_gap_pvs_profile_decoded_datasupportentriesvaluation_selected_bound + (pvs_exponent_profile_decoded_datasupportentries) = (n)) /\ (exists bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_selected. ((exists bpvi_b_pvs_profile_decoded_datasupportentriesvaluation_selected_power bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_profile_decoded_datasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_profile_decoded_datasupportentriesvaluation_selected_power + S bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_selected_power = pvs_exponent_profile_decoded_datasupportentries) -> (((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_repeat + S (pvs_prime_profile_decoded_datasupportentries) = S ((S (bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_profile_decoded_datasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_selected_power) + (pvs_prime_profile_decoded_datasupportentries)))) /\ (exists bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_selected_power bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_start. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_start. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_selected) = S ((S (pvs_exponent_profile_decoded_datasupportentries)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_profile_decoded_datasupportentries)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power) + (bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_profile_decoded_datasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_profile_decoded_datasupportentriesvaluation_selected_power + S bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power = pvs_exponent_profile_decoded_datasupportentries) -> exists bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_selected_power bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_selected_power bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_profile_decoded_datasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_selected_power = bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_selected_power * bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_decoded_datasupportentriesvaluation_selected. n = bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_profile_decoded_datasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_profile_decoded_datasupportentriesvaluation. (exists bpd_gap_pvs_profile_decoded_datasupportentriesvaluation_candidate_bound. bpd_gap_pvs_profile_decoded_datasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_profile_decoded_datasupportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_profile_decoded_datasupportentriesvaluation_candidate_power bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_profile_decoded_datasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_profile_decoded_datasupportentriesvaluation_candidate_power + S bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_decoded_datasupportentriesvaluation) -> (((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_profile_decoded_datasupportentries) = S ((S (bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) + (pvs_prime_profile_decoded_datasupportentries)))) /\ (exists bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_candidate_power bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_profile_decoded_datasupportentriesvaluation)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_profile_decoded_datasupportentriesvaluation)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_profile_decoded_datasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_profile_decoded_datasupportentriesvaluation_candidate_power + S bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_decoded_datasupportentriesvaluation) -> exists bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_candidate_power bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_decoded_datasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_decoded_datasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power = bpvi_partial_pvs_profile_decoded_datasupportentriesvaluation_candidate_power * bpvi_factor_pvs_profile_decoded_datasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_decoded_datasupportentriesvaluation_candidate. n = bpvi_result_pvs_profile_decoded_datasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_profile_decoded_datasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_profile_decoded_datasupportentriesvaluation_maximal. bpd_gap_pvs_profile_decoded_datasupportentriesvaluation_maximal + (bpd_candidate_pvs_profile_decoded_datasupportentriesvaluation) = (pvs_exponent_profile_decoded_datasupportentries))) /\ (exists pa_b_pvs_profile_decoded_datasupportentriesvalue pa_c_pvs_profile_decoded_datasupportentriesvalue. ((forall pa_i_pvs_profile_decoded_datasupportentriesvalue_repeat. (exists pa_lt_pvs_profile_decoded_datasupportentriesvalue_repeat_bound. pa_lt_pvs_profile_decoded_datasupportentriesvalue_repeat_bound + S pa_i_pvs_profile_decoded_datasupportentriesvalue_repeat = pvs_exponent_profile_decoded_datasupportentries) -> (((exists pa_h_pvs_profile_decoded_datasupportentriesvalue_repeat_decoded. pa_h_pvs_profile_decoded_datasupportentriesvalue_repeat_decoded + S (pvs_prime_profile_decoded_datasupportentries) = S ((S (pa_i_pvs_profile_decoded_datasupportentriesvalue_repeat)) * pa_c_pvs_profile_decoded_datasupportentriesvalue)) /\ exists pa_q_pvs_profile_decoded_datasupportentriesvalue_repeat_decoded. pa_b_pvs_profile_decoded_datasupportentriesvalue = pa_q_pvs_profile_decoded_datasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_profile_decoded_datasupportentriesvalue_repeat)) * pa_c_pvs_profile_decoded_datasupportentriesvalue) + (pvs_prime_profile_decoded_datasupportentries)))) /\ (exists pa_u_pvs_profile_decoded_datasupportentriesvalue_product pa_v_pvs_profile_decoded_datasupportentriesvalue_product. ((((exists pa_h_pvs_profile_decoded_datasupportentriesvalue_product_start. pa_h_pvs_profile_decoded_datasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decoded_datasupportentriesvalue_product_start. pa_u_pvs_profile_decoded_datasupportentriesvalue_product = pa_q_pvs_profile_decoded_datasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_profile_decoded_datasupportentriesvalue_product_terminal. pa_h_pvs_profile_decoded_datasupportentriesvalue_product_terminal + S (pvs_power_profile_decoded_datasupportentries) = S ((S (pvs_exponent_profile_decoded_datasupportentries)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decoded_datasupportentriesvalue_product_terminal. pa_u_pvs_profile_decoded_datasupportentriesvalue_product = pa_q_pvs_profile_decoded_datasupportentriesvalue_product_terminal * S ((S (pvs_exponent_profile_decoded_datasupportentries)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product) + (pvs_power_profile_decoded_datasupportentries))) /\ forall pa_i_pvs_profile_decoded_datasupportentriesvalue_product. (exists pa_lt_pvs_profile_decoded_datasupportentriesvalue_product_bound. pa_lt_pvs_profile_decoded_datasupportentriesvalue_product_bound + S pa_i_pvs_profile_decoded_datasupportentriesvalue_product = pvs_exponent_profile_decoded_datasupportentries) -> exists pa_p_pvs_profile_decoded_datasupportentriesvalue_product pa_r_pvs_profile_decoded_datasupportentriesvalue_product pa_s_pvs_profile_decoded_datasupportentriesvalue_product. ((((exists pa_h_pvs_profile_decoded_datasupportentriesvalue_product_factor. pa_h_pvs_profile_decoded_datasupportentriesvalue_product_factor + S (pa_p_pvs_profile_decoded_datasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_decoded_datasupportentriesvalue_product)) * pa_c_pvs_profile_decoded_datasupportentriesvalue)) /\ exists pa_q_pvs_profile_decoded_datasupportentriesvalue_product_factor. pa_b_pvs_profile_decoded_datasupportentriesvalue = pa_q_pvs_profile_decoded_datasupportentriesvalue_product_factor * S ((S (pa_i_pvs_profile_decoded_datasupportentriesvalue_product)) * pa_c_pvs_profile_decoded_datasupportentriesvalue) + (pa_p_pvs_profile_decoded_datasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_decoded_datasupportentriesvalue_product_partial. pa_h_pvs_profile_decoded_datasupportentriesvalue_product_partial + S (pa_r_pvs_profile_decoded_datasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_decoded_datasupportentriesvalue_product)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decoded_datasupportentriesvalue_product_partial. pa_u_pvs_profile_decoded_datasupportentriesvalue_product = pa_q_pvs_profile_decoded_datasupportentriesvalue_product_partial * S ((S (pa_i_pvs_profile_decoded_datasupportentriesvalue_product)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product) + (pa_r_pvs_profile_decoded_datasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_decoded_datasupportentriesvalue_product_successor. pa_h_pvs_profile_decoded_datasupportentriesvalue_product_successor + S (pa_s_pvs_profile_decoded_datasupportentriesvalue_product) = S ((S (S pa_i_pvs_profile_decoded_datasupportentriesvalue_product)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_decoded_datasupportentriesvalue_product_successor. pa_u_pvs_profile_decoded_datasupportentriesvalue_product = pa_q_pvs_profile_decoded_datasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_profile_decoded_datasupportentriesvalue_product)) * pa_v_pvs_profile_decoded_datasupportentriesvalue_product) + (pa_s_pvs_profile_decoded_datasupportentriesvalue_product))) /\ pa_s_pvs_profile_decoded_datasupportentriesvalue_product = pa_r_pvs_profile_decoded_datasupportentriesvalue_product * pa_p_pvs_profile_decoded_datasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_profile_decoded_datasupportcover. (~((pvs_divisor_profile_decoded_datasupportcover) = 1) /\ forall pvs_left_profile_decoded_datasupportcoverprime pvs_right_profile_decoded_datasupportcoverprime. (pvs_divisor_profile_decoded_datasupportcover) = pvs_left_profile_decoded_datasupportcoverprime * pvs_right_profile_decoded_datasupportcoverprime -> pvs_left_profile_decoded_datasupportcoverprime = 1 \/ pvs_right_profile_decoded_datasupportcoverprime = 1) -> (exists pvs_factor_profile_decoded_datasupportcoverdivides. (n) = (pvs_divisor_profile_decoded_datasupportcover) * pvs_factor_profile_decoded_datasupportcoverdivides) -> exists pvs_position_profile_decoded_datasupportcover. (exists pvs_gap_profile_decoded_datasupportcoverbound. pvs_gap_profile_decoded_datasupportcoverbound + S (pvs_position_profile_decoded_datasupportcover) = (l)) /\ (((exists ff_h_pvs_profile_decoded_datasupportcoverentry. ff_h_pvs_profile_decoded_datasupportcoverentry + S (pvs_divisor_profile_decoded_datasupportcover) = S ((S (pvs_position_profile_decoded_datasupportcover)) * pc)) /\ exists ff_q_pvs_profile_decoded_datasupportcoverentry. pb = ff_q_pvs_profile_decoded_datasupportcoverentry * S ((S (pvs_position_profile_decoded_datasupportcover)) * pc) + (pvs_divisor_profile_decoded_datasupportcover)))) /\ (exists ff_u_pvs_profile_decoded_datasupportproduct ff_v_pvs_profile_decoded_datasupportproduct. ((((exists ff_h_pvs_profile_decoded_datasupportproduct_start. ff_h_pvs_profile_decoded_datasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_profile_decoded_datasupportproduct)) /\ exists ff_q_pvs_profile_decoded_datasupportproduct_start. ff_u_pvs_profile_decoded_datasupportproduct = ff_q_pvs_profile_decoded_datasupportproduct_start * S ((S (0)) * ff_v_pvs_profile_decoded_datasupportproduct) + (1))) /\ ((((exists ff_h_pvs_profile_decoded_datasupportproduct_terminal. ff_h_pvs_profile_decoded_datasupportproduct_terminal + S (n) = S ((S (l)) * ff_v_pvs_profile_decoded_datasupportproduct)) /\ exists ff_q_pvs_profile_decoded_datasupportproduct_terminal. ff_u_pvs_profile_decoded_datasupportproduct = ff_q_pvs_profile_decoded_datasupportproduct_terminal * S ((S (l)) * ff_v_pvs_profile_decoded_datasupportproduct) + (n))) /\ forall ff_i_pvs_profile_decoded_datasupportproduct. (exists ff_lt_pvs_profile_decoded_datasupportproduct_bound. ff_lt_pvs_profile_decoded_datasupportproduct_bound + S ff_i_pvs_profile_decoded_datasupportproduct = l) -> exists ff_p_pvs_profile_decoded_datasupportproduct ff_r_pvs_profile_decoded_datasupportproduct ff_s_pvs_profile_decoded_datasupportproduct. ((((exists ff_h_pvs_profile_decoded_datasupportproduct_factor. ff_h_pvs_profile_decoded_datasupportproduct_factor + S (ff_p_pvs_profile_decoded_datasupportproduct) = S ((S (ff_i_pvs_profile_decoded_datasupportproduct)) * vc)) /\ exists ff_q_pvs_profile_decoded_datasupportproduct_factor. vb = ff_q_pvs_profile_decoded_datasupportproduct_factor * S ((S (ff_i_pvs_profile_decoded_datasupportproduct)) * vc) + (ff_p_pvs_profile_decoded_datasupportproduct))) /\ ((((exists ff_h_pvs_profile_decoded_datasupportproduct_partial. ff_h_pvs_profile_decoded_datasupportproduct_partial + S (ff_r_pvs_profile_decoded_datasupportproduct) = S ((S (ff_i_pvs_profile_decoded_datasupportproduct)) * ff_v_pvs_profile_decoded_datasupportproduct)) /\ exists ff_q_pvs_profile_decoded_datasupportproduct_partial. ff_u_pvs_profile_decoded_datasupportproduct = ff_q_pvs_profile_decoded_datasupportproduct_partial * S ((S (ff_i_pvs_profile_decoded_datasupportproduct)) * ff_v_pvs_profile_decoded_datasupportproduct) + (ff_r_pvs_profile_decoded_datasupportproduct))) /\ ((((exists ff_h_pvs_profile_decoded_datasupportproduct_successor. ff_h_pvs_profile_decoded_datasupportproduct_successor + S (ff_s_pvs_profile_decoded_datasupportproduct) = S ((S (S ff_i_pvs_profile_decoded_datasupportproduct)) * ff_v_pvs_profile_decoded_datasupportproduct)) /\ exists ff_q_pvs_profile_decoded_datasupportproduct_successor. ff_u_pvs_profile_decoded_datasupportproduct = ff_q_pvs_profile_decoded_datasupportproduct_successor * S ((S (S ff_i_pvs_profile_decoded_datasupportproduct)) * ff_v_pvs_profile_decoded_datasupportproduct) + (ff_s_pvs_profile_decoded_datasupportproduct))) /\ ff_s_pvs_profile_decoded_datasupportproduct = ff_r_pvs_profile_decoded_datasupportproduct * ff_p_pvs_profile_decoded_datasupportproduct)))))))))))))) /\ (((((forall ppf_index_profile_decoded_datagcdcommon ppf_entry_profile_decoded_datagcdcommon. (exists pvs_gap_profile_decoded_datagcdcommonbound. pvs_gap_profile_decoded_datagcdcommonbound + S (ppf_index_profile_decoded_datagcdcommon) = (l)) -> (((exists ff_h_pvs_profile_decoded_datagcdcommonentry. ff_h_pvs_profile_decoded_datagcdcommonentry + S (ppf_entry_profile_decoded_datagcdcommon) = S ((S (ppf_index_profile_decoded_datagcdcommon)) * ec)) /\ exists ff_q_pvs_profile_decoded_datagcdcommonentry. eb = ff_q_pvs_profile_decoded_datagcdcommonentry * S ((S (ppf_index_profile_decoded_datagcdcommon)) * ec) + (ppf_entry_profile_decoded_datagcdcommon))) -> (exists pvs_factor_profile_decoded_datagcdcommondivisor. (ppf_entry_profile_decoded_datagcdcommon) = (g) * pvs_factor_profile_decoded_datagcdcommondivisor)) /\ (forall ppf_common_profile_decoded_datagcd. (forall ppf_index_profile_decoded_datagcdother ppf_entry_profile_decoded_datagcdother. (exists pvs_gap_profile_decoded_datagcdotherbound. pvs_gap_profile_decoded_datagcdotherbound + S (ppf_index_profile_decoded_datagcdother) = (l)) -> (((exists ff_h_pvs_profile_decoded_datagcdotherentry. ff_h_pvs_profile_decoded_datagcdotherentry + S (ppf_entry_profile_decoded_datagcdother) = S ((S (ppf_index_profile_decoded_datagcdother)) * ec)) /\ exists ff_q_pvs_profile_decoded_datagcdotherentry. eb = ff_q_pvs_profile_decoded_datagcdotherentry * S ((S (ppf_index_profile_decoded_datagcdother)) * ec) + (ppf_entry_profile_decoded_datagcdother))) -> (exists pvs_factor_profile_decoded_datagcdotherdivisor. (ppf_entry_profile_decoded_datagcdother) = (ppf_common_profile_decoded_datagcd) * pvs_factor_profile_decoded_datagcdotherdivisor)) -> (exists pvs_factor_profile_decoded_datagcdgreatest. (g) = (ppf_common_profile_decoded_datagcd) * pvs_factor_profile_decoded_datagcdgreatest)))) /\ (((~((g) = 0)) /\ (forall ppf_table_degree_profile_decoded_dataroots. ~(ppf_table_degree_profile_decoded_dataroots = 0) -> (exists pvs_factor_profile_decoded_datarootsdivisor. (g) = (ppf_table_degree_profile_decoded_dataroots) * pvs_factor_profile_decoded_datarootsdivisor) -> exists ppf_table_root_profile_decoded_dataroots. (((exists ff_h_pvs_profile_decoded_datarootsentry. ff_h_pvs_profile_decoded_datarootsentry + S (ppf_table_root_profile_decoded_dataroots) = S ((S (ppf_table_degree_profile_decoded_dataroots)) * rc)) /\ exists ff_q_pvs_profile_decoded_datarootsentry. rb = ff_q_pvs_profile_decoded_datarootsentry * S ((S (ppf_table_degree_profile_decoded_dataroots)) * rc) + (ppf_table_root_profile_decoded_dataroots))) /\ (exists pa_b_pvs_profile_decoded_datarootspower pa_c_pvs_profile_decoded_datarootspower. ((forall pa_i_pvs_profile_decoded_datarootspower_repeat. (exists pa_lt_pvs_profile_decoded_datarootspower_repeat_bound. pa_lt_pvs_profile_decoded_datarootspower_repeat_bound + S pa_i_pvs_profile_decoded_datarootspower_repeat = ppf_table_degree_profile_decoded_dataroots) -> (((exists pa_h_pvs_profile_decoded_datarootspower_repeat_decoded. pa_h_pvs_profile_decoded_datarootspower_repeat_decoded + S (ppf_table_root_profile_decoded_dataroots) = S ((S (pa_i_pvs_profile_decoded_datarootspower_repeat)) * pa_c_pvs_profile_decoded_datarootspower)) /\ exists pa_q_pvs_profile_decoded_datarootspower_repeat_decoded. pa_b_pvs_profile_decoded_datarootspower = pa_q_pvs_profile_decoded_datarootspower_repeat_decoded * S ((S (pa_i_pvs_profile_decoded_datarootspower_repeat)) * pa_c_pvs_profile_decoded_datarootspower) + (ppf_table_root_profile_decoded_dataroots)))) /\ (exists pa_u_pvs_profile_decoded_datarootspower_product pa_v_pvs_profile_decoded_datarootspower_product. ((((exists pa_h_pvs_profile_decoded_datarootspower_product_start. pa_h_pvs_profile_decoded_datarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_decoded_datarootspower_product)) /\ exists pa_q_pvs_profile_decoded_datarootspower_product_start. pa_u_pvs_profile_decoded_datarootspower_product = pa_q_pvs_profile_decoded_datarootspower_product_start * S ((S (0)) * pa_v_pvs_profile_decoded_datarootspower_product) + (1))) /\ ((((exists pa_h_pvs_profile_decoded_datarootspower_product_terminal. pa_h_pvs_profile_decoded_datarootspower_product_terminal + S (n) = S ((S (ppf_table_degree_profile_decoded_dataroots)) * pa_v_pvs_profile_decoded_datarootspower_product)) /\ exists pa_q_pvs_profile_decoded_datarootspower_product_terminal. pa_u_pvs_profile_decoded_datarootspower_product = pa_q_pvs_profile_decoded_datarootspower_product_terminal * S ((S (ppf_table_degree_profile_decoded_dataroots)) * pa_v_pvs_profile_decoded_datarootspower_product) + (n))) /\ forall pa_i_pvs_profile_decoded_datarootspower_product. (exists pa_lt_pvs_profile_decoded_datarootspower_product_bound. pa_lt_pvs_profile_decoded_datarootspower_product_bound + S pa_i_pvs_profile_decoded_datarootspower_product = ppf_table_degree_profile_decoded_dataroots) -> exists pa_p_pvs_profile_decoded_datarootspower_product pa_r_pvs_profile_decoded_datarootspower_product pa_s_pvs_profile_decoded_datarootspower_product. ((((exists pa_h_pvs_profile_decoded_datarootspower_product_factor. pa_h_pvs_profile_decoded_datarootspower_product_factor + S (pa_p_pvs_profile_decoded_datarootspower_product) = S ((S (pa_i_pvs_profile_decoded_datarootspower_product)) * pa_c_pvs_profile_decoded_datarootspower)) /\ exists pa_q_pvs_profile_decoded_datarootspower_product_factor. pa_b_pvs_profile_decoded_datarootspower = pa_q_pvs_profile_decoded_datarootspower_product_factor * S ((S (pa_i_pvs_profile_decoded_datarootspower_product)) * pa_c_pvs_profile_decoded_datarootspower) + (pa_p_pvs_profile_decoded_datarootspower_product))) /\ ((((exists pa_h_pvs_profile_decoded_datarootspower_product_partial. pa_h_pvs_profile_decoded_datarootspower_product_partial + S (pa_r_pvs_profile_decoded_datarootspower_product) = S ((S (pa_i_pvs_profile_decoded_datarootspower_product)) * pa_v_pvs_profile_decoded_datarootspower_product)) /\ exists pa_q_pvs_profile_decoded_datarootspower_product_partial. pa_u_pvs_profile_decoded_datarootspower_product = pa_q_pvs_profile_decoded_datarootspower_product_partial * S ((S (pa_i_pvs_profile_decoded_datarootspower_product)) * pa_v_pvs_profile_decoded_datarootspower_product) + (pa_r_pvs_profile_decoded_datarootspower_product))) /\ ((((exists pa_h_pvs_profile_decoded_datarootspower_product_successor. pa_h_pvs_profile_decoded_datarootspower_product_successor + S (pa_s_pvs_profile_decoded_datarootspower_product) = S ((S (S pa_i_pvs_profile_decoded_datarootspower_product)) * pa_v_pvs_profile_decoded_datarootspower_product)) /\ exists pa_q_pvs_profile_decoded_datarootspower_product_successor. pa_u_pvs_profile_decoded_datarootspower_product = pa_q_pvs_profile_decoded_datarootspower_product_successor * S ((S (S pa_i_pvs_profile_decoded_datarootspower_product)) * pa_v_pvs_profile_decoded_datarootspower_product) + (pa_s_pvs_profile_decoded_datarootspower_product))) /\ pa_s_pvs_profile_decoded_datarootspower_product = pa_r_pvs_profile_decoded_datarootspower_product * pa_p_pvs_profile_decoded_datarootspower_product)))))))))))))))))))