Definition in prerequisite notation
∃ pft_row_bottomlayer. ∃ pft_column_bottomlayer. i = pft_row_bottomlayer · p + pft_column_bottomlayer ∧ FpMul(p,pft_row_bottomlayer,pft_column_bottomlayer,v)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists pft_row_bottomlayer pft_column_bottomlayer. ((((i)) = pft_row_bottomlayer * ((p)) + pft_column_bottomlayer) /\ ((((exists pfa_gap_bottomlayeroperationleft. pfa_gap_bottomlayeroperationleft + S (pft_row_bottomlayer) = ((p))) /\ (((exists pfa_gap_bottomlayeroperationright. pfa_gap_bottomlayeroperationright + S (pft_column_bottomlayer) = ((p))) /\ ((((exists pfa_gap_bottomlayeroperationresultbound. pfa_gap_bottomlayeroperationresultbound + S ((v)) = ((p))) /\ ((exists pfa_offset_left_bottomlayeroperationresultcongruence pfa_offset_right_bottomlayeroperationresultcongruence. ((pft_row_bottomlayer) * (pft_column_bottomlayer)) + ((p)) * pfa_offset_left_bottomlayeroperationresultcongruence = ((v)) + ((p)) * pfa_offset_right_bottomlayeroperationresultcongruence)))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.