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
∀ pftrim_index_polynomial_division_definition. ∀ pftrim_value_polynomial_division_definition. Lt(pftrim_index_polynomial_division_definition,M) → BetaAt(b,c,t + pftrim_index_polynomial_division_definition,pftrim_value_polynomial_division_definition) → BetaAt(d,e,pftrim_index_polynomial_division_definition,pftrim_value_polynomial_division_definition)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall pftrim_index_polynomial_division_definition pftrim_value_polynomial_division_definition. (exists pfa_gap_polynomial_division_definitionbound. pfa_gap_polynomial_division_definitionbound + S (pftrim_index_polynomial_division_definition) = ((M))) -> (((exists ff_h_pfp_polynomial_division_definitionsource. ff_h_pfp_polynomial_division_definitionsource + S (pftrim_value_polynomial_division_definition) = S ((S (((t))+pftrim_index_polynomial_division_definition)) * (c))) /\ exists ff_q_pfp_polynomial_division_definitionsource. (b) = ff_q_pfp_polynomial_division_definitionsource * S ((S (((t))+pftrim_index_polynomial_division_definition)) * (c)) + (pftrim_value_polynomial_division_definition))) -> (((exists ff_h_pfp_polynomial_division_definitionoutput. ff_h_pfp_polynomial_division_definitionoutput + S (pftrim_value_polynomial_division_definition) = S ((S (pftrim_index_polynomial_division_definition)) * (e))) /\ exists ff_q_pfp_polynomial_division_definitionoutput. (d) = ff_q_pfp_polynomial_division_definitionoutput * S ((S (pftrim_index_polynomial_division_definition)) * (e)) + (pftrim_value_polynomial_division_definition)))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.