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.
Hygienic expanded first-order definition
exists h. h + S a = bThe unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
Checked theorems using this definition
TF0001 · beta_two_square_prefix_drop_lastTF0002 · beta_two_square_prefix_last_representedTF0003 · beta_two_square_represented_factor_productTF0004 · beta_all_prime_entry_is_primeTF0005 · beta_admissible_prime_factor_product_is_two_squareTF0011 · euclid_three_prime_divisor_exceeds_boundTF0012 · infinitely_many_primes_three_mod_four