PerfectPowerProfileData(n,w,pb,pc,eb,ec,vb,vc,l,g,rb,rc)

((~(((n)) = 1)) /\ (((exists ppf_code_0_prioritylayercode ppf_code_1_prioritylayercode ppf_code_2_prioritylayercode ppf_code_3_prioritylayercode ppf_code_4_prioritylayercode ppf_code_5_prioritylayercode ppf_code_6_prioritylayercode ppf_code_7_prioritylayercode. (((((w)) = (((pb)) + (ppf_code_0_prioritylayercode)) * S (((pb)) + (ppf_code_0_prioritylayercode)) + ((ppf_code_0_prioritylayercode) + (ppf_code_0_prioritylayercode))) /\ ((((ppf_code_0_prioritylayercode) = (((pc)) + (ppf_code_1_prioritylayercode)) * S (((pc)) + (ppf_code_1_prioritylayercode)) + ((ppf_code_1_prioritylayercode) + (ppf_code_1_prioritylayercode))) /\ ((((ppf_code_1_prioritylayercode) = (((eb)) + (ppf_code_2_prioritylayercode)) * S (((eb)) + (ppf_code_2_prioritylayercode)) + ((ppf_code_2_prioritylayercode) + (ppf_code_2_prioritylayercode))) /\ ((((ppf_code_2_prioritylayercode) = (((ec)) + (ppf_code_3_prioritylayercode)) * S (((ec)) + (ppf_code_3_prioritylayercode)) + ((ppf_code_3_prioritylayercode) + (ppf_code_3_prioritylayercode))) /\ ((((ppf_code_3_prioritylayercode) = (((vb)) + (ppf_code_4_prioritylayercode)) * S (((vb)) + (ppf_code_4_prioritylayercode)) + ((ppf_code_4_prioritylayercode) + (ppf_code_4_prioritylayercode))) /\ ((((ppf_code_4_prioritylayercode) = (((vc)) + (ppf_code_5_prioritylayercode)) * S (((vc)) + (ppf_code_5_prioritylayercode)) + ((ppf_code_5_prioritylayercode) + (ppf_code_5_prioritylayercode))) /\ ((((ppf_code_5_prioritylayercode) = (((l)) + (ppf_code_6_prioritylayercode)) * S (((l)) + (ppf_code_6_prioritylayercode)) + ((ppf_code_6_prioritylayercode) + (ppf_code_6_prioritylayercode))) /\ ((((ppf_code_6_prioritylayercode) = (((g)) + (ppf_code_7_prioritylayercode)) * S (((g)) + (ppf_code_7_prioritylayercode)) + ((ppf_code_7_prioritylayercode) + (ppf_code_7_prioritylayercode))) /\ ((ppf_code_7_prioritylayercode) = (((rb)) + ((rc))) * S (((rb)) + ((rc))) + (((rc)) + ((rc))))))))))))))))))))) /\ (((((~(((n)) = 0)) /\ (((forall pfp_i_pvs_prioritylayersupportdistinct pfp_j_pvs_prioritylayersupportdistinct pfp_a_pvs_prioritylayersupportdistinct. (exists pfp_gap_pvs_prioritylayersupportdistinctfirst. pfp_gap_pvs_prioritylayersupportdistinctfirst + S (pfp_i_pvs_prioritylayersupportdistinct) = ((l))) -> (exists pfp_gap_pvs_prioritylayersupportdistinctsecond. pfp_gap_pvs_prioritylayersupportdistinctsecond + S (pfp_j_pvs_prioritylayersupportdistinct) = ((l))) -> (((exists ff_h_pfp_pvs_prioritylayersupportdistinctleft. ff_h_pfp_pvs_prioritylayersupportdistinctleft + S (pfp_a_pvs_prioritylayersupportdistinct) = S ((S (pfp_i_pvs_prioritylayersupportdistinct)) * (pc))) /\ exists ff_q_pfp_pvs_prioritylayersupportdistinctleft. (pb) = ff_q_pfp_pvs_prioritylayersupportdistinctleft * S ((S (pfp_i_pvs_prioritylayersupportdistinct)) * (pc)) + (pfp_a_pvs_prioritylayersupportdistinct))) -> (((exists ff_h_pfp_pvs_prioritylayersupportdistinctright. ff_h_pfp_pvs_prioritylayersupportdistinctright + S (pfp_a_pvs_prioritylayersupportdistinct) = S ((S (pfp_j_pvs_prioritylayersupportdistinct)) * (pc))) /\ exists ff_q_pfp_pvs_prioritylayersupportdistinctright. (pb) = ff_q_pfp_pvs_prioritylayersupportdistinctright * S ((S (pfp_j_pvs_prioritylayersupportdistinct)) * (pc)) + (pfp_a_pvs_prioritylayersupportdistinct))) -> pfp_i_pvs_prioritylayersupportdistinct = pfp_j_pvs_prioritylayersupportdistinct) /\ (((forall pvs_index_prioritylayersupportentries. (exists pvs_gap_prioritylayersupportentriesindex. pvs_gap_prioritylayersupportentriesindex + S (pvs_index_prioritylayersupportentries) = ((l))) -> exists pvs_prime_prioritylayersupportentries pvs_exponent_prioritylayersupportentries pvs_power_prioritylayersupportentries. (((((exists ff_h_pvs_prioritylayersupportentriesprime. ff_h_pvs_prioritylayersupportentriesprime + S (pvs_prime_prioritylayersupportentries) = S ((S (pvs_index_prioritylayersupportentries)) * (pc))) /\ exists ff_q_pvs_prioritylayersupportentriesprime. (pb) = ff_q_pvs_prioritylayersupportentriesprime * S ((S (pvs_index_prioritylayersupportentries)) * (pc)) + (pvs_prime_prioritylayersupportentries))) /\ (((((exists ff_h_pvs_prioritylayersupportentriesexponent. ff_h_pvs_prioritylayersupportentriesexponent + S (pvs_exponent_prioritylayersupportentries) = S ((S (pvs_index_prioritylayersupportentries)) * (ec))) /\ exists ff_q_pvs_prioritylayersupportentriesexponent. (eb) = ff_q_pvs_prioritylayersupportentriesexponent * S ((S (pvs_index_prioritylayersupportentries)) * (ec)) + (pvs_exponent_prioritylayersupportentries))) /\ (((((exists ff_h_pvs_prioritylayersupportentriespower. ff_h_pvs_prioritylayersupportentriespower + S (pvs_power_prioritylayersupportentries) = S ((S (pvs_index_prioritylayersupportentries)) * (vc))) /\ exists ff_q_pvs_prioritylayersupportentriespower. (vb) = ff_q_pvs_prioritylayersupportentriespower * S ((S (pvs_index_prioritylayersupportentries)) * (vc)) + (pvs_power_prioritylayersupportentries))) /\ (((~((pvs_prime_prioritylayersupportentries) = 1) /\ forall pvs_left_prioritylayersupportentriesdomain pvs_right_prioritylayersupportentriesdomain. (pvs_prime_prioritylayersupportentries) = pvs_left_prioritylayersupportentriesdomain * pvs_right_prioritylayersupportentriesdomain -> pvs_left_prioritylayersupportentriesdomain = 1 \/ pvs_right_prioritylayersupportentriesdomain = 1) /\ (((~(pvs_exponent_prioritylayersupportentries = 0)) /\ (((((exists bpd_gap_pvs_prioritylayersupportentriesvaluation_selected_bound. bpd_gap_pvs_prioritylayersupportentriesvaluation_selected_bound + (pvs_exponent_prioritylayersupportentries) = ((n))) /\ (exists bpvi_result_pvs_prioritylayersupportentriesvaluation_selected. ((exists bpvi_b_pvs_prioritylayersupportentriesvaluation_selected_power bpvi_c_pvs_prioritylayersupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_prioritylayersupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_prioritylayersupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_prioritylayersupportentriesvaluation_selected_power + S bpvi_i_pvs_prioritylayersupportentriesvaluation_selected_power = pvs_exponent_prioritylayersupportentries) -> (((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_repeat + S (pvs_prime_prioritylayersupportentries) = S ((S (bpvi_i_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_prioritylayersupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_selected_power) + (pvs_prime_prioritylayersupportentries)))) /\ (exists bpvi_u_pvs_prioritylayersupportentriesvaluation_selected_power bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_start. bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_start. bpvi_u_pvs_prioritylayersupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_prioritylayersupportentriesvaluation_selected) = S ((S (pvs_exponent_prioritylayersupportentries)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_prioritylayersupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_prioritylayersupportentries)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power) + (bpvi_result_pvs_prioritylayersupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_prioritylayersupportentriesvaluation_selected_power. bpvi_product_gap_pvs_prioritylayersupportentriesvaluation_selected_power + S bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power = pvs_exponent_prioritylayersupportentries) -> exists bpvi_factor_pvs_prioritylayersupportentriesvaluation_selected_power bpvi_partial_pvs_prioritylayersupportentriesvaluation_selected_power bpvi_successor_pvs_prioritylayersupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_factor. bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_prioritylayersupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_factor. bpvi_b_pvs_prioritylayersupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_selected_power) + (bpvi_factor_pvs_prioritylayersupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_partial. bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_prioritylayersupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_partial. bpvi_u_pvs_prioritylayersupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power) + (bpvi_partial_pvs_prioritylayersupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_successor. bpvi_h_pvs_prioritylayersupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_prioritylayersupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_successor. bpvi_u_pvs_prioritylayersupportentriesvaluation_selected_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_prioritylayersupportentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_selected_power) + (bpvi_successor_pvs_prioritylayersupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_prioritylayersupportentriesvaluation_selected_power = bpvi_partial_pvs_prioritylayersupportentriesvaluation_selected_power * bpvi_factor_pvs_prioritylayersupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayersupportentriesvaluation_selected. (n) = bpvi_result_pvs_prioritylayersupportentriesvaluation_selected * bpvi_divisor_factor_pvs_prioritylayersupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_prioritylayersupportentriesvaluation. (exists bpd_gap_pvs_prioritylayersupportentriesvaluation_candidate_bound. bpd_gap_pvs_prioritylayersupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_prioritylayersupportentriesvaluation) = ((n))) -> (exists bpvi_result_pvs_prioritylayersupportentriesvaluation_candidate. ((exists bpvi_b_pvs_prioritylayersupportentriesvaluation_candidate_power bpvi_c_pvs_prioritylayersupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_prioritylayersupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_prioritylayersupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_prioritylayersupportentriesvaluation_candidate_power + S bpvi_i_pvs_prioritylayersupportentriesvaluation_candidate_power = bpd_candidate_pvs_prioritylayersupportentriesvaluation) -> (((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_repeat + S (pvs_prime_prioritylayersupportentries) = S ((S (bpvi_i_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_prioritylayersupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_candidate_power) + (pvs_prime_prioritylayersupportentries)))) /\ (exists bpvi_u_pvs_prioritylayersupportentriesvaluation_candidate_power bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_start. bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_start. bpvi_u_pvs_prioritylayersupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_prioritylayersupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_prioritylayersupportentriesvaluation)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_prioritylayersupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_prioritylayersupportentriesvaluation)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power) + (bpvi_result_pvs_prioritylayersupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_prioritylayersupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_prioritylayersupportentriesvaluation_candidate_power + S bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power = bpd_candidate_pvs_prioritylayersupportentriesvaluation) -> exists bpvi_factor_pvs_prioritylayersupportentriesvaluation_candidate_power bpvi_partial_pvs_prioritylayersupportentriesvaluation_candidate_power bpvi_successor_pvs_prioritylayersupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_prioritylayersupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_prioritylayersupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayersupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_prioritylayersupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_prioritylayersupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_prioritylayersupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_prioritylayersupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_prioritylayersupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_prioritylayersupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_prioritylayersupportentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayersupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_prioritylayersupportentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayersupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_prioritylayersupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_prioritylayersupportentriesvaluation_candidate_power = bpvi_partial_pvs_prioritylayersupportentriesvaluation_candidate_power * bpvi_factor_pvs_prioritylayersupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayersupportentriesvaluation_candidate. (n) = bpvi_result_pvs_prioritylayersupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_prioritylayersupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_prioritylayersupportentriesvaluation_maximal. bpd_gap_pvs_prioritylayersupportentriesvaluation_maximal + (bpd_candidate_pvs_prioritylayersupportentriesvaluation) = (pvs_exponent_prioritylayersupportentries))) /\ (exists pa_b_pvs_prioritylayersupportentriesvalue pa_c_pvs_prioritylayersupportentriesvalue. ((forall pa_i_pvs_prioritylayersupportentriesvalue_repeat. (exists pa_lt_pvs_prioritylayersupportentriesvalue_repeat_bound. pa_lt_pvs_prioritylayersupportentriesvalue_repeat_bound + S pa_i_pvs_prioritylayersupportentriesvalue_repeat = pvs_exponent_prioritylayersupportentries) -> (((exists pa_h_pvs_prioritylayersupportentriesvalue_repeat_decoded. pa_h_pvs_prioritylayersupportentriesvalue_repeat_decoded + S (pvs_prime_prioritylayersupportentries) = S ((S (pa_i_pvs_prioritylayersupportentriesvalue_repeat)) * pa_c_pvs_prioritylayersupportentriesvalue)) /\ exists pa_q_pvs_prioritylayersupportentriesvalue_repeat_decoded. pa_b_pvs_prioritylayersupportentriesvalue = pa_q_pvs_prioritylayersupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_prioritylayersupportentriesvalue_repeat)) * pa_c_pvs_prioritylayersupportentriesvalue) + (pvs_prime_prioritylayersupportentries)))) /\ (exists pa_u_pvs_prioritylayersupportentriesvalue_product pa_v_pvs_prioritylayersupportentriesvalue_product. ((((exists pa_h_pvs_prioritylayersupportentriesvalue_product_start. pa_h_pvs_prioritylayersupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayersupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayersupportentriesvalue_product_start. pa_u_pvs_prioritylayersupportentriesvalue_product = pa_q_pvs_prioritylayersupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_prioritylayersupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayersupportentriesvalue_product_terminal. pa_h_pvs_prioritylayersupportentriesvalue_product_terminal + S (pvs_power_prioritylayersupportentries) = S ((S (pvs_exponent_prioritylayersupportentries)) * pa_v_pvs_prioritylayersupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayersupportentriesvalue_product_terminal. pa_u_pvs_prioritylayersupportentriesvalue_product = pa_q_pvs_prioritylayersupportentriesvalue_product_terminal * S ((S (pvs_exponent_prioritylayersupportentries)) * pa_v_pvs_prioritylayersupportentriesvalue_product) + (pvs_power_prioritylayersupportentries))) /\ forall pa_i_pvs_prioritylayersupportentriesvalue_product. (exists pa_lt_pvs_prioritylayersupportentriesvalue_product_bound. pa_lt_pvs_prioritylayersupportentriesvalue_product_bound + S pa_i_pvs_prioritylayersupportentriesvalue_product = pvs_exponent_prioritylayersupportentries) -> exists pa_p_pvs_prioritylayersupportentriesvalue_product pa_r_pvs_prioritylayersupportentriesvalue_product pa_s_pvs_prioritylayersupportentriesvalue_product. ((((exists pa_h_pvs_prioritylayersupportentriesvalue_product_factor. pa_h_pvs_prioritylayersupportentriesvalue_product_factor + S (pa_p_pvs_prioritylayersupportentriesvalue_product) = S ((S (pa_i_pvs_prioritylayersupportentriesvalue_product)) * pa_c_pvs_prioritylayersupportentriesvalue)) /\ exists pa_q_pvs_prioritylayersupportentriesvalue_product_factor. pa_b_pvs_prioritylayersupportentriesvalue = pa_q_pvs_prioritylayersupportentriesvalue_product_factor * S ((S (pa_i_pvs_prioritylayersupportentriesvalue_product)) * pa_c_pvs_prioritylayersupportentriesvalue) + (pa_p_pvs_prioritylayersupportentriesvalue_product))) /\ ((((exists pa_h_pvs_prioritylayersupportentriesvalue_product_partial. pa_h_pvs_prioritylayersupportentriesvalue_product_partial + S (pa_r_pvs_prioritylayersupportentriesvalue_product) = S ((S (pa_i_pvs_prioritylayersupportentriesvalue_product)) * pa_v_pvs_prioritylayersupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayersupportentriesvalue_product_partial. pa_u_pvs_prioritylayersupportentriesvalue_product = pa_q_pvs_prioritylayersupportentriesvalue_product_partial * S ((S (pa_i_pvs_prioritylayersupportentriesvalue_product)) * pa_v_pvs_prioritylayersupportentriesvalue_product) + (pa_r_pvs_prioritylayersupportentriesvalue_product))) /\ ((((exists pa_h_pvs_prioritylayersupportentriesvalue_product_successor. pa_h_pvs_prioritylayersupportentriesvalue_product_successor + S (pa_s_pvs_prioritylayersupportentriesvalue_product) = S ((S (S pa_i_pvs_prioritylayersupportentriesvalue_product)) * pa_v_pvs_prioritylayersupportentriesvalue_product)) /\ exists pa_q_pvs_prioritylayersupportentriesvalue_product_successor. pa_u_pvs_prioritylayersupportentriesvalue_product = pa_q_pvs_prioritylayersupportentriesvalue_product_successor * S ((S (S pa_i_pvs_prioritylayersupportentriesvalue_product)) * pa_v_pvs_prioritylayersupportentriesvalue_product) + (pa_s_pvs_prioritylayersupportentriesvalue_product))) /\ pa_s_pvs_prioritylayersupportentriesvalue_product = pa_r_pvs_prioritylayersupportentriesvalue_product * pa_p_pvs_prioritylayersupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_prioritylayersupportcover. (~((pvs_divisor_prioritylayersupportcover) = 1) /\ forall pvs_left_prioritylayersupportcoverprime pvs_right_prioritylayersupportcoverprime. (pvs_divisor_prioritylayersupportcover) = pvs_left_prioritylayersupportcoverprime * pvs_right_prioritylayersupportcoverprime -> pvs_left_prioritylayersupportcoverprime = 1 \/ pvs_right_prioritylayersupportcoverprime = 1) -> (exists pvs_factor_prioritylayersupportcoverdivides. ((n)) = (pvs_divisor_prioritylayersupportcover) * pvs_factor_prioritylayersupportcoverdivides) -> exists pvs_position_prioritylayersupportcover. (exists pvs_gap_prioritylayersupportcoverbound. pvs_gap_prioritylayersupportcoverbound + S (pvs_position_prioritylayersupportcover) = ((l))) /\ (((exists ff_h_pvs_prioritylayersupportcoverentry. ff_h_pvs_prioritylayersupportcoverentry + S (pvs_divisor_prioritylayersupportcover) = S ((S (pvs_position_prioritylayersupportcover)) * (pc))) /\ exists ff_q_pvs_prioritylayersupportcoverentry. (pb) = ff_q_pvs_prioritylayersupportcoverentry * S ((S (pvs_position_prioritylayersupportcover)) * (pc)) + (pvs_divisor_prioritylayersupportcover)))) /\ (exists ff_u_pvs_prioritylayersupportproduct ff_v_pvs_prioritylayersupportproduct. ((((exists ff_h_pvs_prioritylayersupportproduct_start. ff_h_pvs_prioritylayersupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_prioritylayersupportproduct)) /\ exists ff_q_pvs_prioritylayersupportproduct_start. ff_u_pvs_prioritylayersupportproduct = ff_q_pvs_prioritylayersupportproduct_start * S ((S (0)) * ff_v_pvs_prioritylayersupportproduct) + (1))) /\ ((((exists ff_h_pvs_prioritylayersupportproduct_terminal. ff_h_pvs_prioritylayersupportproduct_terminal + S ((n)) = S ((S ((l))) * ff_v_pvs_prioritylayersupportproduct)) /\ exists ff_q_pvs_prioritylayersupportproduct_terminal. ff_u_pvs_prioritylayersupportproduct = ff_q_pvs_prioritylayersupportproduct_terminal * S ((S ((l))) * ff_v_pvs_prioritylayersupportproduct) + ((n)))) /\ forall ff_i_pvs_prioritylayersupportproduct. (exists ff_lt_pvs_prioritylayersupportproduct_bound. ff_lt_pvs_prioritylayersupportproduct_bound + S ff_i_pvs_prioritylayersupportproduct = (l)) -> exists ff_p_pvs_prioritylayersupportproduct ff_r_pvs_prioritylayersupportproduct ff_s_pvs_prioritylayersupportproduct. ((((exists ff_h_pvs_prioritylayersupportproduct_factor. ff_h_pvs_prioritylayersupportproduct_factor + S (ff_p_pvs_prioritylayersupportproduct) = S ((S (ff_i_pvs_prioritylayersupportproduct)) * (vc))) /\ exists ff_q_pvs_prioritylayersupportproduct_factor. (vb) = ff_q_pvs_prioritylayersupportproduct_factor * S ((S (ff_i_pvs_prioritylayersupportproduct)) * (vc)) + (ff_p_pvs_prioritylayersupportproduct))) /\ ((((exists ff_h_pvs_prioritylayersupportproduct_partial. ff_h_pvs_prioritylayersupportproduct_partial + S (ff_r_pvs_prioritylayersupportproduct) = S ((S (ff_i_pvs_prioritylayersupportproduct)) * ff_v_pvs_prioritylayersupportproduct)) /\ exists ff_q_pvs_prioritylayersupportproduct_partial. ff_u_pvs_prioritylayersupportproduct = ff_q_pvs_prioritylayersupportproduct_partial * S ((S (ff_i_pvs_prioritylayersupportproduct)) * ff_v_pvs_prioritylayersupportproduct) + (ff_r_pvs_prioritylayersupportproduct))) /\ ((((exists ff_h_pvs_prioritylayersupportproduct_successor. ff_h_pvs_prioritylayersupportproduct_successor + S (ff_s_pvs_prioritylayersupportproduct) = S ((S (S ff_i_pvs_prioritylayersupportproduct)) * ff_v_pvs_prioritylayersupportproduct)) /\ exists ff_q_pvs_prioritylayersupportproduct_successor. ff_u_pvs_prioritylayersupportproduct = ff_q_pvs_prioritylayersupportproduct_successor * S ((S (S ff_i_pvs_prioritylayersupportproduct)) * ff_v_pvs_prioritylayersupportproduct) + (ff_s_pvs_prioritylayersupportproduct))) /\ ff_s_pvs_prioritylayersupportproduct = ff_r_pvs_prioritylayersupportproduct * ff_p_pvs_prioritylayersupportproduct)))))))))))))) /\ (((((forall ppf_index_prioritylayergcdcommon ppf_entry_prioritylayergcdcommon. (exists pvs_gap_prioritylayergcdcommonbound. pvs_gap_prioritylayergcdcommonbound + S (ppf_index_prioritylayergcdcommon) = ((l))) -> (((exists ff_h_pvs_prioritylayergcdcommonentry. ff_h_pvs_prioritylayergcdcommonentry + S (ppf_entry_prioritylayergcdcommon) = S ((S (ppf_index_prioritylayergcdcommon)) * (ec))) /\ exists ff_q_pvs_prioritylayergcdcommonentry. (eb) = ff_q_pvs_prioritylayergcdcommonentry * S ((S (ppf_index_prioritylayergcdcommon)) * (ec)) + (ppf_entry_prioritylayergcdcommon))) -> (exists pvs_factor_prioritylayergcdcommondivisor. (ppf_entry_prioritylayergcdcommon) = ((g)) * pvs_factor_prioritylayergcdcommondivisor)) /\ (forall ppf_common_prioritylayergcd. (forall ppf_index_prioritylayergcdother ppf_entry_prioritylayergcdother. (exists pvs_gap_prioritylayergcdotherbound. pvs_gap_prioritylayergcdotherbound + S (ppf_index_prioritylayergcdother) = ((l))) -> (((exists ff_h_pvs_prioritylayergcdotherentry. ff_h_pvs_prioritylayergcdotherentry + S (ppf_entry_prioritylayergcdother) = S ((S (ppf_index_prioritylayergcdother)) * (ec))) /\ exists ff_q_pvs_prioritylayergcdotherentry. (eb) = ff_q_pvs_prioritylayergcdotherentry * S ((S (ppf_index_prioritylayergcdother)) * (ec)) + (ppf_entry_prioritylayergcdother))) -> (exists pvs_factor_prioritylayergcdotherdivisor. (ppf_entry_prioritylayergcdother) = (ppf_common_prioritylayergcd) * pvs_factor_prioritylayergcdotherdivisor)) -> (exists pvs_factor_prioritylayergcdgreatest. ((g)) = (ppf_common_prioritylayergcd) * pvs_factor_prioritylayergcdgreatest)))) /\ (((~(((g)) = 0)) /\ (forall ppf_table_degree_prioritylayerroots. ~(ppf_table_degree_prioritylayerroots = 0) -> (exists pvs_factor_prioritylayerrootsdivisor. ((g)) = (ppf_table_degree_prioritylayerroots) * pvs_factor_prioritylayerrootsdivisor) -> exists ppf_table_root_prioritylayerroots. (((exists ff_h_pvs_prioritylayerrootsentry. ff_h_pvs_prioritylayerrootsentry + S (ppf_table_root_prioritylayerroots) = S ((S (ppf_table_degree_prioritylayerroots)) * (rc))) /\ exists ff_q_pvs_prioritylayerrootsentry. (rb) = ff_q_pvs_prioritylayerrootsentry * S ((S (ppf_table_degree_prioritylayerroots)) * (rc)) + (ppf_table_root_prioritylayerroots))) /\ (exists pa_b_pvs_prioritylayerrootspower pa_c_pvs_prioritylayerrootspower. ((forall pa_i_pvs_prioritylayerrootspower_repeat. (exists pa_lt_pvs_prioritylayerrootspower_repeat_bound. pa_lt_pvs_prioritylayerrootspower_repeat_bound + S pa_i_pvs_prioritylayerrootspower_repeat = ppf_table_degree_prioritylayerroots) -> (((exists pa_h_pvs_prioritylayerrootspower_repeat_decoded. pa_h_pvs_prioritylayerrootspower_repeat_decoded + S (ppf_table_root_prioritylayerroots) = S ((S (pa_i_pvs_prioritylayerrootspower_repeat)) * pa_c_pvs_prioritylayerrootspower)) /\ exists pa_q_pvs_prioritylayerrootspower_repeat_decoded. pa_b_pvs_prioritylayerrootspower = pa_q_pvs_prioritylayerrootspower_repeat_decoded * S ((S (pa_i_pvs_prioritylayerrootspower_repeat)) * pa_c_pvs_prioritylayerrootspower) + (ppf_table_root_prioritylayerroots)))) /\ (exists pa_u_pvs_prioritylayerrootspower_product pa_v_pvs_prioritylayerrootspower_product. ((((exists pa_h_pvs_prioritylayerrootspower_product_start. pa_h_pvs_prioritylayerrootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayerrootspower_product)) /\ exists pa_q_pvs_prioritylayerrootspower_product_start. pa_u_pvs_prioritylayerrootspower_product = pa_q_pvs_prioritylayerrootspower_product_start * S ((S (0)) * pa_v_pvs_prioritylayerrootspower_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayerrootspower_product_terminal. pa_h_pvs_prioritylayerrootspower_product_terminal + S ((n)) = S ((S (ppf_table_degree_prioritylayerroots)) * pa_v_pvs_prioritylayerrootspower_product)) /\ exists pa_q_pvs_prioritylayerrootspower_product_terminal. pa_u_pvs_prioritylayerrootspower_product = pa_q_pvs_prioritylayerrootspower_product_terminal * S ((S (ppf_table_degree_prioritylayerroots)) * pa_v_pvs_prioritylayerrootspower_product) + ((n)))) /\ forall pa_i_pvs_prioritylayerrootspower_product. (exists pa_lt_pvs_prioritylayerrootspower_product_bound. pa_lt_pvs_prioritylayerrootspower_product_bound + S pa_i_pvs_prioritylayerrootspower_product = ppf_table_degree_prioritylayerroots) -> exists pa_p_pvs_prioritylayerrootspower_product pa_r_pvs_prioritylayerrootspower_product pa_s_pvs_prioritylayerrootspower_product. ((((exists pa_h_pvs_prioritylayerrootspower_product_factor. pa_h_pvs_prioritylayerrootspower_product_factor + S (pa_p_pvs_prioritylayerrootspower_product) = S ((S (pa_i_pvs_prioritylayerrootspower_product)) * pa_c_pvs_prioritylayerrootspower)) /\ exists pa_q_pvs_prioritylayerrootspower_product_factor. pa_b_pvs_prioritylayerrootspower = pa_q_pvs_prioritylayerrootspower_product_factor * S ((S (pa_i_pvs_prioritylayerrootspower_product)) * pa_c_pvs_prioritylayerrootspower) + (pa_p_pvs_prioritylayerrootspower_product))) /\ ((((exists pa_h_pvs_prioritylayerrootspower_product_partial. pa_h_pvs_prioritylayerrootspower_product_partial + S (pa_r_pvs_prioritylayerrootspower_product) = S ((S (pa_i_pvs_prioritylayerrootspower_product)) * pa_v_pvs_prioritylayerrootspower_product)) /\ exists pa_q_pvs_prioritylayerrootspower_product_partial. pa_u_pvs_prioritylayerrootspower_product = pa_q_pvs_prioritylayerrootspower_product_partial * S ((S (pa_i_pvs_prioritylayerrootspower_product)) * pa_v_pvs_prioritylayerrootspower_product) + (pa_r_pvs_prioritylayerrootspower_product))) /\ ((((exists pa_h_pvs_prioritylayerrootspower_product_successor. pa_h_pvs_prioritylayerrootspower_product_successor + S (pa_s_pvs_prioritylayerrootspower_product) = S ((S (S pa_i_pvs_prioritylayerrootspower_product)) * pa_v_pvs_prioritylayerrootspower_product)) /\ exists pa_q_pvs_prioritylayerrootspower_product_successor. pa_u_pvs_prioritylayerrootspower_product = pa_q_pvs_prioritylayerrootspower_product_successor * S ((S (S pa_i_pvs_prioritylayerrootspower_product)) * pa_v_pvs_prioritylayerrootspower_product) + (pa_s_pvs_prioritylayerrootspower_product))) /\ pa_s_pvs_prioritylayerrootspower_product = pa_r_pvs_prioritylayerrootspower_product * pa_p_pvs_prioritylayerrootspower_product))))))))))))))))))

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