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 ff_h_cf_egt_transport_state. ff_h_cf_egt_transport_state + S (((a) + (((b) + (q)) * S ((b) + (q)) + ((q) + (q)))) * S ((a) + (((b) + (q)) * S ((b) + (q)) + ((q) + (q)))) + ((((b) + (q)) * S ((b) + (q)) + ((q) + (q))) + (((b) + (q)) * S ((b) + (q)) + ((q) + (q))))) = S ((S (i)) * s)) /\ exists ff_q_cf_egt_transport_state. h = ff_q_cf_egt_transport_state * S ((S (i)) * s) + (((a) + (((b) + (q)) * S ((b) + (q)) + ((q) + (q)))) * S ((a) + (((b) + (q)) * S ((b) + (q)) + ((q) + (q)))) + ((((b) + (q)) * S ((b) + (q)) + ((q) + (q))) + (((b) + (q)) * S ((b) + (q)) + ((q) + (q))))))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
none directly; see definition consumers
Separate complete second-wave branches: Full T13 proof · Alpha v27.