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
S x ≤ S (S i · c) ∧ (∃ y. b = y · S (S i · c) + x)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
SignedDeterminantNodeAt(b,c,i,d,pb,pc,nb,nc,p,n)SignedDeterminantChildPrefix(b,c,limit,pb,pc,nb,nc,q,eb,ec,fb,fc,l)Sum(b,c,l,z)SignedEvaluatedCofactors(pb,pc,nb,nc,q,eb,ec,fb,fc)SignedMatrixPrefixEquality(pb,pc,nb,nc,qb,qc,rb,rc,d)UniformBetaPrefixBox(c,T,l,B)FiniteMatrixSelector(b,c,l,B)SignedSelectedSubmatrix(pb,pc,nb,nc,w,rb,rc,cb,cc,q,ub,uc,vb,vc)IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l)IntegerVectorZero(ab,ac,db,dc,l)IntegerVectorAdd(ab,ac,db,dc,eb,ec,fb,fc,pb,pc,nb,nc,l)IdentityMatrixSelector(b,c,l)
Checked theorems using this definition
DL0002 · matrix_recursive_prefix_reflDL0003 · matrix_recursive_prefix_transDL0004 · matrix_recursive_prefix_restrictDL0005 · matrix_recursive_record_transportDL0006 · matrix_recursive_record_appendDL0008 · matrix_recursive_children_transportDL0009 · matrix_recursive_step_transportDL000A · matrix_recursive_history_transportDL000B · matrix_recursive_history_extendDL000C · matrix_recursive_zero_extensionDL000E · matrix_recursive_children_recodeDL000F · matrix_recursive_children_extendDL0010 · matrix_recursive_cofactor_prefix_from_recursionDL0011 · matrix_recursive_successor_extensionDL0012 · matrix_recursive_all_extensionsDL0013 · signed_recursive_determinant_existsDL0018 · signed_recursive_determinant_successor_decompositionDL001C · matrix_recursive_minor_cell_transportDL001D · matrix_recursive_minor_prefix_transportDL001E · matrix_recursive_minor_prefix_functionalDL0020 · matrix_recursive_alternating_prefix_transportDL0021 · matrix_recursive_alternating_fold_transportDL0022 · matrix_recursive_alternating_fold_extensionalDL0024 · matrix_recursive_initial_row_prefixDL0025 · matrix_recursive_cofactor_streams_from_functionalityDL0026 · matrix_recursive_determinant_extensionalDL0029 · signed_recursive_determinant_from_evaluated_cofactorsDL002B · signed_recursive_determinant_emptyDL002D · matrix_rank_bounded_prefix_valueDL0030 · matrix_rank_recode_congruences_existsDL0031 · matrix_rank_bounded_recode_in_fixed_boxDL0034 · matrix_rank_prefix_equality_symmetricDL0035 · matrix_rank_bounded_prefix_transportDL0036 · matrix_rank_injective_prefix_transportDL0037 · matrix_rank_injective_prefix_decidableDL0038 · matrix_rank_bounded_prefix_emptyDL0039 · matrix_rank_bounded_prefix_drop_lastDL003A · matrix_rank_bounded_prefix_extendDL003B · matrix_rank_bounded_prefix_decidableDL003C · matrix_rank_selector_transportDL003D · matrix_rank_selector_decidableDL0040 · matrix_rank_selected_point_existsDL0041 · matrix_rank_selected_point_functionalDL0042 · matrix_rank_selected_prefix_emptyDL0043 · matrix_rank_selected_prefix_extendDL0044 · matrix_rank_selected_prefix_exists_nonzeroDL0045 · matrix_rank_selected_square_existsDL0046 · matrix_rank_signed_selected_square_existsDL0047 · matrix_rank_selected_prefix_functionalDL004B · matrix_rank_selected_point_selector_transportDL004C · matrix_rank_selected_prefix_selector_transportDL004D · matrix_rank_signed_selected_selector_transportDL004E · matrix_rank_selected_determinant_selector_transportDL0051 · matrix_rank_nonzero_selected_minor_transportDL0057 · matrix_rank_nonzero_minor_recode_in_boxDL0064 · integer_span_dot_product_pointwise_addDL0065 · integer_span_natural_cell_add_rightDL0066 · integer_span_natural_product_entryDL0068 · integer_span_pointwise_add_interchangeDL006F · integer_vector_equal_transitiveDL0075 · integer_vector_add_transport_inputsDL0076 · integer_vector_add_functionalDL008A · matrix_integer_signed_sum_balanceDL008B · matrix_integer_alternating_prefix_balanceDL008D · matrix_integer_minor_cell_at_sourceDL008F · matrix_integer_minor_prefix_cell_at_coordinatesDL0092 · matrix_integer_cofactor_streams_from_recursionDL0096 · matrix_integer_selected_point_at_sourceDL0097 · matrix_integer_selected_point_balanceDL0098 · matrix_integer_selected_prefix_point_atDL00AE · matrix_lattice_identity_selector_existsDL00B0 · matrix_lattice_identity_selected_natural