positive_squarefree_kernel_and_power_profile

Exact expanded first-order arithmetic statement

forall n. ~(n = 0) -> exists r s w. (((~((r) = 0)) /\ (forall sfd_prime_campaign_kernel. (~((sfd_prime_campaign_kernel) = 1) /\ forall pvs_left_campaign_kerneldomain pvs_right_campaign_kerneldomain. (sfd_prime_campaign_kernel) = pvs_left_campaign_kerneldomain * pvs_right_campaign_kerneldomain -> pvs_left_campaign_kerneldomain = 1 \/ pvs_right_campaign_kerneldomain = 1) -> (exists pvs_le_gap_campaign_kernelbound. pvs_le_gap_campaign_kernelbound + (sfd_prime_campaign_kernel) = (r)) -> ~(exists pvs_factor_campaign_kernelsquare. (r) = (sfd_prime_campaign_kernel * sfd_prime_campaign_kernel) * pvs_factor_campaign_kernelsquare)))) /\ (n = r * (s * s) /\ ((((((n) = 1) /\ ((((w) = 0) /\ (forall ppf_unit_degree_campaign_profileunit. ~(ppf_unit_degree_campaign_profileunit = 0) -> (exists pa_b_pvs_campaign_profileunitidentity pa_c_pvs_campaign_profileunitidentity. ((forall pa_i_pvs_campaign_profileunitidentity_repeat. (exists pa_lt_pvs_campaign_profileunitidentity_repeat_bound. pa_lt_pvs_campaign_profileunitidentity_repeat_bound + S pa_i_pvs_campaign_profileunitidentity_repeat = ppf_unit_degree_campaign_profileunit) -> (((exists pa_h_pvs_campaign_profileunitidentity_repeat_decoded. pa_h_pvs_campaign_profileunitidentity_repeat_decoded + S (1) = S ((S (pa_i_pvs_campaign_profileunitidentity_repeat)) * pa_c_pvs_campaign_profileunitidentity)) /\ exists pa_q_pvs_campaign_profileunitidentity_repeat_decoded. pa_b_pvs_campaign_profileunitidentity = pa_q_pvs_campaign_profileunitidentity_repeat_decoded * S ((S (pa_i_pvs_campaign_profileunitidentity_repeat)) * pa_c_pvs_campaign_profileunitidentity) + (1)))) /\ (exists pa_u_pvs_campaign_profileunitidentity_product pa_v_pvs_campaign_profileunitidentity_product. ((((exists pa_h_pvs_campaign_profileunitidentity_product_start. pa_h_pvs_campaign_profileunitidentity_product_start + S (1) = S ((S (0)) * pa_v_pvs_campaign_profileunitidentity_product)) /\ exists pa_q_pvs_campaign_profileunitidentity_product_start. pa_u_pvs_campaign_profileunitidentity_product = pa_q_pvs_campaign_profileunitidentity_product_start * S ((S (0)) * pa_v_pvs_campaign_profileunitidentity_product) + (1))) /\ ((((exists pa_h_pvs_campaign_profileunitidentity_product_terminal. pa_h_pvs_campaign_profileunitidentity_product_terminal + S (1) = S ((S (ppf_unit_degree_campaign_profileunit)) * pa_v_pvs_campaign_profileunitidentity_product)) /\ exists pa_q_pvs_campaign_profileunitidentity_product_terminal. pa_u_pvs_campaign_profileunitidentity_product = pa_q_pvs_campaign_profileunitidentity_product_terminal * S ((S (ppf_unit_degree_campaign_profileunit)) * pa_v_pvs_campaign_profileunitidentity_product) + (1))) /\ forall pa_i_pvs_campaign_profileunitidentity_product. (exists pa_lt_pvs_campaign_profileunitidentity_product_bound. pa_lt_pvs_campaign_profileunitidentity_product_bound + S pa_i_pvs_campaign_profileunitidentity_product = ppf_unit_degree_campaign_profileunit) -> exists pa_p_pvs_campaign_profileunitidentity_product pa_r_pvs_campaign_profileunitidentity_product pa_s_pvs_campaign_profileunitidentity_product. ((((exists pa_h_pvs_campaign_profileunitidentity_product_factor. pa_h_pvs_campaign_profileunitidentity_product_factor + S (pa_p_pvs_campaign_profileunitidentity_product) = S ((S (pa_i_pvs_campaign_profileunitidentity_product)) * pa_c_pvs_campaign_profileunitidentity)) /\ exists pa_q_pvs_campaign_profileunitidentity_product_factor. pa_b_pvs_campaign_profileunitidentity = pa_q_pvs_campaign_profileunitidentity_product_factor * S ((S (pa_i_pvs_campaign_profileunitidentity_product)) * pa_c_pvs_campaign_profileunitidentity) + (pa_p_pvs_campaign_profileunitidentity_product))) /\ ((((exists pa_h_pvs_campaign_profileunitidentity_product_partial. pa_h_pvs_campaign_profileunitidentity_product_partial + S (pa_r_pvs_campaign_profileunitidentity_product) = S ((S (pa_i_pvs_campaign_profileunitidentity_product)) * pa_v_pvs_campaign_profileunitidentity_product)) /\ exists pa_q_pvs_campaign_profileunitidentity_product_partial. pa_u_pvs_campaign_profileunitidentity_product = pa_q_pvs_campaign_profileunitidentity_product_partial * S ((S (pa_i_pvs_campaign_profileunitidentity_product)) * pa_v_pvs_campaign_profileunitidentity_product) + (pa_r_pvs_campaign_profileunitidentity_product))) /\ ((((exists pa_h_pvs_campaign_profileunitidentity_product_successor. pa_h_pvs_campaign_profileunitidentity_product_successor + S (pa_s_pvs_campaign_profileunitidentity_product) = S ((S (S pa_i_pvs_campaign_profileunitidentity_product)) * pa_v_pvs_campaign_profileunitidentity_product)) /\ exists pa_q_pvs_campaign_profileunitidentity_product_successor. pa_u_pvs_campaign_profileunitidentity_product = pa_q_pvs_campaign_profileunitidentity_product_successor * S ((S (S pa_i_pvs_campaign_profileunitidentity_product)) * pa_v_pvs_campaign_profileunitidentity_product) + (pa_s_pvs_campaign_profileunitidentity_product))) /\ pa_s_pvs_campaign_profileunitidentity_product = pa_r_pvs_campaign_profileunitidentity_product * pa_p_pvs_campaign_profileunitidentity_product))))))))))))) \/ (exists ppf_pb_campaign_profile ppf_pc_campaign_profile ppf_eb_campaign_profile ppf_ec_campaign_profile ppf_vb_campaign_profile ppf_vc_campaign_profile ppf_length_campaign_profile ppf_gcd_campaign_profile ppf_rb_campaign_profile ppf_rc_campaign_profile. (((~((n) = 1)) /\ (((exists ppf_code_0_campaign_profiledatacode ppf_code_1_campaign_profiledatacode ppf_code_2_campaign_profiledatacode ppf_code_3_campaign_profiledatacode ppf_code_4_campaign_profiledatacode ppf_code_5_campaign_profiledatacode ppf_code_6_campaign_profiledatacode ppf_code_7_campaign_profiledatacode. ((((w) = ((ppf_pb_campaign_profile) + (ppf_code_0_campaign_profiledatacode)) * S ((ppf_pb_campaign_profile) + (ppf_code_0_campaign_profiledatacode)) + ((ppf_code_0_campaign_profiledatacode) + (ppf_code_0_campaign_profiledatacode))) /\ ((((ppf_code_0_campaign_profiledatacode) = ((ppf_pc_campaign_profile) + (ppf_code_1_campaign_profiledatacode)) * S ((ppf_pc_campaign_profile) + (ppf_code_1_campaign_profiledatacode)) + ((ppf_code_1_campaign_profiledatacode) + (ppf_code_1_campaign_profiledatacode))) /\ ((((ppf_code_1_campaign_profiledatacode) = ((ppf_eb_campaign_profile) + (ppf_code_2_campaign_profiledatacode)) * S ((ppf_eb_campaign_profile) + (ppf_code_2_campaign_profiledatacode)) + ((ppf_code_2_campaign_profiledatacode) + (ppf_code_2_campaign_profiledatacode))) /\ ((((ppf_code_2_campaign_profiledatacode) = ((ppf_ec_campaign_profile) + (ppf_code_3_campaign_profiledatacode)) * S ((ppf_ec_campaign_profile) + (ppf_code_3_campaign_profiledatacode)) + ((ppf_code_3_campaign_profiledatacode) + (ppf_code_3_campaign_profiledatacode))) /\ ((((ppf_code_3_campaign_profiledatacode) = ((ppf_vb_campaign_profile) + (ppf_code_4_campaign_profiledatacode)) * S ((ppf_vb_campaign_profile) + (ppf_code_4_campaign_profiledatacode)) + ((ppf_code_4_campaign_profiledatacode) + (ppf_code_4_campaign_profiledatacode))) /\ ((((ppf_code_4_campaign_profiledatacode) = ((ppf_vc_campaign_profile) + (ppf_code_5_campaign_profiledatacode)) * S ((ppf_vc_campaign_profile) + (ppf_code_5_campaign_profiledatacode)) + ((ppf_code_5_campaign_profiledatacode) + (ppf_code_5_campaign_profiledatacode))) /\ ((((ppf_code_5_campaign_profiledatacode) = ((ppf_length_campaign_profile) + (ppf_code_6_campaign_profiledatacode)) * S ((ppf_length_campaign_profile) + (ppf_code_6_campaign_profiledatacode)) + ((ppf_code_6_campaign_profiledatacode) + (ppf_code_6_campaign_profiledatacode))) /\ ((((ppf_code_6_campaign_profiledatacode) = ((ppf_gcd_campaign_profile) + (ppf_code_7_campaign_profiledatacode)) * S ((ppf_gcd_campaign_profile) + (ppf_code_7_campaign_profiledatacode)) + ((ppf_code_7_campaign_profiledatacode) + (ppf_code_7_campaign_profiledatacode))) /\ ((ppf_code_7_campaign_profiledatacode) = ((ppf_rb_campaign_profile) + (ppf_rc_campaign_profile)) * S ((ppf_rb_campaign_profile) + (ppf_rc_campaign_profile)) + ((ppf_rc_campaign_profile) + (ppf_rc_campaign_profile)))))))))))))))))))) /\ (((((~((n) = 0)) /\ (((forall pfp_i_pvs_campaign_profiledatasupportdistinct pfp_j_pvs_campaign_profiledatasupportdistinct pfp_a_pvs_campaign_profiledatasupportdistinct. (exists pfp_gap_pvs_campaign_profiledatasupportdistinctfirst. pfp_gap_pvs_campaign_profiledatasupportdistinctfirst + S (pfp_i_pvs_campaign_profiledatasupportdistinct) = (ppf_length_campaign_profile)) -> (exists pfp_gap_pvs_campaign_profiledatasupportdistinctsecond. pfp_gap_pvs_campaign_profiledatasupportdistinctsecond + S (pfp_j_pvs_campaign_profiledatasupportdistinct) = (ppf_length_campaign_profile)) -> (((exists ff_h_pfp_pvs_campaign_profiledatasupportdistinctleft. ff_h_pfp_pvs_campaign_profiledatasupportdistinctleft + S (pfp_a_pvs_campaign_profiledatasupportdistinct) = S ((S (pfp_i_pvs_campaign_profiledatasupportdistinct)) * ppf_pc_campaign_profile)) /\ exists ff_q_pfp_pvs_campaign_profiledatasupportdistinctleft. ppf_pb_campaign_profile = ff_q_pfp_pvs_campaign_profiledatasupportdistinctleft * S ((S (pfp_i_pvs_campaign_profiledatasupportdistinct)) * ppf_pc_campaign_profile) + (pfp_a_pvs_campaign_profiledatasupportdistinct))) -> (((exists ff_h_pfp_pvs_campaign_profiledatasupportdistinctright. ff_h_pfp_pvs_campaign_profiledatasupportdistinctright + S (pfp_a_pvs_campaign_profiledatasupportdistinct) = S ((S (pfp_j_pvs_campaign_profiledatasupportdistinct)) * ppf_pc_campaign_profile)) /\ exists ff_q_pfp_pvs_campaign_profiledatasupportdistinctright. ppf_pb_campaign_profile = ff_q_pfp_pvs_campaign_profiledatasupportdistinctright * S ((S (pfp_j_pvs_campaign_profiledatasupportdistinct)) * ppf_pc_campaign_profile) + (pfp_a_pvs_campaign_profiledatasupportdistinct))) -> pfp_i_pvs_campaign_profiledatasupportdistinct = pfp_j_pvs_campaign_profiledatasupportdistinct) /\ (((forall pvs_index_campaign_profiledatasupportentries. (exists pvs_gap_campaign_profiledatasupportentriesindex. pvs_gap_campaign_profiledatasupportentriesindex + S (pvs_index_campaign_profiledatasupportentries) = (ppf_length_campaign_profile)) -> exists pvs_prime_campaign_profiledatasupportentries pvs_exponent_campaign_profiledatasupportentries pvs_power_campaign_profiledatasupportentries. (((((exists ff_h_pvs_campaign_profiledatasupportentriesprime. ff_h_pvs_campaign_profiledatasupportentriesprime + S (pvs_prime_campaign_profiledatasupportentries) = S ((S (pvs_index_campaign_profiledatasupportentries)) * ppf_pc_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatasupportentriesprime. ppf_pb_campaign_profile = ff_q_pvs_campaign_profiledatasupportentriesprime * S ((S (pvs_index_campaign_profiledatasupportentries)) * ppf_pc_campaign_profile) + (pvs_prime_campaign_profiledatasupportentries))) /\ (((((exists ff_h_pvs_campaign_profiledatasupportentriesexponent. ff_h_pvs_campaign_profiledatasupportentriesexponent + S (pvs_exponent_campaign_profiledatasupportentries) = S ((S (pvs_index_campaign_profiledatasupportentries)) * ppf_ec_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatasupportentriesexponent. ppf_eb_campaign_profile = ff_q_pvs_campaign_profiledatasupportentriesexponent * S ((S (pvs_index_campaign_profiledatasupportentries)) * ppf_ec_campaign_profile) + (pvs_exponent_campaign_profiledatasupportentries))) /\ (((((exists ff_h_pvs_campaign_profiledatasupportentriespower. ff_h_pvs_campaign_profiledatasupportentriespower + S (pvs_power_campaign_profiledatasupportentries) = S ((S (pvs_index_campaign_profiledatasupportentries)) * ppf_vc_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatasupportentriespower. ppf_vb_campaign_profile = ff_q_pvs_campaign_profiledatasupportentriespower * S ((S (pvs_index_campaign_profiledatasupportentries)) * ppf_vc_campaign_profile) + (pvs_power_campaign_profiledatasupportentries))) /\ (((~((pvs_prime_campaign_profiledatasupportentries) = 1) /\ forall pvs_left_campaign_profiledatasupportentriesdomain pvs_right_campaign_profiledatasupportentriesdomain. (pvs_prime_campaign_profiledatasupportentries) = pvs_left_campaign_profiledatasupportentriesdomain * pvs_right_campaign_profiledatasupportentriesdomain -> pvs_left_campaign_profiledatasupportentriesdomain = 1 \/ pvs_right_campaign_profiledatasupportentriesdomain = 1) /\ (((~(pvs_exponent_campaign_profiledatasupportentries = 0)) /\ (((((exists bpd_gap_pvs_campaign_profiledatasupportentriesvaluation_selected_bound. bpd_gap_pvs_campaign_profiledatasupportentriesvaluation_selected_bound + (pvs_exponent_campaign_profiledatasupportentries) = (n)) /\ (exists bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_selected. ((exists bpvi_b_pvs_campaign_profiledatasupportentriesvaluation_selected_power bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_campaign_profiledatasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_campaign_profiledatasupportentriesvaluation_selected_power + S bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_selected_power = pvs_exponent_campaign_profiledatasupportentries) -> (((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_repeat + S (pvs_prime_campaign_profiledatasupportentries) = S ((S (bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_campaign_profiledatasupportentriesvaluation_selected_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_selected_power) + (pvs_prime_campaign_profiledatasupportentries)))) /\ (exists bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_selected_power bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_start. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_start. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_selected_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_selected) = S ((S (pvs_exponent_campaign_profiledatasupportentries)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_selected_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_campaign_profiledatasupportentries)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power) + (bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_campaign_profiledatasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_campaign_profiledatasupportentriesvaluation_selected_power + S bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power = pvs_exponent_campaign_profiledatasupportentries) -> exists bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_selected_power bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_selected_power bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_campaign_profiledatasupportentriesvaluation_selected_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_selected_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_selected_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_selected_power = bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_selected_power * bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_campaign_profiledatasupportentriesvaluation_selected. n = bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_campaign_profiledatasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_campaign_profiledatasupportentriesvaluation. (exists bpd_gap_pvs_campaign_profiledatasupportentriesvaluation_candidate_bound. bpd_gap_pvs_campaign_profiledatasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_campaign_profiledatasupportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_campaign_profiledatasupportentriesvaluation_candidate_power bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_campaign_profiledatasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_campaign_profiledatasupportentriesvaluation_candidate_power + S bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_campaign_profiledatasupportentriesvaluation) -> (((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_campaign_profiledatasupportentries) = S ((S (bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) + (pvs_prime_campaign_profiledatasupportentries)))) /\ (exists bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_candidate_power bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_campaign_profiledatasupportentriesvaluation)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_campaign_profiledatasupportentriesvaluation)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_campaign_profiledatasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_campaign_profiledatasupportentriesvaluation_candidate_power + S bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_campaign_profiledatasupportentriesvaluation) -> exists bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_candidate_power bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpvi_q_pvs_campaign_profiledatasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_campaign_profiledatasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power = bpvi_partial_pvs_campaign_profiledatasupportentriesvaluation_candidate_power * bpvi_factor_pvs_campaign_profiledatasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_campaign_profiledatasupportentriesvaluation_candidate. n = bpvi_result_pvs_campaign_profiledatasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_campaign_profiledatasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_campaign_profiledatasupportentriesvaluation_maximal. bpd_gap_pvs_campaign_profiledatasupportentriesvaluation_maximal + (bpd_candidate_pvs_campaign_profiledatasupportentriesvaluation) = (pvs_exponent_campaign_profiledatasupportentries))) /\ (exists pa_b_pvs_campaign_profiledatasupportentriesvalue pa_c_pvs_campaign_profiledatasupportentriesvalue. ((forall pa_i_pvs_campaign_profiledatasupportentriesvalue_repeat. (exists pa_lt_pvs_campaign_profiledatasupportentriesvalue_repeat_bound. pa_lt_pvs_campaign_profiledatasupportentriesvalue_repeat_bound + S pa_i_pvs_campaign_profiledatasupportentriesvalue_repeat = pvs_exponent_campaign_profiledatasupportentries) -> (((exists pa_h_pvs_campaign_profiledatasupportentriesvalue_repeat_decoded. pa_h_pvs_campaign_profiledatasupportentriesvalue_repeat_decoded + S (pvs_prime_campaign_profiledatasupportentries) = S ((S (pa_i_pvs_campaign_profiledatasupportentriesvalue_repeat)) * pa_c_pvs_campaign_profiledatasupportentriesvalue)) /\ exists pa_q_pvs_campaign_profiledatasupportentriesvalue_repeat_decoded. pa_b_pvs_campaign_profiledatasupportentriesvalue = pa_q_pvs_campaign_profiledatasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_campaign_profiledatasupportentriesvalue_repeat)) * pa_c_pvs_campaign_profiledatasupportentriesvalue) + (pvs_prime_campaign_profiledatasupportentries)))) /\ (exists pa_u_pvs_campaign_profiledatasupportentriesvalue_product pa_v_pvs_campaign_profiledatasupportentriesvalue_product. ((((exists pa_h_pvs_campaign_profiledatasupportentriesvalue_product_start. pa_h_pvs_campaign_profiledatasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product)) /\ exists pa_q_pvs_campaign_profiledatasupportentriesvalue_product_start. pa_u_pvs_campaign_profiledatasupportentriesvalue_product = pa_q_pvs_campaign_profiledatasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_campaign_profiledatasupportentriesvalue_product_terminal. pa_h_pvs_campaign_profiledatasupportentriesvalue_product_terminal + S (pvs_power_campaign_profiledatasupportentries) = S ((S (pvs_exponent_campaign_profiledatasupportentries)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product)) /\ exists pa_q_pvs_campaign_profiledatasupportentriesvalue_product_terminal. pa_u_pvs_campaign_profiledatasupportentriesvalue_product = pa_q_pvs_campaign_profiledatasupportentriesvalue_product_terminal * S ((S (pvs_exponent_campaign_profiledatasupportentries)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product) + (pvs_power_campaign_profiledatasupportentries))) /\ forall pa_i_pvs_campaign_profiledatasupportentriesvalue_product. (exists pa_lt_pvs_campaign_profiledatasupportentriesvalue_product_bound. pa_lt_pvs_campaign_profiledatasupportentriesvalue_product_bound + S pa_i_pvs_campaign_profiledatasupportentriesvalue_product = pvs_exponent_campaign_profiledatasupportentries) -> exists pa_p_pvs_campaign_profiledatasupportentriesvalue_product pa_r_pvs_campaign_profiledatasupportentriesvalue_product pa_s_pvs_campaign_profiledatasupportentriesvalue_product. ((((exists pa_h_pvs_campaign_profiledatasupportentriesvalue_product_factor. pa_h_pvs_campaign_profiledatasupportentriesvalue_product_factor + S (pa_p_pvs_campaign_profiledatasupportentriesvalue_product) = S ((S (pa_i_pvs_campaign_profiledatasupportentriesvalue_product)) * pa_c_pvs_campaign_profiledatasupportentriesvalue)) /\ exists pa_q_pvs_campaign_profiledatasupportentriesvalue_product_factor. pa_b_pvs_campaign_profiledatasupportentriesvalue = pa_q_pvs_campaign_profiledatasupportentriesvalue_product_factor * S ((S (pa_i_pvs_campaign_profiledatasupportentriesvalue_product)) * pa_c_pvs_campaign_profiledatasupportentriesvalue) + (pa_p_pvs_campaign_profiledatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_campaign_profiledatasupportentriesvalue_product_partial. pa_h_pvs_campaign_profiledatasupportentriesvalue_product_partial + S (pa_r_pvs_campaign_profiledatasupportentriesvalue_product) = S ((S (pa_i_pvs_campaign_profiledatasupportentriesvalue_product)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product)) /\ exists pa_q_pvs_campaign_profiledatasupportentriesvalue_product_partial. pa_u_pvs_campaign_profiledatasupportentriesvalue_product = pa_q_pvs_campaign_profiledatasupportentriesvalue_product_partial * S ((S (pa_i_pvs_campaign_profiledatasupportentriesvalue_product)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product) + (pa_r_pvs_campaign_profiledatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_campaign_profiledatasupportentriesvalue_product_successor. pa_h_pvs_campaign_profiledatasupportentriesvalue_product_successor + S (pa_s_pvs_campaign_profiledatasupportentriesvalue_product) = S ((S (S pa_i_pvs_campaign_profiledatasupportentriesvalue_product)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product)) /\ exists pa_q_pvs_campaign_profiledatasupportentriesvalue_product_successor. pa_u_pvs_campaign_profiledatasupportentriesvalue_product = pa_q_pvs_campaign_profiledatasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_campaign_profiledatasupportentriesvalue_product)) * pa_v_pvs_campaign_profiledatasupportentriesvalue_product) + (pa_s_pvs_campaign_profiledatasupportentriesvalue_product))) /\ pa_s_pvs_campaign_profiledatasupportentriesvalue_product = pa_r_pvs_campaign_profiledatasupportentriesvalue_product * pa_p_pvs_campaign_profiledatasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_campaign_profiledatasupportcover. (~((pvs_divisor_campaign_profiledatasupportcover) = 1) /\ forall pvs_left_campaign_profiledatasupportcoverprime pvs_right_campaign_profiledatasupportcoverprime. (pvs_divisor_campaign_profiledatasupportcover) = pvs_left_campaign_profiledatasupportcoverprime * pvs_right_campaign_profiledatasupportcoverprime -> pvs_left_campaign_profiledatasupportcoverprime = 1 \/ pvs_right_campaign_profiledatasupportcoverprime = 1) -> (exists pvs_factor_campaign_profiledatasupportcoverdivides. (n) = (pvs_divisor_campaign_profiledatasupportcover) * pvs_factor_campaign_profiledatasupportcoverdivides) -> exists pvs_position_campaign_profiledatasupportcover. (exists pvs_gap_campaign_profiledatasupportcoverbound. pvs_gap_campaign_profiledatasupportcoverbound + S (pvs_position_campaign_profiledatasupportcover) = (ppf_length_campaign_profile)) /\ (((exists ff_h_pvs_campaign_profiledatasupportcoverentry. ff_h_pvs_campaign_profiledatasupportcoverentry + S (pvs_divisor_campaign_profiledatasupportcover) = S ((S (pvs_position_campaign_profiledatasupportcover)) * ppf_pc_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatasupportcoverentry. ppf_pb_campaign_profile = ff_q_pvs_campaign_profiledatasupportcoverentry * S ((S (pvs_position_campaign_profiledatasupportcover)) * ppf_pc_campaign_profile) + (pvs_divisor_campaign_profiledatasupportcover)))) /\ (exists ff_u_pvs_campaign_profiledatasupportproduct ff_v_pvs_campaign_profiledatasupportproduct. ((((exists ff_h_pvs_campaign_profiledatasupportproduct_start. ff_h_pvs_campaign_profiledatasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_campaign_profiledatasupportproduct)) /\ exists ff_q_pvs_campaign_profiledatasupportproduct_start. ff_u_pvs_campaign_profiledatasupportproduct = ff_q_pvs_campaign_profiledatasupportproduct_start * S ((S (0)) * ff_v_pvs_campaign_profiledatasupportproduct) + (1))) /\ ((((exists ff_h_pvs_campaign_profiledatasupportproduct_terminal. ff_h_pvs_campaign_profiledatasupportproduct_terminal + S (n) = S ((S (ppf_length_campaign_profile)) * ff_v_pvs_campaign_profiledatasupportproduct)) /\ exists ff_q_pvs_campaign_profiledatasupportproduct_terminal. ff_u_pvs_campaign_profiledatasupportproduct = ff_q_pvs_campaign_profiledatasupportproduct_terminal * S ((S (ppf_length_campaign_profile)) * ff_v_pvs_campaign_profiledatasupportproduct) + (n))) /\ forall ff_i_pvs_campaign_profiledatasupportproduct. (exists ff_lt_pvs_campaign_profiledatasupportproduct_bound. ff_lt_pvs_campaign_profiledatasupportproduct_bound + S ff_i_pvs_campaign_profiledatasupportproduct = ppf_length_campaign_profile) -> exists ff_p_pvs_campaign_profiledatasupportproduct ff_r_pvs_campaign_profiledatasupportproduct ff_s_pvs_campaign_profiledatasupportproduct. ((((exists ff_h_pvs_campaign_profiledatasupportproduct_factor. ff_h_pvs_campaign_profiledatasupportproduct_factor + S (ff_p_pvs_campaign_profiledatasupportproduct) = S ((S (ff_i_pvs_campaign_profiledatasupportproduct)) * ppf_vc_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatasupportproduct_factor. ppf_vb_campaign_profile = ff_q_pvs_campaign_profiledatasupportproduct_factor * S ((S (ff_i_pvs_campaign_profiledatasupportproduct)) * ppf_vc_campaign_profile) + (ff_p_pvs_campaign_profiledatasupportproduct))) /\ ((((exists ff_h_pvs_campaign_profiledatasupportproduct_partial. ff_h_pvs_campaign_profiledatasupportproduct_partial + S (ff_r_pvs_campaign_profiledatasupportproduct) = S ((S (ff_i_pvs_campaign_profiledatasupportproduct)) * ff_v_pvs_campaign_profiledatasupportproduct)) /\ exists ff_q_pvs_campaign_profiledatasupportproduct_partial. ff_u_pvs_campaign_profiledatasupportproduct = ff_q_pvs_campaign_profiledatasupportproduct_partial * S ((S (ff_i_pvs_campaign_profiledatasupportproduct)) * ff_v_pvs_campaign_profiledatasupportproduct) + (ff_r_pvs_campaign_profiledatasupportproduct))) /\ ((((exists ff_h_pvs_campaign_profiledatasupportproduct_successor. ff_h_pvs_campaign_profiledatasupportproduct_successor + S (ff_s_pvs_campaign_profiledatasupportproduct) = S ((S (S ff_i_pvs_campaign_profiledatasupportproduct)) * ff_v_pvs_campaign_profiledatasupportproduct)) /\ exists ff_q_pvs_campaign_profiledatasupportproduct_successor. ff_u_pvs_campaign_profiledatasupportproduct = ff_q_pvs_campaign_profiledatasupportproduct_successor * S ((S (S ff_i_pvs_campaign_profiledatasupportproduct)) * ff_v_pvs_campaign_profiledatasupportproduct) + (ff_s_pvs_campaign_profiledatasupportproduct))) /\ ff_s_pvs_campaign_profiledatasupportproduct = ff_r_pvs_campaign_profiledatasupportproduct * ff_p_pvs_campaign_profiledatasupportproduct)))))))))))))) /\ (((((forall ppf_index_campaign_profiledatagcdcommon ppf_entry_campaign_profiledatagcdcommon. (exists pvs_gap_campaign_profiledatagcdcommonbound. pvs_gap_campaign_profiledatagcdcommonbound + S (ppf_index_campaign_profiledatagcdcommon) = (ppf_length_campaign_profile)) -> (((exists ff_h_pvs_campaign_profiledatagcdcommonentry. ff_h_pvs_campaign_profiledatagcdcommonentry + S (ppf_entry_campaign_profiledatagcdcommon) = S ((S (ppf_index_campaign_profiledatagcdcommon)) * ppf_ec_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatagcdcommonentry. ppf_eb_campaign_profile = ff_q_pvs_campaign_profiledatagcdcommonentry * S ((S (ppf_index_campaign_profiledatagcdcommon)) * ppf_ec_campaign_profile) + (ppf_entry_campaign_profiledatagcdcommon))) -> (exists pvs_factor_campaign_profiledatagcdcommondivisor. (ppf_entry_campaign_profiledatagcdcommon) = (ppf_gcd_campaign_profile) * pvs_factor_campaign_profiledatagcdcommondivisor)) /\ (forall ppf_common_campaign_profiledatagcd. (forall ppf_index_campaign_profiledatagcdother ppf_entry_campaign_profiledatagcdother. (exists pvs_gap_campaign_profiledatagcdotherbound. pvs_gap_campaign_profiledatagcdotherbound + S (ppf_index_campaign_profiledatagcdother) = (ppf_length_campaign_profile)) -> (((exists ff_h_pvs_campaign_profiledatagcdotherentry. ff_h_pvs_campaign_profiledatagcdotherentry + S (ppf_entry_campaign_profiledatagcdother) = S ((S (ppf_index_campaign_profiledatagcdother)) * ppf_ec_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatagcdotherentry. ppf_eb_campaign_profile = ff_q_pvs_campaign_profiledatagcdotherentry * S ((S (ppf_index_campaign_profiledatagcdother)) * ppf_ec_campaign_profile) + (ppf_entry_campaign_profiledatagcdother))) -> (exists pvs_factor_campaign_profiledatagcdotherdivisor. (ppf_entry_campaign_profiledatagcdother) = (ppf_common_campaign_profiledatagcd) * pvs_factor_campaign_profiledatagcdotherdivisor)) -> (exists pvs_factor_campaign_profiledatagcdgreatest. (ppf_gcd_campaign_profile) = (ppf_common_campaign_profiledatagcd) * pvs_factor_campaign_profiledatagcdgreatest)))) /\ (((~((ppf_gcd_campaign_profile) = 0)) /\ (forall ppf_table_degree_campaign_profiledataroots. ~(ppf_table_degree_campaign_profiledataroots = 0) -> (exists pvs_factor_campaign_profiledatarootsdivisor. (ppf_gcd_campaign_profile) = (ppf_table_degree_campaign_profiledataroots) * pvs_factor_campaign_profiledatarootsdivisor) -> exists ppf_table_root_campaign_profiledataroots. (((exists ff_h_pvs_campaign_profiledatarootsentry. ff_h_pvs_campaign_profiledatarootsentry + S (ppf_table_root_campaign_profiledataroots) = S ((S (ppf_table_degree_campaign_profiledataroots)) * ppf_rc_campaign_profile)) /\ exists ff_q_pvs_campaign_profiledatarootsentry. ppf_rb_campaign_profile = ff_q_pvs_campaign_profiledatarootsentry * S ((S (ppf_table_degree_campaign_profiledataroots)) * ppf_rc_campaign_profile) + (ppf_table_root_campaign_profiledataroots))) /\ (exists pa_b_pvs_campaign_profiledatarootspower pa_c_pvs_campaign_profiledatarootspower. ((forall pa_i_pvs_campaign_profiledatarootspower_repeat. (exists pa_lt_pvs_campaign_profiledatarootspower_repeat_bound. pa_lt_pvs_campaign_profiledatarootspower_repeat_bound + S pa_i_pvs_campaign_profiledatarootspower_repeat = ppf_table_degree_campaign_profiledataroots) -> (((exists pa_h_pvs_campaign_profiledatarootspower_repeat_decoded. pa_h_pvs_campaign_profiledatarootspower_repeat_decoded + S (ppf_table_root_campaign_profiledataroots) = S ((S (pa_i_pvs_campaign_profiledatarootspower_repeat)) * pa_c_pvs_campaign_profiledatarootspower)) /\ exists pa_q_pvs_campaign_profiledatarootspower_repeat_decoded. pa_b_pvs_campaign_profiledatarootspower = pa_q_pvs_campaign_profiledatarootspower_repeat_decoded * S ((S (pa_i_pvs_campaign_profiledatarootspower_repeat)) * pa_c_pvs_campaign_profiledatarootspower) + (ppf_table_root_campaign_profiledataroots)))) /\ (exists pa_u_pvs_campaign_profiledatarootspower_product pa_v_pvs_campaign_profiledatarootspower_product. ((((exists pa_h_pvs_campaign_profiledatarootspower_product_start. pa_h_pvs_campaign_profiledatarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_campaign_profiledatarootspower_product)) /\ exists pa_q_pvs_campaign_profiledatarootspower_product_start. pa_u_pvs_campaign_profiledatarootspower_product = pa_q_pvs_campaign_profiledatarootspower_product_start * S ((S (0)) * pa_v_pvs_campaign_profiledatarootspower_product) + (1))) /\ ((((exists pa_h_pvs_campaign_profiledatarootspower_product_terminal. pa_h_pvs_campaign_profiledatarootspower_product_terminal + S (n) = S ((S (ppf_table_degree_campaign_profiledataroots)) * pa_v_pvs_campaign_profiledatarootspower_product)) /\ exists pa_q_pvs_campaign_profiledatarootspower_product_terminal. pa_u_pvs_campaign_profiledatarootspower_product = pa_q_pvs_campaign_profiledatarootspower_product_terminal * S ((S (ppf_table_degree_campaign_profiledataroots)) * pa_v_pvs_campaign_profiledatarootspower_product) + (n))) /\ forall pa_i_pvs_campaign_profiledatarootspower_product. (exists pa_lt_pvs_campaign_profiledatarootspower_product_bound. pa_lt_pvs_campaign_profiledatarootspower_product_bound + S pa_i_pvs_campaign_profiledatarootspower_product = ppf_table_degree_campaign_profiledataroots) -> exists pa_p_pvs_campaign_profiledatarootspower_product pa_r_pvs_campaign_profiledatarootspower_product pa_s_pvs_campaign_profiledatarootspower_product. ((((exists pa_h_pvs_campaign_profiledatarootspower_product_factor. pa_h_pvs_campaign_profiledatarootspower_product_factor + S (pa_p_pvs_campaign_profiledatarootspower_product) = S ((S (pa_i_pvs_campaign_profiledatarootspower_product)) * pa_c_pvs_campaign_profiledatarootspower)) /\ exists pa_q_pvs_campaign_profiledatarootspower_product_factor. pa_b_pvs_campaign_profiledatarootspower = pa_q_pvs_campaign_profiledatarootspower_product_factor * S ((S (pa_i_pvs_campaign_profiledatarootspower_product)) * pa_c_pvs_campaign_profiledatarootspower) + (pa_p_pvs_campaign_profiledatarootspower_product))) /\ ((((exists pa_h_pvs_campaign_profiledatarootspower_product_partial. pa_h_pvs_campaign_profiledatarootspower_product_partial + S (pa_r_pvs_campaign_profiledatarootspower_product) = S ((S (pa_i_pvs_campaign_profiledatarootspower_product)) * pa_v_pvs_campaign_profiledatarootspower_product)) /\ exists pa_q_pvs_campaign_profiledatarootspower_product_partial. pa_u_pvs_campaign_profiledatarootspower_product = pa_q_pvs_campaign_profiledatarootspower_product_partial * S ((S (pa_i_pvs_campaign_profiledatarootspower_product)) * pa_v_pvs_campaign_profiledatarootspower_product) + (pa_r_pvs_campaign_profiledatarootspower_product))) /\ ((((exists pa_h_pvs_campaign_profiledatarootspower_product_successor. pa_h_pvs_campaign_profiledatarootspower_product_successor + S (pa_s_pvs_campaign_profiledatarootspower_product) = S ((S (S pa_i_pvs_campaign_profiledatarootspower_product)) * pa_v_pvs_campaign_profiledatarootspower_product)) /\ exists pa_q_pvs_campaign_profiledatarootspower_product_successor. pa_u_pvs_campaign_profiledatarootspower_product = pa_q_pvs_campaign_profiledatarootspower_product_successor * S ((S (S pa_i_pvs_campaign_profiledatarootspower_product)) * pa_v_pvs_campaign_profiledatarootspower_product) + (pa_s_pvs_campaign_profiledatarootspower_product))) /\ pa_s_pvs_campaign_profiledatarootspower_product = pa_r_pvs_campaign_profiledatarootspower_product * pa_p_pvs_campaign_profiledatarootspower_product))))))))))))))))))))) /\ forall u v. (((~((u) = 0)) /\ (forall sfd_prime_campaign_other_kernel. (~((sfd_prime_campaign_other_kernel) = 1) /\ forall pvs_left_campaign_other_kerneldomain pvs_right_campaign_other_kerneldomain. (sfd_prime_campaign_other_kernel) = pvs_left_campaign_other_kerneldomain * pvs_right_campaign_other_kerneldomain -> pvs_left_campaign_other_kerneldomain = 1 \/ pvs_right_campaign_other_kerneldomain = 1) -> (exists pvs_le_gap_campaign_other_kernelbound. pvs_le_gap_campaign_other_kernelbound + (sfd_prime_campaign_other_kernel) = (u)) -> ~(exists pvs_factor_campaign_other_kernelsquare. (u) = (sfd_prime_campaign_other_kernel * sfd_prime_campaign_other_kernel) * pvs_factor_campaign_other_kernelsquare)))) -> n = u * (v * v) -> u = r /\ v = s))