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
∀ pvs_divisor_prioritylayer. Prime(pvs_divisor_prioritylayer) → Dvd(pvs_divisor_prioritylayer,n) → ∃ x. Lt(x,l) ∧ BetaAt(pb,pc,x,pvs_divisor_prioritylayer)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall pvs_divisor_prioritylayer. (~((pvs_divisor_prioritylayer) = 1) /\ forall pvs_left_prioritylayerprime pvs_right_prioritylayerprime. (pvs_divisor_prioritylayer) = pvs_left_prioritylayerprime * pvs_right_prioritylayerprime -> pvs_left_prioritylayerprime = 1 \/ pvs_right_prioritylayerprime = 1) -> (exists pvs_factor_prioritylayerdivides. ((n)) = (pvs_divisor_prioritylayer) * pvs_factor_prioritylayerdivides) -> exists pvs_position_prioritylayer. (exists pvs_gap_prioritylayerbound. pvs_gap_prioritylayerbound + S (pvs_position_prioritylayer) = ((l))) /\ (((exists ff_h_pvs_prioritylayerentry. ff_h_pvs_prioritylayerentry + S (pvs_divisor_prioritylayer) = S ((S (pvs_position_prioritylayer)) * (pc))) /\ exists ff_q_pvs_prioritylayerentry. (pb) = ff_q_pvs_prioritylayerentry * S ((S (pvs_position_prioritylayer)) * (pc)) + (pvs_divisor_prioritylayer)))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
Checked theorems using this definition
none directly; see definition consumers