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
∃ sif_positive_lowerlayer. ∃ sif_negative_lowerlayer. ∃ sif_quotient_positive_lowerlayer. ∃ sif_quotient_negative_lowerlayer. SignedDecode(a,sif_positive_lowerlayer,sif_negative_lowerlayer) ∧ (SignedDecode(q,sif_quotient_positive_lowerlayer,sif_quotient_negative_lowerlayer) ∧ SignedFloor(sif_positive_lowerlayer,sif_negative_lowerlayer,m,sif_quotient_positive_lowerlayer,sif_quotient_negative_lowerlayer,r))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists sif_positive_lowerlayer sif_negative_lowerlayer sif_quotient_positive_lowerlayer sif_quotient_negative_lowerlayer. (((a = 2 * sif_positive_lowerlayer /\ sif_negative_lowerlayer = 0) \/ exists sd_half_sif_lowerlayer_input. ((a = 2 * sd_half_sif_lowerlayer_input + 1 /\ sif_positive_lowerlayer = 0) /\ sif_negative_lowerlayer = S sd_half_sif_lowerlayer_input)) /\ (((q = 2 * sif_quotient_positive_lowerlayer /\ sif_quotient_negative_lowerlayer = 0) \/ exists sd_half_sif_lowerlayer_quotient. ((q = 2 * sd_half_sif_lowerlayer_quotient + 1 /\ sif_quotient_positive_lowerlayer = 0) /\ sif_quotient_negative_lowerlayer = S sd_half_sif_lowerlayer_quotient)) /\ (((sif_positive_lowerlayer) + (m) * (sif_quotient_negative_lowerlayer) = ((sif_negative_lowerlayer) + (m) * (sif_quotient_positive_lowerlayer)) + (r) /\ exists sif_gap_lowerlayer. sif_gap_lowerlayer + S (r) = (m)))))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
none