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
BetaAt(b,c,0,0) ∧ (BetaAt(b,c,n,r) ∧ FpUnitSteps(p,b,c,n))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((((exists ff_h_pft_bottomlayerstart. ff_h_pft_bottomlayerstart + S (0) = S ((S (0)) * (c))) /\ exists ff_q_pft_bottomlayerstart. (b) = ff_q_pft_bottomlayerstart * S ((S (0)) * (c)) + (0))) /\ (((((exists ff_h_pft_bottomlayerterminal. ff_h_pft_bottomlayerterminal + S ((r)) = S ((S ((n))) * (c))) /\ exists ff_q_pft_bottomlayerterminal. (b) = ff_q_pft_bottomlayerterminal * S ((S ((n))) * (c)) + ((r)))) /\ ((forall pff_trace_index_bottomlayersteps. (exists pfa_gap_bottomlayerstepsindex. pfa_gap_bottomlayerstepsindex + S (pff_trace_index_bottomlayersteps) = ((n))) -> exists pff_trace_before_bottomlayersteps pff_trace_after_bottomlayersteps. ((((exists ff_h_pft_bottomlayerstepsbefore. ff_h_pft_bottomlayerstepsbefore + S (pff_trace_before_bottomlayersteps) = S ((S (pff_trace_index_bottomlayersteps)) * (c))) /\ exists ff_q_pft_bottomlayerstepsbefore. (b) = ff_q_pft_bottomlayerstepsbefore * S ((S (pff_trace_index_bottomlayersteps)) * (c)) + (pff_trace_before_bottomlayersteps))) /\ (((((exists ff_h_pft_bottomlayerstepsafter. ff_h_pft_bottomlayerstepsafter + S (pff_trace_after_bottomlayersteps) = S ((S (S (pff_trace_index_bottomlayersteps))) * (c))) /\ exists ff_q_pft_bottomlayerstepsafter. (b) = ff_q_pft_bottomlayerstepsafter * S ((S (S (pff_trace_index_bottomlayersteps))) * (c)) + (pff_trace_after_bottomlayersteps))) /\ ((((exists pfa_gap_bottomlayerstepsadditionleft. pfa_gap_bottomlayerstepsadditionleft + S (pff_trace_before_bottomlayersteps) = ((p))) /\ (((exists pfa_gap_bottomlayerstepsadditionright. pfa_gap_bottomlayerstepsadditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayerstepsadditionresultbound. pfa_gap_bottomlayerstepsadditionresultbound + S (pff_trace_after_bottomlayersteps) = ((p))) /\ ((exists pfa_offset_left_bottomlayerstepsadditionresultcongruence pfa_offset_right_bottomlayerstepsadditionresultcongruence. ((pff_trace_before_bottomlayersteps) + (1)) + ((p)) * pfa_offset_left_bottomlayerstepsadditionresultcongruence = (pff_trace_after_bottomlayersteps) + ((p)) * pfa_offset_right_bottomlayerstepsadditionresultcongruence))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.