PrimeCount(x,z)

exists pc_code_secondwave pc_scale_secondwave. (forall pc_index_secondwave_mask. (exists pc_lt_secondwave_mask_bound. pc_lt_secondwave_mask_bound + S (pc_index_secondwave_mask) = (x)) -> exists pc_bit_secondwave_mask. (((exists fs_h_pc_secondwave_mask_entry. fs_h_pc_secondwave_mask_entry + S (pc_bit_secondwave_mask) = S ((S (pc_index_secondwave_mask)) * pc_scale_secondwave)) /\ exists fs_q_pc_secondwave_mask_entry. pc_code_secondwave = fs_q_pc_secondwave_mask_entry * S ((S (pc_index_secondwave_mask)) * pc_scale_secondwave) + (pc_bit_secondwave_mask))) /\ (((((~(S (pc_index_secondwave_mask) = 1) /\ forall bpr_left_pc_secondwave_mask_choice_prime bpr_right_pc_secondwave_mask_choice_prime. S (pc_index_secondwave_mask) = bpr_left_pc_secondwave_mask_choice_prime * bpr_right_pc_secondwave_mask_choice_prime -> bpr_left_pc_secondwave_mask_choice_prime = 1 \/ bpr_right_pc_secondwave_mask_choice_prime = 1)) /\ pc_bit_secondwave_mask = 1) \/ (~((~(S (pc_index_secondwave_mask) = 1) /\ forall bpr_left_pc_secondwave_mask_choice_prime bpr_right_pc_secondwave_mask_choice_prime. S (pc_index_secondwave_mask) = bpr_left_pc_secondwave_mask_choice_prime * bpr_right_pc_secondwave_mask_choice_prime -> bpr_left_pc_secondwave_mask_choice_prime = 1 \/ bpr_right_pc_secondwave_mask_choice_prime = 1)) /\ pc_bit_secondwave_mask = 0)))) /\ (exists fs_u_pc_secondwave_sum fs_v_pc_secondwave_sum. ((((exists fs_h_pc_secondwave_sum_body_start. fs_h_pc_secondwave_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_secondwave_sum)) /\ exists fs_q_pc_secondwave_sum_body_start. fs_u_pc_secondwave_sum = fs_q_pc_secondwave_sum_body_start * S ((S (0)) * fs_v_pc_secondwave_sum) + (0))) /\ ((((exists fs_h_pc_secondwave_sum_body_terminal. fs_h_pc_secondwave_sum_body_terminal + S (z) = S ((S (x)) * fs_v_pc_secondwave_sum)) /\ exists fs_q_pc_secondwave_sum_body_terminal. fs_u_pc_secondwave_sum = fs_q_pc_secondwave_sum_body_terminal * S ((S (x)) * fs_v_pc_secondwave_sum) + (z))) /\ forall fs_i_pc_secondwave_sum_body_steps. (exists fs_lt_pc_secondwave_sum_body_steps_bound. fs_lt_pc_secondwave_sum_body_steps_bound + S fs_i_pc_secondwave_sum_body_steps = x) -> exists fs_a_pc_secondwave_sum_body_steps fs_r_pc_secondwave_sum_body_steps fs_s_pc_secondwave_sum_body_steps. ((((exists fs_h_pc_secondwave_sum_body_steps_summand. fs_h_pc_secondwave_sum_body_steps_summand + S (fs_a_pc_secondwave_sum_body_steps) = S ((S (fs_i_pc_secondwave_sum_body_steps)) * pc_scale_secondwave)) /\ exists fs_q_pc_secondwave_sum_body_steps_summand. pc_code_secondwave = fs_q_pc_secondwave_sum_body_steps_summand * S ((S (fs_i_pc_secondwave_sum_body_steps)) * pc_scale_secondwave) + (fs_a_pc_secondwave_sum_body_steps))) /\ ((((exists fs_h_pc_secondwave_sum_body_steps_partial. fs_h_pc_secondwave_sum_body_steps_partial + S (fs_r_pc_secondwave_sum_body_steps) = S ((S (fs_i_pc_secondwave_sum_body_steps)) * fs_v_pc_secondwave_sum)) /\ exists fs_q_pc_secondwave_sum_body_steps_partial. fs_u_pc_secondwave_sum = fs_q_pc_secondwave_sum_body_steps_partial * S ((S (fs_i_pc_secondwave_sum_body_steps)) * fs_v_pc_secondwave_sum) + (fs_r_pc_secondwave_sum_body_steps))) /\ ((((exists fs_h_pc_secondwave_sum_body_steps_successor. fs_h_pc_secondwave_sum_body_steps_successor + S (fs_s_pc_secondwave_sum_body_steps) = S ((S (S fs_i_pc_secondwave_sum_body_steps)) * fs_v_pc_secondwave_sum)) /\ exists fs_q_pc_secondwave_sum_body_steps_successor. fs_u_pc_secondwave_sum = fs_q_pc_secondwave_sum_body_steps_successor * S ((S (S fs_i_pc_secondwave_sum_body_steps)) * fs_v_pc_secondwave_sum) + (fs_s_pc_secondwave_sum_body_steps))) /\ fs_s_pc_secondwave_sum_body_steps = fs_r_pc_secondwave_sum_body_steps + fs_a_pc_secondwave_sum_body_steps))))))

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