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
∃ cfc_left_prioritylayer. ∃ cfc_right_prioritylayer. ∃ cfc_matrix_prioritylayer. NaturalPair(cfc_left_prioritylayer,u,U) ∧ (NaturalPair(cfc_right_prioritylayer,v,V) ∧ (NaturalPair(cfc_matrix_prioritylayer,cfc_left_prioritylayer,cfc_right_prioritylayer) ∧ NaturalPair(z,s,cfc_matrix_prioritylayer)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists cfc_left_prioritylayer cfc_right_prioritylayer cfc_matrix_prioritylayer. ((cfc_left_prioritylayer = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_prioritylayer = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_prioritylayer = ((cfc_left_prioritylayer) + (cfc_right_prioritylayer)) * S ((cfc_left_prioritylayer) + (cfc_right_prioritylayer)) + ((cfc_right_prioritylayer) + (cfc_right_prioritylayer))) /\ ((z) = ((s) + (cfc_matrix_prioritylayer)) * S ((s) + (cfc_matrix_prioritylayer)) + ((cfc_matrix_prioritylayer) + (cfc_matrix_prioritylayer))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.