Phi(n,t)

(~((n)=0) /\ (exists eut_code_prioritylayer_count eut_scale_prioritylayer_count. (forall eut_index_prioritylayer_count_mask. (exists eut_gap_prioritylayer_count_mask_bound. eut_gap_prioritylayer_count_mask_bound + S (eut_index_prioritylayer_count_mask) = (n)) -> exists eut_bit_prioritylayer_count_mask. (((exists fs_h_eut_prioritylayer_count_mask_entry. fs_h_eut_prioritylayer_count_mask_entry + S (eut_bit_prioritylayer_count_mask) = S ((S (eut_index_prioritylayer_count_mask)) * eut_scale_prioritylayer_count)) /\ exists fs_q_eut_prioritylayer_count_mask_entry. eut_code_prioritylayer_count = fs_q_eut_prioritylayer_count_mask_entry * S ((S (eut_index_prioritylayer_count_mask)) * eut_scale_prioritylayer_count) + (eut_bit_prioritylayer_count_mask))) /\ ((((forall eut_divisor_prioritylayer_count_mask_choice_coprime. (exists eut_left_prioritylayer_count_mask_choice_coprime. (eut_index_prioritylayer_count_mask) = eut_divisor_prioritylayer_count_mask_choice_coprime * eut_left_prioritylayer_count_mask_choice_coprime) -> (exists eut_right_prioritylayer_count_mask_choice_coprime. (n) = eut_divisor_prioritylayer_count_mask_choice_coprime * eut_right_prioritylayer_count_mask_choice_coprime) -> eut_divisor_prioritylayer_count_mask_choice_coprime = 1) /\ (eut_bit_prioritylayer_count_mask) = 1) \/ (~(forall eut_divisor_prioritylayer_count_mask_choice_coprime. (exists eut_left_prioritylayer_count_mask_choice_coprime. (eut_index_prioritylayer_count_mask) = eut_divisor_prioritylayer_count_mask_choice_coprime * eut_left_prioritylayer_count_mask_choice_coprime) -> (exists eut_right_prioritylayer_count_mask_choice_coprime. (n) = eut_divisor_prioritylayer_count_mask_choice_coprime * eut_right_prioritylayer_count_mask_choice_coprime) -> eut_divisor_prioritylayer_count_mask_choice_coprime = 1) /\ (eut_bit_prioritylayer_count_mask) = 0)))) /\ (exists fs_u_eut_prioritylayer_count_sum fs_v_eut_prioritylayer_count_sum. ((((exists fs_h_eut_prioritylayer_count_sum_body_start. fs_h_eut_prioritylayer_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_prioritylayer_count_sum)) /\ exists fs_q_eut_prioritylayer_count_sum_body_start. fs_u_eut_prioritylayer_count_sum = fs_q_eut_prioritylayer_count_sum_body_start * S ((S (0)) * fs_v_eut_prioritylayer_count_sum) + (0))) /\ ((((exists fs_h_eut_prioritylayer_count_sum_body_terminal. fs_h_eut_prioritylayer_count_sum_body_terminal + S (t) = S ((S (n)) * fs_v_eut_prioritylayer_count_sum)) /\ exists fs_q_eut_prioritylayer_count_sum_body_terminal. fs_u_eut_prioritylayer_count_sum = fs_q_eut_prioritylayer_count_sum_body_terminal * S ((S (n)) * fs_v_eut_prioritylayer_count_sum) + (t))) /\ forall fs_i_eut_prioritylayer_count_sum_body_steps. (exists fs_lt_eut_prioritylayer_count_sum_body_steps_bound. fs_lt_eut_prioritylayer_count_sum_body_steps_bound + S fs_i_eut_prioritylayer_count_sum_body_steps = n) -> exists fs_a_eut_prioritylayer_count_sum_body_steps fs_r_eut_prioritylayer_count_sum_body_steps fs_s_eut_prioritylayer_count_sum_body_steps. ((((exists fs_h_eut_prioritylayer_count_sum_body_steps_summand. fs_h_eut_prioritylayer_count_sum_body_steps_summand + S (fs_a_eut_prioritylayer_count_sum_body_steps) = S ((S (fs_i_eut_prioritylayer_count_sum_body_steps)) * eut_scale_prioritylayer_count)) /\ exists fs_q_eut_prioritylayer_count_sum_body_steps_summand. eut_code_prioritylayer_count = fs_q_eut_prioritylayer_count_sum_body_steps_summand * S ((S (fs_i_eut_prioritylayer_count_sum_body_steps)) * eut_scale_prioritylayer_count) + (fs_a_eut_prioritylayer_count_sum_body_steps))) /\ ((((exists fs_h_eut_prioritylayer_count_sum_body_steps_partial. fs_h_eut_prioritylayer_count_sum_body_steps_partial + S (fs_r_eut_prioritylayer_count_sum_body_steps) = S ((S (fs_i_eut_prioritylayer_count_sum_body_steps)) * fs_v_eut_prioritylayer_count_sum)) /\ exists fs_q_eut_prioritylayer_count_sum_body_steps_partial. fs_u_eut_prioritylayer_count_sum = fs_q_eut_prioritylayer_count_sum_body_steps_partial * S ((S (fs_i_eut_prioritylayer_count_sum_body_steps)) * fs_v_eut_prioritylayer_count_sum) + (fs_r_eut_prioritylayer_count_sum_body_steps))) /\ ((((exists fs_h_eut_prioritylayer_count_sum_body_steps_successor. fs_h_eut_prioritylayer_count_sum_body_steps_successor + S (fs_s_eut_prioritylayer_count_sum_body_steps) = S ((S (S fs_i_eut_prioritylayer_count_sum_body_steps)) * fs_v_eut_prioritylayer_count_sum)) /\ exists fs_q_eut_prioritylayer_count_sum_body_steps_successor. fs_u_eut_prioritylayer_count_sum = fs_q_eut_prioritylayer_count_sum_body_steps_successor * S ((S (S fs_i_eut_prioritylayer_count_sum_body_steps)) * fs_v_eut_prioritylayer_count_sum) + (fs_s_eut_prioritylayer_count_sum_body_steps))) /\ fs_s_eut_prioritylayer_count_sum_body_steps = fs_r_eut_prioritylayer_count_sum_body_steps + fs_a_eut_prioritylayer_count_sum_body_steps))))))))

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