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
∃ ssr_flat_row_g009_definition. ∃ ssr_flat_column_g009_definition. k = S M · ssr_flat_row_g009_definition + ssr_flat_column_g009_definition ∧ (Lt(ssr_flat_column_g009_definition,S M) ∧ SignedIncidenceEntry(A,r,s,ssr_flat_row_g009_definition,ssr_flat_column_g009_definition,z))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ssr_flat_row_g009_definition ssr_flat_column_g009_definition. ((((k))=(((S ((M)))*(ssr_flat_row_g009_definition)+(ssr_flat_column_g009_definition)))) /\ (((exists pvs_gap_g009_definitionremainder. pvs_gap_g009_definitionremainder + S (ssr_flat_column_g009_definition) = (S ((M)))) /\ (exists ssr_entry_value_g009_definitionentry ssr_entry_image_g009_definitionentry. ((exists dst_positive_code_g009_definitionentrysource dst_positive_scale_g009_definitionentrysource dst_negative_code_g009_definitionentrysource dst_negative_scale_g009_definitionentrysource dst_positive_g009_definitionentrysource dst_negative_g009_definitionentrysource. ((((A)) = (((((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) * S ((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) + ((dst_positive_scale_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource))) + (((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)))) * S ((((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) * S ((dst_positive_code_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource)) + ((dst_positive_scale_g009_definitionentrysource) + (dst_positive_scale_g009_definitionentrysource))) + (((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)))) + ((((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource))) + (((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) * S ((dst_negative_code_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)) + ((dst_negative_scale_g009_definitionentrysource) + (dst_negative_scale_g009_definitionentrysource)))))) /\ (((((exists ff_h_pvs_g009_definitionentrysourcepositive. ff_h_pvs_g009_definitionentrysourcepositive + S (dst_positive_g009_definitionentrysource) = S ((S (ssr_flat_row_g009_definition)) * dst_positive_scale_g009_definitionentrysource)) /\ exists ff_q_pvs_g009_definitionentrysourcepositive. dst_positive_code_g009_definitionentrysource = ff_q_pvs_g009_definitionentrysourcepositive * S ((S (ssr_flat_row_g009_definition)) * dst_positive_scale_g009_definitionentrysource) + (dst_positive_g009_definitionentrysource))) /\ (((((exists ff_h_pvs_g009_definitionentrysourcenegative. ff_h_pvs_g009_definitionentrysourcenegative + S (dst_negative_g009_definitionentrysource) = S ((S (ssr_flat_row_g009_definition)) * dst_negative_scale_g009_definitionentrysource)) /\ exists ff_q_pvs_g009_definitionentrysourcenegative. dst_negative_code_g009_definitionentrysource = ff_q_pvs_g009_definitionentrysourcenegative * S ((S (ssr_flat_row_g009_definition)) * dst_negative_scale_g009_definitionentrysource) + (dst_negative_g009_definitionentrysource))) /\ (exists ge_balance_positive_g009_definitionentrysourcevalue ge_balance_negative_g009_definitionentrysourcevalue. (((((ssr_entry_value_g009_definitionentry) = 2 * (ge_balance_positive_g009_definitionentrysourcevalue) /\ (ge_balance_negative_g009_definitionentrysourcevalue) = 0) \/ exists ge_signed_half_g009_definitionentrysourcevaluedecode. (((ssr_entry_value_g009_definitionentry) = 2 * ge_signed_half_g009_definitionentrysourcevaluedecode + 1 /\ (ge_balance_positive_g009_definitionentrysourcevalue) = 0) /\ (ge_balance_negative_g009_definitionentrysourcevalue) = S ge_signed_half_g009_definitionentrysourcevaluedecode))) /\ ((dst_positive_g009_definitionentrysource) + ge_balance_negative_g009_definitionentrysourcevalue = (dst_negative_g009_definitionentrysource) + ge_balance_positive_g009_definitionentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_g009_definitionentrymap. ff_h_pvs_g009_definitionentrymap + S (ssr_entry_image_g009_definitionentry) = S ((S (ssr_flat_row_g009_definition)) * (s))) /\ exists ff_q_pvs_g009_definitionentrymap. (r) = ff_q_pvs_g009_definitionentrymap * S ((S (ssr_flat_row_g009_definition)) * (s)) + (ssr_entry_image_g009_definitionentry))) /\ (((((ssr_flat_column_g009_definition)=(ssr_entry_image_g009_definitionentry)) /\ (((z))=(ssr_entry_value_g009_definitionentry)))) \/ (((~((ssr_flat_column_g009_definition)=(ssr_entry_image_g009_definitionentry))) /\ (((z))=0)))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.