FpHornerSteps(p,b,c,x,l,u,v)

forall pfh_index_lowertier. (exists pfa_gap_lowertierindex. pfa_gap_lowertierindex + S (pfh_index_lowertier) = ((l))) -> (exists pfh_coefficient_lowertierstep pfh_before_lowertierstep pfh_after_lowertierstep pfh_product_lowertierstep. ((((exists ff_h_pfp_lowertierstepcoefficient. ff_h_pfp_lowertierstepcoefficient + S (pfh_coefficient_lowertierstep) = S ((S (pfh_index_lowertier)) * (c))) /\ exists ff_q_pfp_lowertierstepcoefficient. (b) = ff_q_pfp_lowertierstepcoefficient * S ((S (pfh_index_lowertier)) * (c)) + (pfh_coefficient_lowertierstep))) /\ (((((exists ff_h_pfp_lowertierstepbefore. ff_h_pfp_lowertierstepbefore + S (pfh_before_lowertierstep) = S ((S (pfh_index_lowertier)) * (v))) /\ exists ff_q_pfp_lowertierstepbefore. (u) = ff_q_pfp_lowertierstepbefore * S ((S (pfh_index_lowertier)) * (v)) + (pfh_before_lowertierstep))) /\ (((((exists ff_h_pfp_lowertierstepafter. ff_h_pfp_lowertierstepafter + S (pfh_after_lowertierstep) = S ((S (S (pfh_index_lowertier))) * (v))) /\ exists ff_q_pfp_lowertierstepafter. (u) = ff_q_pfp_lowertierstepafter * S ((S (S (pfh_index_lowertier))) * (v)) + (pfh_after_lowertierstep))) /\ (((((exists pfa_gap_lowertierstepmultiplyleft. pfa_gap_lowertierstepmultiplyleft + S (pfh_before_lowertierstep) = ((p))) /\ (((exists pfa_gap_lowertierstepmultiplyright. pfa_gap_lowertierstepmultiplyright + S ((x)) = ((p))) /\ ((((exists pfa_gap_lowertierstepmultiplyresultbound. pfa_gap_lowertierstepmultiplyresultbound + S (pfh_product_lowertierstep) = ((p))) /\ ((exists pfa_offset_left_lowertierstepmultiplyresultcongruence pfa_offset_right_lowertierstepmultiplyresultcongruence. ((pfh_before_lowertierstep) * ((x))) + ((p)) * pfa_offset_left_lowertierstepmultiplyresultcongruence = (pfh_product_lowertierstep) + ((p)) * pfa_offset_right_lowertierstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_lowertierstepaddleft. pfa_gap_lowertierstepaddleft + S (pfh_product_lowertierstep) = ((p))) /\ (((exists pfa_gap_lowertierstepaddright. pfa_gap_lowertierstepaddright + S (pfh_coefficient_lowertierstep) = ((p))) /\ ((((exists pfa_gap_lowertierstepaddresultbound. pfa_gap_lowertierstepaddresultbound + S (pfh_after_lowertierstep) = ((p))) /\ ((exists pfa_offset_left_lowertierstepaddresultcongruence pfa_offset_right_lowertierstepaddresultcongruence. ((pfh_product_lowertierstep) + (pfh_coefficient_lowertierstep)) + ((p)) * pfa_offset_left_lowertierstepaddresultcongruence = (pfh_after_lowertierstep) + ((p)) * pfa_offset_right_lowertierstepaddresultcongruence))))))))))))))))))

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