PrimeValuationSupport(n,pb,pc,eb,ec,vb,vc,l)

((~(((n)) = 0)) /\ (((forall pfp_i_pvs_prioritylayerdistinct pfp_j_pvs_prioritylayerdistinct pfp_a_pvs_prioritylayerdistinct. (exists pfp_gap_pvs_prioritylayerdistinctfirst. pfp_gap_pvs_prioritylayerdistinctfirst + S (pfp_i_pvs_prioritylayerdistinct) = ((l))) -> (exists pfp_gap_pvs_prioritylayerdistinctsecond. pfp_gap_pvs_prioritylayerdistinctsecond + S (pfp_j_pvs_prioritylayerdistinct) = ((l))) -> (((exists ff_h_pfp_pvs_prioritylayerdistinctleft. ff_h_pfp_pvs_prioritylayerdistinctleft + S (pfp_a_pvs_prioritylayerdistinct) = S ((S (pfp_i_pvs_prioritylayerdistinct)) * (pc))) /\ exists ff_q_pfp_pvs_prioritylayerdistinctleft. (pb) = ff_q_pfp_pvs_prioritylayerdistinctleft * S ((S (pfp_i_pvs_prioritylayerdistinct)) * (pc)) + (pfp_a_pvs_prioritylayerdistinct))) -> (((exists ff_h_pfp_pvs_prioritylayerdistinctright. ff_h_pfp_pvs_prioritylayerdistinctright + S (pfp_a_pvs_prioritylayerdistinct) = S ((S (pfp_j_pvs_prioritylayerdistinct)) * (pc))) /\ exists ff_q_pfp_pvs_prioritylayerdistinctright. (pb) = ff_q_pfp_pvs_prioritylayerdistinctright * S ((S (pfp_j_pvs_prioritylayerdistinct)) * (pc)) + (pfp_a_pvs_prioritylayerdistinct))) -> pfp_i_pvs_prioritylayerdistinct = pfp_j_pvs_prioritylayerdistinct) /\ (((forall pvs_index_prioritylayerentries. (exists pvs_gap_prioritylayerentriesindex. pvs_gap_prioritylayerentriesindex + S (pvs_index_prioritylayerentries) = ((l))) -> exists pvs_prime_prioritylayerentries pvs_exponent_prioritylayerentries pvs_power_prioritylayerentries. (((((exists ff_h_pvs_prioritylayerentriesprime. ff_h_pvs_prioritylayerentriesprime + S (pvs_prime_prioritylayerentries) = S ((S (pvs_index_prioritylayerentries)) * (pc))) /\ exists ff_q_pvs_prioritylayerentriesprime. (pb) = ff_q_pvs_prioritylayerentriesprime * S ((S (pvs_index_prioritylayerentries)) * (pc)) + (pvs_prime_prioritylayerentries))) /\ (((((exists ff_h_pvs_prioritylayerentriesexponent. ff_h_pvs_prioritylayerentriesexponent + S (pvs_exponent_prioritylayerentries) = S ((S (pvs_index_prioritylayerentries)) * (ec))) /\ exists ff_q_pvs_prioritylayerentriesexponent. (eb) = ff_q_pvs_prioritylayerentriesexponent * S ((S (pvs_index_prioritylayerentries)) * (ec)) + (pvs_exponent_prioritylayerentries))) /\ (((((exists ff_h_pvs_prioritylayerentriespower. ff_h_pvs_prioritylayerentriespower + S (pvs_power_prioritylayerentries) = S ((S (pvs_index_prioritylayerentries)) * (vc))) /\ exists ff_q_pvs_prioritylayerentriespower. (vb) = ff_q_pvs_prioritylayerentriespower * S ((S (pvs_index_prioritylayerentries)) * (vc)) + (pvs_power_prioritylayerentries))) /\ (((~((pvs_prime_prioritylayerentries) = 1) /\ forall pvs_left_prioritylayerentriesdomain pvs_right_prioritylayerentriesdomain. (pvs_prime_prioritylayerentries) = pvs_left_prioritylayerentriesdomain * pvs_right_prioritylayerentriesdomain -> pvs_left_prioritylayerentriesdomain = 1 \/ pvs_right_prioritylayerentriesdomain = 1) /\ (((~(pvs_exponent_prioritylayerentries = 0)) /\ (((((exists bpd_gap_pvs_prioritylayerentriesvaluation_selected_bound. bpd_gap_pvs_prioritylayerentriesvaluation_selected_bound + (pvs_exponent_prioritylayerentries) = ((n))) /\ (exists bpvi_result_pvs_prioritylayerentriesvaluation_selected. ((exists bpvi_b_pvs_prioritylayerentriesvaluation_selected_power bpvi_c_pvs_prioritylayerentriesvaluation_selected_power. ((forall bpvi_i_pvs_prioritylayerentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_prioritylayerentriesvaluation_selected_power. bpvi_repeat_gap_pvs_prioritylayerentriesvaluation_selected_power + S bpvi_i_pvs_prioritylayerentriesvaluation_selected_power = pvs_exponent_prioritylayerentries) -> (((exists bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_repeat. bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_repeat + S (pvs_prime_prioritylayerentries) = S ((S (bpvi_i_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_repeat. bpvi_b_pvs_prioritylayerentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_selected_power) + (pvs_prime_prioritylayerentries)))) /\ (exists bpvi_u_pvs_prioritylayerentriesvaluation_selected_power bpvi_v_pvs_prioritylayerentriesvaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_start. bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_start. bpvi_u_pvs_prioritylayerentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_terminal. bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_prioritylayerentriesvaluation_selected) = S ((S (pvs_exponent_prioritylayerentries)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_terminal. bpvi_u_pvs_prioritylayerentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_prioritylayerentries)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power) + (bpvi_result_pvs_prioritylayerentriesvaluation_selected))) /\ forall bpvi_j_pvs_prioritylayerentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_prioritylayerentriesvaluation_selected_power. bpvi_product_gap_pvs_prioritylayerentriesvaluation_selected_power + S bpvi_j_pvs_prioritylayerentriesvaluation_selected_power = pvs_exponent_prioritylayerentries) -> exists bpvi_factor_pvs_prioritylayerentriesvaluation_selected_power bpvi_partial_pvs_prioritylayerentriesvaluation_selected_power bpvi_successor_pvs_prioritylayerentriesvaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_factor. bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_prioritylayerentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_factor. bpvi_b_pvs_prioritylayerentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_selected_power) + (bpvi_factor_pvs_prioritylayerentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_partial. bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_prioritylayerentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_partial. bpvi_u_pvs_prioritylayerentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power) + (bpvi_partial_pvs_prioritylayerentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_successor. bpvi_h_pvs_prioritylayerentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_prioritylayerentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_successor. bpvi_u_pvs_prioritylayerentriesvaluation_selected_power = bpvi_q_pvs_prioritylayerentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_prioritylayerentriesvaluation_selected_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_selected_power) + (bpvi_successor_pvs_prioritylayerentriesvaluation_selected_power))) /\ bpvi_successor_pvs_prioritylayerentriesvaluation_selected_power = bpvi_partial_pvs_prioritylayerentriesvaluation_selected_power * bpvi_factor_pvs_prioritylayerentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayerentriesvaluation_selected. (n) = bpvi_result_pvs_prioritylayerentriesvaluation_selected * bpvi_divisor_factor_pvs_prioritylayerentriesvaluation_selected))) /\ forall bpd_candidate_pvs_prioritylayerentriesvaluation. (exists bpd_gap_pvs_prioritylayerentriesvaluation_candidate_bound. bpd_gap_pvs_prioritylayerentriesvaluation_candidate_bound + (bpd_candidate_pvs_prioritylayerentriesvaluation) = ((n))) -> (exists bpvi_result_pvs_prioritylayerentriesvaluation_candidate. ((exists bpvi_b_pvs_prioritylayerentriesvaluation_candidate_power bpvi_c_pvs_prioritylayerentriesvaluation_candidate_power. ((forall bpvi_i_pvs_prioritylayerentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_prioritylayerentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_prioritylayerentriesvaluation_candidate_power + S bpvi_i_pvs_prioritylayerentriesvaluation_candidate_power = bpd_candidate_pvs_prioritylayerentriesvaluation) -> (((exists bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_repeat. bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_repeat + S (pvs_prime_prioritylayerentries) = S ((S (bpvi_i_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_repeat. bpvi_b_pvs_prioritylayerentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_candidate_power) + (pvs_prime_prioritylayerentries)))) /\ (exists bpvi_u_pvs_prioritylayerentriesvaluation_candidate_power bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_start. bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_start. bpvi_u_pvs_prioritylayerentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_terminal. bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_prioritylayerentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_prioritylayerentriesvaluation)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_terminal. bpvi_u_pvs_prioritylayerentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_prioritylayerentriesvaluation)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power) + (bpvi_result_pvs_prioritylayerentriesvaluation_candidate))) /\ forall bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_prioritylayerentriesvaluation_candidate_power. bpvi_product_gap_pvs_prioritylayerentriesvaluation_candidate_power + S bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power = bpd_candidate_pvs_prioritylayerentriesvaluation) -> exists bpvi_factor_pvs_prioritylayerentriesvaluation_candidate_power bpvi_partial_pvs_prioritylayerentriesvaluation_candidate_power bpvi_successor_pvs_prioritylayerentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_factor. bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_prioritylayerentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_factor. bpvi_b_pvs_prioritylayerentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_c_pvs_prioritylayerentriesvaluation_candidate_power) + (bpvi_factor_pvs_prioritylayerentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_partial. bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_prioritylayerentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_partial. bpvi_u_pvs_prioritylayerentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power) + (bpvi_partial_pvs_prioritylayerentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_successor. bpvi_h_pvs_prioritylayerentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_prioritylayerentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_successor. bpvi_u_pvs_prioritylayerentriesvaluation_candidate_power = bpvi_q_pvs_prioritylayerentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_prioritylayerentriesvaluation_candidate_power)) * bpvi_v_pvs_prioritylayerentriesvaluation_candidate_power) + (bpvi_successor_pvs_prioritylayerentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_prioritylayerentriesvaluation_candidate_power = bpvi_partial_pvs_prioritylayerentriesvaluation_candidate_power * bpvi_factor_pvs_prioritylayerentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayerentriesvaluation_candidate. (n) = bpvi_result_pvs_prioritylayerentriesvaluation_candidate * bpvi_divisor_factor_pvs_prioritylayerentriesvaluation_candidate)) -> (exists bpd_gap_pvs_prioritylayerentriesvaluation_maximal. bpd_gap_pvs_prioritylayerentriesvaluation_maximal + (bpd_candidate_pvs_prioritylayerentriesvaluation) = (pvs_exponent_prioritylayerentries))) /\ (exists pa_b_pvs_prioritylayerentriesvalue pa_c_pvs_prioritylayerentriesvalue. ((forall pa_i_pvs_prioritylayerentriesvalue_repeat. (exists pa_lt_pvs_prioritylayerentriesvalue_repeat_bound. pa_lt_pvs_prioritylayerentriesvalue_repeat_bound + S pa_i_pvs_prioritylayerentriesvalue_repeat = pvs_exponent_prioritylayerentries) -> (((exists pa_h_pvs_prioritylayerentriesvalue_repeat_decoded. pa_h_pvs_prioritylayerentriesvalue_repeat_decoded + S (pvs_prime_prioritylayerentries) = S ((S (pa_i_pvs_prioritylayerentriesvalue_repeat)) * pa_c_pvs_prioritylayerentriesvalue)) /\ exists pa_q_pvs_prioritylayerentriesvalue_repeat_decoded. pa_b_pvs_prioritylayerentriesvalue = pa_q_pvs_prioritylayerentriesvalue_repeat_decoded * S ((S (pa_i_pvs_prioritylayerentriesvalue_repeat)) * pa_c_pvs_prioritylayerentriesvalue) + (pvs_prime_prioritylayerentries)))) /\ (exists pa_u_pvs_prioritylayerentriesvalue_product pa_v_pvs_prioritylayerentriesvalue_product. ((((exists pa_h_pvs_prioritylayerentriesvalue_product_start. pa_h_pvs_prioritylayerentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayerentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerentriesvalue_product_start. pa_u_pvs_prioritylayerentriesvalue_product = pa_q_pvs_prioritylayerentriesvalue_product_start * S ((S (0)) * pa_v_pvs_prioritylayerentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayerentriesvalue_product_terminal. pa_h_pvs_prioritylayerentriesvalue_product_terminal + S (pvs_power_prioritylayerentries) = S ((S (pvs_exponent_prioritylayerentries)) * pa_v_pvs_prioritylayerentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerentriesvalue_product_terminal. pa_u_pvs_prioritylayerentriesvalue_product = pa_q_pvs_prioritylayerentriesvalue_product_terminal * S ((S (pvs_exponent_prioritylayerentries)) * pa_v_pvs_prioritylayerentriesvalue_product) + (pvs_power_prioritylayerentries))) /\ forall pa_i_pvs_prioritylayerentriesvalue_product. (exists pa_lt_pvs_prioritylayerentriesvalue_product_bound. pa_lt_pvs_prioritylayerentriesvalue_product_bound + S pa_i_pvs_prioritylayerentriesvalue_product = pvs_exponent_prioritylayerentries) -> exists pa_p_pvs_prioritylayerentriesvalue_product pa_r_pvs_prioritylayerentriesvalue_product pa_s_pvs_prioritylayerentriesvalue_product. ((((exists pa_h_pvs_prioritylayerentriesvalue_product_factor. pa_h_pvs_prioritylayerentriesvalue_product_factor + S (pa_p_pvs_prioritylayerentriesvalue_product) = S ((S (pa_i_pvs_prioritylayerentriesvalue_product)) * pa_c_pvs_prioritylayerentriesvalue)) /\ exists pa_q_pvs_prioritylayerentriesvalue_product_factor. pa_b_pvs_prioritylayerentriesvalue = pa_q_pvs_prioritylayerentriesvalue_product_factor * S ((S (pa_i_pvs_prioritylayerentriesvalue_product)) * pa_c_pvs_prioritylayerentriesvalue) + (pa_p_pvs_prioritylayerentriesvalue_product))) /\ ((((exists pa_h_pvs_prioritylayerentriesvalue_product_partial. pa_h_pvs_prioritylayerentriesvalue_product_partial + S (pa_r_pvs_prioritylayerentriesvalue_product) = S ((S (pa_i_pvs_prioritylayerentriesvalue_product)) * pa_v_pvs_prioritylayerentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerentriesvalue_product_partial. pa_u_pvs_prioritylayerentriesvalue_product = pa_q_pvs_prioritylayerentriesvalue_product_partial * S ((S (pa_i_pvs_prioritylayerentriesvalue_product)) * pa_v_pvs_prioritylayerentriesvalue_product) + (pa_r_pvs_prioritylayerentriesvalue_product))) /\ ((((exists pa_h_pvs_prioritylayerentriesvalue_product_successor. pa_h_pvs_prioritylayerentriesvalue_product_successor + S (pa_s_pvs_prioritylayerentriesvalue_product) = S ((S (S pa_i_pvs_prioritylayerentriesvalue_product)) * pa_v_pvs_prioritylayerentriesvalue_product)) /\ exists pa_q_pvs_prioritylayerentriesvalue_product_successor. pa_u_pvs_prioritylayerentriesvalue_product = pa_q_pvs_prioritylayerentriesvalue_product_successor * S ((S (S pa_i_pvs_prioritylayerentriesvalue_product)) * pa_v_pvs_prioritylayerentriesvalue_product) + (pa_s_pvs_prioritylayerentriesvalue_product))) /\ pa_s_pvs_prioritylayerentriesvalue_product = pa_r_pvs_prioritylayerentriesvalue_product * pa_p_pvs_prioritylayerentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_prioritylayercover. (~((pvs_divisor_prioritylayercover) = 1) /\ forall pvs_left_prioritylayercoverprime pvs_right_prioritylayercoverprime. (pvs_divisor_prioritylayercover) = pvs_left_prioritylayercoverprime * pvs_right_prioritylayercoverprime -> pvs_left_prioritylayercoverprime = 1 \/ pvs_right_prioritylayercoverprime = 1) -> (exists pvs_factor_prioritylayercoverdivides. ((n)) = (pvs_divisor_prioritylayercover) * pvs_factor_prioritylayercoverdivides) -> exists pvs_position_prioritylayercover. (exists pvs_gap_prioritylayercoverbound. pvs_gap_prioritylayercoverbound + S (pvs_position_prioritylayercover) = ((l))) /\ (((exists ff_h_pvs_prioritylayercoverentry. ff_h_pvs_prioritylayercoverentry + S (pvs_divisor_prioritylayercover) = S ((S (pvs_position_prioritylayercover)) * (pc))) /\ exists ff_q_pvs_prioritylayercoverentry. (pb) = ff_q_pvs_prioritylayercoverentry * S ((S (pvs_position_prioritylayercover)) * (pc)) + (pvs_divisor_prioritylayercover)))) /\ (exists ff_u_pvs_prioritylayerproduct ff_v_pvs_prioritylayerproduct. ((((exists ff_h_pvs_prioritylayerproduct_start. ff_h_pvs_prioritylayerproduct_start + S (1) = S ((S (0)) * ff_v_pvs_prioritylayerproduct)) /\ exists ff_q_pvs_prioritylayerproduct_start. ff_u_pvs_prioritylayerproduct = ff_q_pvs_prioritylayerproduct_start * S ((S (0)) * ff_v_pvs_prioritylayerproduct) + (1))) /\ ((((exists ff_h_pvs_prioritylayerproduct_terminal. ff_h_pvs_prioritylayerproduct_terminal + S ((n)) = S ((S ((l))) * ff_v_pvs_prioritylayerproduct)) /\ exists ff_q_pvs_prioritylayerproduct_terminal. ff_u_pvs_prioritylayerproduct = ff_q_pvs_prioritylayerproduct_terminal * S ((S ((l))) * ff_v_pvs_prioritylayerproduct) + ((n)))) /\ forall ff_i_pvs_prioritylayerproduct. (exists ff_lt_pvs_prioritylayerproduct_bound. ff_lt_pvs_prioritylayerproduct_bound + S ff_i_pvs_prioritylayerproduct = (l)) -> exists ff_p_pvs_prioritylayerproduct ff_r_pvs_prioritylayerproduct ff_s_pvs_prioritylayerproduct. ((((exists ff_h_pvs_prioritylayerproduct_factor. ff_h_pvs_prioritylayerproduct_factor + S (ff_p_pvs_prioritylayerproduct) = S ((S (ff_i_pvs_prioritylayerproduct)) * (vc))) /\ exists ff_q_pvs_prioritylayerproduct_factor. (vb) = ff_q_pvs_prioritylayerproduct_factor * S ((S (ff_i_pvs_prioritylayerproduct)) * (vc)) + (ff_p_pvs_prioritylayerproduct))) /\ ((((exists ff_h_pvs_prioritylayerproduct_partial. ff_h_pvs_prioritylayerproduct_partial + S (ff_r_pvs_prioritylayerproduct) = S ((S (ff_i_pvs_prioritylayerproduct)) * ff_v_pvs_prioritylayerproduct)) /\ exists ff_q_pvs_prioritylayerproduct_partial. ff_u_pvs_prioritylayerproduct = ff_q_pvs_prioritylayerproduct_partial * S ((S (ff_i_pvs_prioritylayerproduct)) * ff_v_pvs_prioritylayerproduct) + (ff_r_pvs_prioritylayerproduct))) /\ ((((exists ff_h_pvs_prioritylayerproduct_successor. ff_h_pvs_prioritylayerproduct_successor + S (ff_s_pvs_prioritylayerproduct) = S ((S (S ff_i_pvs_prioritylayerproduct)) * ff_v_pvs_prioritylayerproduct)) /\ exists ff_q_pvs_prioritylayerproduct_successor. ff_u_pvs_prioritylayerproduct = ff_q_pvs_prioritylayerproduct_successor * S ((S (S ff_i_pvs_prioritylayerproduct)) * ff_v_pvs_prioritylayerproduct) + (ff_s_pvs_prioritylayerproduct))) /\ ff_s_pvs_prioritylayerproduct = ff_r_pvs_prioritylayerproduct * ff_p_pvs_prioritylayerproduct)))))))))))))

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