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
∃ mdr_a_secondwave. ∃ mdr_b_secondwave. ∃ mdr_c_secondwave. ∃ mdr_e_secondwave. ∃ mdr_f_secondwave. mdr_a_secondwave = (d + pb) · S (d + pb) + (pb + pb) ∧ (mdr_b_secondwave = (pc + nb) · S (pc + nb) + (nb + nb) ∧ (mdr_c_secondwave = (mdr_a_secondwave + mdr_b_secondwave) · S (mdr_a_secondwave + mdr_b_secondwave) + (mdr_b_secondwave + mdr_b_secondwave) ∧ (mdr_e_secondwave = (p + n) · S (p + n) + (n + n) ∧ (mdr_f_secondwave = (nc + mdr_e_secondwave) · S (nc + mdr_e_secondwave) + (mdr_e_secondwave + mdr_e_secondwave) ∧ z = (mdr_c_secondwave + mdr_f_secondwave) · S (mdr_c_secondwave + mdr_f_secondwave) + (mdr_f_secondwave + mdr_f_secondwave)))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists mdr_a_secondwave mdr_b_secondwave mdr_c_secondwave mdr_e_secondwave mdr_f_secondwave. ((mdr_a_secondwave = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_secondwave = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_secondwave = ((mdr_a_secondwave) + (mdr_b_secondwave)) * S ((mdr_a_secondwave) + (mdr_b_secondwave)) + ((mdr_b_secondwave) + (mdr_b_secondwave))) /\ ((mdr_e_secondwave = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_secondwave = ((nc) + (mdr_e_secondwave)) * S ((nc) + (mdr_e_secondwave)) + ((mdr_e_secondwave) + (mdr_e_secondwave))) /\ ((z) = ((mdr_c_secondwave) + (mdr_f_secondwave)) * S ((mdr_c_secondwave) + (mdr_f_secondwave)) + ((mdr_f_secondwave) + (mdr_f_secondwave))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only