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
∀ pfc_index_lowercontinuation. Lt(pfc_index_lowercontinuation,l) → ∃ x. BetaAt(db,dc,pfc_index_lowercontinuation,x) ∧ PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,pfc_index_lowercontinuation,x)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall pfc_index_lowercontinuation. (exists pfa_gap_lowercontinuationbound. pfa_gap_lowercontinuationbound + S (pfc_index_lowercontinuation) = ((l))) -> exists pfc_value_lowercontinuation. ((((exists ff_h_pfp_lowercontinuationentry. ff_h_pfp_lowercontinuationentry + S (pfc_value_lowercontinuation) = S ((S (pfc_index_lowercontinuation)) * (dc))) /\ exists ff_q_pfp_lowercontinuationentry. (db) = ff_q_pfp_lowercontinuationentry * S ((S (pfc_index_lowercontinuation)) * (dc)) + (pfc_value_lowercontinuation))) /\ ((exists pfc_complement_lowercontinuationterm pfc_left_lowercontinuationterm pfc_right_lowercontinuationterm. (((pfc_index_lowercontinuation)+pfc_complement_lowercontinuationterm=((i))) /\ ((((((exists pfa_gap_lowercontinuationtermleftinside. pfa_gap_lowercontinuationtermleftinside + S (pfc_index_lowercontinuation) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationtermleftentry. ff_h_pfp_lowercontinuationtermleftentry + S (pfc_left_lowercontinuationterm) = S ((S (pfc_index_lowercontinuation)) * (ac))) /\ exists ff_q_pfp_lowercontinuationtermleftentry. (ab) = ff_q_pfp_lowercontinuationtermleftentry * S ((S (pfc_index_lowercontinuation)) * (ac)) + (pfc_left_lowercontinuationterm)))))) \/ (((exists pfc_gap_lowercontinuationtermleftoutside. pfc_gap_lowercontinuationtermleftoutside+((L))=(pfc_index_lowercontinuation)) /\ (((pfc_left_lowercontinuationterm)=0))))) /\ ((((((exists pfa_gap_lowercontinuationtermrightinside. pfa_gap_lowercontinuationtermrightinside + S (pfc_complement_lowercontinuationterm) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationtermrightentry. ff_h_pfp_lowercontinuationtermrightentry + S (pfc_right_lowercontinuationterm) = S ((S (pfc_complement_lowercontinuationterm)) * (bc))) /\ exists ff_q_pfp_lowercontinuationtermrightentry. (bb) = ff_q_pfp_lowercontinuationtermrightentry * S ((S (pfc_complement_lowercontinuationterm)) * (bc)) + (pfc_right_lowercontinuationterm)))))) \/ (((exists pfc_gap_lowercontinuationtermrightoutside. pfc_gap_lowercontinuationtermrightoutside+((M))=(pfc_complement_lowercontinuationterm)) /\ (((pfc_right_lowercontinuationterm)=0))))) /\ (((pfc_value_lowercontinuation)=pfc_left_lowercontinuationterm*pfc_right_lowercontinuationterm))))))))))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
PX0002 · polynomial_diagonal_prefix_left_transportPX0007 · polynomial_diagonal_sum_left_appendPX0044 · polynomial_diagonal_sum_left_add_congruentPX0045 · polynomial_diagonal_sum_right_add_congruentPX0064 · polynomial_diagonal_left_padding_leftPX0065 · polynomial_diagonal_left_padding_rightPX0066 · prime_field_convolution_coefficient_left_padding_leftPX0067 · prime_field_convolution_coefficient_left_padding_right