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
∀ eut_index_prioritylayer. Lt(eut_index_prioritylayer,l) → ∃ x. BetaAt(b,c,eut_index_prioritylayer,x) ∧ (Coprime(eut_index_prioritylayer,n) ∧ x = 1 ∨ ¬Coprime(eut_index_prioritylayer,n) ∧ x = 0)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall eut_index_prioritylayer. (exists eut_gap_prioritylayer_bound. eut_gap_prioritylayer_bound + S (eut_index_prioritylayer) = (l)) -> exists eut_bit_prioritylayer. (((exists fs_h_eut_prioritylayer_entry. fs_h_eut_prioritylayer_entry + S (eut_bit_prioritylayer) = S ((S (eut_index_prioritylayer)) * c)) /\ exists fs_q_eut_prioritylayer_entry. b = fs_q_eut_prioritylayer_entry * S ((S (eut_index_prioritylayer)) * c) + (eut_bit_prioritylayer))) /\ ((((forall eut_divisor_prioritylayer_choice_coprime. (exists eut_left_prioritylayer_choice_coprime. (eut_index_prioritylayer) = eut_divisor_prioritylayer_choice_coprime * eut_left_prioritylayer_choice_coprime) -> (exists eut_right_prioritylayer_choice_coprime. (n) = eut_divisor_prioritylayer_choice_coprime * eut_right_prioritylayer_choice_coprime) -> eut_divisor_prioritylayer_choice_coprime = 1) /\ (eut_bit_prioritylayer) = 1) \/ (~(forall eut_divisor_prioritylayer_choice_coprime. (exists eut_left_prioritylayer_choice_coprime. (eut_index_prioritylayer) = eut_divisor_prioritylayer_choice_coprime * eut_left_prioritylayer_choice_coprime) -> (exists eut_right_prioritylayer_choice_coprime. (n) = eut_divisor_prioritylayer_choice_coprime * eut_right_prioritylayer_choice_coprime) -> eut_divisor_prioritylayer_choice_coprime = 1) /\ (eut_bit_prioritylayer) = 0)))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.