PrimeValuationsDivisible(n,k)

forall ppf_prime_prioritylayer ppf_exponent_prioritylayer. (~((ppf_prime_prioritylayer) = 1) /\ forall pvs_left_prioritylayerdomain pvs_right_prioritylayerdomain. (ppf_prime_prioritylayer) = pvs_left_prioritylayerdomain * pvs_right_prioritylayerdomain -> pvs_left_prioritylayerdomain = 1 \/ pvs_right_prioritylayerdomain = 1) -> (((exists bpd_gap_pvs_prioritylayervaluation_selected_bound. bpd_gap_pvs_prioritylayervaluation_selected_bound + (ppf_exponent_prioritylayer) = ((n))) /\ (exists bpvi_result_pvs_prioritylayervaluation_selected. ((exists bpvi_b_pvs_prioritylayervaluation_selected_power bpvi_c_pvs_prioritylayervaluation_selected_power. ((forall bpvi_i_pvs_prioritylayervaluation_selected_power. (exists bpvi_repeat_gap_pvs_prioritylayervaluation_selected_power. bpvi_repeat_gap_pvs_prioritylayervaluation_selected_power + S bpvi_i_pvs_prioritylayervaluation_selected_power = ppf_exponent_prioritylayer) -> (((exists bpvi_h_pvs_prioritylayervaluation_selected_power_repeat. bpvi_h_pvs_prioritylayervaluation_selected_power_repeat + S (ppf_prime_prioritylayer) = S ((S (bpvi_i_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_repeat. bpvi_b_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_repeat * S ((S (bpvi_i_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power) + (ppf_prime_prioritylayer)))) /\ (exists bpvi_u_pvs_prioritylayervaluation_selected_power bpvi_v_pvs_prioritylayervaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_start. bpvi_h_pvs_prioritylayervaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_start. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_terminal. bpvi_h_pvs_prioritylayervaluation_selected_power_terminal + S (bpvi_result_pvs_prioritylayervaluation_selected) = S ((S (ppf_exponent_prioritylayer)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_terminal. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_terminal * S ((S (ppf_exponent_prioritylayer)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (bpvi_result_pvs_prioritylayervaluation_selected))) /\ forall bpvi_j_pvs_prioritylayervaluation_selected_power. (exists bpvi_product_gap_pvs_prioritylayervaluation_selected_power. bpvi_product_gap_pvs_prioritylayervaluation_selected_power + S bpvi_j_pvs_prioritylayervaluation_selected_power = ppf_exponent_prioritylayer) -> exists bpvi_factor_pvs_prioritylayervaluation_selected_power bpvi_partial_pvs_prioritylayervaluation_selected_power bpvi_successor_pvs_prioritylayervaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_factor. bpvi_h_pvs_prioritylayervaluation_selected_power_factor + S (bpvi_factor_pvs_prioritylayervaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_factor. bpvi_b_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_factor * S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power) + (bpvi_factor_pvs_prioritylayervaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_partial. bpvi_h_pvs_prioritylayervaluation_selected_power_partial + S (bpvi_partial_pvs_prioritylayervaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_partial. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_partial * S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (bpvi_partial_pvs_prioritylayervaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_successor. bpvi_h_pvs_prioritylayervaluation_selected_power_successor + S (bpvi_successor_pvs_prioritylayervaluation_selected_power) = S ((S (S bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_successor. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_successor * S ((S (S bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (bpvi_successor_pvs_prioritylayervaluation_selected_power))) /\ bpvi_successor_pvs_prioritylayervaluation_selected_power = bpvi_partial_pvs_prioritylayervaluation_selected_power * bpvi_factor_pvs_prioritylayervaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayervaluation_selected. (n) = bpvi_result_pvs_prioritylayervaluation_selected * bpvi_divisor_factor_pvs_prioritylayervaluation_selected))) /\ forall bpd_candidate_pvs_prioritylayervaluation. (exists bpd_gap_pvs_prioritylayervaluation_candidate_bound. bpd_gap_pvs_prioritylayervaluation_candidate_bound + (bpd_candidate_pvs_prioritylayervaluation) = ((n))) -> (exists bpvi_result_pvs_prioritylayervaluation_candidate. ((exists bpvi_b_pvs_prioritylayervaluation_candidate_power bpvi_c_pvs_prioritylayervaluation_candidate_power. ((forall bpvi_i_pvs_prioritylayervaluation_candidate_power. (exists bpvi_repeat_gap_pvs_prioritylayervaluation_candidate_power. bpvi_repeat_gap_pvs_prioritylayervaluation_candidate_power + S bpvi_i_pvs_prioritylayervaluation_candidate_power = bpd_candidate_pvs_prioritylayervaluation) -> (((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_repeat. bpvi_h_pvs_prioritylayervaluation_candidate_power_repeat + S (ppf_prime_prioritylayer) = S ((S (bpvi_i_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_repeat. bpvi_b_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power) + (ppf_prime_prioritylayer)))) /\ (exists bpvi_u_pvs_prioritylayervaluation_candidate_power bpvi_v_pvs_prioritylayervaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_start. bpvi_h_pvs_prioritylayervaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_start. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_terminal. bpvi_h_pvs_prioritylayervaluation_candidate_power_terminal + S (bpvi_result_pvs_prioritylayervaluation_candidate) = S ((S (bpd_candidate_pvs_prioritylayervaluation)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_terminal. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_prioritylayervaluation)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (bpvi_result_pvs_prioritylayervaluation_candidate))) /\ forall bpvi_j_pvs_prioritylayervaluation_candidate_power. (exists bpvi_product_gap_pvs_prioritylayervaluation_candidate_power. bpvi_product_gap_pvs_prioritylayervaluation_candidate_power + S bpvi_j_pvs_prioritylayervaluation_candidate_power = bpd_candidate_pvs_prioritylayervaluation) -> exists bpvi_factor_pvs_prioritylayervaluation_candidate_power bpvi_partial_pvs_prioritylayervaluation_candidate_power bpvi_successor_pvs_prioritylayervaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_factor. bpvi_h_pvs_prioritylayervaluation_candidate_power_factor + S (bpvi_factor_pvs_prioritylayervaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_factor. bpvi_b_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_factor * S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power) + (bpvi_factor_pvs_prioritylayervaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_partial. bpvi_h_pvs_prioritylayervaluation_candidate_power_partial + S (bpvi_partial_pvs_prioritylayervaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_partial. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_partial * S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (bpvi_partial_pvs_prioritylayervaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_successor. bpvi_h_pvs_prioritylayervaluation_candidate_power_successor + S (bpvi_successor_pvs_prioritylayervaluation_candidate_power) = S ((S (S bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_successor. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (bpvi_successor_pvs_prioritylayervaluation_candidate_power))) /\ bpvi_successor_pvs_prioritylayervaluation_candidate_power = bpvi_partial_pvs_prioritylayervaluation_candidate_power * bpvi_factor_pvs_prioritylayervaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayervaluation_candidate. (n) = bpvi_result_pvs_prioritylayervaluation_candidate * bpvi_divisor_factor_pvs_prioritylayervaluation_candidate)) -> (exists bpd_gap_pvs_prioritylayervaluation_maximal. bpd_gap_pvs_prioritylayervaluation_maximal + (bpd_candidate_pvs_prioritylayervaluation) = (ppf_exponent_prioritylayer))) -> (exists pvs_factor_prioritylayerdivides. (ppf_exponent_prioritylayer) = ((k)) * pvs_factor_prioritylayerdivides)

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