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
(∀ x. ∀ y. Lt(x,d · d) → BetaAt(pb,pc,x,y) → BetaAt(qb,qc,x,y)) ∧ (∀ x. ∀ y. Lt(x,d · d) → BetaAt(nb,nc,x,y) → BetaAt(rb,rc,x,y))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((forall mdr_i_secondwavep mdr_a_secondwavep. (exists mdr_gap_secondwavepb. mdr_gap_secondwavepb + S (mdr_i_secondwavep) = ((d) * (d))) -> (((exists ff_h_mdr_secondwavepo. ff_h_mdr_secondwavepo + S (mdr_a_secondwavep) = S ((S (mdr_i_secondwavep)) * pc)) /\ exists ff_q_mdr_secondwavepo. pb = ff_q_mdr_secondwavepo * S ((S (mdr_i_secondwavep)) * pc) + (mdr_a_secondwavep))) -> (((exists ff_h_mdr_secondwavepn. ff_h_mdr_secondwavepn + S (mdr_a_secondwavep) = S ((S (mdr_i_secondwavep)) * qc)) /\ exists ff_q_mdr_secondwavepn. qb = ff_q_mdr_secondwavepn * S ((S (mdr_i_secondwavep)) * qc) + (mdr_a_secondwavep)))) /\ (forall mdr_i_secondwaven mdr_a_secondwaven. (exists mdr_gap_secondwavenb. mdr_gap_secondwavenb + S (mdr_i_secondwaven) = ((d) * (d))) -> (((exists ff_h_mdr_secondwaveno. ff_h_mdr_secondwaveno + S (mdr_a_secondwaven) = S ((S (mdr_i_secondwaven)) * nc)) /\ exists ff_q_mdr_secondwaveno. nb = ff_q_mdr_secondwaveno * S ((S (mdr_i_secondwaven)) * nc) + (mdr_a_secondwaven))) -> (((exists ff_h_mdr_secondwavenn. ff_h_mdr_secondwavenn + S (mdr_a_secondwaven) = S ((S (mdr_i_secondwaven)) * rc)) /\ exists ff_q_mdr_secondwavenn. rb = ff_q_mdr_secondwavenn * S ((S (mdr_i_secondwaven)) * rc) + (mdr_a_secondwaven)))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none