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
∃ ppf_code_0_prioritylayer. ∃ ppf_code_1_prioritylayer. ∃ ppf_code_2_prioritylayer. ∃ ppf_code_3_prioritylayer. ∃ ppf_code_4_prioritylayer. ∃ ppf_code_5_prioritylayer. ∃ ppf_code_6_prioritylayer. ∃ ppf_code_7_prioritylayer. NaturalPair(w,pb,ppf_code_0_prioritylayer) ∧ (NaturalPair(ppf_code_0_prioritylayer,pc,ppf_code_1_prioritylayer) ∧ (NaturalPair(ppf_code_1_prioritylayer,eb,ppf_code_2_prioritylayer) ∧ (NaturalPair(ppf_code_2_prioritylayer,ec,ppf_code_3_prioritylayer) ∧ (NaturalPair(ppf_code_3_prioritylayer,vb,ppf_code_4_prioritylayer) ∧ (NaturalPair(ppf_code_4_prioritylayer,vc,ppf_code_5_prioritylayer) ∧ (NaturalPair(ppf_code_5_prioritylayer,l,ppf_code_6_prioritylayer) ∧ (NaturalPair(ppf_code_6_prioritylayer,g,ppf_code_7_prioritylayer) ∧ NaturalPair(ppf_code_7_prioritylayer,rb,rc))))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ppf_code_0_prioritylayer ppf_code_1_prioritylayer ppf_code_2_prioritylayer ppf_code_3_prioritylayer ppf_code_4_prioritylayer ppf_code_5_prioritylayer ppf_code_6_prioritylayer ppf_code_7_prioritylayer. (((((w)) = (((pb)) + (ppf_code_0_prioritylayer)) * S (((pb)) + (ppf_code_0_prioritylayer)) + ((ppf_code_0_prioritylayer) + (ppf_code_0_prioritylayer))) /\ ((((ppf_code_0_prioritylayer) = (((pc)) + (ppf_code_1_prioritylayer)) * S (((pc)) + (ppf_code_1_prioritylayer)) + ((ppf_code_1_prioritylayer) + (ppf_code_1_prioritylayer))) /\ ((((ppf_code_1_prioritylayer) = (((eb)) + (ppf_code_2_prioritylayer)) * S (((eb)) + (ppf_code_2_prioritylayer)) + ((ppf_code_2_prioritylayer) + (ppf_code_2_prioritylayer))) /\ ((((ppf_code_2_prioritylayer) = (((ec)) + (ppf_code_3_prioritylayer)) * S (((ec)) + (ppf_code_3_prioritylayer)) + ((ppf_code_3_prioritylayer) + (ppf_code_3_prioritylayer))) /\ ((((ppf_code_3_prioritylayer) = (((vb)) + (ppf_code_4_prioritylayer)) * S (((vb)) + (ppf_code_4_prioritylayer)) + ((ppf_code_4_prioritylayer) + (ppf_code_4_prioritylayer))) /\ ((((ppf_code_4_prioritylayer) = (((vc)) + (ppf_code_5_prioritylayer)) * S (((vc)) + (ppf_code_5_prioritylayer)) + ((ppf_code_5_prioritylayer) + (ppf_code_5_prioritylayer))) /\ ((((ppf_code_5_prioritylayer) = (((l)) + (ppf_code_6_prioritylayer)) * S (((l)) + (ppf_code_6_prioritylayer)) + ((ppf_code_6_prioritylayer) + (ppf_code_6_prioritylayer))) /\ ((((ppf_code_6_prioritylayer) = (((g)) + (ppf_code_7_prioritylayer)) * S (((g)) + (ppf_code_7_prioritylayer)) + ((ppf_code_7_prioritylayer) + (ppf_code_7_prioritylayer))) /\ ((ppf_code_7_prioritylayer) = (((rb)) + ((rc))) * S (((rb)) + ((rc))) + (((rc)) + ((rc))))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.