Definition in prerequisite notation
∀ mdr_i_pfp_lowertier. ∀ mdr_a_pfp_lowertier. Lt(mdr_i_pfp_lowertier,l) → BetaAt(b,c,mdr_i_pfp_lowertier,mdr_a_pfp_lowertier) → BetaAt(d,e,mdr_i_pfp_lowertier,mdr_a_pfp_lowertier)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall mdr_i_pfp_lowertier mdr_a_pfp_lowertier. (exists mdr_gap_pfp_lowertierb. mdr_gap_pfp_lowertierb + S (mdr_i_pfp_lowertier) = ((l))) -> (((exists ff_h_mdr_pfp_lowertiero. ff_h_mdr_pfp_lowertiero + S (mdr_a_pfp_lowertier) = S ((S (mdr_i_pfp_lowertier)) * (c))) /\ exists ff_q_mdr_pfp_lowertiero. (b) = ff_q_mdr_pfp_lowertiero * S ((S (mdr_i_pfp_lowertier)) * (c)) + (mdr_a_pfp_lowertier))) -> (((exists ff_h_mdr_pfp_lowertiern. ff_h_mdr_pfp_lowertiern + S (mdr_a_pfp_lowertier) = S ((S (mdr_i_pfp_lowertier)) * (e))) /\ exists ff_q_mdr_pfp_lowertiern. (d) = ff_q_mdr_pfp_lowertiern * S ((S (mdr_i_pfp_lowertier)) * (e)) + (mdr_a_pfp_lowertier)))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
Checked theorems using this definition
PP0005 · prime_field_polynomial_normalization_functionalPP0007 · prime_field_polynomial_normalization_transportPP0008 · prime_field_polynomial_normalization_idempotentPP0010 · prime_field_polynomial_add_functionalPP0011 · prime_field_polynomial_add_transportPP0018 · prime_field_polynomial_scale_functionalPP0019 · prime_field_polynomial_scale_transportPP001C · prime_field_polynomial_add_associativePP001D · prime_field_polynomial_scale_associativePP001E · prime_field_polynomial_scale_distributes_over_addPP001F · prime_field_polynomial_scalar_add_distributesPP0026 · prime_field_polynomial_horner_transport