FpMonicNormalization(p,k,ab,ac,bb,bc,L)

((~(((L)) = 0)) /\ (((exists pfm_leading_polynomial_division_definition. ((((exists ff_h_pfp_polynomial_division_definitionsource. ff_h_pfp_polynomial_division_definitionsource + S (pfm_leading_polynomial_division_definition) = S ((S (0)) * (ac))) /\ exists ff_q_pfp_polynomial_division_definitionsource. (ab) = ff_q_pfp_polynomial_division_definitionsource * S ((S (0)) * (ac)) + (pfm_leading_polynomial_division_definition))) /\ ((((~((pfm_leading_polynomial_division_definition) = 0)) /\ ((((exists pfa_gap_polynomial_division_definitioninversemultiplicationleft. pfa_gap_polynomial_division_definitioninversemultiplicationleft + S (pfm_leading_polynomial_division_definition) = ((p))) /\ (((exists pfa_gap_polynomial_division_definitioninversemultiplicationright. pfa_gap_polynomial_division_definitioninversemultiplicationright + S ((k)) = ((p))) /\ ((((exists pfa_gap_polynomial_division_definitioninversemultiplicationresultbound. pfa_gap_polynomial_division_definitioninversemultiplicationresultbound + S (1) = ((p))) /\ ((exists pfa_offset_left_polynomial_division_definitioninversemultiplicationresultcongruence pfa_offset_right_polynomial_division_definitioninversemultiplicationresultcongruence. ((pfm_leading_polynomial_division_definition) * ((k))) + ((p)) * pfa_offset_left_polynomial_division_definitioninversemultiplicationresultcongruence = (1) + ((p)) * pfa_offset_right_polynomial_division_definitioninversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_polynomial_division_definitionscalescalar. pfa_gap_polynomial_division_definitionscalescalar + S ((k)) = ((p))) /\ ((forall pfp_index_polynomial_division_definitionscale. (exists pfa_gap_polynomial_division_definitionscaleindex. pfa_gap_polynomial_division_definitionscaleindex + S (pfp_index_polynomial_division_definitionscale) = ((L))) -> exists pfp_source_polynomial_division_definitionscale pfp_value_polynomial_division_definitionscale. ((((exists ff_h_pfp_polynomial_division_definitionscalesource. ff_h_pfp_polynomial_division_definitionscalesource + S (pfp_source_polynomial_division_definitionscale) = S ((S (pfp_index_polynomial_division_definitionscale)) * (ac))) /\ exists ff_q_pfp_polynomial_division_definitionscalesource. (ab) = ff_q_pfp_polynomial_division_definitionscalesource * S ((S (pfp_index_polynomial_division_definitionscale)) * (ac)) + (pfp_source_polynomial_division_definitionscale))) /\ (((((exists ff_h_pfp_polynomial_division_definitionscaletarget. ff_h_pfp_polynomial_division_definitionscaletarget + S (pfp_value_polynomial_division_definitionscale) = S ((S (pfp_index_polynomial_division_definitionscale)) * (bc))) /\ exists ff_q_pfp_polynomial_division_definitionscaletarget. (bb) = ff_q_pfp_polynomial_division_definitionscaletarget * S ((S (pfp_index_polynomial_division_definitionscale)) * (bc)) + (pfp_value_polynomial_division_definitionscale))) /\ ((((exists pfa_gap_polynomial_division_definitionscaleoperationleft. pfa_gap_polynomial_division_definitionscaleoperationleft + S ((k)) = ((p))) /\ (((exists pfa_gap_polynomial_division_definitionscaleoperationright. pfa_gap_polynomial_division_definitionscaleoperationright + S (pfp_source_polynomial_division_definitionscale) = ((p))) /\ ((((exists pfa_gap_polynomial_division_definitionscaleoperationresultbound. pfa_gap_polynomial_division_definitionscaleoperationresultbound + S (pfp_value_polynomial_division_definitionscale) = ((p))) /\ ((exists pfa_offset_left_polynomial_division_definitionscaleoperationresultcongruence pfa_offset_right_polynomial_division_definitionscaleoperationresultcongruence. (((k)) * (pfp_source_polynomial_division_definitionscale)) + ((p)) * pfa_offset_left_polynomial_division_definitionscaleoperationresultcongruence = (pfp_value_polynomial_division_definitionscale) + ((p)) * pfa_offset_right_polynomial_division_definitionscaleoperationresultcongruence)))))))))))))))))))))

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