perfect_power_profile_exists

Exact expanded first-order arithmetic statement

forall n. ~(n = 0) -> exists w. (((((n) = 1) /\ ((((w) = 0) /\ (forall ppf_unit_degree_profile_constructedunit. ~(ppf_unit_degree_profile_constructedunit = 0) -> (exists pa_b_pvs_profile_constructedunitidentity pa_c_pvs_profile_constructedunitidentity. ((forall pa_i_pvs_profile_constructedunitidentity_repeat. (exists pa_lt_pvs_profile_constructedunitidentity_repeat_bound. pa_lt_pvs_profile_constructedunitidentity_repeat_bound + S pa_i_pvs_profile_constructedunitidentity_repeat = ppf_unit_degree_profile_constructedunit) -> (((exists pa_h_pvs_profile_constructedunitidentity_repeat_decoded. pa_h_pvs_profile_constructedunitidentity_repeat_decoded + S (1) = S ((S (pa_i_pvs_profile_constructedunitidentity_repeat)) * pa_c_pvs_profile_constructedunitidentity)) /\ exists pa_q_pvs_profile_constructedunitidentity_repeat_decoded. pa_b_pvs_profile_constructedunitidentity = pa_q_pvs_profile_constructedunitidentity_repeat_decoded * S ((S (pa_i_pvs_profile_constructedunitidentity_repeat)) * pa_c_pvs_profile_constructedunitidentity) + (1)))) /\ (exists pa_u_pvs_profile_constructedunitidentity_product pa_v_pvs_profile_constructedunitidentity_product. ((((exists pa_h_pvs_profile_constructedunitidentity_product_start. pa_h_pvs_profile_constructedunitidentity_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_constructedunitidentity_product)) /\ exists pa_q_pvs_profile_constructedunitidentity_product_start. pa_u_pvs_profile_constructedunitidentity_product = pa_q_pvs_profile_constructedunitidentity_product_start * S ((S (0)) * pa_v_pvs_profile_constructedunitidentity_product) + (1))) /\ ((((exists pa_h_pvs_profile_constructedunitidentity_product_terminal. pa_h_pvs_profile_constructedunitidentity_product_terminal + S (1) = S ((S (ppf_unit_degree_profile_constructedunit)) * pa_v_pvs_profile_constructedunitidentity_product)) /\ exists pa_q_pvs_profile_constructedunitidentity_product_terminal. pa_u_pvs_profile_constructedunitidentity_product = pa_q_pvs_profile_constructedunitidentity_product_terminal * S ((S (ppf_unit_degree_profile_constructedunit)) * pa_v_pvs_profile_constructedunitidentity_product) + (1))) /\ forall pa_i_pvs_profile_constructedunitidentity_product. (exists pa_lt_pvs_profile_constructedunitidentity_product_bound. pa_lt_pvs_profile_constructedunitidentity_product_bound + S pa_i_pvs_profile_constructedunitidentity_product = ppf_unit_degree_profile_constructedunit) -> exists pa_p_pvs_profile_constructedunitidentity_product pa_r_pvs_profile_constructedunitidentity_product pa_s_pvs_profile_constructedunitidentity_product. ((((exists pa_h_pvs_profile_constructedunitidentity_product_factor. pa_h_pvs_profile_constructedunitidentity_product_factor + S (pa_p_pvs_profile_constructedunitidentity_product) = S ((S (pa_i_pvs_profile_constructedunitidentity_product)) * pa_c_pvs_profile_constructedunitidentity)) /\ exists pa_q_pvs_profile_constructedunitidentity_product_factor. pa_b_pvs_profile_constructedunitidentity = pa_q_pvs_profile_constructedunitidentity_product_factor * S ((S (pa_i_pvs_profile_constructedunitidentity_product)) * pa_c_pvs_profile_constructedunitidentity) + (pa_p_pvs_profile_constructedunitidentity_product))) /\ ((((exists pa_h_pvs_profile_constructedunitidentity_product_partial. pa_h_pvs_profile_constructedunitidentity_product_partial + S (pa_r_pvs_profile_constructedunitidentity_product) = S ((S (pa_i_pvs_profile_constructedunitidentity_product)) * pa_v_pvs_profile_constructedunitidentity_product)) /\ exists pa_q_pvs_profile_constructedunitidentity_product_partial. pa_u_pvs_profile_constructedunitidentity_product = pa_q_pvs_profile_constructedunitidentity_product_partial * S ((S (pa_i_pvs_profile_constructedunitidentity_product)) * pa_v_pvs_profile_constructedunitidentity_product) + (pa_r_pvs_profile_constructedunitidentity_product))) /\ ((((exists pa_h_pvs_profile_constructedunitidentity_product_successor. pa_h_pvs_profile_constructedunitidentity_product_successor + S (pa_s_pvs_profile_constructedunitidentity_product) = S ((S (S pa_i_pvs_profile_constructedunitidentity_product)) * pa_v_pvs_profile_constructedunitidentity_product)) /\ exists pa_q_pvs_profile_constructedunitidentity_product_successor. pa_u_pvs_profile_constructedunitidentity_product = pa_q_pvs_profile_constructedunitidentity_product_successor * S ((S (S pa_i_pvs_profile_constructedunitidentity_product)) * pa_v_pvs_profile_constructedunitidentity_product) + (pa_s_pvs_profile_constructedunitidentity_product))) /\ pa_s_pvs_profile_constructedunitidentity_product = pa_r_pvs_profile_constructedunitidentity_product * pa_p_pvs_profile_constructedunitidentity_product))))))))))))) \/ (exists ppf_pb_profile_constructed ppf_pc_profile_constructed ppf_eb_profile_constructed ppf_ec_profile_constructed ppf_vb_profile_constructed ppf_vc_profile_constructed ppf_length_profile_constructed ppf_gcd_profile_constructed ppf_rb_profile_constructed ppf_rc_profile_constructed. (((~((n) = 1)) /\ (((exists ppf_code_0_profile_constructeddatacode ppf_code_1_profile_constructeddatacode ppf_code_2_profile_constructeddatacode ppf_code_3_profile_constructeddatacode ppf_code_4_profile_constructeddatacode ppf_code_5_profile_constructeddatacode ppf_code_6_profile_constructeddatacode ppf_code_7_profile_constructeddatacode. ((((w) = ((ppf_pb_profile_constructed) + (ppf_code_0_profile_constructeddatacode)) * S ((ppf_pb_profile_constructed) + (ppf_code_0_profile_constructeddatacode)) + ((ppf_code_0_profile_constructeddatacode) + (ppf_code_0_profile_constructeddatacode))) /\ ((((ppf_code_0_profile_constructeddatacode) = ((ppf_pc_profile_constructed) + (ppf_code_1_profile_constructeddatacode)) * S ((ppf_pc_profile_constructed) + (ppf_code_1_profile_constructeddatacode)) + ((ppf_code_1_profile_constructeddatacode) + (ppf_code_1_profile_constructeddatacode))) /\ ((((ppf_code_1_profile_constructeddatacode) = ((ppf_eb_profile_constructed) + (ppf_code_2_profile_constructeddatacode)) * S ((ppf_eb_profile_constructed) + (ppf_code_2_profile_constructeddatacode)) + ((ppf_code_2_profile_constructeddatacode) + (ppf_code_2_profile_constructeddatacode))) /\ ((((ppf_code_2_profile_constructeddatacode) = ((ppf_ec_profile_constructed) + (ppf_code_3_profile_constructeddatacode)) * S ((ppf_ec_profile_constructed) + (ppf_code_3_profile_constructeddatacode)) + ((ppf_code_3_profile_constructeddatacode) + (ppf_code_3_profile_constructeddatacode))) /\ ((((ppf_code_3_profile_constructeddatacode) = ((ppf_vb_profile_constructed) + (ppf_code_4_profile_constructeddatacode)) * S ((ppf_vb_profile_constructed) + (ppf_code_4_profile_constructeddatacode)) + ((ppf_code_4_profile_constructeddatacode) + (ppf_code_4_profile_constructeddatacode))) /\ ((((ppf_code_4_profile_constructeddatacode) = ((ppf_vc_profile_constructed) + (ppf_code_5_profile_constructeddatacode)) * S ((ppf_vc_profile_constructed) + (ppf_code_5_profile_constructeddatacode)) + ((ppf_code_5_profile_constructeddatacode) + (ppf_code_5_profile_constructeddatacode))) /\ ((((ppf_code_5_profile_constructeddatacode) = ((ppf_length_profile_constructed) + (ppf_code_6_profile_constructeddatacode)) * S ((ppf_length_profile_constructed) + (ppf_code_6_profile_constructeddatacode)) + ((ppf_code_6_profile_constructeddatacode) + (ppf_code_6_profile_constructeddatacode))) /\ ((((ppf_code_6_profile_constructeddatacode) = ((ppf_gcd_profile_constructed) + (ppf_code_7_profile_constructeddatacode)) * S ((ppf_gcd_profile_constructed) + (ppf_code_7_profile_constructeddatacode)) + ((ppf_code_7_profile_constructeddatacode) + (ppf_code_7_profile_constructeddatacode))) /\ ((ppf_code_7_profile_constructeddatacode) = ((ppf_rb_profile_constructed) + (ppf_rc_profile_constructed)) * S ((ppf_rb_profile_constructed) + (ppf_rc_profile_constructed)) + ((ppf_rc_profile_constructed) + (ppf_rc_profile_constructed)))))))))))))))))))) /\ (((((~((n) = 0)) /\ (((forall pfp_i_pvs_profile_constructeddatasupportdistinct pfp_j_pvs_profile_constructeddatasupportdistinct pfp_a_pvs_profile_constructeddatasupportdistinct. (exists pfp_gap_pvs_profile_constructeddatasupportdistinctfirst. pfp_gap_pvs_profile_constructeddatasupportdistinctfirst + S (pfp_i_pvs_profile_constructeddatasupportdistinct) = (ppf_length_profile_constructed)) -> (exists pfp_gap_pvs_profile_constructeddatasupportdistinctsecond. pfp_gap_pvs_profile_constructeddatasupportdistinctsecond + S (pfp_j_pvs_profile_constructeddatasupportdistinct) = (ppf_length_profile_constructed)) -> (((exists ff_h_pfp_pvs_profile_constructeddatasupportdistinctleft. ff_h_pfp_pvs_profile_constructeddatasupportdistinctleft + S (pfp_a_pvs_profile_constructeddatasupportdistinct) = S ((S (pfp_i_pvs_profile_constructeddatasupportdistinct)) * ppf_pc_profile_constructed)) /\ exists ff_q_pfp_pvs_profile_constructeddatasupportdistinctleft. ppf_pb_profile_constructed = ff_q_pfp_pvs_profile_constructeddatasupportdistinctleft * S ((S (pfp_i_pvs_profile_constructeddatasupportdistinct)) * ppf_pc_profile_constructed) + (pfp_a_pvs_profile_constructeddatasupportdistinct))) -> (((exists ff_h_pfp_pvs_profile_constructeddatasupportdistinctright. ff_h_pfp_pvs_profile_constructeddatasupportdistinctright + S (pfp_a_pvs_profile_constructeddatasupportdistinct) = S ((S (pfp_j_pvs_profile_constructeddatasupportdistinct)) * ppf_pc_profile_constructed)) /\ exists ff_q_pfp_pvs_profile_constructeddatasupportdistinctright. ppf_pb_profile_constructed = ff_q_pfp_pvs_profile_constructeddatasupportdistinctright * S ((S (pfp_j_pvs_profile_constructeddatasupportdistinct)) * ppf_pc_profile_constructed) + (pfp_a_pvs_profile_constructeddatasupportdistinct))) -> pfp_i_pvs_profile_constructeddatasupportdistinct = pfp_j_pvs_profile_constructeddatasupportdistinct) /\ (((forall pvs_index_profile_constructeddatasupportentries. (exists pvs_gap_profile_constructeddatasupportentriesindex. pvs_gap_profile_constructeddatasupportentriesindex + S (pvs_index_profile_constructeddatasupportentries) = (ppf_length_profile_constructed)) -> exists pvs_prime_profile_constructeddatasupportentries pvs_exponent_profile_constructeddatasupportentries pvs_power_profile_constructeddatasupportentries. (((((exists ff_h_pvs_profile_constructeddatasupportentriesprime. ff_h_pvs_profile_constructeddatasupportentriesprime + S (pvs_prime_profile_constructeddatasupportentries) = S ((S (pvs_index_profile_constructeddatasupportentries)) * ppf_pc_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatasupportentriesprime. ppf_pb_profile_constructed = ff_q_pvs_profile_constructeddatasupportentriesprime * S ((S (pvs_index_profile_constructeddatasupportentries)) * ppf_pc_profile_constructed) + (pvs_prime_profile_constructeddatasupportentries))) /\ (((((exists ff_h_pvs_profile_constructeddatasupportentriesexponent. ff_h_pvs_profile_constructeddatasupportentriesexponent + S (pvs_exponent_profile_constructeddatasupportentries) = S ((S (pvs_index_profile_constructeddatasupportentries)) * ppf_ec_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatasupportentriesexponent. ppf_eb_profile_constructed = ff_q_pvs_profile_constructeddatasupportentriesexponent * S ((S (pvs_index_profile_constructeddatasupportentries)) * ppf_ec_profile_constructed) + (pvs_exponent_profile_constructeddatasupportentries))) /\ (((((exists ff_h_pvs_profile_constructeddatasupportentriespower. ff_h_pvs_profile_constructeddatasupportentriespower + S (pvs_power_profile_constructeddatasupportentries) = S ((S (pvs_index_profile_constructeddatasupportentries)) * ppf_vc_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatasupportentriespower. ppf_vb_profile_constructed = ff_q_pvs_profile_constructeddatasupportentriespower * S ((S (pvs_index_profile_constructeddatasupportentries)) * ppf_vc_profile_constructed) + (pvs_power_profile_constructeddatasupportentries))) /\ (((~((pvs_prime_profile_constructeddatasupportentries) = 1) /\ forall pvs_left_profile_constructeddatasupportentriesdomain pvs_right_profile_constructeddatasupportentriesdomain. (pvs_prime_profile_constructeddatasupportentries) = pvs_left_profile_constructeddatasupportentriesdomain * pvs_right_profile_constructeddatasupportentriesdomain -> pvs_left_profile_constructeddatasupportentriesdomain = 1 \/ pvs_right_profile_constructeddatasupportentriesdomain = 1) /\ (((~(pvs_exponent_profile_constructeddatasupportentries = 0)) /\ (((((exists bpd_gap_pvs_profile_constructeddatasupportentriesvaluation_selected_bound. bpd_gap_pvs_profile_constructeddatasupportentriesvaluation_selected_bound + (pvs_exponent_profile_constructeddatasupportentries) = (n)) /\ (exists bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_selected. ((exists bpvi_b_pvs_profile_constructeddatasupportentriesvaluation_selected_power bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_profile_constructeddatasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_profile_constructeddatasupportentriesvaluation_selected_power + S bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_selected_power = pvs_exponent_profile_constructeddatasupportentries) -> (((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_repeat + S (pvs_prime_profile_constructeddatasupportentries) = S ((S (bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_profile_constructeddatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_selected_power) + (pvs_prime_profile_constructeddatasupportentries)))) /\ (exists bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_selected_power bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_start. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_start. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_selected) = S ((S (pvs_exponent_profile_constructeddatasupportentries)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_profile_constructeddatasupportentries)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power) + (bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_profile_constructeddatasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_profile_constructeddatasupportentriesvaluation_selected_power + S bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power = pvs_exponent_profile_constructeddatasupportentries) -> exists bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_selected_power bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_selected_power bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_profile_constructeddatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_selected_power = bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_selected_power * bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_constructeddatasupportentriesvaluation_selected. n = bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_profile_constructeddatasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_profile_constructeddatasupportentriesvaluation. (exists bpd_gap_pvs_profile_constructeddatasupportentriesvaluation_candidate_bound. bpd_gap_pvs_profile_constructeddatasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_profile_constructeddatasupportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_profile_constructeddatasupportentriesvaluation_candidate_power bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_profile_constructeddatasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_profile_constructeddatasupportentriesvaluation_candidate_power + S bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_constructeddatasupportentriesvaluation) -> (((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_profile_constructeddatasupportentries) = S ((S (bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) + (pvs_prime_profile_constructeddatasupportentries)))) /\ (exists bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_candidate_power bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_profile_constructeddatasupportentriesvaluation)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_profile_constructeddatasupportentriesvaluation)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_profile_constructeddatasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_profile_constructeddatasupportentriesvaluation_candidate_power + S bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_constructeddatasupportentriesvaluation) -> exists bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_candidate_power bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_constructeddatasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_constructeddatasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power = bpvi_partial_pvs_profile_constructeddatasupportentriesvaluation_candidate_power * bpvi_factor_pvs_profile_constructeddatasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_constructeddatasupportentriesvaluation_candidate. n = bpvi_result_pvs_profile_constructeddatasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_profile_constructeddatasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_profile_constructeddatasupportentriesvaluation_maximal. bpd_gap_pvs_profile_constructeddatasupportentriesvaluation_maximal + (bpd_candidate_pvs_profile_constructeddatasupportentriesvaluation) = (pvs_exponent_profile_constructeddatasupportentries))) /\ (exists pa_b_pvs_profile_constructeddatasupportentriesvalue pa_c_pvs_profile_constructeddatasupportentriesvalue. ((forall pa_i_pvs_profile_constructeddatasupportentriesvalue_repeat. (exists pa_lt_pvs_profile_constructeddatasupportentriesvalue_repeat_bound. pa_lt_pvs_profile_constructeddatasupportentriesvalue_repeat_bound + S pa_i_pvs_profile_constructeddatasupportentriesvalue_repeat = pvs_exponent_profile_constructeddatasupportentries) -> (((exists pa_h_pvs_profile_constructeddatasupportentriesvalue_repeat_decoded. pa_h_pvs_profile_constructeddatasupportentriesvalue_repeat_decoded + S (pvs_prime_profile_constructeddatasupportentries) = S ((S (pa_i_pvs_profile_constructeddatasupportentriesvalue_repeat)) * pa_c_pvs_profile_constructeddatasupportentriesvalue)) /\ exists pa_q_pvs_profile_constructeddatasupportentriesvalue_repeat_decoded. pa_b_pvs_profile_constructeddatasupportentriesvalue = pa_q_pvs_profile_constructeddatasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_profile_constructeddatasupportentriesvalue_repeat)) * pa_c_pvs_profile_constructeddatasupportentriesvalue) + (pvs_prime_profile_constructeddatasupportentries)))) /\ (exists pa_u_pvs_profile_constructeddatasupportentriesvalue_product pa_v_pvs_profile_constructeddatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_constructeddatasupportentriesvalue_product_start. pa_h_pvs_profile_constructeddatasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_constructeddatasupportentriesvalue_product_start. pa_u_pvs_profile_constructeddatasupportentriesvalue_product = pa_q_pvs_profile_constructeddatasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_profile_constructeddatasupportentriesvalue_product_terminal. pa_h_pvs_profile_constructeddatasupportentriesvalue_product_terminal + S (pvs_power_profile_constructeddatasupportentries) = S ((S (pvs_exponent_profile_constructeddatasupportentries)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_constructeddatasupportentriesvalue_product_terminal. pa_u_pvs_profile_constructeddatasupportentriesvalue_product = pa_q_pvs_profile_constructeddatasupportentriesvalue_product_terminal * S ((S (pvs_exponent_profile_constructeddatasupportentries)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product) + (pvs_power_profile_constructeddatasupportentries))) /\ forall pa_i_pvs_profile_constructeddatasupportentriesvalue_product. (exists pa_lt_pvs_profile_constructeddatasupportentriesvalue_product_bound. pa_lt_pvs_profile_constructeddatasupportentriesvalue_product_bound + S pa_i_pvs_profile_constructeddatasupportentriesvalue_product = pvs_exponent_profile_constructeddatasupportentries) -> exists pa_p_pvs_profile_constructeddatasupportentriesvalue_product pa_r_pvs_profile_constructeddatasupportentriesvalue_product pa_s_pvs_profile_constructeddatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_constructeddatasupportentriesvalue_product_factor. pa_h_pvs_profile_constructeddatasupportentriesvalue_product_factor + S (pa_p_pvs_profile_constructeddatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_constructeddatasupportentriesvalue_product)) * pa_c_pvs_profile_constructeddatasupportentriesvalue)) /\ exists pa_q_pvs_profile_constructeddatasupportentriesvalue_product_factor. pa_b_pvs_profile_constructeddatasupportentriesvalue = pa_q_pvs_profile_constructeddatasupportentriesvalue_product_factor * S ((S (pa_i_pvs_profile_constructeddatasupportentriesvalue_product)) * pa_c_pvs_profile_constructeddatasupportentriesvalue) + (pa_p_pvs_profile_constructeddatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_constructeddatasupportentriesvalue_product_partial. pa_h_pvs_profile_constructeddatasupportentriesvalue_product_partial + S (pa_r_pvs_profile_constructeddatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_constructeddatasupportentriesvalue_product)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_constructeddatasupportentriesvalue_product_partial. pa_u_pvs_profile_constructeddatasupportentriesvalue_product = pa_q_pvs_profile_constructeddatasupportentriesvalue_product_partial * S ((S (pa_i_pvs_profile_constructeddatasupportentriesvalue_product)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product) + (pa_r_pvs_profile_constructeddatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_constructeddatasupportentriesvalue_product_successor. pa_h_pvs_profile_constructeddatasupportentriesvalue_product_successor + S (pa_s_pvs_profile_constructeddatasupportentriesvalue_product) = S ((S (S pa_i_pvs_profile_constructeddatasupportentriesvalue_product)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_constructeddatasupportentriesvalue_product_successor. pa_u_pvs_profile_constructeddatasupportentriesvalue_product = pa_q_pvs_profile_constructeddatasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_profile_constructeddatasupportentriesvalue_product)) * pa_v_pvs_profile_constructeddatasupportentriesvalue_product) + (pa_s_pvs_profile_constructeddatasupportentriesvalue_product))) /\ pa_s_pvs_profile_constructeddatasupportentriesvalue_product = pa_r_pvs_profile_constructeddatasupportentriesvalue_product * pa_p_pvs_profile_constructeddatasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_profile_constructeddatasupportcover. (~((pvs_divisor_profile_constructeddatasupportcover) = 1) /\ forall pvs_left_profile_constructeddatasupportcoverprime pvs_right_profile_constructeddatasupportcoverprime. (pvs_divisor_profile_constructeddatasupportcover) = pvs_left_profile_constructeddatasupportcoverprime * pvs_right_profile_constructeddatasupportcoverprime -> pvs_left_profile_constructeddatasupportcoverprime = 1 \/ pvs_right_profile_constructeddatasupportcoverprime = 1) -> (exists pvs_factor_profile_constructeddatasupportcoverdivides. (n) = (pvs_divisor_profile_constructeddatasupportcover) * pvs_factor_profile_constructeddatasupportcoverdivides) -> exists pvs_position_profile_constructeddatasupportcover. (exists pvs_gap_profile_constructeddatasupportcoverbound. pvs_gap_profile_constructeddatasupportcoverbound + S (pvs_position_profile_constructeddatasupportcover) = (ppf_length_profile_constructed)) /\ (((exists ff_h_pvs_profile_constructeddatasupportcoverentry. ff_h_pvs_profile_constructeddatasupportcoverentry + S (pvs_divisor_profile_constructeddatasupportcover) = S ((S (pvs_position_profile_constructeddatasupportcover)) * ppf_pc_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatasupportcoverentry. ppf_pb_profile_constructed = ff_q_pvs_profile_constructeddatasupportcoverentry * S ((S (pvs_position_profile_constructeddatasupportcover)) * ppf_pc_profile_constructed) + (pvs_divisor_profile_constructeddatasupportcover)))) /\ (exists ff_u_pvs_profile_constructeddatasupportproduct ff_v_pvs_profile_constructeddatasupportproduct. ((((exists ff_h_pvs_profile_constructeddatasupportproduct_start. ff_h_pvs_profile_constructeddatasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_profile_constructeddatasupportproduct)) /\ exists ff_q_pvs_profile_constructeddatasupportproduct_start. ff_u_pvs_profile_constructeddatasupportproduct = ff_q_pvs_profile_constructeddatasupportproduct_start * S ((S (0)) * ff_v_pvs_profile_constructeddatasupportproduct) + (1))) /\ ((((exists ff_h_pvs_profile_constructeddatasupportproduct_terminal. ff_h_pvs_profile_constructeddatasupportproduct_terminal + S (n) = S ((S (ppf_length_profile_constructed)) * ff_v_pvs_profile_constructeddatasupportproduct)) /\ exists ff_q_pvs_profile_constructeddatasupportproduct_terminal. ff_u_pvs_profile_constructeddatasupportproduct = ff_q_pvs_profile_constructeddatasupportproduct_terminal * S ((S (ppf_length_profile_constructed)) * ff_v_pvs_profile_constructeddatasupportproduct) + (n))) /\ forall ff_i_pvs_profile_constructeddatasupportproduct. (exists ff_lt_pvs_profile_constructeddatasupportproduct_bound. ff_lt_pvs_profile_constructeddatasupportproduct_bound + S ff_i_pvs_profile_constructeddatasupportproduct = ppf_length_profile_constructed) -> exists ff_p_pvs_profile_constructeddatasupportproduct ff_r_pvs_profile_constructeddatasupportproduct ff_s_pvs_profile_constructeddatasupportproduct. ((((exists ff_h_pvs_profile_constructeddatasupportproduct_factor. ff_h_pvs_profile_constructeddatasupportproduct_factor + S (ff_p_pvs_profile_constructeddatasupportproduct) = S ((S (ff_i_pvs_profile_constructeddatasupportproduct)) * ppf_vc_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatasupportproduct_factor. ppf_vb_profile_constructed = ff_q_pvs_profile_constructeddatasupportproduct_factor * S ((S (ff_i_pvs_profile_constructeddatasupportproduct)) * ppf_vc_profile_constructed) + (ff_p_pvs_profile_constructeddatasupportproduct))) /\ ((((exists ff_h_pvs_profile_constructeddatasupportproduct_partial. ff_h_pvs_profile_constructeddatasupportproduct_partial + S (ff_r_pvs_profile_constructeddatasupportproduct) = S ((S (ff_i_pvs_profile_constructeddatasupportproduct)) * ff_v_pvs_profile_constructeddatasupportproduct)) /\ exists ff_q_pvs_profile_constructeddatasupportproduct_partial. ff_u_pvs_profile_constructeddatasupportproduct = ff_q_pvs_profile_constructeddatasupportproduct_partial * S ((S (ff_i_pvs_profile_constructeddatasupportproduct)) * ff_v_pvs_profile_constructeddatasupportproduct) + (ff_r_pvs_profile_constructeddatasupportproduct))) /\ ((((exists ff_h_pvs_profile_constructeddatasupportproduct_successor. ff_h_pvs_profile_constructeddatasupportproduct_successor + S (ff_s_pvs_profile_constructeddatasupportproduct) = S ((S (S ff_i_pvs_profile_constructeddatasupportproduct)) * ff_v_pvs_profile_constructeddatasupportproduct)) /\ exists ff_q_pvs_profile_constructeddatasupportproduct_successor. ff_u_pvs_profile_constructeddatasupportproduct = ff_q_pvs_profile_constructeddatasupportproduct_successor * S ((S (S ff_i_pvs_profile_constructeddatasupportproduct)) * ff_v_pvs_profile_constructeddatasupportproduct) + (ff_s_pvs_profile_constructeddatasupportproduct))) /\ ff_s_pvs_profile_constructeddatasupportproduct = ff_r_pvs_profile_constructeddatasupportproduct * ff_p_pvs_profile_constructeddatasupportproduct)))))))))))))) /\ (((((forall ppf_index_profile_constructeddatagcdcommon ppf_entry_profile_constructeddatagcdcommon. (exists pvs_gap_profile_constructeddatagcdcommonbound. pvs_gap_profile_constructeddatagcdcommonbound + S (ppf_index_profile_constructeddatagcdcommon) = (ppf_length_profile_constructed)) -> (((exists ff_h_pvs_profile_constructeddatagcdcommonentry. ff_h_pvs_profile_constructeddatagcdcommonentry + S (ppf_entry_profile_constructeddatagcdcommon) = S ((S (ppf_index_profile_constructeddatagcdcommon)) * ppf_ec_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatagcdcommonentry. ppf_eb_profile_constructed = ff_q_pvs_profile_constructeddatagcdcommonentry * S ((S (ppf_index_profile_constructeddatagcdcommon)) * ppf_ec_profile_constructed) + (ppf_entry_profile_constructeddatagcdcommon))) -> (exists pvs_factor_profile_constructeddatagcdcommondivisor. (ppf_entry_profile_constructeddatagcdcommon) = (ppf_gcd_profile_constructed) * pvs_factor_profile_constructeddatagcdcommondivisor)) /\ (forall ppf_common_profile_constructeddatagcd. (forall ppf_index_profile_constructeddatagcdother ppf_entry_profile_constructeddatagcdother. (exists pvs_gap_profile_constructeddatagcdotherbound. pvs_gap_profile_constructeddatagcdotherbound + S (ppf_index_profile_constructeddatagcdother) = (ppf_length_profile_constructed)) -> (((exists ff_h_pvs_profile_constructeddatagcdotherentry. ff_h_pvs_profile_constructeddatagcdotherentry + S (ppf_entry_profile_constructeddatagcdother) = S ((S (ppf_index_profile_constructeddatagcdother)) * ppf_ec_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatagcdotherentry. ppf_eb_profile_constructed = ff_q_pvs_profile_constructeddatagcdotherentry * S ((S (ppf_index_profile_constructeddatagcdother)) * ppf_ec_profile_constructed) + (ppf_entry_profile_constructeddatagcdother))) -> (exists pvs_factor_profile_constructeddatagcdotherdivisor. (ppf_entry_profile_constructeddatagcdother) = (ppf_common_profile_constructeddatagcd) * pvs_factor_profile_constructeddatagcdotherdivisor)) -> (exists pvs_factor_profile_constructeddatagcdgreatest. (ppf_gcd_profile_constructed) = (ppf_common_profile_constructeddatagcd) * pvs_factor_profile_constructeddatagcdgreatest)))) /\ (((~((ppf_gcd_profile_constructed) = 0)) /\ (forall ppf_table_degree_profile_constructeddataroots. ~(ppf_table_degree_profile_constructeddataroots = 0) -> (exists pvs_factor_profile_constructeddatarootsdivisor. (ppf_gcd_profile_constructed) = (ppf_table_degree_profile_constructeddataroots) * pvs_factor_profile_constructeddatarootsdivisor) -> exists ppf_table_root_profile_constructeddataroots. (((exists ff_h_pvs_profile_constructeddatarootsentry. ff_h_pvs_profile_constructeddatarootsentry + S (ppf_table_root_profile_constructeddataroots) = S ((S (ppf_table_degree_profile_constructeddataroots)) * ppf_rc_profile_constructed)) /\ exists ff_q_pvs_profile_constructeddatarootsentry. ppf_rb_profile_constructed = ff_q_pvs_profile_constructeddatarootsentry * S ((S (ppf_table_degree_profile_constructeddataroots)) * ppf_rc_profile_constructed) + (ppf_table_root_profile_constructeddataroots))) /\ (exists pa_b_pvs_profile_constructeddatarootspower pa_c_pvs_profile_constructeddatarootspower. ((forall pa_i_pvs_profile_constructeddatarootspower_repeat. (exists pa_lt_pvs_profile_constructeddatarootspower_repeat_bound. pa_lt_pvs_profile_constructeddatarootspower_repeat_bound + S pa_i_pvs_profile_constructeddatarootspower_repeat = ppf_table_degree_profile_constructeddataroots) -> (((exists pa_h_pvs_profile_constructeddatarootspower_repeat_decoded. pa_h_pvs_profile_constructeddatarootspower_repeat_decoded + S (ppf_table_root_profile_constructeddataroots) = S ((S (pa_i_pvs_profile_constructeddatarootspower_repeat)) * pa_c_pvs_profile_constructeddatarootspower)) /\ exists pa_q_pvs_profile_constructeddatarootspower_repeat_decoded. pa_b_pvs_profile_constructeddatarootspower = pa_q_pvs_profile_constructeddatarootspower_repeat_decoded * S ((S (pa_i_pvs_profile_constructeddatarootspower_repeat)) * pa_c_pvs_profile_constructeddatarootspower) + (ppf_table_root_profile_constructeddataroots)))) /\ (exists pa_u_pvs_profile_constructeddatarootspower_product pa_v_pvs_profile_constructeddatarootspower_product. ((((exists pa_h_pvs_profile_constructeddatarootspower_product_start. pa_h_pvs_profile_constructeddatarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_constructeddatarootspower_product)) /\ exists pa_q_pvs_profile_constructeddatarootspower_product_start. pa_u_pvs_profile_constructeddatarootspower_product = pa_q_pvs_profile_constructeddatarootspower_product_start * S ((S (0)) * pa_v_pvs_profile_constructeddatarootspower_product) + (1))) /\ ((((exists pa_h_pvs_profile_constructeddatarootspower_product_terminal. pa_h_pvs_profile_constructeddatarootspower_product_terminal + S (n) = S ((S (ppf_table_degree_profile_constructeddataroots)) * pa_v_pvs_profile_constructeddatarootspower_product)) /\ exists pa_q_pvs_profile_constructeddatarootspower_product_terminal. pa_u_pvs_profile_constructeddatarootspower_product = pa_q_pvs_profile_constructeddatarootspower_product_terminal * S ((S (ppf_table_degree_profile_constructeddataroots)) * pa_v_pvs_profile_constructeddatarootspower_product) + (n))) /\ forall pa_i_pvs_profile_constructeddatarootspower_product. (exists pa_lt_pvs_profile_constructeddatarootspower_product_bound. pa_lt_pvs_profile_constructeddatarootspower_product_bound + S pa_i_pvs_profile_constructeddatarootspower_product = ppf_table_degree_profile_constructeddataroots) -> exists pa_p_pvs_profile_constructeddatarootspower_product pa_r_pvs_profile_constructeddatarootspower_product pa_s_pvs_profile_constructeddatarootspower_product. ((((exists pa_h_pvs_profile_constructeddatarootspower_product_factor. pa_h_pvs_profile_constructeddatarootspower_product_factor + S (pa_p_pvs_profile_constructeddatarootspower_product) = S ((S (pa_i_pvs_profile_constructeddatarootspower_product)) * pa_c_pvs_profile_constructeddatarootspower)) /\ exists pa_q_pvs_profile_constructeddatarootspower_product_factor. pa_b_pvs_profile_constructeddatarootspower = pa_q_pvs_profile_constructeddatarootspower_product_factor * S ((S (pa_i_pvs_profile_constructeddatarootspower_product)) * pa_c_pvs_profile_constructeddatarootspower) + (pa_p_pvs_profile_constructeddatarootspower_product))) /\ ((((exists pa_h_pvs_profile_constructeddatarootspower_product_partial. pa_h_pvs_profile_constructeddatarootspower_product_partial + S (pa_r_pvs_profile_constructeddatarootspower_product) = S ((S (pa_i_pvs_profile_constructeddatarootspower_product)) * pa_v_pvs_profile_constructeddatarootspower_product)) /\ exists pa_q_pvs_profile_constructeddatarootspower_product_partial. pa_u_pvs_profile_constructeddatarootspower_product = pa_q_pvs_profile_constructeddatarootspower_product_partial * S ((S (pa_i_pvs_profile_constructeddatarootspower_product)) * pa_v_pvs_profile_constructeddatarootspower_product) + (pa_r_pvs_profile_constructeddatarootspower_product))) /\ ((((exists pa_h_pvs_profile_constructeddatarootspower_product_successor. pa_h_pvs_profile_constructeddatarootspower_product_successor + S (pa_s_pvs_profile_constructeddatarootspower_product) = S ((S (S pa_i_pvs_profile_constructeddatarootspower_product)) * pa_v_pvs_profile_constructeddatarootspower_product)) /\ exists pa_q_pvs_profile_constructeddatarootspower_product_successor. pa_u_pvs_profile_constructeddatarootspower_product = pa_q_pvs_profile_constructeddatarootspower_product_successor * S ((S (S pa_i_pvs_profile_constructeddatarootspower_product)) * pa_v_pvs_profile_constructeddatarootspower_product) + (pa_s_pvs_profile_constructeddatarootspower_product))) /\ pa_s_pvs_profile_constructeddatarootspower_product = pa_r_pvs_profile_constructeddatarootspower_product * pa_p_pvs_profile_constructeddatarootspower_product)))))))))))))))))))))