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
ModEq(p,a,z · u) ∧ ModEq(p,r + z · t,0) ∨ ModEq(p,a + z · u,0) ∧ ModEq(p,r,z · t)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(((exists hgcrt_mod_left_cor_secondwave_ap hgcrt_mod_right_cor_secondwave_ap. a + p * hgcrt_mod_left_cor_secondwave_ap = (z * u) + p * hgcrt_mod_right_cor_secondwave_ap) /\ (exists hgcrt_mod_left_cor_secondwave_rn hgcrt_mod_right_cor_secondwave_rn. (r + z * t) + p * hgcrt_mod_left_cor_secondwave_rn = 0 + p * hgcrt_mod_right_cor_secondwave_rn)) \/ ((exists hgcrt_mod_left_cor_secondwave_an hgcrt_mod_right_cor_secondwave_an. (a + z * u) + p * hgcrt_mod_left_cor_secondwave_an = 0 + p * hgcrt_mod_right_cor_secondwave_an) /\ (exists hgcrt_mod_left_cor_secondwave_rp hgcrt_mod_right_cor_secondwave_rp. r + p * hgcrt_mod_left_cor_secondwave_rp = (z * t) + p * hgcrt_mod_right_cor_secondwave_rp)))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.