FpPolynomialTrim(p,b,c,L,t,d,e,M)

((((L))=((t))+((M))) /\ (((forall fom_index_pfp_polynomial_division_definitioninput. (exists fom_gap_pfp_polynomial_division_definitioninput_index_bound. fom_gap_pfp_polynomial_division_definitioninput_index_bound + S (fom_index_pfp_polynomial_division_definitioninput) = (L)) -> exists fom_value_pfp_polynomial_division_definitioninput. ((((exists fom_beta_height_pfp_polynomial_division_definitioninput_entry. fom_beta_height_pfp_polynomial_division_definitioninput_entry + S (fom_value_pfp_polynomial_division_definitioninput) = S ((S (fom_index_pfp_polynomial_division_definitioninput)) * (c))) /\ exists fom_beta_quotient_pfp_polynomial_division_definitioninput_entry. (b) = fom_beta_quotient_pfp_polynomial_division_definitioninput_entry * S ((S (fom_index_pfp_polynomial_division_definitioninput)) * (c)) + (fom_value_pfp_polynomial_division_definitioninput))) /\ (exists fom_gap_pfp_polynomial_division_definitioninput_value_bound. fom_gap_pfp_polynomial_division_definitioninput_value_bound + S (fom_value_pfp_polynomial_division_definitioninput) = (p)))) /\ (((forall pfp_repeat_index_polynomial_division_definitionremoved. (exists pfa_gap_polynomial_division_definitionremovedindex. pfa_gap_polynomial_division_definitionremovedindex + S (pfp_repeat_index_polynomial_division_definitionremoved) = ((t))) -> (((exists ff_h_pfp_polynomial_division_definitionremovedentry. ff_h_pfp_polynomial_division_definitionremovedentry + S (0) = S ((S (pfp_repeat_index_polynomial_division_definitionremoved)) * (c))) /\ exists ff_q_pfp_polynomial_division_definitionremovedentry. (b) = ff_q_pfp_polynomial_division_definitionremovedentry * S ((S (pfp_repeat_index_polynomial_division_definitionremoved)) * (c)) + (0)))) /\ (((forall pftrim_index_polynomial_division_definitionsuffix pftrim_value_polynomial_division_definitionsuffix. (exists pfa_gap_polynomial_division_definitionsuffixbound. pfa_gap_polynomial_division_definitionsuffixbound + S (pftrim_index_polynomial_division_definitionsuffix) = ((M))) -> (((exists ff_h_pfp_polynomial_division_definitionsuffixsource. ff_h_pfp_polynomial_division_definitionsuffixsource + S (pftrim_value_polynomial_division_definitionsuffix) = S ((S (((t))+pftrim_index_polynomial_division_definitionsuffix)) * (c))) /\ exists ff_q_pfp_polynomial_division_definitionsuffixsource. (b) = ff_q_pfp_polynomial_division_definitionsuffixsource * S ((S (((t))+pftrim_index_polynomial_division_definitionsuffix)) * (c)) + (pftrim_value_polynomial_division_definitionsuffix))) -> (((exists ff_h_pfp_polynomial_division_definitionsuffixoutput. ff_h_pfp_polynomial_division_definitionsuffixoutput + S (pftrim_value_polynomial_division_definitionsuffix) = S ((S (pftrim_index_polynomial_division_definitionsuffix)) * (e))) /\ exists ff_q_pfp_polynomial_division_definitionsuffixoutput. (d) = ff_q_pfp_polynomial_division_definitionsuffixoutput * S ((S (pftrim_index_polynomial_division_definitionsuffix)) * (e)) + (pftrim_value_polynomial_division_definitionsuffix)))) /\ ((((M))=0 \/ (exists pftrim_leading_polynomial_division_definitionnormal. ((((exists ff_h_pfp_polynomial_division_definitionnormalentry. ff_h_pfp_polynomial_division_definitionnormalentry + S (pftrim_leading_polynomial_division_definitionnormal) = S ((S (0)) * (e))) /\ exists ff_q_pfp_polynomial_division_definitionnormalentry. (d) = ff_q_pfp_polynomial_division_definitionnormalentry * S ((S (0)) * (e)) + (pftrim_leading_polynomial_division_definitionnormal))) /\ ((~(pftrim_leading_polynomial_division_definitionnormal=0))))))))))))))

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