FpOperationTables(p,ab,ac,mb,mc,nb,nc,ib,ic)

((forall pft_index_bottomlayeradd. (exists pfa_gap_bottomlayeraddprefix. pfa_gap_bottomlayeraddprefix + S (pft_index_bottomlayeradd) = (((p)) * ((p)))) -> exists pft_value_bottomlayeradd. (((((exists ff_h_pft_bottomlayeraddpointentry. ff_h_pft_bottomlayeraddpointentry + S (pft_value_bottomlayeradd) = S ((S (pft_index_bottomlayeradd)) * (ac))) /\ exists ff_q_pft_bottomlayeraddpointentry. (ab) = ff_q_pft_bottomlayeraddpointentry * S ((S (pft_index_bottomlayeradd)) * (ac)) + (pft_value_bottomlayeradd))) /\ ((exists pft_row_bottomlayeraddpointvalue pft_column_bottomlayeraddpointvalue. (((pft_index_bottomlayeradd) = pft_row_bottomlayeraddpointvalue * ((p)) + pft_column_bottomlayeraddpointvalue) /\ ((((exists pfa_gap_bottomlayeraddpointvalueoperationleft. pfa_gap_bottomlayeraddpointvalueoperationleft + S (pft_row_bottomlayeraddpointvalue) = ((p))) /\ (((exists pfa_gap_bottomlayeraddpointvalueoperationright. pfa_gap_bottomlayeraddpointvalueoperationright + S (pft_column_bottomlayeraddpointvalue) = ((p))) /\ ((((exists pfa_gap_bottomlayeraddpointvalueoperationresultbound. pfa_gap_bottomlayeraddpointvalueoperationresultbound + S (pft_value_bottomlayeradd) = ((p))) /\ ((exists pfa_offset_left_bottomlayeraddpointvalueoperationresultcongruence pfa_offset_right_bottomlayeraddpointvalueoperationresultcongruence. ((pft_row_bottomlayeraddpointvalue) + (pft_column_bottomlayeraddpointvalue)) + ((p)) * pfa_offset_left_bottomlayeraddpointvalueoperationresultcongruence = (pft_value_bottomlayeradd) + ((p)) * pfa_offset_right_bottomlayeraddpointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_bottomlayermultiply. (exists pfa_gap_bottomlayermultiplyprefix. pfa_gap_bottomlayermultiplyprefix + S (pft_index_bottomlayermultiply) = (((p)) * ((p)))) -> exists pft_value_bottomlayermultiply. (((((exists ff_h_pft_bottomlayermultiplypointentry. ff_h_pft_bottomlayermultiplypointentry + S (pft_value_bottomlayermultiply) = S ((S (pft_index_bottomlayermultiply)) * (mc))) /\ exists ff_q_pft_bottomlayermultiplypointentry. (mb) = ff_q_pft_bottomlayermultiplypointentry * S ((S (pft_index_bottomlayermultiply)) * (mc)) + (pft_value_bottomlayermultiply))) /\ ((exists pft_row_bottomlayermultiplypointvalue pft_column_bottomlayermultiplypointvalue. (((pft_index_bottomlayermultiply) = pft_row_bottomlayermultiplypointvalue * ((p)) + pft_column_bottomlayermultiplypointvalue) /\ ((((exists pfa_gap_bottomlayermultiplypointvalueoperationleft. pfa_gap_bottomlayermultiplypointvalueoperationleft + S (pft_row_bottomlayermultiplypointvalue) = ((p))) /\ (((exists pfa_gap_bottomlayermultiplypointvalueoperationright. pfa_gap_bottomlayermultiplypointvalueoperationright + S (pft_column_bottomlayermultiplypointvalue) = ((p))) /\ ((((exists pfa_gap_bottomlayermultiplypointvalueoperationresultbound. pfa_gap_bottomlayermultiplypointvalueoperationresultbound + S (pft_value_bottomlayermultiply) = ((p))) /\ ((exists pfa_offset_left_bottomlayermultiplypointvalueoperationresultcongruence pfa_offset_right_bottomlayermultiplypointvalueoperationresultcongruence. ((pft_row_bottomlayermultiplypointvalue) * (pft_column_bottomlayermultiplypointvalue)) + ((p)) * pfa_offset_left_bottomlayermultiplypointvalueoperationresultcongruence = (pft_value_bottomlayermultiply) + ((p)) * pfa_offset_right_bottomlayermultiplypointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_bottomlayernegate. (exists pfa_gap_bottomlayernegateprefix. pfa_gap_bottomlayernegateprefix + S (pft_index_bottomlayernegate) = ((p))) -> exists pft_value_bottomlayernegate. (((((exists ff_h_pft_bottomlayernegatepointentry. ff_h_pft_bottomlayernegatepointentry + S (pft_value_bottomlayernegate) = S ((S (pft_index_bottomlayernegate)) * (nc))) /\ exists ff_q_pft_bottomlayernegatepointentry. (nb) = ff_q_pft_bottomlayernegatepointentry * S ((S (pft_index_bottomlayernegate)) * (nc)) + (pft_value_bottomlayernegate))) /\ ((((exists pfa_gap_bottomlayernegatepointvalueadditionleft. pfa_gap_bottomlayernegatepointvalueadditionleft + S (pft_index_bottomlayernegate) = ((p))) /\ (((exists pfa_gap_bottomlayernegatepointvalueadditionright. pfa_gap_bottomlayernegatepointvalueadditionright + S (pft_value_bottomlayernegate) = ((p))) /\ ((((exists pfa_gap_bottomlayernegatepointvalueadditionresultbound. pfa_gap_bottomlayernegatepointvalueadditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayernegatepointvalueadditionresultcongruence pfa_offset_right_bottomlayernegatepointvalueadditionresultcongruence. ((pft_index_bottomlayernegate) + (pft_value_bottomlayernegate)) + ((p)) * pfa_offset_left_bottomlayernegatepointvalueadditionresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayernegatepointvalueadditionresultcongruence))))))))))))) /\ ((forall pft_index_bottomlayerinverse. (exists pfa_gap_bottomlayerinverseprefix. pfa_gap_bottomlayerinverseprefix + S (pft_index_bottomlayerinverse) = ((p))) -> exists pft_value_bottomlayerinverse. (((((exists ff_h_pft_bottomlayerinversepointentry. ff_h_pft_bottomlayerinversepointentry + S (pft_value_bottomlayerinverse) = S ((S (pft_index_bottomlayerinverse)) * (ic))) /\ exists ff_q_pft_bottomlayerinversepointentry. (ib) = ff_q_pft_bottomlayerinversepointentry * S ((S (pft_index_bottomlayerinverse)) * (ic)) + (pft_value_bottomlayerinverse))) /\ ((((exists pfa_gap_bottomlayerinversepointvalueinput. pfa_gap_bottomlayerinversepointvalueinput + S (pft_index_bottomlayerinverse) = ((p))) /\ (((exists pfa_gap_bottomlayerinversepointvalueoutput. pfa_gap_bottomlayerinversepointvalueoutput + S (pft_value_bottomlayerinverse) = ((p))) /\ ((((pft_index_bottomlayerinverse) = 0 /\ (pft_value_bottomlayerinverse) = 0) \/ (((~((pft_index_bottomlayerinverse) = 0)) /\ ((((exists pfa_gap_bottomlayerinversepointvaluenonzeromultiplicationleft. pfa_gap_bottomlayerinversepointvaluenonzeromultiplicationleft + S (pft_index_bottomlayerinverse) = ((p))) /\ (((exists pfa_gap_bottomlayerinversepointvaluenonzeromultiplicationright. pfa_gap_bottomlayerinversepointvaluenonzeromultiplicationright + S (pft_value_bottomlayerinverse) = ((p))) /\ ((((exists pfa_gap_bottomlayerinversepointvaluenonzeromultiplicationresultbound. pfa_gap_bottomlayerinversepointvaluenonzeromultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_bottomlayerinversepointvaluenonzeromultiplicationresultcongruence pfa_offset_right_bottomlayerinversepointvaluenonzeromultiplicationresultcongruence. ((pft_index_bottomlayerinverse) * (pft_value_bottomlayerinverse)) + ((p)) * pfa_offset_left_bottomlayerinversepointvaluenonzeromultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_bottomlayerinversepointvaluenonzeromultiplicationresultcongruence))))))))))))))))))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.