Definition in prerequisite notation
∃ pff_history_code_bottomlayer. ∃ pff_history_scale_bottomlayer. FpUnitTrace(p,pff_history_code_bottomlayer,pff_history_scale_bottomlayer,n,r)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists pff_history_code_bottomlayer pff_history_scale_bottomlayer. (((((exists ff_h_pft_bottomlayerhistorystart. ff_h_pft_bottomlayerhistorystart + S (0) = S ((S (0)) * pff_history_scale_bottomlayer)) /\ exists ff_q_pft_bottomlayerhistorystart. pff_history_code_bottomlayer = ff_q_pft_bottomlayerhistorystart * S ((S (0)) * pff_history_scale_bottomlayer) + (0))) /\ (((((exists ff_h_pft_bottomlayerhistoryterminal. ff_h_pft_bottomlayerhistoryterminal + S ((r)) = S ((S ((n))) * pff_history_scale_bottomlayer)) /\ exists ff_q_pft_bottomlayerhistoryterminal. pff_history_code_bottomlayer = ff_q_pft_bottomlayerhistoryterminal * S ((S ((n))) * pff_history_scale_bottomlayer) + ((r)))) /\ ((forall pff_trace_index_bottomlayerhistorysteps. (exists pfa_gap_bottomlayerhistorystepsindex. pfa_gap_bottomlayerhistorystepsindex + S (pff_trace_index_bottomlayerhistorysteps) = ((n))) -> exists pff_trace_before_bottomlayerhistorysteps pff_trace_after_bottomlayerhistorysteps. ((((exists ff_h_pft_bottomlayerhistorystepsbefore. ff_h_pft_bottomlayerhistorystepsbefore + S (pff_trace_before_bottomlayerhistorysteps) = S ((S (pff_trace_index_bottomlayerhistorysteps)) * pff_history_scale_bottomlayer)) /\ exists ff_q_pft_bottomlayerhistorystepsbefore. pff_history_code_bottomlayer = ff_q_pft_bottomlayerhistorystepsbefore * S ((S (pff_trace_index_bottomlayerhistorysteps)) * pff_history_scale_bottomlayer) + (pff_trace_before_bottomlayerhistorysteps))) /\ (((((exists ff_h_pft_bottomlayerhistorystepsafter. ff_h_pft_bottomlayerhistorystepsafter + S (pff_trace_after_bottomlayerhistorysteps) = S ((S (S (pff_trace_index_bottomlayerhistorysteps))) * pff_history_scale_bottomlayer)) /\ exists ff_q_pft_bottomlayerhistorystepsafter. pff_history_code_bottomlayer = ff_q_pft_bottomlayerhistorystepsafter * S ((S (S (pff_trace_index_bottomlayerhistorysteps))) * pff_history_scale_bottomlayer) + (pff_trace_after_bottomlayerhistorysteps))) /\ ((((exists pfa_gap_bottomlayerhistorystepsadditionleft. pfa_gap_bottomlayerhistorystepsadditionleft + S (pff_trace_before_bottomlayerhistorysteps) = ((p))) /\ (((exists pfa_gap_bottomlayerhistorystepsadditionright. pfa_gap_bottomlayerhistorystepsadditionright + S (1) = ((p))) /\ ((((exists pfa_gap_bottomlayerhistorystepsadditionresultbound. pfa_gap_bottomlayerhistorystepsadditionresultbound + S (pff_trace_after_bottomlayerhistorysteps) = ((p))) /\ ((exists pfa_offset_left_bottomlayerhistorystepsadditionresultcongruence pfa_offset_right_bottomlayerhistorystepsadditionresultcongruence. ((pff_trace_before_bottomlayerhistorysteps) + (1)) + ((p)) * pfa_offset_left_bottomlayerhistorystepsadditionresultcongruence = (pff_trace_after_bottomlayerhistorysteps) + ((p)) * pfa_offset_right_bottomlayerhistorystepsadditionresultcongruence)))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.