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
FpUnitMultiple(p,p,0) ∧ (∀ x. Lt(x,p) → ¬x = 0 → ¬FpUnitMultiple(p,x,0))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists pff_history_code_bottomlayermodulus pff_history_scale_bottomlayermodulus. (((((exists ff_h_pft_bottomlayermodulushistorystart. ff_h_pft_bottomlayermodulushistorystart + S (0) = S ((S (0)) * pff_history_scale_bottomlayermodulus)) /\ exists ff_q_pft_bottomlayermodulushistorystart. pff_history_code_bottomlayermodulus = ff_q_pft_bottomlayermodulushistorystart * S ((S (0)) * pff_history_scale_bottomlayermodulus) + (0))) /\ (((((exists ff_h_pft_bottomlayermodulushistoryterminal. ff_h_pft_bottomlayermodulushistoryterminal + S (0) = S ((S ((p))) * pff_history_scale_bottomlayermodulus)) /\ exists ff_q_pft_bottomlayermodulushistoryterminal. pff_history_code_bottomlayermodulus = ff_q_pft_bottomlayermodulushistoryterminal * S ((S ((p))) * pff_history_scale_bottomlayermodulus) + (0))) /\ ((forall pff_trace_index_bottomlayermodulushistorysteps. (exists pfa_gap_bottomlayermodulushistorystepsindex. pfa_gap_bottomlayermodulushistorystepsindex + S (pff_trace_index_bottomlayermodulushistorysteps) = ((p))) -> exists pff_trace_before_bottomlayermodulushistorysteps pff_trace_after_bottomlayermodulushistorysteps. ((((exists ff_h_pft_bottomlayermodulushistorystepsbefore. ff_h_pft_bottomlayermodulushistorystepsbefore + S (pff_trace_before_bottomlayermodulushistorysteps) = S ((S (pff_trace_index_bottomlayermodulushistorysteps)) * pff_history_scale_bottomlayermodulus)) /\ exists ff_q_pft_bottomlayermodulushistorystepsbefore. pff_history_code_bottomlayermodulus = ff_q_pft_bottomlayermodulushistorystepsbefore * S ((S (pff_trace_index_bottomlayermodulushistorysteps)) * pff_history_scale_bottomlayermodulus) + (pff_trace_before_bottomlayermodulushistorysteps))) /\ (((((exists ff_h_pft_bottomlayermodulushistorystepsafter. ff_h_pft_bottomlayermodulushistorystepsafter + S (pff_trace_after_bottomlayermodulushistorysteps) = S ((S (S (pff_trace_index_bottomlayermodulushistorysteps))) * pff_history_scale_bottomlayermodulus)) /\ exists ff_q_pft_bottomlayermodulushistorystepsafter. pff_history_code_bottomlayermodulus = ff_q_pft_bottomlayermodulushistorystepsafter * S ((S (S (pff_trace_index_bottomlayermodulushistorysteps))) * pff_history_scale_bottomlayermodulus) + (pff_trace_after_bottomlayermodulushistorysteps))) /\ ((((exists pfa_gap_bottomlayermodulushistorystepsadditionleft. pfa_gap_bottomlayermodulushistorystepsadditionleft + S (pff_trace_before_bottomlayermodulushistorysteps) = ((p))) /\ (((exists pfa_gap_bottomlayermodulushistorystepsadditionright. pfa_gap_bottomlayermodulushistorystepsadditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayermodulushistorystepsadditionresultbound. pfa_gap_bottomlayermodulushistorystepsadditionresultbound + S (pff_trace_after_bottomlayermodulushistorysteps) = ((p))) /\ ((exists pfa_offset_left_bottomlayermodulushistorystepsadditionresultcongruence pfa_offset_right_bottomlayermodulushistorystepsadditionresultcongruence. ((pff_trace_before_bottomlayermodulushistorysteps) + (1)) + ((p)) * pfa_offset_left_bottomlayermodulushistorystepsadditionresultcongruence = (pff_trace_after_bottomlayermodulushistorysteps) + ((p)) * pfa_offset_right_bottomlayermodulushistorystepsadditionresultcongruence)))))))))))))))))))) /\ ((forall pff_smaller_positive_bottomlayer. (exists pfa_gap_bottomlayerstrict. pfa_gap_bottomlayerstrict + S (pff_smaller_positive_bottomlayer) = ((p))) -> ~(pff_smaller_positive_bottomlayer = 0) -> ~(exists pff_history_code_bottomlayersmaller pff_history_scale_bottomlayersmaller. (((((exists ff_h_pft_bottomlayersmallerhistorystart. ff_h_pft_bottomlayersmallerhistorystart + S (0) = S ((S (0)) * pff_history_scale_bottomlayersmaller)) /\ exists ff_q_pft_bottomlayersmallerhistorystart. pff_history_code_bottomlayersmaller = ff_q_pft_bottomlayersmallerhistorystart * S ((S (0)) * pff_history_scale_bottomlayersmaller) + (0))) /\ (((((exists ff_h_pft_bottomlayersmallerhistoryterminal. ff_h_pft_bottomlayersmallerhistoryterminal + S (0) = S ((S (pff_smaller_positive_bottomlayer)) * pff_history_scale_bottomlayersmaller)) /\ exists ff_q_pft_bottomlayersmallerhistoryterminal. pff_history_code_bottomlayersmaller = ff_q_pft_bottomlayersmallerhistoryterminal * S ((S (pff_smaller_positive_bottomlayer)) * pff_history_scale_bottomlayersmaller) + (0))) /\ ((forall pff_trace_index_bottomlayersmallerhistorysteps. (exists pfa_gap_bottomlayersmallerhistorystepsindex. pfa_gap_bottomlayersmallerhistorystepsindex + S (pff_trace_index_bottomlayersmallerhistorysteps) = (pff_smaller_positive_bottomlayer)) -> exists pff_trace_before_bottomlayersmallerhistorysteps pff_trace_after_bottomlayersmallerhistorysteps. ((((exists ff_h_pft_bottomlayersmallerhistorystepsbefore. ff_h_pft_bottomlayersmallerhistorystepsbefore + S (pff_trace_before_bottomlayersmallerhistorysteps) = S ((S (pff_trace_index_bottomlayersmallerhistorysteps)) * pff_history_scale_bottomlayersmaller)) /\ exists ff_q_pft_bottomlayersmallerhistorystepsbefore. pff_history_code_bottomlayersmaller = ff_q_pft_bottomlayersmallerhistorystepsbefore * S ((S (pff_trace_index_bottomlayersmallerhistorysteps)) * pff_history_scale_bottomlayersmaller) + (pff_trace_before_bottomlayersmallerhistorysteps))) /\ (((((exists ff_h_pft_bottomlayersmallerhistorystepsafter. ff_h_pft_bottomlayersmallerhistorystepsafter + S (pff_trace_after_bottomlayersmallerhistorysteps) = S ((S (S (pff_trace_index_bottomlayersmallerhistorysteps))) * pff_history_scale_bottomlayersmaller)) /\ exists ff_q_pft_bottomlayersmallerhistorystepsafter. pff_history_code_bottomlayersmaller = ff_q_pft_bottomlayersmallerhistorystepsafter * S ((S (S (pff_trace_index_bottomlayersmallerhistorysteps))) * pff_history_scale_bottomlayersmaller) + (pff_trace_after_bottomlayersmallerhistorysteps))) /\ ((((exists pfa_gap_bottomlayersmallerhistorystepsadditionleft. pfa_gap_bottomlayersmallerhistorystepsadditionleft + S (pff_trace_before_bottomlayersmallerhistorysteps) = ((p))) /\ (((exists pfa_gap_bottomlayersmallerhistorystepsadditionright. pfa_gap_bottomlayersmallerhistorystepsadditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayersmallerhistorystepsadditionresultbound. pfa_gap_bottomlayersmallerhistorystepsadditionresultbound + S (pff_trace_after_bottomlayersmallerhistorysteps) = ((p))) /\ ((exists pfa_offset_left_bottomlayersmallerhistorystepsadditionresultcongruence pfa_offset_right_bottomlayersmallerhistorystepsadditionresultcongruence. ((pff_trace_before_bottomlayersmallerhistorysteps) + (1)) + ((p)) * pfa_offset_left_bottomlayersmallerhistorystepsadditionresultcongruence = (pff_trace_after_bottomlayersmallerhistorysteps) + ((p)) * pfa_offset_right_bottomlayersmallerhistorystepsadditionresultcongruence)))))))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.