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
¬L = 0 ∧ (BetaPrefixInto(b,c,L,p) ∧ BetaAt(b,c,0,1))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((~(((L)) = 0)) /\ (((forall fom_index_pfp_polynomial_division_definitioncoefficients. (exists fom_gap_pfp_polynomial_division_definitioncoefficients_index_bound. fom_gap_pfp_polynomial_division_definitioncoefficients_index_bound + S (fom_index_pfp_polynomial_division_definitioncoefficients) = (L)) -> exists fom_value_pfp_polynomial_division_definitioncoefficients. ((((exists fom_beta_height_pfp_polynomial_division_definitioncoefficients_entry. fom_beta_height_pfp_polynomial_division_definitioncoefficients_entry + S (fom_value_pfp_polynomial_division_definitioncoefficients) = S ((S (fom_index_pfp_polynomial_division_definitioncoefficients)) * (c))) /\ exists fom_beta_quotient_pfp_polynomial_division_definitioncoefficients_entry. (b) = fom_beta_quotient_pfp_polynomial_division_definitioncoefficients_entry * S ((S (fom_index_pfp_polynomial_division_definitioncoefficients)) * (c)) + (fom_value_pfp_polynomial_division_definitioncoefficients))) /\ (exists fom_gap_pfp_polynomial_division_definitioncoefficients_value_bound. fom_gap_pfp_polynomial_division_definitioncoefficients_value_bound + S (fom_value_pfp_polynomial_division_definitioncoefficients) = (p)))) /\ ((((exists ff_h_pfp_polynomial_division_definitionleading. ff_h_pfp_polynomial_division_definitionleading + S (1) = S ((S (0)) * (c))) /\ exists ff_q_pfp_polynomial_division_definitionleading. (b) = ff_q_pfp_polynomial_division_definitionleading * S ((S (0)) * (c)) + (1)))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.