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_entry_value_g009_definition. ∃ ssr_entry_image_g009_definition. ArithAt(A,i,ssr_entry_value_g009_definition) ∧ (BetaAt(r,s,i,ssr_entry_image_g009_definition) ∧ (j = ssr_entry_image_g009_definition ∧ z = ssr_entry_value_g009_definition ∨ ¬j = ssr_entry_image_g009_definition ∧ z = 0))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ssr_entry_value_g009_definition ssr_entry_image_g009_definition. ((exists dst_positive_code_g009_definitionsource dst_positive_scale_g009_definitionsource dst_negative_code_g009_definitionsource dst_negative_scale_g009_definitionsource dst_positive_g009_definitionsource dst_negative_g009_definitionsource. ((((A)) = (((((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) * S ((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) + ((dst_positive_scale_g009_definitionsource) + (dst_positive_scale_g009_definitionsource))) + (((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)))) * S ((((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) * S ((dst_positive_code_g009_definitionsource) + (dst_positive_scale_g009_definitionsource)) + ((dst_positive_scale_g009_definitionsource) + (dst_positive_scale_g009_definitionsource))) + (((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)))) + ((((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource))) + (((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) * S ((dst_negative_code_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)) + ((dst_negative_scale_g009_definitionsource) + (dst_negative_scale_g009_definitionsource)))))) /\ (((((exists ff_h_pvs_g009_definitionsourcepositive. ff_h_pvs_g009_definitionsourcepositive + S (dst_positive_g009_definitionsource) = S ((S ((i))) * dst_positive_scale_g009_definitionsource)) /\ exists ff_q_pvs_g009_definitionsourcepositive. dst_positive_code_g009_definitionsource = ff_q_pvs_g009_definitionsourcepositive * S ((S ((i))) * dst_positive_scale_g009_definitionsource) + (dst_positive_g009_definitionsource))) /\ (((((exists ff_h_pvs_g009_definitionsourcenegative. ff_h_pvs_g009_definitionsourcenegative + S (dst_negative_g009_definitionsource) = S ((S ((i))) * dst_negative_scale_g009_definitionsource)) /\ exists ff_q_pvs_g009_definitionsourcenegative. dst_negative_code_g009_definitionsource = ff_q_pvs_g009_definitionsourcenegative * S ((S ((i))) * dst_negative_scale_g009_definitionsource) + (dst_negative_g009_definitionsource))) /\ (exists ge_balance_positive_g009_definitionsourcevalue ge_balance_negative_g009_definitionsourcevalue. (((((ssr_entry_value_g009_definition) = 2 * (ge_balance_positive_g009_definitionsourcevalue) /\ (ge_balance_negative_g009_definitionsourcevalue) = 0) \/ exists ge_signed_half_g009_definitionsourcevaluedecode. (((ssr_entry_value_g009_definition) = 2 * ge_signed_half_g009_definitionsourcevaluedecode + 1 /\ (ge_balance_positive_g009_definitionsourcevalue) = 0) /\ (ge_balance_negative_g009_definitionsourcevalue) = S ge_signed_half_g009_definitionsourcevaluedecode))) /\ ((dst_positive_g009_definitionsource) + ge_balance_negative_g009_definitionsourcevalue = (dst_negative_g009_definitionsource) + ge_balance_positive_g009_definitionsourcevalue))))))))) /\ (((((exists ff_h_pvs_g009_definitionmap. ff_h_pvs_g009_definitionmap + S (ssr_entry_image_g009_definition) = S ((S ((i))) * (s))) /\ exists ff_q_pvs_g009_definitionmap. (r) = ff_q_pvs_g009_definitionmap * S ((S ((i))) * (s)) + (ssr_entry_image_g009_definition))) /\ ((((((j))=(ssr_entry_image_g009_definition)) /\ (((z))=(ssr_entry_value_g009_definition)))) \/ (((~(((j))=(ssr_entry_image_g009_definition))) /\ (((z))=0)))))))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
MX0036 · signed_support_incidence_entry_hitMX0037 · signed_support_incidence_entry_missMX0038 · signed_support_incidence_entry_decodeMX0039 · signed_support_incidence_entry_functionalMX003A · signed_support_incidence_entry_existsMX003B · signed_support_incidence_zero_source_valueMX003C · signed_support_incidence_nonzero_source_imageMX003D · signed_support_incidence_flat_entry_existsMX003E · signed_support_incidence_flat_entry_coordinatesMX0044 · signed_support_incidence_row_lookupMX0045 · signed_support_incidence_column_lookup