prime_field_polynomial_horner_constant

Exact expanded first-order arithmetic statement

forall p b c t a. (~((p) = 1) /\ forall pfa_factor_left_constant_prime pfa_factor_right_constant_prime. (p) = pfa_factor_left_constant_prime * pfa_factor_right_constant_prime -> pfa_factor_left_constant_prime = 1 \/ pfa_factor_right_constant_prime = 1) -> (exists pfa_gap_constant_base. pfa_gap_constant_base + S (t) = (p)) -> (exists pfa_gap_constant_value. pfa_gap_constant_value + S (a) = (p)) -> (((exists ff_h_pfp_constant_coefficient. ff_h_pfp_constant_coefficient + S (a) = S ((S (0)) * c)) /\ exists ff_q_pfp_constant_coefficient. b = ff_q_pfp_constant_coefficient * S ((S (0)) * c) + (a))) -> (exists pfh_trace_code_constant_execution pfh_trace_scale_constant_execution. (((exists pfa_gap_constant_executiontracebase. pfa_gap_constant_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_constant_executiontraceinitial. ff_h_pfp_constant_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_constant_execution)) /\ exists ff_q_pfp_constant_executiontraceinitial. pfh_trace_code_constant_execution = ff_q_pfp_constant_executiontraceinitial * S ((S (0)) * pfh_trace_scale_constant_execution) + (0))) /\ (((((exists ff_h_pfp_constant_executiontraceterminal. ff_h_pfp_constant_executiontraceterminal + S (a) = S ((S (1)) * pfh_trace_scale_constant_execution)) /\ exists ff_q_pfp_constant_executiontraceterminal. pfh_trace_code_constant_execution = ff_q_pfp_constant_executiontraceterminal * S ((S (1)) * pfh_trace_scale_constant_execution) + (a))) /\ ((forall pfh_index_constant_executiontracesteps. (exists pfa_gap_constant_executiontracestepsindex. pfa_gap_constant_executiontracestepsindex + S (pfh_index_constant_executiontracesteps) = (1)) -> (exists pfh_coefficient_constant_executiontracestepsstep pfh_before_constant_executiontracestepsstep pfh_after_constant_executiontracestepsstep pfh_product_constant_executiontracestepsstep. ((((exists ff_h_pfp_constant_executiontracestepsstepcoefficient. ff_h_pfp_constant_executiontracestepsstepcoefficient + S (pfh_coefficient_constant_executiontracestepsstep) = S ((S (pfh_index_constant_executiontracesteps)) * c)) /\ exists ff_q_pfp_constant_executiontracestepsstepcoefficient. b = ff_q_pfp_constant_executiontracestepsstepcoefficient * S ((S (pfh_index_constant_executiontracesteps)) * c) + (pfh_coefficient_constant_executiontracestepsstep))) /\ (((((exists ff_h_pfp_constant_executiontracestepsstepbefore. ff_h_pfp_constant_executiontracestepsstepbefore + S (pfh_before_constant_executiontracestepsstep) = S ((S (pfh_index_constant_executiontracesteps)) * pfh_trace_scale_constant_execution)) /\ exists ff_q_pfp_constant_executiontracestepsstepbefore. pfh_trace_code_constant_execution = ff_q_pfp_constant_executiontracestepsstepbefore * S ((S (pfh_index_constant_executiontracesteps)) * pfh_trace_scale_constant_execution) + (pfh_before_constant_executiontracestepsstep))) /\ (((((exists ff_h_pfp_constant_executiontracestepsstepafter. ff_h_pfp_constant_executiontracestepsstepafter + S (pfh_after_constant_executiontracestepsstep) = S ((S (S (pfh_index_constant_executiontracesteps))) * pfh_trace_scale_constant_execution)) /\ exists ff_q_pfp_constant_executiontracestepsstepafter. pfh_trace_code_constant_execution = ff_q_pfp_constant_executiontracestepsstepafter * S ((S (S (pfh_index_constant_executiontracesteps))) * pfh_trace_scale_constant_execution) + (pfh_after_constant_executiontracestepsstep))) /\ (((((exists pfa_gap_constant_executiontracestepsstepmultiplyleft. pfa_gap_constant_executiontracestepsstepmultiplyleft + S (pfh_before_constant_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_constant_executiontracestepsstepmultiplyright. pfa_gap_constant_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_constant_executiontracestepsstepmultiplyresultbound. pfa_gap_constant_executiontracestepsstepmultiplyresultbound + S (pfh_product_constant_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_constant_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_constant_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_constant_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_constant_executiontracestepsstepmultiplyresultcongruence = (pfh_product_constant_executiontracestepsstep) + (p) * pfa_offset_right_constant_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_constant_executiontracestepsstepaddleft. pfa_gap_constant_executiontracestepsstepaddleft + S (pfh_product_constant_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_constant_executiontracestepsstepaddright. pfa_gap_constant_executiontracestepsstepaddright + S (pfh_coefficient_constant_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_constant_executiontracestepsstepaddresultbound. pfa_gap_constant_executiontracestepsstepaddresultbound + S (pfh_after_constant_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_constant_executiontracestepsstepaddresultcongruence pfa_offset_right_constant_executiontracestepsstepaddresultcongruence. ((pfh_product_constant_executiontracestepsstep) + (pfh_coefficient_constant_executiontracestepsstep)) + (p) * pfa_offset_left_constant_executiontracestepsstepaddresultcongruence = (pfh_after_constant_executiontracestepsstep) + (p) * pfa_offset_right_constant_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))