FpSyntheticDivision(p,b,c,a,n,qb,qc,r)

exists pfs_history_code_polynomial_division_definition pfs_history_scale_polynomial_division_definition. ((((exists pfa_gap_polynomial_division_definitiontracebase. pfa_gap_polynomial_division_definitiontracebase + S ((a)) = ((p))) /\ (((((exists ff_h_pfp_polynomial_division_definitiontraceinitial. ff_h_pfp_polynomial_division_definitiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_polynomial_division_definition)) /\ exists ff_q_pfp_polynomial_division_definitiontraceinitial. pfs_history_code_polynomial_division_definition = ff_q_pfp_polynomial_division_definitiontraceinitial * S ((S (0)) * pfs_history_scale_polynomial_division_definition) + (0))) /\ (((((exists ff_h_pfp_polynomial_division_definitiontraceterminal. ff_h_pfp_polynomial_division_definitiontraceterminal + S ((r)) = S ((S (S ((n)))) * pfs_history_scale_polynomial_division_definition)) /\ exists ff_q_pfp_polynomial_division_definitiontraceterminal. pfs_history_code_polynomial_division_definition = ff_q_pfp_polynomial_division_definitiontraceterminal * S ((S (S ((n)))) * pfs_history_scale_polynomial_division_definition) + ((r)))) /\ ((forall pfh_index_polynomial_division_definitiontracesteps. (exists pfa_gap_polynomial_division_definitiontracestepsindex. pfa_gap_polynomial_division_definitiontracestepsindex + S (pfh_index_polynomial_division_definitiontracesteps) = (S ((n)))) -> (exists pfh_coefficient_polynomial_division_definitiontracestepsstep pfh_before_polynomial_division_definitiontracestepsstep pfh_after_polynomial_division_definitiontracestepsstep pfh_product_polynomial_division_definitiontracestepsstep. ((((exists ff_h_pfp_polynomial_division_definitiontracestepsstepcoefficient. ff_h_pfp_polynomial_division_definitiontracestepsstepcoefficient + S (pfh_coefficient_polynomial_division_definitiontracestepsstep) = S ((S (pfh_index_polynomial_division_definitiontracesteps)) * (c))) /\ exists ff_q_pfp_polynomial_division_definitiontracestepsstepcoefficient. (b) = ff_q_pfp_polynomial_division_definitiontracestepsstepcoefficient * S ((S (pfh_index_polynomial_division_definitiontracesteps)) * (c)) + (pfh_coefficient_polynomial_division_definitiontracestepsstep))) /\ (((((exists ff_h_pfp_polynomial_division_definitiontracestepsstepbefore. ff_h_pfp_polynomial_division_definitiontracestepsstepbefore + S (pfh_before_polynomial_division_definitiontracestepsstep) = S ((S (pfh_index_polynomial_division_definitiontracesteps)) * pfs_history_scale_polynomial_division_definition)) /\ exists ff_q_pfp_polynomial_division_definitiontracestepsstepbefore. pfs_history_code_polynomial_division_definition = ff_q_pfp_polynomial_division_definitiontracestepsstepbefore * S ((S (pfh_index_polynomial_division_definitiontracesteps)) * pfs_history_scale_polynomial_division_definition) + (pfh_before_polynomial_division_definitiontracestepsstep))) /\ (((((exists ff_h_pfp_polynomial_division_definitiontracestepsstepafter. ff_h_pfp_polynomial_division_definitiontracestepsstepafter + S (pfh_after_polynomial_division_definitiontracestepsstep) = S ((S (S (pfh_index_polynomial_division_definitiontracesteps))) * pfs_history_scale_polynomial_division_definition)) /\ exists ff_q_pfp_polynomial_division_definitiontracestepsstepafter. pfs_history_code_polynomial_division_definition = ff_q_pfp_polynomial_division_definitiontracestepsstepafter * S ((S (S (pfh_index_polynomial_division_definitiontracesteps))) * pfs_history_scale_polynomial_division_definition) + (pfh_after_polynomial_division_definitiontracestepsstep))) /\ (((((exists pfa_gap_polynomial_division_definitiontracestepsstepmultiplyleft. pfa_gap_polynomial_division_definitiontracestepsstepmultiplyleft + S (pfh_before_polynomial_division_definitiontracestepsstep) = ((p))) /\ (((exists pfa_gap_polynomial_division_definitiontracestepsstepmultiplyright. pfa_gap_polynomial_division_definitiontracestepsstepmultiplyright + S ((a)) = ((p))) /\ ((((exists pfa_gap_polynomial_division_definitiontracestepsstepmultiplyresultbound. pfa_gap_polynomial_division_definitiontracestepsstepmultiplyresultbound + S (pfh_product_polynomial_division_definitiontracestepsstep) = ((p))) /\ ((exists pfa_offset_left_polynomial_division_definitiontracestepsstepmultiplyresultcongruence pfa_offset_right_polynomial_division_definitiontracestepsstepmultiplyresultcongruence. ((pfh_before_polynomial_division_definitiontracestepsstep) * ((a))) + ((p)) * pfa_offset_left_polynomial_division_definitiontracestepsstepmultiplyresultcongruence = (pfh_product_polynomial_division_definitiontracestepsstep) + ((p)) * pfa_offset_right_polynomial_division_definitiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_polynomial_division_definitiontracestepsstepaddleft. pfa_gap_polynomial_division_definitiontracestepsstepaddleft + S (pfh_product_polynomial_division_definitiontracestepsstep) = ((p))) /\ (((exists pfa_gap_polynomial_division_definitiontracestepsstepaddright. pfa_gap_polynomial_division_definitiontracestepsstepaddright + S (pfh_coefficient_polynomial_division_definitiontracestepsstep) = ((p))) /\ ((((exists pfa_gap_polynomial_division_definitiontracestepsstepaddresultbound. pfa_gap_polynomial_division_definitiontracestepsstepaddresultbound + S (pfh_after_polynomial_division_definitiontracestepsstep) = ((p))) /\ ((exists pfa_offset_left_polynomial_division_definitiontracestepsstepaddresultcongruence pfa_offset_right_polynomial_division_definitiontracestepsstepaddresultcongruence. ((pfh_product_polynomial_division_definitiontracestepsstep) + (pfh_coefficient_polynomial_division_definitiontracestepsstep)) + ((p)) * pfa_offset_left_polynomial_division_definitiontracestepsstepaddresultcongruence = (pfh_after_polynomial_division_definitiontracestepsstep) + ((p)) * pfa_offset_right_polynomial_division_definitiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_polynomial_division_definitionquotient ff_source_mcp_pfs_polynomial_division_definitionquotient ff_target_mcp_pfs_polynomial_division_definitionquotient. (exists mcp_gap_pfs_polynomial_division_definitionquotient_bound. mcp_gap_pfs_polynomial_division_definitionquotient_bound + S (ff_index_mcp_pfs_polynomial_division_definitionquotient) = ((n))) -> (((exists fs_h_mcp_pfs_polynomial_division_definitionquotient_source. fs_h_mcp_pfs_polynomial_division_definitionquotient_source + S (ff_source_mcp_pfs_polynomial_division_definitionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_polynomial_division_definitionquotient)) * pfs_history_scale_polynomial_division_definition)) /\ exists fs_q_mcp_pfs_polynomial_division_definitionquotient_source. pfs_history_code_polynomial_division_definition = fs_q_mcp_pfs_polynomial_division_definitionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_polynomial_division_definitionquotient)) * pfs_history_scale_polynomial_division_definition) + (ff_source_mcp_pfs_polynomial_division_definitionquotient))) -> (((exists fs_h_mcp_pfs_polynomial_division_definitionquotient_target. fs_h_mcp_pfs_polynomial_division_definitionquotient_target + S (ff_target_mcp_pfs_polynomial_division_definitionquotient) = S ((S (ff_index_mcp_pfs_polynomial_division_definitionquotient)) * (qc))) /\ exists fs_q_mcp_pfs_polynomial_division_definitionquotient_target. (qb) = fs_q_mcp_pfs_polynomial_division_definitionquotient_target * S ((S (ff_index_mcp_pfs_polynomial_division_definitionquotient)) * (qc)) + (ff_target_mcp_pfs_polynomial_division_definitionquotient))) -> ff_target_mcp_pfs_polynomial_division_definitionquotient = ff_source_mcp_pfs_polynomial_division_definitionquotient)))

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