Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
∀ mdr_i_secondwave. Lt(mdr_i_secondwave,l) → BetaAt(b,c,mdr_i_secondwave,mdr_i_secondwave)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall mdr_i_secondwave. (exists mdr_gap_secondwavebound. mdr_gap_secondwavebound + S (mdr_i_secondwave) = (l)) -> (((exists ff_h_mdr_secondwaveentry. ff_h_mdr_secondwaveentry + S (mdr_i_secondwave) = S ((S (mdr_i_secondwave)) * c)) /\ exists ff_q_mdr_secondwaveentry. b = ff_q_mdr_secondwaveentry * S ((S (mdr_i_secondwave)) * c) + (mdr_i_secondwave)))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.