perfect_power_profile_positive

Exact expanded first-order arithmetic statement

forall n w. (((((n) = 1) /\ ((((w) = 0) /\ (forall ppf_unit_degree_profile_domainunit. ~(ppf_unit_degree_profile_domainunit = 0) -> (exists pa_b_pvs_profile_domainunitidentity pa_c_pvs_profile_domainunitidentity. ((forall pa_i_pvs_profile_domainunitidentity_repeat. (exists pa_lt_pvs_profile_domainunitidentity_repeat_bound. pa_lt_pvs_profile_domainunitidentity_repeat_bound + S pa_i_pvs_profile_domainunitidentity_repeat = ppf_unit_degree_profile_domainunit) -> (((exists pa_h_pvs_profile_domainunitidentity_repeat_decoded. pa_h_pvs_profile_domainunitidentity_repeat_decoded + S (1) = S ((S (pa_i_pvs_profile_domainunitidentity_repeat)) * pa_c_pvs_profile_domainunitidentity)) /\ exists pa_q_pvs_profile_domainunitidentity_repeat_decoded. pa_b_pvs_profile_domainunitidentity = pa_q_pvs_profile_domainunitidentity_repeat_decoded * S ((S (pa_i_pvs_profile_domainunitidentity_repeat)) * pa_c_pvs_profile_domainunitidentity) + (1)))) /\ (exists pa_u_pvs_profile_domainunitidentity_product pa_v_pvs_profile_domainunitidentity_product. ((((exists pa_h_pvs_profile_domainunitidentity_product_start. pa_h_pvs_profile_domainunitidentity_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_domainunitidentity_product)) /\ exists pa_q_pvs_profile_domainunitidentity_product_start. pa_u_pvs_profile_domainunitidentity_product = pa_q_pvs_profile_domainunitidentity_product_start * S ((S (0)) * pa_v_pvs_profile_domainunitidentity_product) + (1))) /\ ((((exists pa_h_pvs_profile_domainunitidentity_product_terminal. pa_h_pvs_profile_domainunitidentity_product_terminal + S (1) = S ((S (ppf_unit_degree_profile_domainunit)) * pa_v_pvs_profile_domainunitidentity_product)) /\ exists pa_q_pvs_profile_domainunitidentity_product_terminal. pa_u_pvs_profile_domainunitidentity_product = pa_q_pvs_profile_domainunitidentity_product_terminal * S ((S (ppf_unit_degree_profile_domainunit)) * pa_v_pvs_profile_domainunitidentity_product) + (1))) /\ forall pa_i_pvs_profile_domainunitidentity_product. (exists pa_lt_pvs_profile_domainunitidentity_product_bound. pa_lt_pvs_profile_domainunitidentity_product_bound + S pa_i_pvs_profile_domainunitidentity_product = ppf_unit_degree_profile_domainunit) -> exists pa_p_pvs_profile_domainunitidentity_product pa_r_pvs_profile_domainunitidentity_product pa_s_pvs_profile_domainunitidentity_product. ((((exists pa_h_pvs_profile_domainunitidentity_product_factor. pa_h_pvs_profile_domainunitidentity_product_factor + S (pa_p_pvs_profile_domainunitidentity_product) = S ((S (pa_i_pvs_profile_domainunitidentity_product)) * pa_c_pvs_profile_domainunitidentity)) /\ exists pa_q_pvs_profile_domainunitidentity_product_factor. pa_b_pvs_profile_domainunitidentity = pa_q_pvs_profile_domainunitidentity_product_factor * S ((S (pa_i_pvs_profile_domainunitidentity_product)) * pa_c_pvs_profile_domainunitidentity) + (pa_p_pvs_profile_domainunitidentity_product))) /\ ((((exists pa_h_pvs_profile_domainunitidentity_product_partial. pa_h_pvs_profile_domainunitidentity_product_partial + S (pa_r_pvs_profile_domainunitidentity_product) = S ((S (pa_i_pvs_profile_domainunitidentity_product)) * pa_v_pvs_profile_domainunitidentity_product)) /\ exists pa_q_pvs_profile_domainunitidentity_product_partial. pa_u_pvs_profile_domainunitidentity_product = pa_q_pvs_profile_domainunitidentity_product_partial * S ((S (pa_i_pvs_profile_domainunitidentity_product)) * pa_v_pvs_profile_domainunitidentity_product) + (pa_r_pvs_profile_domainunitidentity_product))) /\ ((((exists pa_h_pvs_profile_domainunitidentity_product_successor. pa_h_pvs_profile_domainunitidentity_product_successor + S (pa_s_pvs_profile_domainunitidentity_product) = S ((S (S pa_i_pvs_profile_domainunitidentity_product)) * pa_v_pvs_profile_domainunitidentity_product)) /\ exists pa_q_pvs_profile_domainunitidentity_product_successor. pa_u_pvs_profile_domainunitidentity_product = pa_q_pvs_profile_domainunitidentity_product_successor * S ((S (S pa_i_pvs_profile_domainunitidentity_product)) * pa_v_pvs_profile_domainunitidentity_product) + (pa_s_pvs_profile_domainunitidentity_product))) /\ pa_s_pvs_profile_domainunitidentity_product = pa_r_pvs_profile_domainunitidentity_product * pa_p_pvs_profile_domainunitidentity_product))))))))))))) \/ (exists ppf_pb_profile_domain ppf_pc_profile_domain ppf_eb_profile_domain ppf_ec_profile_domain ppf_vb_profile_domain ppf_vc_profile_domain ppf_length_profile_domain ppf_gcd_profile_domain ppf_rb_profile_domain ppf_rc_profile_domain. (((~((n) = 1)) /\ (((exists ppf_code_0_profile_domaindatacode ppf_code_1_profile_domaindatacode ppf_code_2_profile_domaindatacode ppf_code_3_profile_domaindatacode ppf_code_4_profile_domaindatacode ppf_code_5_profile_domaindatacode ppf_code_6_profile_domaindatacode ppf_code_7_profile_domaindatacode. ((((w) = ((ppf_pb_profile_domain) + (ppf_code_0_profile_domaindatacode)) * S ((ppf_pb_profile_domain) + (ppf_code_0_profile_domaindatacode)) + ((ppf_code_0_profile_domaindatacode) + (ppf_code_0_profile_domaindatacode))) /\ ((((ppf_code_0_profile_domaindatacode) = ((ppf_pc_profile_domain) + (ppf_code_1_profile_domaindatacode)) * S ((ppf_pc_profile_domain) + (ppf_code_1_profile_domaindatacode)) + ((ppf_code_1_profile_domaindatacode) + (ppf_code_1_profile_domaindatacode))) /\ ((((ppf_code_1_profile_domaindatacode) = ((ppf_eb_profile_domain) + (ppf_code_2_profile_domaindatacode)) * S ((ppf_eb_profile_domain) + (ppf_code_2_profile_domaindatacode)) + ((ppf_code_2_profile_domaindatacode) + (ppf_code_2_profile_domaindatacode))) /\ ((((ppf_code_2_profile_domaindatacode) = ((ppf_ec_profile_domain) + (ppf_code_3_profile_domaindatacode)) * S ((ppf_ec_profile_domain) + (ppf_code_3_profile_domaindatacode)) + ((ppf_code_3_profile_domaindatacode) + (ppf_code_3_profile_domaindatacode))) /\ ((((ppf_code_3_profile_domaindatacode) = ((ppf_vb_profile_domain) + (ppf_code_4_profile_domaindatacode)) * S ((ppf_vb_profile_domain) + (ppf_code_4_profile_domaindatacode)) + ((ppf_code_4_profile_domaindatacode) + (ppf_code_4_profile_domaindatacode))) /\ ((((ppf_code_4_profile_domaindatacode) = ((ppf_vc_profile_domain) + (ppf_code_5_profile_domaindatacode)) * S ((ppf_vc_profile_domain) + (ppf_code_5_profile_domaindatacode)) + ((ppf_code_5_profile_domaindatacode) + (ppf_code_5_profile_domaindatacode))) /\ ((((ppf_code_5_profile_domaindatacode) = ((ppf_length_profile_domain) + (ppf_code_6_profile_domaindatacode)) * S ((ppf_length_profile_domain) + (ppf_code_6_profile_domaindatacode)) + ((ppf_code_6_profile_domaindatacode) + (ppf_code_6_profile_domaindatacode))) /\ ((((ppf_code_6_profile_domaindatacode) = ((ppf_gcd_profile_domain) + (ppf_code_7_profile_domaindatacode)) * S ((ppf_gcd_profile_domain) + (ppf_code_7_profile_domaindatacode)) + ((ppf_code_7_profile_domaindatacode) + (ppf_code_7_profile_domaindatacode))) /\ ((ppf_code_7_profile_domaindatacode) = ((ppf_rb_profile_domain) + (ppf_rc_profile_domain)) * S ((ppf_rb_profile_domain) + (ppf_rc_profile_domain)) + ((ppf_rc_profile_domain) + (ppf_rc_profile_domain)))))))))))))))))))) /\ (((((~((n) = 0)) /\ (((forall pfp_i_pvs_profile_domaindatasupportdistinct pfp_j_pvs_profile_domaindatasupportdistinct pfp_a_pvs_profile_domaindatasupportdistinct. (exists pfp_gap_pvs_profile_domaindatasupportdistinctfirst. pfp_gap_pvs_profile_domaindatasupportdistinctfirst + S (pfp_i_pvs_profile_domaindatasupportdistinct) = (ppf_length_profile_domain)) -> (exists pfp_gap_pvs_profile_domaindatasupportdistinctsecond. pfp_gap_pvs_profile_domaindatasupportdistinctsecond + S (pfp_j_pvs_profile_domaindatasupportdistinct) = (ppf_length_profile_domain)) -> (((exists ff_h_pfp_pvs_profile_domaindatasupportdistinctleft. ff_h_pfp_pvs_profile_domaindatasupportdistinctleft + S (pfp_a_pvs_profile_domaindatasupportdistinct) = S ((S (pfp_i_pvs_profile_domaindatasupportdistinct)) * ppf_pc_profile_domain)) /\ exists ff_q_pfp_pvs_profile_domaindatasupportdistinctleft. ppf_pb_profile_domain = ff_q_pfp_pvs_profile_domaindatasupportdistinctleft * S ((S (pfp_i_pvs_profile_domaindatasupportdistinct)) * ppf_pc_profile_domain) + (pfp_a_pvs_profile_domaindatasupportdistinct))) -> (((exists ff_h_pfp_pvs_profile_domaindatasupportdistinctright. ff_h_pfp_pvs_profile_domaindatasupportdistinctright + S (pfp_a_pvs_profile_domaindatasupportdistinct) = S ((S (pfp_j_pvs_profile_domaindatasupportdistinct)) * ppf_pc_profile_domain)) /\ exists ff_q_pfp_pvs_profile_domaindatasupportdistinctright. ppf_pb_profile_domain = ff_q_pfp_pvs_profile_domaindatasupportdistinctright * S ((S (pfp_j_pvs_profile_domaindatasupportdistinct)) * ppf_pc_profile_domain) + (pfp_a_pvs_profile_domaindatasupportdistinct))) -> pfp_i_pvs_profile_domaindatasupportdistinct = pfp_j_pvs_profile_domaindatasupportdistinct) /\ (((forall pvs_index_profile_domaindatasupportentries. (exists pvs_gap_profile_domaindatasupportentriesindex. pvs_gap_profile_domaindatasupportentriesindex + S (pvs_index_profile_domaindatasupportentries) = (ppf_length_profile_domain)) -> exists pvs_prime_profile_domaindatasupportentries pvs_exponent_profile_domaindatasupportentries pvs_power_profile_domaindatasupportentries. (((((exists ff_h_pvs_profile_domaindatasupportentriesprime. ff_h_pvs_profile_domaindatasupportentriesprime + S (pvs_prime_profile_domaindatasupportentries) = S ((S (pvs_index_profile_domaindatasupportentries)) * ppf_pc_profile_domain)) /\ exists ff_q_pvs_profile_domaindatasupportentriesprime. ppf_pb_profile_domain = ff_q_pvs_profile_domaindatasupportentriesprime * S ((S (pvs_index_profile_domaindatasupportentries)) * ppf_pc_profile_domain) + (pvs_prime_profile_domaindatasupportentries))) /\ (((((exists ff_h_pvs_profile_domaindatasupportentriesexponent. ff_h_pvs_profile_domaindatasupportentriesexponent + S (pvs_exponent_profile_domaindatasupportentries) = S ((S (pvs_index_profile_domaindatasupportentries)) * ppf_ec_profile_domain)) /\ exists ff_q_pvs_profile_domaindatasupportentriesexponent. ppf_eb_profile_domain = ff_q_pvs_profile_domaindatasupportentriesexponent * S ((S (pvs_index_profile_domaindatasupportentries)) * ppf_ec_profile_domain) + (pvs_exponent_profile_domaindatasupportentries))) /\ (((((exists ff_h_pvs_profile_domaindatasupportentriespower. ff_h_pvs_profile_domaindatasupportentriespower + S (pvs_power_profile_domaindatasupportentries) = S ((S (pvs_index_profile_domaindatasupportentries)) * ppf_vc_profile_domain)) /\ exists ff_q_pvs_profile_domaindatasupportentriespower. ppf_vb_profile_domain = ff_q_pvs_profile_domaindatasupportentriespower * S ((S (pvs_index_profile_domaindatasupportentries)) * ppf_vc_profile_domain) + (pvs_power_profile_domaindatasupportentries))) /\ (((~((pvs_prime_profile_domaindatasupportentries) = 1) /\ forall pvs_left_profile_domaindatasupportentriesdomain pvs_right_profile_domaindatasupportentriesdomain. (pvs_prime_profile_domaindatasupportentries) = pvs_left_profile_domaindatasupportentriesdomain * pvs_right_profile_domaindatasupportentriesdomain -> pvs_left_profile_domaindatasupportentriesdomain = 1 \/ pvs_right_profile_domaindatasupportentriesdomain = 1) /\ (((~(pvs_exponent_profile_domaindatasupportentries = 0)) /\ (((((exists bpd_gap_pvs_profile_domaindatasupportentriesvaluation_selected_bound. bpd_gap_pvs_profile_domaindatasupportentriesvaluation_selected_bound + (pvs_exponent_profile_domaindatasupportentries) = (n)) /\ (exists bpvi_result_pvs_profile_domaindatasupportentriesvaluation_selected. ((exists bpvi_b_pvs_profile_domaindatasupportentriesvaluation_selected_power bpvi_c_pvs_profile_domaindatasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_profile_domaindatasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_profile_domaindatasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_profile_domaindatasupportentriesvaluation_selected_power + S bpvi_i_pvs_profile_domaindatasupportentriesvaluation_selected_power = pvs_exponent_profile_domaindatasupportentries) -> (((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_repeat + S (pvs_prime_profile_domaindatasupportentries) = S ((S (bpvi_i_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_profile_domaindatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_selected_power) + (pvs_prime_profile_domaindatasupportentries)))) /\ (exists bpvi_u_pvs_profile_domaindatasupportentriesvaluation_selected_power bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_start. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_start. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_profile_domaindatasupportentriesvaluation_selected) = S ((S (pvs_exponent_profile_domaindatasupportentries)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_profile_domaindatasupportentries)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power) + (bpvi_result_pvs_profile_domaindatasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_profile_domaindatasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_profile_domaindatasupportentriesvaluation_selected_power + S bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power = pvs_exponent_profile_domaindatasupportentries) -> exists bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_selected_power bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_selected_power bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_profile_domaindatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_profile_domaindatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_selected_power = bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_selected_power * bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_domaindatasupportentriesvaluation_selected. n = bpvi_result_pvs_profile_domaindatasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_profile_domaindatasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_profile_domaindatasupportentriesvaluation. (exists bpd_gap_pvs_profile_domaindatasupportentriesvaluation_candidate_bound. bpd_gap_pvs_profile_domaindatasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_profile_domaindatasupportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_profile_domaindatasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_profile_domaindatasupportentriesvaluation_candidate_power bpvi_c_pvs_profile_domaindatasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_profile_domaindatasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_profile_domaindatasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_profile_domaindatasupportentriesvaluation_candidate_power + S bpvi_i_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_domaindatasupportentriesvaluation) -> (((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_profile_domaindatasupportentries) = S ((S (bpvi_i_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_candidate_power) + (pvs_prime_profile_domaindatasupportentries)))) /\ (exists bpvi_u_pvs_profile_domaindatasupportentriesvaluation_candidate_power bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_profile_domaindatasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_profile_domaindatasupportentriesvaluation)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_profile_domaindatasupportentriesvaluation)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_profile_domaindatasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_profile_domaindatasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_profile_domaindatasupportentriesvaluation_candidate_power + S bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_domaindatasupportentriesvaluation) -> exists bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_candidate_power bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_candidate_power bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_domaindatasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_profile_domaindatasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_domaindatasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_profile_domaindatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_domaindatasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_profile_domaindatasupportentriesvaluation_candidate_power = bpvi_partial_pvs_profile_domaindatasupportentriesvaluation_candidate_power * bpvi_factor_pvs_profile_domaindatasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_domaindatasupportentriesvaluation_candidate. n = bpvi_result_pvs_profile_domaindatasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_profile_domaindatasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_profile_domaindatasupportentriesvaluation_maximal. bpd_gap_pvs_profile_domaindatasupportentriesvaluation_maximal + (bpd_candidate_pvs_profile_domaindatasupportentriesvaluation) = (pvs_exponent_profile_domaindatasupportentries))) /\ (exists pa_b_pvs_profile_domaindatasupportentriesvalue pa_c_pvs_profile_domaindatasupportentriesvalue. ((forall pa_i_pvs_profile_domaindatasupportentriesvalue_repeat. (exists pa_lt_pvs_profile_domaindatasupportentriesvalue_repeat_bound. pa_lt_pvs_profile_domaindatasupportentriesvalue_repeat_bound + S pa_i_pvs_profile_domaindatasupportentriesvalue_repeat = pvs_exponent_profile_domaindatasupportentries) -> (((exists pa_h_pvs_profile_domaindatasupportentriesvalue_repeat_decoded. pa_h_pvs_profile_domaindatasupportentriesvalue_repeat_decoded + S (pvs_prime_profile_domaindatasupportentries) = S ((S (pa_i_pvs_profile_domaindatasupportentriesvalue_repeat)) * pa_c_pvs_profile_domaindatasupportentriesvalue)) /\ exists pa_q_pvs_profile_domaindatasupportentriesvalue_repeat_decoded. pa_b_pvs_profile_domaindatasupportentriesvalue = pa_q_pvs_profile_domaindatasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_profile_domaindatasupportentriesvalue_repeat)) * pa_c_pvs_profile_domaindatasupportentriesvalue) + (pvs_prime_profile_domaindatasupportentries)))) /\ (exists pa_u_pvs_profile_domaindatasupportentriesvalue_product pa_v_pvs_profile_domaindatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_domaindatasupportentriesvalue_product_start. pa_h_pvs_profile_domaindatasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_domaindatasupportentriesvalue_product_start. pa_u_pvs_profile_domaindatasupportentriesvalue_product = pa_q_pvs_profile_domaindatasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_profile_domaindatasupportentriesvalue_product_terminal. pa_h_pvs_profile_domaindatasupportentriesvalue_product_terminal + S (pvs_power_profile_domaindatasupportentries) = S ((S (pvs_exponent_profile_domaindatasupportentries)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_domaindatasupportentriesvalue_product_terminal. pa_u_pvs_profile_domaindatasupportentriesvalue_product = pa_q_pvs_profile_domaindatasupportentriesvalue_product_terminal * S ((S (pvs_exponent_profile_domaindatasupportentries)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product) + (pvs_power_profile_domaindatasupportentries))) /\ forall pa_i_pvs_profile_domaindatasupportentriesvalue_product. (exists pa_lt_pvs_profile_domaindatasupportentriesvalue_product_bound. pa_lt_pvs_profile_domaindatasupportentriesvalue_product_bound + S pa_i_pvs_profile_domaindatasupportentriesvalue_product = pvs_exponent_profile_domaindatasupportentries) -> exists pa_p_pvs_profile_domaindatasupportentriesvalue_product pa_r_pvs_profile_domaindatasupportentriesvalue_product pa_s_pvs_profile_domaindatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_domaindatasupportentriesvalue_product_factor. pa_h_pvs_profile_domaindatasupportentriesvalue_product_factor + S (pa_p_pvs_profile_domaindatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_domaindatasupportentriesvalue_product)) * pa_c_pvs_profile_domaindatasupportentriesvalue)) /\ exists pa_q_pvs_profile_domaindatasupportentriesvalue_product_factor. pa_b_pvs_profile_domaindatasupportentriesvalue = pa_q_pvs_profile_domaindatasupportentriesvalue_product_factor * S ((S (pa_i_pvs_profile_domaindatasupportentriesvalue_product)) * pa_c_pvs_profile_domaindatasupportentriesvalue) + (pa_p_pvs_profile_domaindatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_domaindatasupportentriesvalue_product_partial. pa_h_pvs_profile_domaindatasupportentriesvalue_product_partial + S (pa_r_pvs_profile_domaindatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_domaindatasupportentriesvalue_product)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_domaindatasupportentriesvalue_product_partial. pa_u_pvs_profile_domaindatasupportentriesvalue_product = pa_q_pvs_profile_domaindatasupportentriesvalue_product_partial * S ((S (pa_i_pvs_profile_domaindatasupportentriesvalue_product)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product) + (pa_r_pvs_profile_domaindatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_domaindatasupportentriesvalue_product_successor. pa_h_pvs_profile_domaindatasupportentriesvalue_product_successor + S (pa_s_pvs_profile_domaindatasupportentriesvalue_product) = S ((S (S pa_i_pvs_profile_domaindatasupportentriesvalue_product)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_domaindatasupportentriesvalue_product_successor. pa_u_pvs_profile_domaindatasupportentriesvalue_product = pa_q_pvs_profile_domaindatasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_profile_domaindatasupportentriesvalue_product)) * pa_v_pvs_profile_domaindatasupportentriesvalue_product) + (pa_s_pvs_profile_domaindatasupportentriesvalue_product))) /\ pa_s_pvs_profile_domaindatasupportentriesvalue_product = pa_r_pvs_profile_domaindatasupportentriesvalue_product * pa_p_pvs_profile_domaindatasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_profile_domaindatasupportcover. (~((pvs_divisor_profile_domaindatasupportcover) = 1) /\ forall pvs_left_profile_domaindatasupportcoverprime pvs_right_profile_domaindatasupportcoverprime. (pvs_divisor_profile_domaindatasupportcover) = pvs_left_profile_domaindatasupportcoverprime * pvs_right_profile_domaindatasupportcoverprime -> pvs_left_profile_domaindatasupportcoverprime = 1 \/ pvs_right_profile_domaindatasupportcoverprime = 1) -> (exists pvs_factor_profile_domaindatasupportcoverdivides. (n) = (pvs_divisor_profile_domaindatasupportcover) * pvs_factor_profile_domaindatasupportcoverdivides) -> exists pvs_position_profile_domaindatasupportcover. (exists pvs_gap_profile_domaindatasupportcoverbound. pvs_gap_profile_domaindatasupportcoverbound + S (pvs_position_profile_domaindatasupportcover) = (ppf_length_profile_domain)) /\ (((exists ff_h_pvs_profile_domaindatasupportcoverentry. ff_h_pvs_profile_domaindatasupportcoverentry + S (pvs_divisor_profile_domaindatasupportcover) = S ((S (pvs_position_profile_domaindatasupportcover)) * ppf_pc_profile_domain)) /\ exists ff_q_pvs_profile_domaindatasupportcoverentry. ppf_pb_profile_domain = ff_q_pvs_profile_domaindatasupportcoverentry * S ((S (pvs_position_profile_domaindatasupportcover)) * ppf_pc_profile_domain) + (pvs_divisor_profile_domaindatasupportcover)))) /\ (exists ff_u_pvs_profile_domaindatasupportproduct ff_v_pvs_profile_domaindatasupportproduct. ((((exists ff_h_pvs_profile_domaindatasupportproduct_start. ff_h_pvs_profile_domaindatasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_profile_domaindatasupportproduct)) /\ exists ff_q_pvs_profile_domaindatasupportproduct_start. ff_u_pvs_profile_domaindatasupportproduct = ff_q_pvs_profile_domaindatasupportproduct_start * S ((S (0)) * ff_v_pvs_profile_domaindatasupportproduct) + (1))) /\ ((((exists ff_h_pvs_profile_domaindatasupportproduct_terminal. ff_h_pvs_profile_domaindatasupportproduct_terminal + S (n) = S ((S (ppf_length_profile_domain)) * ff_v_pvs_profile_domaindatasupportproduct)) /\ exists ff_q_pvs_profile_domaindatasupportproduct_terminal. ff_u_pvs_profile_domaindatasupportproduct = ff_q_pvs_profile_domaindatasupportproduct_terminal * S ((S (ppf_length_profile_domain)) * ff_v_pvs_profile_domaindatasupportproduct) + (n))) /\ forall ff_i_pvs_profile_domaindatasupportproduct. (exists ff_lt_pvs_profile_domaindatasupportproduct_bound. ff_lt_pvs_profile_domaindatasupportproduct_bound + S ff_i_pvs_profile_domaindatasupportproduct = ppf_length_profile_domain) -> exists ff_p_pvs_profile_domaindatasupportproduct ff_r_pvs_profile_domaindatasupportproduct ff_s_pvs_profile_domaindatasupportproduct. ((((exists ff_h_pvs_profile_domaindatasupportproduct_factor. ff_h_pvs_profile_domaindatasupportproduct_factor + S (ff_p_pvs_profile_domaindatasupportproduct) = S ((S (ff_i_pvs_profile_domaindatasupportproduct)) * ppf_vc_profile_domain)) /\ exists ff_q_pvs_profile_domaindatasupportproduct_factor. ppf_vb_profile_domain = ff_q_pvs_profile_domaindatasupportproduct_factor * S ((S (ff_i_pvs_profile_domaindatasupportproduct)) * ppf_vc_profile_domain) + (ff_p_pvs_profile_domaindatasupportproduct))) /\ ((((exists ff_h_pvs_profile_domaindatasupportproduct_partial. ff_h_pvs_profile_domaindatasupportproduct_partial + S (ff_r_pvs_profile_domaindatasupportproduct) = S ((S (ff_i_pvs_profile_domaindatasupportproduct)) * ff_v_pvs_profile_domaindatasupportproduct)) /\ exists ff_q_pvs_profile_domaindatasupportproduct_partial. ff_u_pvs_profile_domaindatasupportproduct = ff_q_pvs_profile_domaindatasupportproduct_partial * S ((S (ff_i_pvs_profile_domaindatasupportproduct)) * ff_v_pvs_profile_domaindatasupportproduct) + (ff_r_pvs_profile_domaindatasupportproduct))) /\ ((((exists ff_h_pvs_profile_domaindatasupportproduct_successor. ff_h_pvs_profile_domaindatasupportproduct_successor + S (ff_s_pvs_profile_domaindatasupportproduct) = S ((S (S ff_i_pvs_profile_domaindatasupportproduct)) * ff_v_pvs_profile_domaindatasupportproduct)) /\ exists ff_q_pvs_profile_domaindatasupportproduct_successor. ff_u_pvs_profile_domaindatasupportproduct = ff_q_pvs_profile_domaindatasupportproduct_successor * S ((S (S ff_i_pvs_profile_domaindatasupportproduct)) * ff_v_pvs_profile_domaindatasupportproduct) + (ff_s_pvs_profile_domaindatasupportproduct))) /\ ff_s_pvs_profile_domaindatasupportproduct = ff_r_pvs_profile_domaindatasupportproduct * ff_p_pvs_profile_domaindatasupportproduct)))))))))))))) /\ (((((forall ppf_index_profile_domaindatagcdcommon ppf_entry_profile_domaindatagcdcommon. (exists pvs_gap_profile_domaindatagcdcommonbound. pvs_gap_profile_domaindatagcdcommonbound + S (ppf_index_profile_domaindatagcdcommon) = (ppf_length_profile_domain)) -> (((exists ff_h_pvs_profile_domaindatagcdcommonentry. ff_h_pvs_profile_domaindatagcdcommonentry + S (ppf_entry_profile_domaindatagcdcommon) = S ((S (ppf_index_profile_domaindatagcdcommon)) * ppf_ec_profile_domain)) /\ exists ff_q_pvs_profile_domaindatagcdcommonentry. ppf_eb_profile_domain = ff_q_pvs_profile_domaindatagcdcommonentry * S ((S (ppf_index_profile_domaindatagcdcommon)) * ppf_ec_profile_domain) + (ppf_entry_profile_domaindatagcdcommon))) -> (exists pvs_factor_profile_domaindatagcdcommondivisor. (ppf_entry_profile_domaindatagcdcommon) = (ppf_gcd_profile_domain) * pvs_factor_profile_domaindatagcdcommondivisor)) /\ (forall ppf_common_profile_domaindatagcd. (forall ppf_index_profile_domaindatagcdother ppf_entry_profile_domaindatagcdother. (exists pvs_gap_profile_domaindatagcdotherbound. pvs_gap_profile_domaindatagcdotherbound + S (ppf_index_profile_domaindatagcdother) = (ppf_length_profile_domain)) -> (((exists ff_h_pvs_profile_domaindatagcdotherentry. ff_h_pvs_profile_domaindatagcdotherentry + S (ppf_entry_profile_domaindatagcdother) = S ((S (ppf_index_profile_domaindatagcdother)) * ppf_ec_profile_domain)) /\ exists ff_q_pvs_profile_domaindatagcdotherentry. ppf_eb_profile_domain = ff_q_pvs_profile_domaindatagcdotherentry * S ((S (ppf_index_profile_domaindatagcdother)) * ppf_ec_profile_domain) + (ppf_entry_profile_domaindatagcdother))) -> (exists pvs_factor_profile_domaindatagcdotherdivisor. (ppf_entry_profile_domaindatagcdother) = (ppf_common_profile_domaindatagcd) * pvs_factor_profile_domaindatagcdotherdivisor)) -> (exists pvs_factor_profile_domaindatagcdgreatest. (ppf_gcd_profile_domain) = (ppf_common_profile_domaindatagcd) * pvs_factor_profile_domaindatagcdgreatest)))) /\ (((~((ppf_gcd_profile_domain) = 0)) /\ (forall ppf_table_degree_profile_domaindataroots. ~(ppf_table_degree_profile_domaindataroots = 0) -> (exists pvs_factor_profile_domaindatarootsdivisor. (ppf_gcd_profile_domain) = (ppf_table_degree_profile_domaindataroots) * pvs_factor_profile_domaindatarootsdivisor) -> exists ppf_table_root_profile_domaindataroots. (((exists ff_h_pvs_profile_domaindatarootsentry. ff_h_pvs_profile_domaindatarootsentry + S (ppf_table_root_profile_domaindataroots) = S ((S (ppf_table_degree_profile_domaindataroots)) * ppf_rc_profile_domain)) /\ exists ff_q_pvs_profile_domaindatarootsentry. ppf_rb_profile_domain = ff_q_pvs_profile_domaindatarootsentry * S ((S (ppf_table_degree_profile_domaindataroots)) * ppf_rc_profile_domain) + (ppf_table_root_profile_domaindataroots))) /\ (exists pa_b_pvs_profile_domaindatarootspower pa_c_pvs_profile_domaindatarootspower. ((forall pa_i_pvs_profile_domaindatarootspower_repeat. (exists pa_lt_pvs_profile_domaindatarootspower_repeat_bound. pa_lt_pvs_profile_domaindatarootspower_repeat_bound + S pa_i_pvs_profile_domaindatarootspower_repeat = ppf_table_degree_profile_domaindataroots) -> (((exists pa_h_pvs_profile_domaindatarootspower_repeat_decoded. pa_h_pvs_profile_domaindatarootspower_repeat_decoded + S (ppf_table_root_profile_domaindataroots) = S ((S (pa_i_pvs_profile_domaindatarootspower_repeat)) * pa_c_pvs_profile_domaindatarootspower)) /\ exists pa_q_pvs_profile_domaindatarootspower_repeat_decoded. pa_b_pvs_profile_domaindatarootspower = pa_q_pvs_profile_domaindatarootspower_repeat_decoded * S ((S (pa_i_pvs_profile_domaindatarootspower_repeat)) * pa_c_pvs_profile_domaindatarootspower) + (ppf_table_root_profile_domaindataroots)))) /\ (exists pa_u_pvs_profile_domaindatarootspower_product pa_v_pvs_profile_domaindatarootspower_product. ((((exists pa_h_pvs_profile_domaindatarootspower_product_start. pa_h_pvs_profile_domaindatarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_domaindatarootspower_product)) /\ exists pa_q_pvs_profile_domaindatarootspower_product_start. pa_u_pvs_profile_domaindatarootspower_product = pa_q_pvs_profile_domaindatarootspower_product_start * S ((S (0)) * pa_v_pvs_profile_domaindatarootspower_product) + (1))) /\ ((((exists pa_h_pvs_profile_domaindatarootspower_product_terminal. pa_h_pvs_profile_domaindatarootspower_product_terminal + S (n) = S ((S (ppf_table_degree_profile_domaindataroots)) * pa_v_pvs_profile_domaindatarootspower_product)) /\ exists pa_q_pvs_profile_domaindatarootspower_product_terminal. pa_u_pvs_profile_domaindatarootspower_product = pa_q_pvs_profile_domaindatarootspower_product_terminal * S ((S (ppf_table_degree_profile_domaindataroots)) * pa_v_pvs_profile_domaindatarootspower_product) + (n))) /\ forall pa_i_pvs_profile_domaindatarootspower_product. (exists pa_lt_pvs_profile_domaindatarootspower_product_bound. pa_lt_pvs_profile_domaindatarootspower_product_bound + S pa_i_pvs_profile_domaindatarootspower_product = ppf_table_degree_profile_domaindataroots) -> exists pa_p_pvs_profile_domaindatarootspower_product pa_r_pvs_profile_domaindatarootspower_product pa_s_pvs_profile_domaindatarootspower_product. ((((exists pa_h_pvs_profile_domaindatarootspower_product_factor. pa_h_pvs_profile_domaindatarootspower_product_factor + S (pa_p_pvs_profile_domaindatarootspower_product) = S ((S (pa_i_pvs_profile_domaindatarootspower_product)) * pa_c_pvs_profile_domaindatarootspower)) /\ exists pa_q_pvs_profile_domaindatarootspower_product_factor. pa_b_pvs_profile_domaindatarootspower = pa_q_pvs_profile_domaindatarootspower_product_factor * S ((S (pa_i_pvs_profile_domaindatarootspower_product)) * pa_c_pvs_profile_domaindatarootspower) + (pa_p_pvs_profile_domaindatarootspower_product))) /\ ((((exists pa_h_pvs_profile_domaindatarootspower_product_partial. pa_h_pvs_profile_domaindatarootspower_product_partial + S (pa_r_pvs_profile_domaindatarootspower_product) = S ((S (pa_i_pvs_profile_domaindatarootspower_product)) * pa_v_pvs_profile_domaindatarootspower_product)) /\ exists pa_q_pvs_profile_domaindatarootspower_product_partial. pa_u_pvs_profile_domaindatarootspower_product = pa_q_pvs_profile_domaindatarootspower_product_partial * S ((S (pa_i_pvs_profile_domaindatarootspower_product)) * pa_v_pvs_profile_domaindatarootspower_product) + (pa_r_pvs_profile_domaindatarootspower_product))) /\ ((((exists pa_h_pvs_profile_domaindatarootspower_product_successor. pa_h_pvs_profile_domaindatarootspower_product_successor + S (pa_s_pvs_profile_domaindatarootspower_product) = S ((S (S pa_i_pvs_profile_domaindatarootspower_product)) * pa_v_pvs_profile_domaindatarootspower_product)) /\ exists pa_q_pvs_profile_domaindatarootspower_product_successor. pa_u_pvs_profile_domaindatarootspower_product = pa_q_pvs_profile_domaindatarootspower_product_successor * S ((S (S pa_i_pvs_profile_domaindatarootspower_product)) * pa_v_pvs_profile_domaindatarootspower_product) + (pa_s_pvs_profile_domaindatarootspower_product))) /\ pa_s_pvs_profile_domaindatarootspower_product = pa_r_pvs_profile_domaindatarootspower_product * pa_p_pvs_profile_domaindatarootspower_product))))))))))))))))))))) -> ~(n = 0)