Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
∀ pff_trace_index_bottomlayer. Lt(pff_trace_index_bottomlayer,n) → ∃ x. ∃ y. BetaAt(b,c,pff_trace_index_bottomlayer,x) ∧ (BetaAt(b,c,S pff_trace_index_bottomlayer,y) ∧ FpAdd(p,x,1,y))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall pff_trace_index_bottomlayer. (exists pfa_gap_bottomlayerindex. pfa_gap_bottomlayerindex + S (pff_trace_index_bottomlayer) = ((n))) -> exists pff_trace_before_bottomlayer pff_trace_after_bottomlayer. ((((exists ff_h_pft_bottomlayerbefore. ff_h_pft_bottomlayerbefore + S (pff_trace_before_bottomlayer) = S ((S (pff_trace_index_bottomlayer)) * (c))) /\ exists ff_q_pft_bottomlayerbefore. (b) = ff_q_pft_bottomlayerbefore * S ((S (pff_trace_index_bottomlayer)) * (c)) + (pff_trace_before_bottomlayer))) /\ (((((exists ff_h_pft_bottomlayerafter. ff_h_pft_bottomlayerafter + S (pff_trace_after_bottomlayer) = S ((S (S (pff_trace_index_bottomlayer))) * (c))) /\ exists ff_q_pft_bottomlayerafter. (b) = ff_q_pft_bottomlayerafter * S ((S (S (pff_trace_index_bottomlayer))) * (c)) + (pff_trace_after_bottomlayer))) /\ ((((exists pfa_gap_bottomlayeradditionleft. pfa_gap_bottomlayeradditionleft + S (pff_trace_before_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeradditionright. pfa_gap_bottomlayeradditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayeradditionresultbound. pfa_gap_bottomlayeradditionresultbound + S (pff_trace_after_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayeradditionresultcongruence pfa_offset_right_bottomlayeradditionresultcongruence. ((pff_trace_before_bottomlayer) + (1)) + ((p)) * pfa_offset_left_bottomlayeradditionresultcongruence = (pff_trace_after_bottomlayer) + ((p)) * pfa_offset_right_bottomlayeradditionresultcongruence)))))))))))))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