Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
∃ cor_terminal_a_secondwave. ∃ cor_terminal_u_secondwave. ∃ cor_initial_q_secondwave. CornacchiaStateAt(h,e,0,cor_terminal_a_secondwave,R,cor_terminal_u_secondwave,T,0) ∧ (CornacchiaStateAt(h,e,l,a,r,u,t,cor_initial_q_secondwave) ∧ (¬R = 0 ∧ (¬T = 0 ∧ (Lt(R · R,p) ∧ (∀ x. Lt(x,l) → CornacchiaTransitionAt(p,h,e,x))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists cor_terminal_a_secondwave cor_terminal_u_secondwave cor_initial_q_secondwave. (((((exists ff_h_cor_secondwave_terminal. ff_h_cor_secondwave_terminal + S (((((cor_terminal_a_secondwave) + (R)) * S ((cor_terminal_a_secondwave) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) * S ((((cor_terminal_a_secondwave) + (R)) * S ((cor_terminal_a_secondwave) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) + ((((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))) + (((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cor_secondwave_terminal. h = ff_q_cor_secondwave_terminal * S ((S (0)) * e) + (((((cor_terminal_a_secondwave) + (R)) * S ((cor_terminal_a_secondwave) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) * S ((((cor_terminal_a_secondwave) + (R)) * S ((cor_terminal_a_secondwave) + (R)) + ((R) + (R))) + (((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0)))) + ((((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))) + (((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) * S ((((cor_terminal_u_secondwave) + (T)) * S ((cor_terminal_u_secondwave) + (T)) + ((T) + (T))) + (0)) + ((0) + (0))))))) /\ (((((exists ff_h_cor_secondwave_initial. ff_h_cor_secondwave_initial + S (((((a) + (r)) * S ((a) + (r)) + ((r) + (r))) + (((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave)))) * S ((((a) + (r)) * S ((a) + (r)) + ((r) + (r))) + (((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave)))) + ((((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave))) + (((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave))))) = S ((S (l)) * e)) /\ exists ff_q_cor_secondwave_initial. h = ff_q_cor_secondwave_initial * S ((S (l)) * e) + (((((a) + (r)) * S ((a) + (r)) + ((r) + (r))) + (((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave)))) * S ((((a) + (r)) * S ((a) + (r)) + ((r) + (r))) + (((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave)))) + ((((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave))) + (((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) * S ((((u) + (t)) * S ((u) + (t)) + ((t) + (t))) + (cor_initial_q_secondwave)) + ((cor_initial_q_secondwave) + (cor_initial_q_secondwave))))))) /\ (((~(R = 0)) /\ (((~(T = 0)) /\ (((exists cor_gap_secondwave_stop. cor_gap_secondwave_stop + S (R * R) = (p)) /\ (forall cor_index_secondwave. (exists cor_gap_secondwave_index. cor_gap_secondwave_index + S (cor_index_secondwave) = (l)) -> (exists cor_a_secondwave_step cor_r_secondwave_step cor_u_secondwave_step cor_t_secondwave_step cor_q_secondwave_step cor_next_a_secondwave_step cor_next_r_secondwave_step cor_next_u_secondwave_step cor_next_t_secondwave_step cor_next_q_secondwave_step. (((((exists ff_h_cor_secondwave_step_before. ff_h_cor_secondwave_step_before + S (((((cor_a_secondwave_step) + (cor_r_secondwave_step)) * S ((cor_a_secondwave_step) + (cor_r_secondwave_step)) + ((cor_r_secondwave_step) + (cor_r_secondwave_step))) + (((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step)))) * S ((((cor_a_secondwave_step) + (cor_r_secondwave_step)) * S ((cor_a_secondwave_step) + (cor_r_secondwave_step)) + ((cor_r_secondwave_step) + (cor_r_secondwave_step))) + (((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step)))) + ((((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step))) + (((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step))))) = S ((S (S cor_index_secondwave)) * e)) /\ exists ff_q_cor_secondwave_step_before. h = ff_q_cor_secondwave_step_before * S ((S (S cor_index_secondwave)) * e) + (((((cor_a_secondwave_step) + (cor_r_secondwave_step)) * S ((cor_a_secondwave_step) + (cor_r_secondwave_step)) + ((cor_r_secondwave_step) + (cor_r_secondwave_step))) + (((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step)))) * S ((((cor_a_secondwave_step) + (cor_r_secondwave_step)) * S ((cor_a_secondwave_step) + (cor_r_secondwave_step)) + ((cor_r_secondwave_step) + (cor_r_secondwave_step))) + (((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step)))) + ((((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step))) + (((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) * S ((((cor_u_secondwave_step) + (cor_t_secondwave_step)) * S ((cor_u_secondwave_step) + (cor_t_secondwave_step)) + ((cor_t_secondwave_step) + (cor_t_secondwave_step))) + (cor_q_secondwave_step)) + ((cor_q_secondwave_step) + (cor_q_secondwave_step))))))) /\ (((((exists ff_h_cor_secondwave_step_after. ff_h_cor_secondwave_step_after + S (((((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) * S ((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) + ((cor_next_r_secondwave_step) + (cor_next_r_secondwave_step))) + (((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step)))) * S ((((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) * S ((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) + ((cor_next_r_secondwave_step) + (cor_next_r_secondwave_step))) + (((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step)))) + ((((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step))) + (((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step))))) = S ((S (cor_index_secondwave)) * e)) /\ exists ff_q_cor_secondwave_step_after. h = ff_q_cor_secondwave_step_after * S ((S (cor_index_secondwave)) * e) + (((((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) * S ((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) + ((cor_next_r_secondwave_step) + (cor_next_r_secondwave_step))) + (((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step)))) * S ((((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) * S ((cor_next_a_secondwave_step) + (cor_next_r_secondwave_step)) + ((cor_next_r_secondwave_step) + (cor_next_r_secondwave_step))) + (((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step)))) + ((((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step))) + (((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) * S ((((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) * S ((cor_next_u_secondwave_step) + (cor_next_t_secondwave_step)) + ((cor_next_t_secondwave_step) + (cor_next_t_secondwave_step))) + (cor_next_q_secondwave_step)) + ((cor_next_q_secondwave_step) + (cor_next_q_secondwave_step))))))) /\ (((cor_next_a_secondwave_step = cor_r_secondwave_step) /\ (((cor_next_u_secondwave_step = cor_t_secondwave_step) /\ (((cor_a_secondwave_step = cor_r_secondwave_step * cor_q_secondwave_step + cor_next_r_secondwave_step) /\ (((exists cor_gap_secondwave_step_remainder. cor_gap_secondwave_step_remainder + S (cor_next_r_secondwave_step) = (cor_r_secondwave_step)) /\ (((cor_next_t_secondwave_step = cor_q_secondwave_step * cor_t_secondwave_step + cor_u_secondwave_step) /\ (exists cor_gap_secondwave_step_guard. cor_gap_secondwave_step_guard + S (p) = (cor_r_secondwave_step * cor_r_secondwave_step))))))))))))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.