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_a_secondwave. ∃ cor_r_secondwave. ∃ cor_u_secondwave. ∃ cor_t_secondwave. ∃ cor_q_secondwave. ∃ cor_next_a_secondwave. ∃ cor_next_r_secondwave. ∃ cor_next_u_secondwave. ∃ cor_next_t_secondwave. ∃ cor_next_q_secondwave. CornacchiaStateAt(h,e,S i,cor_a_secondwave,cor_r_secondwave,cor_u_secondwave,cor_t_secondwave,cor_q_secondwave) ∧ (CornacchiaStateAt(h,e,i,cor_next_a_secondwave,cor_next_r_secondwave,cor_next_u_secondwave,cor_next_t_secondwave,cor_next_q_secondwave) ∧ (cor_next_a_secondwave = cor_r_secondwave ∧ (cor_next_u_secondwave = cor_t_secondwave ∧ (cor_a_secondwave = cor_r_secondwave · cor_q_secondwave + cor_next_r_secondwave ∧ (Lt(cor_next_r_secondwave,cor_r_secondwave) ∧ (cor_next_t_secondwave = cor_q_secondwave · cor_t_secondwave + cor_u_secondwave ∧ Lt(p,cor_r_secondwave · cor_r_secondwave)))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists cor_a_secondwave cor_r_secondwave cor_u_secondwave cor_t_secondwave cor_q_secondwave cor_next_a_secondwave cor_next_r_secondwave cor_next_u_secondwave cor_next_t_secondwave cor_next_q_secondwave. (((((exists ff_h_cor_secondwave_before. ff_h_cor_secondwave_before + S (((((cor_a_secondwave) + (cor_r_secondwave)) * S ((cor_a_secondwave) + (cor_r_secondwave)) + ((cor_r_secondwave) + (cor_r_secondwave))) + (((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave)))) * S ((((cor_a_secondwave) + (cor_r_secondwave)) * S ((cor_a_secondwave) + (cor_r_secondwave)) + ((cor_r_secondwave) + (cor_r_secondwave))) + (((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave)))) + ((((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave))) + (((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave))))) = S ((S (S i)) * e)) /\ exists ff_q_cor_secondwave_before. h = ff_q_cor_secondwave_before * S ((S (S i)) * e) + (((((cor_a_secondwave) + (cor_r_secondwave)) * S ((cor_a_secondwave) + (cor_r_secondwave)) + ((cor_r_secondwave) + (cor_r_secondwave))) + (((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave)))) * S ((((cor_a_secondwave) + (cor_r_secondwave)) * S ((cor_a_secondwave) + (cor_r_secondwave)) + ((cor_r_secondwave) + (cor_r_secondwave))) + (((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave)))) + ((((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave))) + (((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) * S ((((cor_u_secondwave) + (cor_t_secondwave)) * S ((cor_u_secondwave) + (cor_t_secondwave)) + ((cor_t_secondwave) + (cor_t_secondwave))) + (cor_q_secondwave)) + ((cor_q_secondwave) + (cor_q_secondwave))))))) /\ (((((exists ff_h_cor_secondwave_after. ff_h_cor_secondwave_after + S (((((cor_next_a_secondwave) + (cor_next_r_secondwave)) * S ((cor_next_a_secondwave) + (cor_next_r_secondwave)) + ((cor_next_r_secondwave) + (cor_next_r_secondwave))) + (((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave)))) * S ((((cor_next_a_secondwave) + (cor_next_r_secondwave)) * S ((cor_next_a_secondwave) + (cor_next_r_secondwave)) + ((cor_next_r_secondwave) + (cor_next_r_secondwave))) + (((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave)))) + ((((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave))) + (((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave))))) = S ((S (i)) * e)) /\ exists ff_q_cor_secondwave_after. h = ff_q_cor_secondwave_after * S ((S (i)) * e) + (((((cor_next_a_secondwave) + (cor_next_r_secondwave)) * S ((cor_next_a_secondwave) + (cor_next_r_secondwave)) + ((cor_next_r_secondwave) + (cor_next_r_secondwave))) + (((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave)))) * S ((((cor_next_a_secondwave) + (cor_next_r_secondwave)) * S ((cor_next_a_secondwave) + (cor_next_r_secondwave)) + ((cor_next_r_secondwave) + (cor_next_r_secondwave))) + (((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave)))) + ((((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave))) + (((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) * S ((((cor_next_u_secondwave) + (cor_next_t_secondwave)) * S ((cor_next_u_secondwave) + (cor_next_t_secondwave)) + ((cor_next_t_secondwave) + (cor_next_t_secondwave))) + (cor_next_q_secondwave)) + ((cor_next_q_secondwave) + (cor_next_q_secondwave))))))) /\ (((cor_next_a_secondwave = cor_r_secondwave) /\ (((cor_next_u_secondwave = cor_t_secondwave) /\ (((cor_a_secondwave = cor_r_secondwave * cor_q_secondwave + cor_next_r_secondwave) /\ (((exists cor_gap_secondwave_remainder. cor_gap_secondwave_remainder + S (cor_next_r_secondwave) = (cor_r_secondwave)) /\ (((cor_next_t_secondwave = cor_q_secondwave * cor_t_secondwave + cor_u_secondwave) /\ (exists cor_gap_secondwave_guard. cor_gap_secondwave_guard + S (p) = (cor_r_secondwave * cor_r_secondwave))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.