perfect_power_profile_unit_code

forall w. (((((1) = 1) /\ ((((w) = 0) /\ (forall ppf_unit_degree_profile_unit_boundaryunit. ~(ppf_unit_degree_profile_unit_boundaryunit = 0) -> (exists pa_b_pvs_profile_unit_boundaryunitidentity pa_c_pvs_profile_unit_boundaryunitidentity. ((forall pa_i_pvs_profile_unit_boundaryunitidentity_repeat. (exists pa_lt_pvs_profile_unit_boundaryunitidentity_repeat_bound. pa_lt_pvs_profile_unit_boundaryunitidentity_repeat_bound + S pa_i_pvs_profile_unit_boundaryunitidentity_repeat = ppf_unit_degree_profile_unit_boundaryunit) -> (((exists pa_h_pvs_profile_unit_boundaryunitidentity_repeat_decoded. pa_h_pvs_profile_unit_boundaryunitidentity_repeat_decoded + S (1) = S ((S (pa_i_pvs_profile_unit_boundaryunitidentity_repeat)) * pa_c_pvs_profile_unit_boundaryunitidentity)) /\ exists pa_q_pvs_profile_unit_boundaryunitidentity_repeat_decoded. pa_b_pvs_profile_unit_boundaryunitidentity = pa_q_pvs_profile_unit_boundaryunitidentity_repeat_decoded * S ((S (pa_i_pvs_profile_unit_boundaryunitidentity_repeat)) * pa_c_pvs_profile_unit_boundaryunitidentity) + (1)))) /\ (exists pa_u_pvs_profile_unit_boundaryunitidentity_product pa_v_pvs_profile_unit_boundaryunitidentity_product. ((((exists pa_h_pvs_profile_unit_boundaryunitidentity_product_start. pa_h_pvs_profile_unit_boundaryunitidentity_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_unit_boundaryunitidentity_product)) /\ exists pa_q_pvs_profile_unit_boundaryunitidentity_product_start. pa_u_pvs_profile_unit_boundaryunitidentity_product = pa_q_pvs_profile_unit_boundaryunitidentity_product_start * S ((S (0)) * pa_v_pvs_profile_unit_boundaryunitidentity_product) + (1))) /\ ((((exists pa_h_pvs_profile_unit_boundaryunitidentity_product_terminal. pa_h_pvs_profile_unit_boundaryunitidentity_product_terminal + S (1) = S ((S (ppf_unit_degree_profile_unit_boundaryunit)) * pa_v_pvs_profile_unit_boundaryunitidentity_product)) /\ exists pa_q_pvs_profile_unit_boundaryunitidentity_product_terminal. pa_u_pvs_profile_unit_boundaryunitidentity_product = pa_q_pvs_profile_unit_boundaryunitidentity_product_terminal * S ((S (ppf_unit_degree_profile_unit_boundaryunit)) * pa_v_pvs_profile_unit_boundaryunitidentity_product) + (1))) /\ forall pa_i_pvs_profile_unit_boundaryunitidentity_product. (exists pa_lt_pvs_profile_unit_boundaryunitidentity_product_bound. pa_lt_pvs_profile_unit_boundaryunitidentity_product_bound + S pa_i_pvs_profile_unit_boundaryunitidentity_product = ppf_unit_degree_profile_unit_boundaryunit) -> exists pa_p_pvs_profile_unit_boundaryunitidentity_product pa_r_pvs_profile_unit_boundaryunitidentity_product pa_s_pvs_profile_unit_boundaryunitidentity_product. ((((exists pa_h_pvs_profile_unit_boundaryunitidentity_product_factor. pa_h_pvs_profile_unit_boundaryunitidentity_product_factor + S (pa_p_pvs_profile_unit_boundaryunitidentity_product) = S ((S (pa_i_pvs_profile_unit_boundaryunitidentity_product)) * pa_c_pvs_profile_unit_boundaryunitidentity)) /\ exists pa_q_pvs_profile_unit_boundaryunitidentity_product_factor. pa_b_pvs_profile_unit_boundaryunitidentity = pa_q_pvs_profile_unit_boundaryunitidentity_product_factor * S ((S (pa_i_pvs_profile_unit_boundaryunitidentity_product)) * pa_c_pvs_profile_unit_boundaryunitidentity) + (pa_p_pvs_profile_unit_boundaryunitidentity_product))) /\ ((((exists pa_h_pvs_profile_unit_boundaryunitidentity_product_partial. pa_h_pvs_profile_unit_boundaryunitidentity_product_partial + S (pa_r_pvs_profile_unit_boundaryunitidentity_product) = S ((S (pa_i_pvs_profile_unit_boundaryunitidentity_product)) * pa_v_pvs_profile_unit_boundaryunitidentity_product)) /\ exists pa_q_pvs_profile_unit_boundaryunitidentity_product_partial. pa_u_pvs_profile_unit_boundaryunitidentity_product = pa_q_pvs_profile_unit_boundaryunitidentity_product_partial * S ((S (pa_i_pvs_profile_unit_boundaryunitidentity_product)) * pa_v_pvs_profile_unit_boundaryunitidentity_product) + (pa_r_pvs_profile_unit_boundaryunitidentity_product))) /\ ((((exists pa_h_pvs_profile_unit_boundaryunitidentity_product_successor. pa_h_pvs_profile_unit_boundaryunitidentity_product_successor + S (pa_s_pvs_profile_unit_boundaryunitidentity_product) = S ((S (S pa_i_pvs_profile_unit_boundaryunitidentity_product)) * pa_v_pvs_profile_unit_boundaryunitidentity_product)) /\ exists pa_q_pvs_profile_unit_boundaryunitidentity_product_successor. pa_u_pvs_profile_unit_boundaryunitidentity_product = pa_q_pvs_profile_unit_boundaryunitidentity_product_successor * S ((S (S pa_i_pvs_profile_unit_boundaryunitidentity_product)) * pa_v_pvs_profile_unit_boundaryunitidentity_product) + (pa_s_pvs_profile_unit_boundaryunitidentity_product))) /\ pa_s_pvs_profile_unit_boundaryunitidentity_product = pa_r_pvs_profile_unit_boundaryunitidentity_product * pa_p_pvs_profile_unit_boundaryunitidentity_product))))))))))))) \/ (exists ppf_pb_profile_unit_boundary ppf_pc_profile_unit_boundary ppf_eb_profile_unit_boundary ppf_ec_profile_unit_boundary ppf_vb_profile_unit_boundary ppf_vc_profile_unit_boundary ppf_length_profile_unit_boundary ppf_gcd_profile_unit_boundary ppf_rb_profile_unit_boundary ppf_rc_profile_unit_boundary. (((~((1) = 1)) /\ (((exists ppf_code_0_profile_unit_boundarydatacode ppf_code_1_profile_unit_boundarydatacode ppf_code_2_profile_unit_boundarydatacode ppf_code_3_profile_unit_boundarydatacode ppf_code_4_profile_unit_boundarydatacode ppf_code_5_profile_unit_boundarydatacode ppf_code_6_profile_unit_boundarydatacode ppf_code_7_profile_unit_boundarydatacode. ((((w) = ((ppf_pb_profile_unit_boundary) + (ppf_code_0_profile_unit_boundarydatacode)) * S ((ppf_pb_profile_unit_boundary) + (ppf_code_0_profile_unit_boundarydatacode)) + ((ppf_code_0_profile_unit_boundarydatacode) + (ppf_code_0_profile_unit_boundarydatacode))) /\ ((((ppf_code_0_profile_unit_boundarydatacode) = ((ppf_pc_profile_unit_boundary) + (ppf_code_1_profile_unit_boundarydatacode)) * S ((ppf_pc_profile_unit_boundary) + (ppf_code_1_profile_unit_boundarydatacode)) + ((ppf_code_1_profile_unit_boundarydatacode) + (ppf_code_1_profile_unit_boundarydatacode))) /\ ((((ppf_code_1_profile_unit_boundarydatacode) = ((ppf_eb_profile_unit_boundary) + (ppf_code_2_profile_unit_boundarydatacode)) * S ((ppf_eb_profile_unit_boundary) + (ppf_code_2_profile_unit_boundarydatacode)) + ((ppf_code_2_profile_unit_boundarydatacode) + (ppf_code_2_profile_unit_boundarydatacode))) /\ ((((ppf_code_2_profile_unit_boundarydatacode) = ((ppf_ec_profile_unit_boundary) + (ppf_code_3_profile_unit_boundarydatacode)) * S ((ppf_ec_profile_unit_boundary) + (ppf_code_3_profile_unit_boundarydatacode)) + ((ppf_code_3_profile_unit_boundarydatacode) + (ppf_code_3_profile_unit_boundarydatacode))) /\ ((((ppf_code_3_profile_unit_boundarydatacode) = ((ppf_vb_profile_unit_boundary) + (ppf_code_4_profile_unit_boundarydatacode)) * S ((ppf_vb_profile_unit_boundary) + (ppf_code_4_profile_unit_boundarydatacode)) + ((ppf_code_4_profile_unit_boundarydatacode) + (ppf_code_4_profile_unit_boundarydatacode))) /\ ((((ppf_code_4_profile_unit_boundarydatacode) = ((ppf_vc_profile_unit_boundary) + (ppf_code_5_profile_unit_boundarydatacode)) * S ((ppf_vc_profile_unit_boundary) + (ppf_code_5_profile_unit_boundarydatacode)) + ((ppf_code_5_profile_unit_boundarydatacode) + (ppf_code_5_profile_unit_boundarydatacode))) /\ ((((ppf_code_5_profile_unit_boundarydatacode) = ((ppf_length_profile_unit_boundary) + (ppf_code_6_profile_unit_boundarydatacode)) * S ((ppf_length_profile_unit_boundary) + (ppf_code_6_profile_unit_boundarydatacode)) + ((ppf_code_6_profile_unit_boundarydatacode) + (ppf_code_6_profile_unit_boundarydatacode))) /\ ((((ppf_code_6_profile_unit_boundarydatacode) = ((ppf_gcd_profile_unit_boundary) + (ppf_code_7_profile_unit_boundarydatacode)) * S ((ppf_gcd_profile_unit_boundary) + (ppf_code_7_profile_unit_boundarydatacode)) + ((ppf_code_7_profile_unit_boundarydatacode) + (ppf_code_7_profile_unit_boundarydatacode))) /\ ((ppf_code_7_profile_unit_boundarydatacode) = ((ppf_rb_profile_unit_boundary) + (ppf_rc_profile_unit_boundary)) * S ((ppf_rb_profile_unit_boundary) + (ppf_rc_profile_unit_boundary)) + ((ppf_rc_profile_unit_boundary) + (ppf_rc_profile_unit_boundary)))))))))))))))))))) /\ (((((~((1) = 0)) /\ (((forall pfp_i_pvs_profile_unit_boundarydatasupportdistinct pfp_j_pvs_profile_unit_boundarydatasupportdistinct pfp_a_pvs_profile_unit_boundarydatasupportdistinct. (exists pfp_gap_pvs_profile_unit_boundarydatasupportdistinctfirst. pfp_gap_pvs_profile_unit_boundarydatasupportdistinctfirst + S (pfp_i_pvs_profile_unit_boundarydatasupportdistinct) = (ppf_length_profile_unit_boundary)) -> (exists pfp_gap_pvs_profile_unit_boundarydatasupportdistinctsecond. pfp_gap_pvs_profile_unit_boundarydatasupportdistinctsecond + S (pfp_j_pvs_profile_unit_boundarydatasupportdistinct) = (ppf_length_profile_unit_boundary)) -> (((exists ff_h_pfp_pvs_profile_unit_boundarydatasupportdistinctleft. ff_h_pfp_pvs_profile_unit_boundarydatasupportdistinctleft + S (pfp_a_pvs_profile_unit_boundarydatasupportdistinct) = S ((S (pfp_i_pvs_profile_unit_boundarydatasupportdistinct)) * ppf_pc_profile_unit_boundary)) /\ exists ff_q_pfp_pvs_profile_unit_boundarydatasupportdistinctleft. ppf_pb_profile_unit_boundary = ff_q_pfp_pvs_profile_unit_boundarydatasupportdistinctleft * S ((S (pfp_i_pvs_profile_unit_boundarydatasupportdistinct)) * ppf_pc_profile_unit_boundary) + (pfp_a_pvs_profile_unit_boundarydatasupportdistinct))) -> (((exists ff_h_pfp_pvs_profile_unit_boundarydatasupportdistinctright. ff_h_pfp_pvs_profile_unit_boundarydatasupportdistinctright + S (pfp_a_pvs_profile_unit_boundarydatasupportdistinct) = S ((S (pfp_j_pvs_profile_unit_boundarydatasupportdistinct)) * ppf_pc_profile_unit_boundary)) /\ exists ff_q_pfp_pvs_profile_unit_boundarydatasupportdistinctright. ppf_pb_profile_unit_boundary = ff_q_pfp_pvs_profile_unit_boundarydatasupportdistinctright * S ((S (pfp_j_pvs_profile_unit_boundarydatasupportdistinct)) * ppf_pc_profile_unit_boundary) + (pfp_a_pvs_profile_unit_boundarydatasupportdistinct))) -> pfp_i_pvs_profile_unit_boundarydatasupportdistinct = pfp_j_pvs_profile_unit_boundarydatasupportdistinct) /\ (((forall pvs_index_profile_unit_boundarydatasupportentries. (exists pvs_gap_profile_unit_boundarydatasupportentriesindex. pvs_gap_profile_unit_boundarydatasupportentriesindex + S (pvs_index_profile_unit_boundarydatasupportentries) = (ppf_length_profile_unit_boundary)) -> exists pvs_prime_profile_unit_boundarydatasupportentries pvs_exponent_profile_unit_boundarydatasupportentries pvs_power_profile_unit_boundarydatasupportentries. (((((exists ff_h_pvs_profile_unit_boundarydatasupportentriesprime. ff_h_pvs_profile_unit_boundarydatasupportentriesprime + S (pvs_prime_profile_unit_boundarydatasupportentries) = S ((S (pvs_index_profile_unit_boundarydatasupportentries)) * ppf_pc_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportentriesprime. ppf_pb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatasupportentriesprime * S ((S (pvs_index_profile_unit_boundarydatasupportentries)) * ppf_pc_profile_unit_boundary) + (pvs_prime_profile_unit_boundarydatasupportentries))) /\ (((((exists ff_h_pvs_profile_unit_boundarydatasupportentriesexponent. ff_h_pvs_profile_unit_boundarydatasupportentriesexponent + S (pvs_exponent_profile_unit_boundarydatasupportentries) = S ((S (pvs_index_profile_unit_boundarydatasupportentries)) * ppf_ec_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportentriesexponent. ppf_eb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatasupportentriesexponent * S ((S (pvs_index_profile_unit_boundarydatasupportentries)) * ppf_ec_profile_unit_boundary) + (pvs_exponent_profile_unit_boundarydatasupportentries))) /\ (((((exists ff_h_pvs_profile_unit_boundarydatasupportentriespower. ff_h_pvs_profile_unit_boundarydatasupportentriespower + S (pvs_power_profile_unit_boundarydatasupportentries) = S ((S (pvs_index_profile_unit_boundarydatasupportentries)) * ppf_vc_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportentriespower. ppf_vb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatasupportentriespower * S ((S (pvs_index_profile_unit_boundarydatasupportentries)) * ppf_vc_profile_unit_boundary) + (pvs_power_profile_unit_boundarydatasupportentries))) /\ (((~((pvs_prime_profile_unit_boundarydatasupportentries) = 1) /\ forall pvs_left_profile_unit_boundarydatasupportentriesdomain pvs_right_profile_unit_boundarydatasupportentriesdomain. (pvs_prime_profile_unit_boundarydatasupportentries) = pvs_left_profile_unit_boundarydatasupportentriesdomain * pvs_right_profile_unit_boundarydatasupportentriesdomain -> pvs_left_profile_unit_boundarydatasupportentriesdomain = 1 \/ pvs_right_profile_unit_boundarydatasupportentriesdomain = 1) /\ (((~(pvs_exponent_profile_unit_boundarydatasupportentries = 0)) /\ (((((exists bpd_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_bound. bpd_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_bound + (pvs_exponent_profile_unit_boundarydatasupportentries) = (1)) /\ (exists bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_selected. ((exists bpvi_b_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power + S bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = pvs_exponent_profile_unit_boundarydatasupportentries) -> (((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_repeat + S (pvs_prime_profile_unit_boundarydatasupportentries) = S ((S (bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) + (pvs_prime_profile_unit_boundarydatasupportentries)))) /\ (exists bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_start. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_start. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_selected) = S ((S (pvs_exponent_profile_unit_boundarydatasupportentries)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_profile_unit_boundarydatasupportentries)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) + (bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power + S bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = pvs_exponent_profile_unit_boundarydatasupportentries) -> exists bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power = bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power * bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected. 1 = bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_profile_unit_boundarydatasupportentriesvaluation. (exists bpd_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_bound. bpd_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_profile_unit_boundarydatasupportentriesvaluation) = (1)) -> (exists bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power + S bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_unit_boundarydatasupportentriesvaluation) -> (((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_profile_unit_boundarydatasupportentries) = S ((S (bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) + (pvs_prime_profile_unit_boundarydatasupportentries)))) /\ (exists bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_profile_unit_boundarydatasupportentriesvaluation)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_profile_unit_boundarydatasupportentriesvaluation)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power + S bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_profile_unit_boundarydatasupportentriesvaluation) -> exists bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpvi_q_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power = bpvi_partial_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power * bpvi_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate. 1 = bpvi_result_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_profile_unit_boundarydatasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_maximal. bpd_gap_pvs_profile_unit_boundarydatasupportentriesvaluation_maximal + (bpd_candidate_pvs_profile_unit_boundarydatasupportentriesvaluation) = (pvs_exponent_profile_unit_boundarydatasupportentries))) /\ (exists pa_b_pvs_profile_unit_boundarydatasupportentriesvalue pa_c_pvs_profile_unit_boundarydatasupportentriesvalue. ((forall pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_repeat. (exists pa_lt_pvs_profile_unit_boundarydatasupportentriesvalue_repeat_bound. pa_lt_pvs_profile_unit_boundarydatasupportentriesvalue_repeat_bound + S pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_repeat = pvs_exponent_profile_unit_boundarydatasupportentries) -> (((exists pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_repeat_decoded. pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_repeat_decoded + S (pvs_prime_profile_unit_boundarydatasupportentries) = S ((S (pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_repeat)) * pa_c_pvs_profile_unit_boundarydatasupportentriesvalue)) /\ exists pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_repeat_decoded. pa_b_pvs_profile_unit_boundarydatasupportentriesvalue = pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_repeat)) * pa_c_pvs_profile_unit_boundarydatasupportentriesvalue) + (pvs_prime_profile_unit_boundarydatasupportentries)))) /\ (exists pa_u_pvs_profile_unit_boundarydatasupportentriesvalue_product pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_start. pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_start. pa_u_pvs_profile_unit_boundarydatasupportentriesvalue_product = pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_terminal. pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_terminal + S (pvs_power_profile_unit_boundarydatasupportentries) = S ((S (pvs_exponent_profile_unit_boundarydatasupportentries)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_terminal. pa_u_pvs_profile_unit_boundarydatasupportentriesvalue_product = pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_terminal * S ((S (pvs_exponent_profile_unit_boundarydatasupportentries)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product) + (pvs_power_profile_unit_boundarydatasupportentries))) /\ forall pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product. (exists pa_lt_pvs_profile_unit_boundarydatasupportentriesvalue_product_bound. pa_lt_pvs_profile_unit_boundarydatasupportentriesvalue_product_bound + S pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product = pvs_exponent_profile_unit_boundarydatasupportentries) -> exists pa_p_pvs_profile_unit_boundarydatasupportentriesvalue_product pa_r_pvs_profile_unit_boundarydatasupportentriesvalue_product pa_s_pvs_profile_unit_boundarydatasupportentriesvalue_product. ((((exists pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_factor. pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_factor + S (pa_p_pvs_profile_unit_boundarydatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product)) * pa_c_pvs_profile_unit_boundarydatasupportentriesvalue)) /\ exists pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_factor. pa_b_pvs_profile_unit_boundarydatasupportentriesvalue = pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_factor * S ((S (pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product)) * pa_c_pvs_profile_unit_boundarydatasupportentriesvalue) + (pa_p_pvs_profile_unit_boundarydatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_partial. pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_partial + S (pa_r_pvs_profile_unit_boundarydatasupportentriesvalue_product) = S ((S (pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_partial. pa_u_pvs_profile_unit_boundarydatasupportentriesvalue_product = pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_partial * S ((S (pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product) + (pa_r_pvs_profile_unit_boundarydatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_successor. pa_h_pvs_profile_unit_boundarydatasupportentriesvalue_product_successor + S (pa_s_pvs_profile_unit_boundarydatasupportentriesvalue_product) = S ((S (S pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product)) /\ exists pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_successor. pa_u_pvs_profile_unit_boundarydatasupportentriesvalue_product = pa_q_pvs_profile_unit_boundarydatasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_profile_unit_boundarydatasupportentriesvalue_product)) * pa_v_pvs_profile_unit_boundarydatasupportentriesvalue_product) + (pa_s_pvs_profile_unit_boundarydatasupportentriesvalue_product))) /\ pa_s_pvs_profile_unit_boundarydatasupportentriesvalue_product = pa_r_pvs_profile_unit_boundarydatasupportentriesvalue_product * pa_p_pvs_profile_unit_boundarydatasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_profile_unit_boundarydatasupportcover. (~((pvs_divisor_profile_unit_boundarydatasupportcover) = 1) /\ forall pvs_left_profile_unit_boundarydatasupportcoverprime pvs_right_profile_unit_boundarydatasupportcoverprime. (pvs_divisor_profile_unit_boundarydatasupportcover) = pvs_left_profile_unit_boundarydatasupportcoverprime * pvs_right_profile_unit_boundarydatasupportcoverprime -> pvs_left_profile_unit_boundarydatasupportcoverprime = 1 \/ pvs_right_profile_unit_boundarydatasupportcoverprime = 1) -> (exists pvs_factor_profile_unit_boundarydatasupportcoverdivides. (1) = (pvs_divisor_profile_unit_boundarydatasupportcover) * pvs_factor_profile_unit_boundarydatasupportcoverdivides) -> exists pvs_position_profile_unit_boundarydatasupportcover. (exists pvs_gap_profile_unit_boundarydatasupportcoverbound. pvs_gap_profile_unit_boundarydatasupportcoverbound + S (pvs_position_profile_unit_boundarydatasupportcover) = (ppf_length_profile_unit_boundary)) /\ (((exists ff_h_pvs_profile_unit_boundarydatasupportcoverentry. ff_h_pvs_profile_unit_boundarydatasupportcoverentry + S (pvs_divisor_profile_unit_boundarydatasupportcover) = S ((S (pvs_position_profile_unit_boundarydatasupportcover)) * ppf_pc_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportcoverentry. ppf_pb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatasupportcoverentry * S ((S (pvs_position_profile_unit_boundarydatasupportcover)) * ppf_pc_profile_unit_boundary) + (pvs_divisor_profile_unit_boundarydatasupportcover)))) /\ (exists ff_u_pvs_profile_unit_boundarydatasupportproduct ff_v_pvs_profile_unit_boundarydatasupportproduct. ((((exists ff_h_pvs_profile_unit_boundarydatasupportproduct_start. ff_h_pvs_profile_unit_boundarydatasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_profile_unit_boundarydatasupportproduct)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportproduct_start. ff_u_pvs_profile_unit_boundarydatasupportproduct = ff_q_pvs_profile_unit_boundarydatasupportproduct_start * S ((S (0)) * ff_v_pvs_profile_unit_boundarydatasupportproduct) + (1))) /\ ((((exists ff_h_pvs_profile_unit_boundarydatasupportproduct_terminal. ff_h_pvs_profile_unit_boundarydatasupportproduct_terminal + S (1) = S ((S (ppf_length_profile_unit_boundary)) * ff_v_pvs_profile_unit_boundarydatasupportproduct)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportproduct_terminal. ff_u_pvs_profile_unit_boundarydatasupportproduct = ff_q_pvs_profile_unit_boundarydatasupportproduct_terminal * S ((S (ppf_length_profile_unit_boundary)) * ff_v_pvs_profile_unit_boundarydatasupportproduct) + (1))) /\ forall ff_i_pvs_profile_unit_boundarydatasupportproduct. (exists ff_lt_pvs_profile_unit_boundarydatasupportproduct_bound. ff_lt_pvs_profile_unit_boundarydatasupportproduct_bound + S ff_i_pvs_profile_unit_boundarydatasupportproduct = ppf_length_profile_unit_boundary) -> exists ff_p_pvs_profile_unit_boundarydatasupportproduct ff_r_pvs_profile_unit_boundarydatasupportproduct ff_s_pvs_profile_unit_boundarydatasupportproduct. ((((exists ff_h_pvs_profile_unit_boundarydatasupportproduct_factor. ff_h_pvs_profile_unit_boundarydatasupportproduct_factor + S (ff_p_pvs_profile_unit_boundarydatasupportproduct) = S ((S (ff_i_pvs_profile_unit_boundarydatasupportproduct)) * ppf_vc_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportproduct_factor. ppf_vb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatasupportproduct_factor * S ((S (ff_i_pvs_profile_unit_boundarydatasupportproduct)) * ppf_vc_profile_unit_boundary) + (ff_p_pvs_profile_unit_boundarydatasupportproduct))) /\ ((((exists ff_h_pvs_profile_unit_boundarydatasupportproduct_partial. ff_h_pvs_profile_unit_boundarydatasupportproduct_partial + S (ff_r_pvs_profile_unit_boundarydatasupportproduct) = S ((S (ff_i_pvs_profile_unit_boundarydatasupportproduct)) * ff_v_pvs_profile_unit_boundarydatasupportproduct)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportproduct_partial. ff_u_pvs_profile_unit_boundarydatasupportproduct = ff_q_pvs_profile_unit_boundarydatasupportproduct_partial * S ((S (ff_i_pvs_profile_unit_boundarydatasupportproduct)) * ff_v_pvs_profile_unit_boundarydatasupportproduct) + (ff_r_pvs_profile_unit_boundarydatasupportproduct))) /\ ((((exists ff_h_pvs_profile_unit_boundarydatasupportproduct_successor. ff_h_pvs_profile_unit_boundarydatasupportproduct_successor + S (ff_s_pvs_profile_unit_boundarydatasupportproduct) = S ((S (S ff_i_pvs_profile_unit_boundarydatasupportproduct)) * ff_v_pvs_profile_unit_boundarydatasupportproduct)) /\ exists ff_q_pvs_profile_unit_boundarydatasupportproduct_successor. ff_u_pvs_profile_unit_boundarydatasupportproduct = ff_q_pvs_profile_unit_boundarydatasupportproduct_successor * S ((S (S ff_i_pvs_profile_unit_boundarydatasupportproduct)) * ff_v_pvs_profile_unit_boundarydatasupportproduct) + (ff_s_pvs_profile_unit_boundarydatasupportproduct))) /\ ff_s_pvs_profile_unit_boundarydatasupportproduct = ff_r_pvs_profile_unit_boundarydatasupportproduct * ff_p_pvs_profile_unit_boundarydatasupportproduct)))))))))))))) /\ (((((forall ppf_index_profile_unit_boundarydatagcdcommon ppf_entry_profile_unit_boundarydatagcdcommon. (exists pvs_gap_profile_unit_boundarydatagcdcommonbound. pvs_gap_profile_unit_boundarydatagcdcommonbound + S (ppf_index_profile_unit_boundarydatagcdcommon) = (ppf_length_profile_unit_boundary)) -> (((exists ff_h_pvs_profile_unit_boundarydatagcdcommonentry. ff_h_pvs_profile_unit_boundarydatagcdcommonentry + S (ppf_entry_profile_unit_boundarydatagcdcommon) = S ((S (ppf_index_profile_unit_boundarydatagcdcommon)) * ppf_ec_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatagcdcommonentry. ppf_eb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatagcdcommonentry * S ((S (ppf_index_profile_unit_boundarydatagcdcommon)) * ppf_ec_profile_unit_boundary) + (ppf_entry_profile_unit_boundarydatagcdcommon))) -> (exists pvs_factor_profile_unit_boundarydatagcdcommondivisor. (ppf_entry_profile_unit_boundarydatagcdcommon) = (ppf_gcd_profile_unit_boundary) * pvs_factor_profile_unit_boundarydatagcdcommondivisor)) /\ (forall ppf_common_profile_unit_boundarydatagcd. (forall ppf_index_profile_unit_boundarydatagcdother ppf_entry_profile_unit_boundarydatagcdother. (exists pvs_gap_profile_unit_boundarydatagcdotherbound. pvs_gap_profile_unit_boundarydatagcdotherbound + S (ppf_index_profile_unit_boundarydatagcdother) = (ppf_length_profile_unit_boundary)) -> (((exists ff_h_pvs_profile_unit_boundarydatagcdotherentry. ff_h_pvs_profile_unit_boundarydatagcdotherentry + S (ppf_entry_profile_unit_boundarydatagcdother) = S ((S (ppf_index_profile_unit_boundarydatagcdother)) * ppf_ec_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatagcdotherentry. ppf_eb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatagcdotherentry * S ((S (ppf_index_profile_unit_boundarydatagcdother)) * ppf_ec_profile_unit_boundary) + (ppf_entry_profile_unit_boundarydatagcdother))) -> (exists pvs_factor_profile_unit_boundarydatagcdotherdivisor. (ppf_entry_profile_unit_boundarydatagcdother) = (ppf_common_profile_unit_boundarydatagcd) * pvs_factor_profile_unit_boundarydatagcdotherdivisor)) -> (exists pvs_factor_profile_unit_boundarydatagcdgreatest. (ppf_gcd_profile_unit_boundary) = (ppf_common_profile_unit_boundarydatagcd) * pvs_factor_profile_unit_boundarydatagcdgreatest)))) /\ (((~((ppf_gcd_profile_unit_boundary) = 0)) /\ (forall ppf_table_degree_profile_unit_boundarydataroots. ~(ppf_table_degree_profile_unit_boundarydataroots = 0) -> (exists pvs_factor_profile_unit_boundarydatarootsdivisor. (ppf_gcd_profile_unit_boundary) = (ppf_table_degree_profile_unit_boundarydataroots) * pvs_factor_profile_unit_boundarydatarootsdivisor) -> exists ppf_table_root_profile_unit_boundarydataroots. (((exists ff_h_pvs_profile_unit_boundarydatarootsentry. ff_h_pvs_profile_unit_boundarydatarootsentry + S (ppf_table_root_profile_unit_boundarydataroots) = S ((S (ppf_table_degree_profile_unit_boundarydataroots)) * ppf_rc_profile_unit_boundary)) /\ exists ff_q_pvs_profile_unit_boundarydatarootsentry. ppf_rb_profile_unit_boundary = ff_q_pvs_profile_unit_boundarydatarootsentry * S ((S (ppf_table_degree_profile_unit_boundarydataroots)) * ppf_rc_profile_unit_boundary) + (ppf_table_root_profile_unit_boundarydataroots))) /\ (exists pa_b_pvs_profile_unit_boundarydatarootspower pa_c_pvs_profile_unit_boundarydatarootspower. ((forall pa_i_pvs_profile_unit_boundarydatarootspower_repeat. (exists pa_lt_pvs_profile_unit_boundarydatarootspower_repeat_bound. pa_lt_pvs_profile_unit_boundarydatarootspower_repeat_bound + S pa_i_pvs_profile_unit_boundarydatarootspower_repeat = ppf_table_degree_profile_unit_boundarydataroots) -> (((exists pa_h_pvs_profile_unit_boundarydatarootspower_repeat_decoded. pa_h_pvs_profile_unit_boundarydatarootspower_repeat_decoded + S (ppf_table_root_profile_unit_boundarydataroots) = S ((S (pa_i_pvs_profile_unit_boundarydatarootspower_repeat)) * pa_c_pvs_profile_unit_boundarydatarootspower)) /\ exists pa_q_pvs_profile_unit_boundarydatarootspower_repeat_decoded. pa_b_pvs_profile_unit_boundarydatarootspower = pa_q_pvs_profile_unit_boundarydatarootspower_repeat_decoded * S ((S (pa_i_pvs_profile_unit_boundarydatarootspower_repeat)) * pa_c_pvs_profile_unit_boundarydatarootspower) + (ppf_table_root_profile_unit_boundarydataroots)))) /\ (exists pa_u_pvs_profile_unit_boundarydatarootspower_product pa_v_pvs_profile_unit_boundarydatarootspower_product. ((((exists pa_h_pvs_profile_unit_boundarydatarootspower_product_start. pa_h_pvs_profile_unit_boundarydatarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_profile_unit_boundarydatarootspower_product)) /\ exists pa_q_pvs_profile_unit_boundarydatarootspower_product_start. pa_u_pvs_profile_unit_boundarydatarootspower_product = pa_q_pvs_profile_unit_boundarydatarootspower_product_start * S ((S (0)) * pa_v_pvs_profile_unit_boundarydatarootspower_product) + (1))) /\ ((((exists pa_h_pvs_profile_unit_boundarydatarootspower_product_terminal. pa_h_pvs_profile_unit_boundarydatarootspower_product_terminal + S (1) = S ((S (ppf_table_degree_profile_unit_boundarydataroots)) * pa_v_pvs_profile_unit_boundarydatarootspower_product)) /\ exists pa_q_pvs_profile_unit_boundarydatarootspower_product_terminal. pa_u_pvs_profile_unit_boundarydatarootspower_product = pa_q_pvs_profile_unit_boundarydatarootspower_product_terminal * S ((S (ppf_table_degree_profile_unit_boundarydataroots)) * pa_v_pvs_profile_unit_boundarydatarootspower_product) + (1))) /\ forall pa_i_pvs_profile_unit_boundarydatarootspower_product. (exists pa_lt_pvs_profile_unit_boundarydatarootspower_product_bound. pa_lt_pvs_profile_unit_boundarydatarootspower_product_bound + S pa_i_pvs_profile_unit_boundarydatarootspower_product = ppf_table_degree_profile_unit_boundarydataroots) -> exists pa_p_pvs_profile_unit_boundarydatarootspower_product pa_r_pvs_profile_unit_boundarydatarootspower_product pa_s_pvs_profile_unit_boundarydatarootspower_product. ((((exists pa_h_pvs_profile_unit_boundarydatarootspower_product_factor. pa_h_pvs_profile_unit_boundarydatarootspower_product_factor + S (pa_p_pvs_profile_unit_boundarydatarootspower_product) = S ((S (pa_i_pvs_profile_unit_boundarydatarootspower_product)) * pa_c_pvs_profile_unit_boundarydatarootspower)) /\ exists pa_q_pvs_profile_unit_boundarydatarootspower_product_factor. pa_b_pvs_profile_unit_boundarydatarootspower = pa_q_pvs_profile_unit_boundarydatarootspower_product_factor * S ((S (pa_i_pvs_profile_unit_boundarydatarootspower_product)) * pa_c_pvs_profile_unit_boundarydatarootspower) + (pa_p_pvs_profile_unit_boundarydatarootspower_product))) /\ ((((exists pa_h_pvs_profile_unit_boundarydatarootspower_product_partial. pa_h_pvs_profile_unit_boundarydatarootspower_product_partial + S (pa_r_pvs_profile_unit_boundarydatarootspower_product) = S ((S (pa_i_pvs_profile_unit_boundarydatarootspower_product)) * pa_v_pvs_profile_unit_boundarydatarootspower_product)) /\ exists pa_q_pvs_profile_unit_boundarydatarootspower_product_partial. pa_u_pvs_profile_unit_boundarydatarootspower_product = pa_q_pvs_profile_unit_boundarydatarootspower_product_partial * S ((S (pa_i_pvs_profile_unit_boundarydatarootspower_product)) * pa_v_pvs_profile_unit_boundarydatarootspower_product) + (pa_r_pvs_profile_unit_boundarydatarootspower_product))) /\ ((((exists pa_h_pvs_profile_unit_boundarydatarootspower_product_successor. pa_h_pvs_profile_unit_boundarydatarootspower_product_successor + S (pa_s_pvs_profile_unit_boundarydatarootspower_product) = S ((S (S pa_i_pvs_profile_unit_boundarydatarootspower_product)) * pa_v_pvs_profile_unit_boundarydatarootspower_product)) /\ exists pa_q_pvs_profile_unit_boundarydatarootspower_product_successor. pa_u_pvs_profile_unit_boundarydatarootspower_product = pa_q_pvs_profile_unit_boundarydatarootspower_product_successor * S ((S (S pa_i_pvs_profile_unit_boundarydatarootspower_product)) * pa_v_pvs_profile_unit_boundarydatarootspower_product) + (pa_s_pvs_profile_unit_boundarydatarootspower_product))) /\ pa_s_pvs_profile_unit_boundarydatarootspower_product = pa_r_pvs_profile_unit_boundarydatarootspower_product * pa_p_pvs_profile_unit_boundarydatarootspower_product))))))))))))))))))))) -> w = 0