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
Even(i) ∧ (p = ap · bp + an · bn ∧ n = ap · bn + an · bp) ∨ Odd(i) ∧ (p = ap · bn + an · bp ∧ n = ap · bp + an · bn)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists ff_even_mce_term_breakthrough. i = 2 * ff_even_mce_term_breakthrough) /\ (p = (ap) * (bp) + (an) * (bn) /\ n = (ap) * (bn) + (an) * (bp))) \/ ((exists ff_odd_mce_term_breakthrough. i = 2 * ff_odd_mce_term_breakthrough + 1) /\ (p = (ap) * (bn) + (an) * (bp) /\ n = (ap) * (bp) + (an) * (bn)))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.