FpHorner(p,b,c,x,l,r)

exists pfh_trace_code_lowertier pfh_trace_scale_lowertier. (((exists pfa_gap_lowertiertracebase. pfa_gap_lowertiertracebase + S ((x)) = ((p))) /\ (((((exists ff_h_pfp_lowertiertraceinitial. ff_h_pfp_lowertiertraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_lowertier)) /\ exists ff_q_pfp_lowertiertraceinitial. pfh_trace_code_lowertier = ff_q_pfp_lowertiertraceinitial * S ((S (0)) * pfh_trace_scale_lowertier) + (0))) /\ (((((exists ff_h_pfp_lowertiertraceterminal. ff_h_pfp_lowertiertraceterminal + S ((r)) = S ((S ((l))) * pfh_trace_scale_lowertier)) /\ exists ff_q_pfp_lowertiertraceterminal. pfh_trace_code_lowertier = ff_q_pfp_lowertiertraceterminal * S ((S ((l))) * pfh_trace_scale_lowertier) + ((r)))) /\ ((forall pfh_index_lowertiertracesteps. (exists pfa_gap_lowertiertracestepsindex. pfa_gap_lowertiertracestepsindex + S (pfh_index_lowertiertracesteps) = ((l))) -> (exists pfh_coefficient_lowertiertracestepsstep pfh_before_lowertiertracestepsstep pfh_after_lowertiertracestepsstep pfh_product_lowertiertracestepsstep. ((((exists ff_h_pfp_lowertiertracestepsstepcoefficient. ff_h_pfp_lowertiertracestepsstepcoefficient + S (pfh_coefficient_lowertiertracestepsstep) = S ((S (pfh_index_lowertiertracesteps)) * (c))) /\ exists ff_q_pfp_lowertiertracestepsstepcoefficient. (b) = ff_q_pfp_lowertiertracestepsstepcoefficient * S ((S (pfh_index_lowertiertracesteps)) * (c)) + (pfh_coefficient_lowertiertracestepsstep))) /\ (((((exists ff_h_pfp_lowertiertracestepsstepbefore. ff_h_pfp_lowertiertracestepsstepbefore + S (pfh_before_lowertiertracestepsstep) = S ((S (pfh_index_lowertiertracesteps)) * pfh_trace_scale_lowertier)) /\ exists ff_q_pfp_lowertiertracestepsstepbefore. pfh_trace_code_lowertier = ff_q_pfp_lowertiertracestepsstepbefore * S ((S (pfh_index_lowertiertracesteps)) * pfh_trace_scale_lowertier) + (pfh_before_lowertiertracestepsstep))) /\ (((((exists ff_h_pfp_lowertiertracestepsstepafter. ff_h_pfp_lowertiertracestepsstepafter + S (pfh_after_lowertiertracestepsstep) = S ((S (S (pfh_index_lowertiertracesteps))) * pfh_trace_scale_lowertier)) /\ exists ff_q_pfp_lowertiertracestepsstepafter. pfh_trace_code_lowertier = ff_q_pfp_lowertiertracestepsstepafter * S ((S (S (pfh_index_lowertiertracesteps))) * pfh_trace_scale_lowertier) + (pfh_after_lowertiertracestepsstep))) /\ (((((exists pfa_gap_lowertiertracestepsstepmultiplyleft. pfa_gap_lowertiertracestepsstepmultiplyleft + S (pfh_before_lowertiertracestepsstep) = ((p))) /\ (((exists pfa_gap_lowertiertracestepsstepmultiplyright. pfa_gap_lowertiertracestepsstepmultiplyright + S ((x)) = ((p))) /\ ((((exists pfa_gap_lowertiertracestepsstepmultiplyresultbound. pfa_gap_lowertiertracestepsstepmultiplyresultbound + S (pfh_product_lowertiertracestepsstep) = ((p))) /\ ((exists pfa_offset_left_lowertiertracestepsstepmultiplyresultcongruence pfa_offset_right_lowertiertracestepsstepmultiplyresultcongruence. ((pfh_before_lowertiertracestepsstep) * ((x))) + ((p)) * pfa_offset_left_lowertiertracestepsstepmultiplyresultcongruence = (pfh_product_lowertiertracestepsstep) + ((p)) * pfa_offset_right_lowertiertracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_lowertiertracestepsstepaddleft. pfa_gap_lowertiertracestepsstepaddleft + S (pfh_product_lowertiertracestepsstep) = ((p))) /\ (((exists pfa_gap_lowertiertracestepsstepaddright. pfa_gap_lowertiertracestepsstepaddright + S (pfh_coefficient_lowertiertracestepsstep) = ((p))) /\ ((((exists pfa_gap_lowertiertracestepsstepaddresultbound. pfa_gap_lowertiertracestepsstepaddresultbound + S (pfh_after_lowertiertracestepsstep) = ((p))) /\ ((exists pfa_offset_left_lowertiertracestepsstepaddresultcongruence pfa_offset_right_lowertiertracestepsstepaddresultcongruence. ((pfh_product_lowertiertracestepsstep) + (pfh_coefficient_lowertiertracestepsstep)) + ((p)) * pfa_offset_left_lowertiertracestepsstepaddresultcongruence = (pfh_after_lowertiertracestepsstep) + ((p)) * pfa_offset_right_lowertiertracestepsstepaddresultcongruence))))))))))))))))))))))))))

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