CornacchiaTrace(p,z,R,T,h,e,l)

(((((~(p = 1) /\ forall frm_prime_left_cor_secondwave_root_prime frm_prime_right_cor_secondwave_root_prime. p = frm_prime_left_cor_secondwave_root_prime * frm_prime_right_cor_secondwave_root_prime -> frm_prime_left_cor_secondwave_root_prime = 1 \/ frm_prime_right_cor_secondwave_root_prime = 1)) /\ (((~(z = 0)) /\ (((exists cor_gap_secondwave_root_bound. cor_gap_secondwave_root_bound + S (z) = (p)) /\ (exists cor_factor_secondwave_root. z * z + 1 = p * cor_factor_secondwave_root))))))) /\ (exists cor_terminal_a_secondwave_run cor_terminal_u_secondwave_run cor_initial_q_secondwave_run. (((((exists ff_h_cor_secondwave_run_terminal. ff_h_cor_secondwave_run_terminal + S (((((cor_terminal_a_secondwave_run) + (R)) * S ((cor_terminal_a_secondwave_run) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) * S ((((cor_terminal_a_secondwave_run) + (R)) * S ((cor_terminal_a_secondwave_run) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) + ((((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))) + (((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cor_secondwave_run_terminal. h = ff_q_cor_secondwave_run_terminal * S ((S (0)) * e) + (((((cor_terminal_a_secondwave_run) + (R)) * S ((cor_terminal_a_secondwave_run) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) * S ((((cor_terminal_a_secondwave_run) + (R)) * S ((cor_terminal_a_secondwave_run) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) + ((((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))) + (((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave_run) + (T)) * S ((cor_terminal_u_secondwave_run) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))))))) /\ (((((exists ff_h_cor_secondwave_run_initial. ff_h_cor_secondwave_run_initial + S (((((p) + (z)) * S ((p) + (z)) + ((z) + (z))) + (((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run)))) * S ((((p) + (z)) * S ((p) + (z)) + ((z) + (z))) + (((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run)))) + ((((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run))) + (((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run))))) = S ((S (l)) * e)) /\ exists ff_q_cor_secondwave_run_initial. h = ff_q_cor_secondwave_run_initial * S ((S (l)) * e) + (((((p) + (z)) * S ((p) + (z)) + ((z) + (z))) + (((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run)))) * S ((((p) + (z)) * S ((p) + (z)) + ((z) + (z))) + (((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run)))) + ((((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run))) + (((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) * S ((((0) + (1)) * S ((0) + (1)) + ((1) + (1))) + (cor_initial_q_secondwave_run)) + ((cor_initial_q_secondwave_run) + (cor_initial_q_secondwave_run))))))) /\ (((~(R = 0)) /\ (((~(T = 0)) /\ (((exists cor_gap_secondwave_run_stop. cor_gap_secondwave_run_stop + S (R * R) = (p)) /\ (forall cor_index_secondwave_run. (exists cor_gap_secondwave_run_index. cor_gap_secondwave_run_index + S (cor_index_secondwave_run) = (l)) -> (exists cor_a_secondwave_run_step cor_r_secondwave_run_step cor_u_secondwave_run_step cor_t_secondwave_run_step cor_q_secondwave_run_step cor_next_a_secondwave_run_step cor_next_r_secondwave_run_step cor_next_u_secondwave_run_step cor_next_t_secondwave_run_step cor_next_q_secondwave_run_step. (((((exists ff_h_cor_secondwave_run_step_before. ff_h_cor_secondwave_run_step_before + S (((((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) * S ((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) + ((cor_r_secondwave_run_step) + (cor_r_secondwave_run_step))) + (((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step)))) * S ((((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) * S ((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) + ((cor_r_secondwave_run_step) + (cor_r_secondwave_run_step))) + (((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step)))) + ((((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step))) + (((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step))))) = S ((S (S cor_index_secondwave_run)) * e)) /\ exists ff_q_cor_secondwave_run_step_before. h = ff_q_cor_secondwave_run_step_before * S ((S (S cor_index_secondwave_run)) * e) + (((((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) * S ((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) + ((cor_r_secondwave_run_step) + (cor_r_secondwave_run_step))) + (((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step)))) * S ((((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) * S ((cor_a_secondwave_run_step) + (cor_r_secondwave_run_step)) + ((cor_r_secondwave_run_step) + (cor_r_secondwave_run_step))) + (((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step)))) + ((((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step))) + (((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) * S ((((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) * S ((cor_u_secondwave_run_step) + (cor_t_secondwave_run_step)) + ((cor_t_secondwave_run_step) + (cor_t_secondwave_run_step))) + (cor_q_secondwave_run_step)) + ((cor_q_secondwave_run_step) + (cor_q_secondwave_run_step))))))) /\ (((((exists ff_h_cor_secondwave_run_step_after. ff_h_cor_secondwave_run_step_after + S (((((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) * S ((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) + ((cor_next_r_secondwave_run_step) + (cor_next_r_secondwave_run_step))) + (((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step)))) * S ((((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) * S ((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) + ((cor_next_r_secondwave_run_step) + (cor_next_r_secondwave_run_step))) + (((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step)))) + ((((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step))) + (((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step))))) = S ((S (cor_index_secondwave_run)) * e)) /\ exists ff_q_cor_secondwave_run_step_after. h = ff_q_cor_secondwave_run_step_after * S ((S (cor_index_secondwave_run)) * e) + (((((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) * S ((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) + ((cor_next_r_secondwave_run_step) + (cor_next_r_secondwave_run_step))) + (((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step)))) * S ((((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) * S ((cor_next_a_secondwave_run_step) + (cor_next_r_secondwave_run_step)) + ((cor_next_r_secondwave_run_step) + (cor_next_r_secondwave_run_step))) + (((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step)))) + ((((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step))) + (((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) * S ((((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) * S ((cor_next_u_secondwave_run_step) + (cor_next_t_secondwave_run_step)) + ((cor_next_t_secondwave_run_step) + (cor_next_t_secondwave_run_step))) + (cor_next_q_secondwave_run_step)) + ((cor_next_q_secondwave_run_step) + (cor_next_q_secondwave_run_step))))))) /\ (((cor_next_a_secondwave_run_step = cor_r_secondwave_run_step) /\ (((cor_next_u_secondwave_run_step = cor_t_secondwave_run_step) /\ (((cor_a_secondwave_run_step = cor_r_secondwave_run_step * cor_q_secondwave_run_step + cor_next_r_secondwave_run_step) /\ (((exists cor_gap_secondwave_run_step_remainder. cor_gap_secondwave_run_step_remainder + S (cor_next_r_secondwave_run_step) = (cor_r_secondwave_run_step)) /\ (((cor_next_t_secondwave_run_step = cor_q_secondwave_run_step * cor_t_secondwave_run_step + cor_u_secondwave_run_step) /\ (exists cor_gap_secondwave_run_step_guard. cor_gap_secondwave_run_step_guard + S (p) = (cor_r_secondwave_run_step * cor_r_secondwave_run_step))))))))))))))))))))))))))))))

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