PowerProfile(n,w)

(((((n)) = 1) /\ (((((w)) = 0) /\ (forall ppf_unit_degree_prioritylayerunit. ~(ppf_unit_degree_prioritylayerunit = 0) -> (exists pa_b_pvs_prioritylayerunitidentity pa_c_pvs_prioritylayerunitidentity. ((forall pa_i_pvs_prioritylayerunitidentity_repeat. (exists pa_lt_pvs_prioritylayerunitidentity_repeat_bound. pa_lt_pvs_prioritylayerunitidentity_repeat_bound + S pa_i_pvs_prioritylayerunitidentity_repeat = ppf_unit_degree_prioritylayerunit) -> (((exists pa_h_pvs_prioritylayerunitidentity_repeat_decoded. pa_h_pvs_prioritylayerunitidentity_repeat_decoded + S (1) = S ((S (pa_i_pvs_prioritylayerunitidentity_repeat)) * pa_c_pvs_prioritylayerunitidentity)) /\ exists pa_q_pvs_prioritylayerunitidentity_repeat_decoded. pa_b_pvs_prioritylayerunitidentity = pa_q_pvs_prioritylayerunitidentity_repeat_decoded * S ((S (pa_i_pvs_prioritylayerunitidentity_repeat)) * pa_c_pvs_prioritylayerunitidentity) + (1)))) /\ (exists pa_u_pvs_prioritylayerunitidentity_product pa_v_pvs_prioritylayerunitidentity_product. ((((exists pa_h_pvs_prioritylayerunitidentity_product_start. pa_h_pvs_prioritylayerunitidentity_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayerunitidentity_product)) /\ exists pa_q_pvs_prioritylayerunitidentity_product_start. pa_u_pvs_prioritylayerunitidentity_product = pa_q_pvs_prioritylayerunitidentity_product_start * S ((S (0)) * pa_v_pvs_prioritylayerunitidentity_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayerunitidentity_product_terminal. pa_h_pvs_prioritylayerunitidentity_product_terminal + S (1) = S ((S (ppf_unit_degree_prioritylayerunit)) * pa_v_pvs_prioritylayerunitidentity_product)) /\ exists pa_q_pvs_prioritylayerunitidentity_product_terminal. pa_u_pvs_prioritylayerunitidentity_product = pa_q_pvs_prioritylayerunitidentity_product_terminal * S ((S (ppf_unit_degree_prioritylayerunit)) * pa_v_pvs_prioritylayerunitidentity_product) + (1))) /\ forall pa_i_pvs_prioritylayerunitidentity_product. (exists pa_lt_pvs_prioritylayerunitidentity_product_bound. pa_lt_pvs_prioritylayerunitidentity_product_bound + S pa_i_pvs_prioritylayerunitidentity_product = ppf_unit_degree_prioritylayerunit) -> exists pa_p_pvs_prioritylayerunitidentity_product pa_r_pvs_prioritylayerunitidentity_product pa_s_pvs_prioritylayerunitidentity_product. ((((exists pa_h_pvs_prioritylayerunitidentity_product_factor. pa_h_pvs_prioritylayerunitidentity_product_factor + S (pa_p_pvs_prioritylayerunitidentity_product) = S ((S (pa_i_pvs_prioritylayerunitidentity_product)) * pa_c_pvs_prioritylayerunitidentity)) /\ exists pa_q_pvs_prioritylayerunitidentity_product_factor. pa_b_pvs_prioritylayerunitidentity = pa_q_pvs_prioritylayerunitidentity_product_factor * S ((S (pa_i_pvs_prioritylayerunitidentity_product)) * pa_c_pvs_prioritylayerunitidentity) + (pa_p_pvs_prioritylayerunitidentity_product))) /\ ((((exists pa_h_pvs_prioritylayerunitidentity_product_partial. pa_h_pvs_prioritylayerunitidentity_product_partial + S (pa_r_pvs_prioritylayerunitidentity_product) = S ((S (pa_i_pvs_prioritylayerunitidentity_product)) * pa_v_pvs_prioritylayerunitidentity_product)) /\ exists pa_q_pvs_prioritylayerunitidentity_product_partial. pa_u_pvs_prioritylayerunitidentity_product = pa_q_pvs_prioritylayerunitidentity_product_partial * S ((S (pa_i_pvs_prioritylayerunitidentity_product)) * pa_v_pvs_prioritylayerunitidentity_product) + (pa_r_pvs_prioritylayerunitidentity_product))) /\ ((((exists pa_h_pvs_prioritylayerunitidentity_product_successor. pa_h_pvs_prioritylayerunitidentity_product_successor + S (pa_s_pvs_prioritylayerunitidentity_product) = S ((S (S pa_i_pvs_prioritylayerunitidentity_product)) * pa_v_pvs_prioritylayerunitidentity_product)) /\ exists pa_q_pvs_prioritylayerunitidentity_product_successor. pa_u_pvs_prioritylayerunitidentity_product = pa_q_pvs_prioritylayerunitidentity_product_successor * S ((S (S pa_i_pvs_prioritylayerunitidentity_product)) * pa_v_pvs_prioritylayerunitidentity_product) + (pa_s_pvs_prioritylayerunitidentity_product))) /\ pa_s_pvs_prioritylayerunitidentity_product = pa_r_pvs_prioritylayerunitidentity_product * pa_p_pvs_prioritylayerunitidentity_product))))))))))))) \/ (exists ppf_pb_prioritylayer ppf_pc_prioritylayer ppf_eb_prioritylayer ppf_ec_prioritylayer ppf_vb_prioritylayer ppf_vc_prioritylayer ppf_length_prioritylayer ppf_gcd_prioritylayer ppf_rb_prioritylayer ppf_rc_prioritylayer. (((~(((n)) = 1)) /\ (((exists ppf_code_0_prioritylayerdatacode ppf_code_1_prioritylayerdatacode ppf_code_2_prioritylayerdatacode ppf_code_3_prioritylayerdatacode ppf_code_4_prioritylayerdatacode ppf_code_5_prioritylayerdatacode ppf_code_6_prioritylayerdatacode ppf_code_7_prioritylayerdatacode. (((((w)) = ((ppf_pb_prioritylayer) + (ppf_code_0_prioritylayerdatacode)) * S ((ppf_pb_prioritylayer) + (ppf_code_0_prioritylayerdatacode)) + ((ppf_code_0_prioritylayerdatacode) + (ppf_code_0_prioritylayerdatacode))) /\ ((((ppf_code_0_prioritylayerdatacode) = ((ppf_pc_prioritylayer) + (ppf_code_1_prioritylayerdatacode)) * S ((ppf_pc_prioritylayer) + (ppf_code_1_prioritylayerdatacode)) + ((ppf_code_1_prioritylayerdatacode) + (ppf_code_1_prioritylayerdatacode))) /\ ((((ppf_code_1_prioritylayerdatacode) = ((ppf_eb_prioritylayer) + (ppf_code_2_prioritylayerdatacode)) * S ((ppf_eb_prioritylayer) + (ppf_code_2_prioritylayerdatacode)) + ((ppf_code_2_prioritylayerdatacode) + (ppf_code_2_prioritylayerdatacode))) /\ ((((ppf_code_2_prioritylayerdatacode) = ((ppf_ec_prioritylayer) + (ppf_code_3_prioritylayerdatacode)) * S ((ppf_ec_prioritylayer) + (ppf_code_3_prioritylayerdatacode)) + ((ppf_code_3_prioritylayerdatacode) + (ppf_code_3_prioritylayerdatacode))) /\ ((((ppf_code_3_prioritylayerdatacode) = ((ppf_vb_prioritylayer) + (ppf_code_4_prioritylayerdatacode)) * S ((ppf_vb_prioritylayer) + (ppf_code_4_prioritylayerdatacode)) + ((ppf_code_4_prioritylayerdatacode) + (ppf_code_4_prioritylayerdatacode))) /\ ((((ppf_code_4_prioritylayerdatacode) = ((ppf_vc_prioritylayer) + (ppf_code_5_prioritylayerdatacode)) * S ((ppf_vc_prioritylayer) + (ppf_code_5_prioritylayerdatacode)) + ((ppf_code_5_prioritylayerdatacode) + (ppf_code_5_prioritylayerdatacode))) /\ ((((ppf_code_5_prioritylayerdatacode) = ((ppf_length_prioritylayer) + (ppf_code_6_prioritylayerdatacode)) * S ((ppf_length_prioritylayer) + (ppf_code_6_prioritylayerdatacode)) + ((ppf_code_6_prioritylayerdatacode) + (ppf_code_6_prioritylayerdatacode))) /\ ((((ppf_code_6_prioritylayerdatacode) = ((ppf_gcd_prioritylayer) + (ppf_code_7_prioritylayerdatacode)) * S ((ppf_gcd_prioritylayer) + (ppf_code_7_prioritylayerdatacode)) + ((ppf_code_7_prioritylayerdatacode) + (ppf_code_7_prioritylayerdatacode))) /\ ((ppf_code_7_prioritylayerdatacode) = ((ppf_rb_prioritylayer) + (ppf_rc_prioritylayer)) * S ((ppf_rb_prioritylayer) + (ppf_rc_prioritylayer)) + ((ppf_rc_prioritylayer) + (ppf_rc_prioritylayer)))))))))))))))))))) /\ (((((~(((n)) = 0)) /\ (((forall pfp_i_pvs_prioritylayerdatasupportdistinct pfp_j_pvs_prioritylayerdatasupportdistinct pfp_a_pvs_prioritylayerdatasupportdistinct. (exists pfp_gap_pvs_prioritylayerdatasupportdistinctfirst. pfp_gap_pvs_prioritylayerdatasupportdistinctfirst + S (pfp_i_pvs_prioritylayerdatasupportdistinct) = (ppf_length_prioritylayer)) -> (exists pfp_gap_pvs_prioritylayerdatasupportdistinctsecond. pfp_gap_pvs_prioritylayerdatasupportdistinctsecond + S (pfp_j_pvs_prioritylayerdatasupportdistinct) = (ppf_length_prioritylayer)) -> (((exists ff_h_pfp_pvs_prioritylayerdatasupportdistinctleft. ff_h_pfp_pvs_prioritylayerdatasupportdistinctleft + S (pfp_a_pvs_prioritylayerdatasupportdistinct) = S ((S (pfp_i_pvs_prioritylayerdatasupportdistinct)) * ppf_pc_prioritylayer)) /\ exists ff_q_pfp_pvs_prioritylayerdatasupportdistinctleft. ppf_pb_prioritylayer = ff_q_pfp_pvs_prioritylayerdatasupportdistinctleft * S ((S (pfp_i_pvs_prioritylayerdatasupportdistinct)) * ppf_pc_prioritylayer) + (pfp_a_pvs_prioritylayerdatasupportdistinct))) -> (((exists ff_h_pfp_pvs_prioritylayerdatasupportdistinctright. ff_h_pfp_pvs_prioritylayerdatasupportdistinctright + S (pfp_a_pvs_prioritylayerdatasupportdistinct) = S ((S (pfp_j_pvs_prioritylayerdatasupportdistinct)) * ppf_pc_prioritylayer)) /\ exists ff_q_pfp_pvs_prioritylayerdatasupportdistinctright. ppf_pb_prioritylayer = ff_q_pfp_pvs_prioritylayerdatasupportdistinctright * S ((S (pfp_j_pvs_prioritylayerdatasupportdistinct)) * ppf_pc_prioritylayer) + (pfp_a_pvs_prioritylayerdatasupportdistinct))) -> pfp_i_pvs_prioritylayerdatasupportdistinct = pfp_j_pvs_prioritylayerdatasupportdistinct) /\ (((forall pvs_index_prioritylayerdatasupportentries. (exists pvs_gap_prioritylayerdatasupportentriesindex. pvs_gap_prioritylayerdatasupportentriesindex + S (pvs_index_prioritylayerdatasupportentries) = (ppf_length_prioritylayer)) -> exists pvs_prime_prioritylayerdatasupportentries pvs_exponent_prioritylayerdatasupportentries pvs_power_prioritylayerdatasupportentries. (((((exists ff_h_pvs_prioritylayerdatasupportentriesprime. ff_h_pvs_prioritylayerdatasupportentriesprime + S (pvs_prime_prioritylayerdatasupportentries) = S ((S (pvs_index_prioritylayerdatasupportentries)) * ppf_pc_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatasupportentriesprime. ppf_pb_prioritylayer = ff_q_pvs_prioritylayerdatasupportentriesprime * S ((S (pvs_index_prioritylayerdatasupportentries)) * ppf_pc_prioritylayer) + (pvs_prime_prioritylayerdatasupportentries))) /\ (((((exists ff_h_pvs_prioritylayerdatasupportentriesexponent. ff_h_pvs_prioritylayerdatasupportentriesexponent + S (pvs_exponent_prioritylayerdatasupportentries) = S ((S (pvs_index_prioritylayerdatasupportentries)) * ppf_ec_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatasupportentriesexponent. ppf_eb_prioritylayer = ff_q_pvs_prioritylayerdatasupportentriesexponent * S ((S (pvs_index_prioritylayerdatasupportentries)) * ppf_ec_prioritylayer) + (pvs_exponent_prioritylayerdatasupportentries))) /\ (((((exists ff_h_pvs_prioritylayerdatasupportentriespower. ff_h_pvs_prioritylayerdatasupportentriespower + S (pvs_power_prioritylayerdatasupportentries) = S ((S (pvs_index_prioritylayerdatasupportentries)) * ppf_vc_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatasupportentriespower. ppf_vb_prioritylayer = ff_q_pvs_prioritylayerdatasupportentriespower * S ((S (pvs_index_prioritylayerdatasupportentries)) * ppf_vc_prioritylayer) + (pvs_power_prioritylayerdatasupportentries))) /\ (((~((pvs_prime_prioritylayerdatasupportentries) = 1) /\ forall pvs_left_prioritylayerdatasupportentriesdomain pvs_right_prioritylayerdatasupportentriesdomain. (pvs_prime_prioritylayerdatasupportentries) = pvs_left_prioritylayerdatasupportentriesdomain * pvs_right_prioritylayerdatasupportentriesdomain -> pvs_left_prioritylayerdatasupportentriesdomain = 1 \/ pvs_right_prioritylayerdatasupportentriesdomain = 1) /\ (((~(pvs_exponent_prioritylayerdatasupportentries = 0)) /\ (((((exists bpd_gap_pvs_prioritylayerdatasupportentriesvaluation_selected_bound. bpd_gap_pvs_prioritylayerdatasupportentriesvaluation_selected_bound + (pvs_exponent_prioritylayerdatasupportentries) = ((n))) /\ (exists bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_selected. ((exists bpvi_b_pvs_prioritylayerdatasupportentriesvaluation_selected_power bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_prioritylayerdatasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_prioritylayerdatasupportentriesvaluation_selected_power + S bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_selected_power = pvs_exponent_prioritylayerdatasupportentries) -> (((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_repeat + S (pvs_prime_prioritylayerdatasupportentries) = S ((S (bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_prioritylayerdatasupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_selected_power) + (pvs_prime_prioritylayerdatasupportentries)))) /\ (exists bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_selected_power bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_start. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_start. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_selected) = S ((S (pvs_exponent_prioritylayerdatasupportentries)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_prioritylayerdatasupportentries)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power) + (bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_prioritylayerdatasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_prioritylayerdatasupportentriesvaluation_selected_power + S bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power = pvs_exponent_prioritylayerdatasupportentries) -> exists bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_selected_power bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_selected_power bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_prioritylayerdatasupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_selected_power = bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_selected_power * bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayerdatasupportentriesvaluation_selected. (n) = bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_prioritylayerdatasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_prioritylayerdatasupportentriesvaluation. (exists bpd_gap_pvs_prioritylayerdatasupportentriesvaluation_candidate_bound. bpd_gap_pvs_prioritylayerdatasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_prioritylayerdatasupportentriesvaluation) = ((n))) -> (exists bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_prioritylayerdatasupportentriesvaluation_candidate_power bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_prioritylayerdatasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_prioritylayerdatasupportentriesvaluation_candidate_power + S bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_prioritylayerdatasupportentriesvaluation) -> (((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_prioritylayerdatasupportentries) = S ((S (bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) + (pvs_prime_prioritylayerdatasupportentries)))) /\ (exists bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_candidate_power bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_prioritylayerdatasupportentriesvaluation)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_prioritylayerdatasupportentriesvaluation)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_prioritylayerdatasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_prioritylayerdatasupportentriesvaluation_candidate_power + S bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpd_candidate_pvs_prioritylayerdatasupportentriesvaluation) -> exists bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_candidate_power bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerdatasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerdatasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power = bpvi_partial_pvs_prioritylayerdatasupportentriesvaluation_candidate_power * bpvi_factor_pvs_prioritylayerdatasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayerdatasupportentriesvaluation_candidate. (n) = bpvi_result_pvs_prioritylayerdatasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_prioritylayerdatasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_prioritylayerdatasupportentriesvaluation_maximal. bpd_gap_pvs_prioritylayerdatasupportentriesvaluation_maximal + (bpd_candidate_pvs_prioritylayerdatasupportentriesvaluation) = (pvs_exponent_prioritylayerdatasupportentries))) /\ (exists pa_b_pvs_prioritylayerdatasupportentriesvalue pa_c_pvs_prioritylayerdatasupportentriesvalue. ((forall pa_i_pvs_prioritylayerdatasupportentriesvalue_repeat. (exists pa_lt_pvs_prioritylayerdatasupportentriesvalue_repeat_bound. pa_lt_pvs_prioritylayerdatasupportentriesvalue_repeat_bound + S pa_i_pvs_prioritylayerdatasupportentriesvalue_repeat = pvs_exponent_prioritylayerdatasupportentries) -> (((exists pa_h_pvs_prioritylayerdatasupportentriesvalue_repeat_decoded. pa_h_pvs_prioritylayerdatasupportentriesvalue_repeat_decoded + S (pvs_prime_prioritylayerdatasupportentries) = S ((S (pa_i_pvs_prioritylayerdatasupportentriesvalue_repeat)) * pa_c_pvs_prioritylayerdatasupportentriesvalue)) /\ exists pa_q_pvs_prioritylayerdatasupportentriesvalue_repeat_decoded. pa_b_pvs_prioritylayerdatasupportentriesvalue = pa_q_pvs_prioritylayerdatasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_prioritylayerdatasupportentriesvalue_repeat)) * pa_c_pvs_prioritylayerdatasupportentriesvalue) + (pvs_prime_prioritylayerdatasupportentries)))) /\ (exists pa_u_pvs_prioritylayerdatasupportentriesvalue_product pa_v_pvs_prioritylayerdatasupportentriesvalue_product. ((((exists pa_h_pvs_prioritylayerdatasupportentriesvalue_product_start. pa_h_pvs_prioritylayerdatasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerdatasupportentriesvalue_product_start. pa_u_pvs_prioritylayerdatasupportentriesvalue_product = pa_q_pvs_prioritylayerdatasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayerdatasupportentriesvalue_product_terminal. pa_h_pvs_prioritylayerdatasupportentriesvalue_product_terminal + S (pvs_power_prioritylayerdatasupportentries) = S ((S (pvs_exponent_prioritylayerdatasupportentries)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerdatasupportentriesvalue_product_terminal. pa_u_pvs_prioritylayerdatasupportentriesvalue_product = pa_q_pvs_prioritylayerdatasupportentriesvalue_product_terminal * S ((S (pvs_exponent_prioritylayerdatasupportentries)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product) + (pvs_power_prioritylayerdatasupportentries))) /\ forall pa_i_pvs_prioritylayerdatasupportentriesvalue_product. (exists pa_lt_pvs_prioritylayerdatasupportentriesvalue_product_bound. pa_lt_pvs_prioritylayerdatasupportentriesvalue_product_bound + S pa_i_pvs_prioritylayerdatasupportentriesvalue_product = pvs_exponent_prioritylayerdatasupportentries) -> exists pa_p_pvs_prioritylayerdatasupportentriesvalue_product pa_r_pvs_prioritylayerdatasupportentriesvalue_product pa_s_pvs_prioritylayerdatasupportentriesvalue_product. ((((exists pa_h_pvs_prioritylayerdatasupportentriesvalue_product_factor. pa_h_pvs_prioritylayerdatasupportentriesvalue_product_factor + S (pa_p_pvs_prioritylayerdatasupportentriesvalue_product) = S ((S (pa_i_pvs_prioritylayerdatasupportentriesvalue_product)) * pa_c_pvs_prioritylayerdatasupportentriesvalue)) /\ exists pa_q_pvs_prioritylayerdatasupportentriesvalue_product_factor. pa_b_pvs_prioritylayerdatasupportentriesvalue = pa_q_pvs_prioritylayerdatasupportentriesvalue_product_factor * S ((S (pa_i_pvs_prioritylayerdatasupportentriesvalue_product)) * pa_c_pvs_prioritylayerdatasupportentriesvalue) + (pa_p_pvs_prioritylayerdatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_prioritylayerdatasupportentriesvalue_product_partial. pa_h_pvs_prioritylayerdatasupportentriesvalue_product_partial + S (pa_r_pvs_prioritylayerdatasupportentriesvalue_product) = S ((S (pa_i_pvs_prioritylayerdatasupportentriesvalue_product)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerdatasupportentriesvalue_product_partial. pa_u_pvs_prioritylayerdatasupportentriesvalue_product = pa_q_pvs_prioritylayerdatasupportentriesvalue_product_partial * S ((S (pa_i_pvs_prioritylayerdatasupportentriesvalue_product)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product) + (pa_r_pvs_prioritylayerdatasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_prioritylayerdatasupportentriesvalue_product_successor. pa_h_pvs_prioritylayerdatasupportentriesvalue_product_successor + S (pa_s_pvs_prioritylayerdatasupportentriesvalue_product) = S ((S (S pa_i_pvs_prioritylayerdatasupportentriesvalue_product)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerdatasupportentriesvalue_product_successor. pa_u_pvs_prioritylayerdatasupportentriesvalue_product = pa_q_pvs_prioritylayerdatasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_prioritylayerdatasupportentriesvalue_product)) * pa_v_pvs_prioritylayerdatasupportentriesvalue_product) + (pa_s_pvs_prioritylayerdatasupportentriesvalue_product))) /\ pa_s_pvs_prioritylayerdatasupportentriesvalue_product = pa_r_pvs_prioritylayerdatasupportentriesvalue_product * pa_p_pvs_prioritylayerdatasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_prioritylayerdatasupportcover. (~((pvs_divisor_prioritylayerdatasupportcover) = 1) /\ forall pvs_left_prioritylayerdatasupportcoverprime pvs_right_prioritylayerdatasupportcoverprime. (pvs_divisor_prioritylayerdatasupportcover) = pvs_left_prioritylayerdatasupportcoverprime * pvs_right_prioritylayerdatasupportcoverprime -> pvs_left_prioritylayerdatasupportcoverprime = 1 \/ pvs_right_prioritylayerdatasupportcoverprime = 1) -> (exists pvs_factor_prioritylayerdatasupportcoverdivides. ((n)) = (pvs_divisor_prioritylayerdatasupportcover) * pvs_factor_prioritylayerdatasupportcoverdivides) -> exists pvs_position_prioritylayerdatasupportcover. (exists pvs_gap_prioritylayerdatasupportcoverbound. pvs_gap_prioritylayerdatasupportcoverbound + S (pvs_position_prioritylayerdatasupportcover) = (ppf_length_prioritylayer)) /\ (((exists ff_h_pvs_prioritylayerdatasupportcoverentry. ff_h_pvs_prioritylayerdatasupportcoverentry + S (pvs_divisor_prioritylayerdatasupportcover) = S ((S (pvs_position_prioritylayerdatasupportcover)) * ppf_pc_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatasupportcoverentry. ppf_pb_prioritylayer = ff_q_pvs_prioritylayerdatasupportcoverentry * S ((S (pvs_position_prioritylayerdatasupportcover)) * ppf_pc_prioritylayer) + (pvs_divisor_prioritylayerdatasupportcover)))) /\ (exists ff_u_pvs_prioritylayerdatasupportproduct ff_v_pvs_prioritylayerdatasupportproduct. ((((exists ff_h_pvs_prioritylayerdatasupportproduct_start. ff_h_pvs_prioritylayerdatasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_prioritylayerdatasupportproduct)) /\ exists ff_q_pvs_prioritylayerdatasupportproduct_start. ff_u_pvs_prioritylayerdatasupportproduct = ff_q_pvs_prioritylayerdatasupportproduct_start * S ((S (0)) * ff_v_pvs_prioritylayerdatasupportproduct) + (1))) /\ ((((exists ff_h_pvs_prioritylayerdatasupportproduct_terminal. ff_h_pvs_prioritylayerdatasupportproduct_terminal + S ((n)) = S ((S (ppf_length_prioritylayer)) * ff_v_pvs_prioritylayerdatasupportproduct)) /\ exists ff_q_pvs_prioritylayerdatasupportproduct_terminal. ff_u_pvs_prioritylayerdatasupportproduct = ff_q_pvs_prioritylayerdatasupportproduct_terminal * S ((S (ppf_length_prioritylayer)) * ff_v_pvs_prioritylayerdatasupportproduct) + ((n)))) /\ forall ff_i_pvs_prioritylayerdatasupportproduct. (exists ff_lt_pvs_prioritylayerdatasupportproduct_bound. ff_lt_pvs_prioritylayerdatasupportproduct_bound + S ff_i_pvs_prioritylayerdatasupportproduct = ppf_length_prioritylayer) -> exists ff_p_pvs_prioritylayerdatasupportproduct ff_r_pvs_prioritylayerdatasupportproduct ff_s_pvs_prioritylayerdatasupportproduct. ((((exists ff_h_pvs_prioritylayerdatasupportproduct_factor. ff_h_pvs_prioritylayerdatasupportproduct_factor + S (ff_p_pvs_prioritylayerdatasupportproduct) = S ((S (ff_i_pvs_prioritylayerdatasupportproduct)) * ppf_vc_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatasupportproduct_factor. ppf_vb_prioritylayer = ff_q_pvs_prioritylayerdatasupportproduct_factor * S ((S (ff_i_pvs_prioritylayerdatasupportproduct)) * ppf_vc_prioritylayer) + (ff_p_pvs_prioritylayerdatasupportproduct))) /\ ((((exists ff_h_pvs_prioritylayerdatasupportproduct_partial. ff_h_pvs_prioritylayerdatasupportproduct_partial + S (ff_r_pvs_prioritylayerdatasupportproduct) = S ((S (ff_i_pvs_prioritylayerdatasupportproduct)) * ff_v_pvs_prioritylayerdatasupportproduct)) /\ exists ff_q_pvs_prioritylayerdatasupportproduct_partial. ff_u_pvs_prioritylayerdatasupportproduct = ff_q_pvs_prioritylayerdatasupportproduct_partial * S ((S (ff_i_pvs_prioritylayerdatasupportproduct)) * ff_v_pvs_prioritylayerdatasupportproduct) + (ff_r_pvs_prioritylayerdatasupportproduct))) /\ ((((exists ff_h_pvs_prioritylayerdatasupportproduct_successor. ff_h_pvs_prioritylayerdatasupportproduct_successor + S (ff_s_pvs_prioritylayerdatasupportproduct) = S ((S (S ff_i_pvs_prioritylayerdatasupportproduct)) * ff_v_pvs_prioritylayerdatasupportproduct)) /\ exists ff_q_pvs_prioritylayerdatasupportproduct_successor. ff_u_pvs_prioritylayerdatasupportproduct = ff_q_pvs_prioritylayerdatasupportproduct_successor * S ((S (S ff_i_pvs_prioritylayerdatasupportproduct)) * ff_v_pvs_prioritylayerdatasupportproduct) + (ff_s_pvs_prioritylayerdatasupportproduct))) /\ ff_s_pvs_prioritylayerdatasupportproduct = ff_r_pvs_prioritylayerdatasupportproduct * ff_p_pvs_prioritylayerdatasupportproduct)))))))))))))) /\ (((((forall ppf_index_prioritylayerdatagcdcommon ppf_entry_prioritylayerdatagcdcommon. (exists pvs_gap_prioritylayerdatagcdcommonbound. pvs_gap_prioritylayerdatagcdcommonbound + S (ppf_index_prioritylayerdatagcdcommon) = (ppf_length_prioritylayer)) -> (((exists ff_h_pvs_prioritylayerdatagcdcommonentry. ff_h_pvs_prioritylayerdatagcdcommonentry + S (ppf_entry_prioritylayerdatagcdcommon) = S ((S (ppf_index_prioritylayerdatagcdcommon)) * ppf_ec_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatagcdcommonentry. ppf_eb_prioritylayer = ff_q_pvs_prioritylayerdatagcdcommonentry * S ((S (ppf_index_prioritylayerdatagcdcommon)) * ppf_ec_prioritylayer) + (ppf_entry_prioritylayerdatagcdcommon))) -> (exists pvs_factor_prioritylayerdatagcdcommondivisor. (ppf_entry_prioritylayerdatagcdcommon) = (ppf_gcd_prioritylayer) * pvs_factor_prioritylayerdatagcdcommondivisor)) /\ (forall ppf_common_prioritylayerdatagcd. (forall ppf_index_prioritylayerdatagcdother ppf_entry_prioritylayerdatagcdother. (exists pvs_gap_prioritylayerdatagcdotherbound. pvs_gap_prioritylayerdatagcdotherbound + S (ppf_index_prioritylayerdatagcdother) = (ppf_length_prioritylayer)) -> (((exists ff_h_pvs_prioritylayerdatagcdotherentry. ff_h_pvs_prioritylayerdatagcdotherentry + S (ppf_entry_prioritylayerdatagcdother) = S ((S (ppf_index_prioritylayerdatagcdother)) * ppf_ec_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatagcdotherentry. ppf_eb_prioritylayer = ff_q_pvs_prioritylayerdatagcdotherentry * S ((S (ppf_index_prioritylayerdatagcdother)) * ppf_ec_prioritylayer) + (ppf_entry_prioritylayerdatagcdother))) -> (exists pvs_factor_prioritylayerdatagcdotherdivisor. (ppf_entry_prioritylayerdatagcdother) = (ppf_common_prioritylayerdatagcd) * pvs_factor_prioritylayerdatagcdotherdivisor)) -> (exists pvs_factor_prioritylayerdatagcdgreatest. (ppf_gcd_prioritylayer) = (ppf_common_prioritylayerdatagcd) * pvs_factor_prioritylayerdatagcdgreatest)))) /\ (((~((ppf_gcd_prioritylayer) = 0)) /\ (forall ppf_table_degree_prioritylayerdataroots. ~(ppf_table_degree_prioritylayerdataroots = 0) -> (exists pvs_factor_prioritylayerdatarootsdivisor. (ppf_gcd_prioritylayer) = (ppf_table_degree_prioritylayerdataroots) * pvs_factor_prioritylayerdatarootsdivisor) -> exists ppf_table_root_prioritylayerdataroots. (((exists ff_h_pvs_prioritylayerdatarootsentry. ff_h_pvs_prioritylayerdatarootsentry + S (ppf_table_root_prioritylayerdataroots) = S ((S (ppf_table_degree_prioritylayerdataroots)) * ppf_rc_prioritylayer)) /\ exists ff_q_pvs_prioritylayerdatarootsentry. ppf_rb_prioritylayer = ff_q_pvs_prioritylayerdatarootsentry * S ((S (ppf_table_degree_prioritylayerdataroots)) * ppf_rc_prioritylayer) + (ppf_table_root_prioritylayerdataroots))) /\ (exists pa_b_pvs_prioritylayerdatarootspower pa_c_pvs_prioritylayerdatarootspower. ((forall pa_i_pvs_prioritylayerdatarootspower_repeat. (exists pa_lt_pvs_prioritylayerdatarootspower_repeat_bound. pa_lt_pvs_prioritylayerdatarootspower_repeat_bound + S pa_i_pvs_prioritylayerdatarootspower_repeat = ppf_table_degree_prioritylayerdataroots) -> (((exists pa_h_pvs_prioritylayerdatarootspower_repeat_decoded. pa_h_pvs_prioritylayerdatarootspower_repeat_decoded + S (ppf_table_root_prioritylayerdataroots) = S ((S (pa_i_pvs_prioritylayerdatarootspower_repeat)) * pa_c_pvs_prioritylayerdatarootspower)) /\ exists pa_q_pvs_prioritylayerdatarootspower_repeat_decoded. pa_b_pvs_prioritylayerdatarootspower = pa_q_pvs_prioritylayerdatarootspower_repeat_decoded * S ((S (pa_i_pvs_prioritylayerdatarootspower_repeat)) * pa_c_pvs_prioritylayerdatarootspower) + (ppf_table_root_prioritylayerdataroots)))) /\ (exists pa_u_pvs_prioritylayerdatarootspower_product pa_v_pvs_prioritylayerdatarootspower_product. ((((exists pa_h_pvs_prioritylayerdatarootspower_product_start. pa_h_pvs_prioritylayerdatarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayerdatarootspower_product)) /\ exists pa_q_pvs_prioritylayerdatarootspower_product_start. pa_u_pvs_prioritylayerdatarootspower_product = pa_q_pvs_prioritylayerdatarootspower_product_start * S ((S (0)) * pa_v_pvs_prioritylayerdatarootspower_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayerdatarootspower_product_terminal. pa_h_pvs_prioritylayerdatarootspower_product_terminal + S ((n)) = S ((S (ppf_table_degree_prioritylayerdataroots)) * pa_v_pvs_prioritylayerdatarootspower_product)) /\ exists pa_q_pvs_prioritylayerdatarootspower_product_terminal. pa_u_pvs_prioritylayerdatarootspower_product = pa_q_pvs_prioritylayerdatarootspower_product_terminal * S ((S (ppf_table_degree_prioritylayerdataroots)) * pa_v_pvs_prioritylayerdatarootspower_product) + ((n)))) /\ forall pa_i_pvs_prioritylayerdatarootspower_product. (exists pa_lt_pvs_prioritylayerdatarootspower_product_bound. pa_lt_pvs_prioritylayerdatarootspower_product_bound + S pa_i_pvs_prioritylayerdatarootspower_product = ppf_table_degree_prioritylayerdataroots) -> exists pa_p_pvs_prioritylayerdatarootspower_product pa_r_pvs_prioritylayerdatarootspower_product pa_s_pvs_prioritylayerdatarootspower_product. ((((exists pa_h_pvs_prioritylayerdatarootspower_product_factor. pa_h_pvs_prioritylayerdatarootspower_product_factor + S (pa_p_pvs_prioritylayerdatarootspower_product) = S ((S (pa_i_pvs_prioritylayerdatarootspower_product)) * pa_c_pvs_prioritylayerdatarootspower)) /\ exists pa_q_pvs_prioritylayerdatarootspower_product_factor. pa_b_pvs_prioritylayerdatarootspower = pa_q_pvs_prioritylayerdatarootspower_product_factor * S ((S (pa_i_pvs_prioritylayerdatarootspower_product)) * pa_c_pvs_prioritylayerdatarootspower) + (pa_p_pvs_prioritylayerdatarootspower_product))) /\ ((((exists pa_h_pvs_prioritylayerdatarootspower_product_partial. pa_h_pvs_prioritylayerdatarootspower_product_partial + S (pa_r_pvs_prioritylayerdatarootspower_product) = S ((S (pa_i_pvs_prioritylayerdatarootspower_product)) * pa_v_pvs_prioritylayerdatarootspower_product)) /\ exists pa_q_pvs_prioritylayerdatarootspower_product_partial. pa_u_pvs_prioritylayerdatarootspower_product = pa_q_pvs_prioritylayerdatarootspower_product_partial * S ((S (pa_i_pvs_prioritylayerdatarootspower_product)) * pa_v_pvs_prioritylayerdatarootspower_product) + (pa_r_pvs_prioritylayerdatarootspower_product))) /\ ((((exists pa_h_pvs_prioritylayerdatarootspower_product_successor. pa_h_pvs_prioritylayerdatarootspower_product_successor + S (pa_s_pvs_prioritylayerdatarootspower_product) = S ((S (S pa_i_pvs_prioritylayerdatarootspower_product)) * pa_v_pvs_prioritylayerdatarootspower_product)) /\ exists pa_q_pvs_prioritylayerdatarootspower_product_successor. pa_u_pvs_prioritylayerdatarootspower_product = pa_q_pvs_prioritylayerdatarootspower_product_successor * S ((S (S pa_i_pvs_prioritylayerdatarootspower_product)) * pa_v_pvs_prioritylayerdatarootspower_product) + (pa_s_pvs_prioritylayerdatarootspower_product))) /\ pa_s_pvs_prioritylayerdatarootspower_product = pa_r_pvs_prioritylayerdatarootspower_product * pa_p_pvs_prioritylayerdatarootspower_product))))))))))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.