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
¬d = 0 ∧ (∃ x. n = d · x ∧ ArithAt(F,d,z)) ∨ (d = 0 ∨ ¬Dvd(d,n)) ∧ z = 0Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(((~(((d))=0)) /\ (exists dm_quotient_lowertier. ((((n))=((d))*dm_quotient_lowertier) /\ (exists dst_positive_code_lowertierinput dst_positive_scale_lowertierinput dst_negative_code_lowertierinput dst_negative_scale_lowertierinput dst_positive_lowertierinput dst_negative_lowertierinput. ((((F)) = (((((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) * S ((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) + ((dst_positive_scale_lowertierinput) + (dst_positive_scale_lowertierinput))) + (((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput)))) * S ((((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) * S ((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) + ((dst_positive_scale_lowertierinput) + (dst_positive_scale_lowertierinput))) + (((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput)))) + ((((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput))) + (((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput)))))) /\ (((((exists ff_h_pvs_lowertierinputpositive. ff_h_pvs_lowertierinputpositive + S (dst_positive_lowertierinput) = S ((S ((d))) * dst_positive_scale_lowertierinput)) /\ exists ff_q_pvs_lowertierinputpositive. dst_positive_code_lowertierinput = ff_q_pvs_lowertierinputpositive * S ((S ((d))) * dst_positive_scale_lowertierinput) + (dst_positive_lowertierinput))) /\ (((((exists ff_h_pvs_lowertierinputnegative. ff_h_pvs_lowertierinputnegative + S (dst_negative_lowertierinput) = S ((S ((d))) * dst_negative_scale_lowertierinput)) /\ exists ff_q_pvs_lowertierinputnegative. dst_negative_code_lowertierinput = ff_q_pvs_lowertierinputnegative * S ((S ((d))) * dst_negative_scale_lowertierinput) + (dst_negative_lowertierinput))) /\ (exists ge_balance_positive_lowertierinputvalue ge_balance_negative_lowertierinputvalue. ((((((z)) = 2 * (ge_balance_positive_lowertierinputvalue) /\ (ge_balance_negative_lowertierinputvalue) = 0) \/ exists ge_signed_half_lowertierinputvaluedecode. ((((z)) = 2 * ge_signed_half_lowertierinputvaluedecode + 1 /\ (ge_balance_positive_lowertierinputvalue) = 0) /\ (ge_balance_negative_lowertierinputvalue) = S ge_signed_half_lowertierinputvaluedecode))) /\ ((dst_positive_lowertierinput) + ge_balance_negative_lowertierinputvalue = (dst_negative_lowertierinput) + ge_balance_positive_lowertierinputvalue))))))))))))) \/ (((((d))=0 \/ ~(exists pvs_factor_lowertiernondivisor. ((n)) = ((d)) * pvs_factor_lowertiernondivisor)) /\ (((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
DV0010 · divisor_mask_entry_zeroDV0011 · divisor_mask_entry_from_quotientDV0012 · divisor_mask_entry_from_nondivisorDV0013 · divisor_mask_entry_existsDV0014 · divisor_mask_entry_functionalDV0015 · divisor_mask_entry_quotient_inputDV0016 · divisor_mask_entry_omitted_valueDV0018 · divisor_mask_prefix_appendDV0019 · divisor_mask_prefix_existsDV001E · divisor_mask_entry_positive_source_extensional