prime_field_polynomial_normalized_horner_iff

Exact expanded first-order arithmetic statement

forall p b c d e t l n r. (~((p) = 1) /\ forall pfa_factor_left_iff_prime pfa_factor_right_iff_prime. (p) = pfa_factor_left_iff_prime * pfa_factor_right_iff_prime -> pfa_factor_left_iff_prime = 1 \/ pfa_factor_right_iff_prime = 1) -> (forall pfp_index_iff_reduction. (exists pfa_gap_iff_reductionindex. pfa_gap_iff_reductionindex + S (pfp_index_iff_reduction) = (l)) -> exists pfp_source_iff_reduction pfp_residue_iff_reduction. ((((exists ff_h_pfp_iff_reductionsource. ff_h_pfp_iff_reductionsource + S (pfp_source_iff_reduction) = S ((S (pfp_index_iff_reduction)) * c)) /\ exists ff_q_pfp_iff_reductionsource. b = ff_q_pfp_iff_reductionsource * S ((S (pfp_index_iff_reduction)) * c) + (pfp_source_iff_reduction))) /\ (((((exists ff_h_pfp_iff_reductiontarget. ff_h_pfp_iff_reductiontarget + S (pfp_residue_iff_reduction) = S ((S (pfp_index_iff_reduction)) * e)) /\ exists ff_q_pfp_iff_reductiontarget. d = ff_q_pfp_iff_reductiontarget * S ((S (pfp_index_iff_reduction)) * e) + (pfp_residue_iff_reduction))) /\ ((((exists pfa_gap_iff_reductionresiduebound. pfa_gap_iff_reductionresiduebound + S (pfp_residue_iff_reduction) = (p)) /\ ((exists pfa_offset_left_iff_reductionresiduecongruence pfa_offset_right_iff_reductionresiduecongruence. (pfp_source_iff_reduction) + (p) * pfa_offset_left_iff_reductionresiduecongruence = (pfp_residue_iff_reduction) + (p) * pfa_offset_right_iff_reductionresiduecongruence))))))))) -> (exists pfa_gap_iff_base. pfa_gap_iff_base + S (t) = (p)) -> (exists ff_u_ph_pfh_iff_natural ff_v_ph_pfh_iff_natural. ((((exists fs_h_ph_pfh_iff_natural_body_start. fs_h_ph_pfh_iff_natural_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_iff_natural)) /\ exists fs_q_ph_pfh_iff_natural_body_start. ff_u_ph_pfh_iff_natural = fs_q_ph_pfh_iff_natural_body_start * S ((S (0)) * ff_v_ph_pfh_iff_natural) + (0))) /\ ((((exists fs_h_ph_pfh_iff_natural_body_terminal. fs_h_ph_pfh_iff_natural_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pfh_iff_natural)) /\ exists fs_q_ph_pfh_iff_natural_body_terminal. ff_u_ph_pfh_iff_natural = fs_q_ph_pfh_iff_natural_body_terminal * S ((S (l)) * ff_v_ph_pfh_iff_natural) + (n))) /\ forall ff_i_ph_pfh_iff_natural_body_steps. (exists ph_bound_pfh_iff_natural_body_steps. ph_bound_pfh_iff_natural_body_steps + S ff_i_ph_pfh_iff_natural_body_steps = l) -> exists ff_coefficient_ph_pfh_iff_natural_body_steps ff_previous_ph_pfh_iff_natural_body_steps ff_current_ph_pfh_iff_natural_body_steps. ((((exists fs_h_ph_pfh_iff_natural_body_steps_coefficient. fs_h_ph_pfh_iff_natural_body_steps_coefficient + S (ff_coefficient_ph_pfh_iff_natural_body_steps) = S ((S (ff_i_ph_pfh_iff_natural_body_steps)) * c)) /\ exists fs_q_ph_pfh_iff_natural_body_steps_coefficient. b = fs_q_ph_pfh_iff_natural_body_steps_coefficient * S ((S (ff_i_ph_pfh_iff_natural_body_steps)) * c) + (ff_coefficient_ph_pfh_iff_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_iff_natural_body_steps_before. fs_h_ph_pfh_iff_natural_body_steps_before + S (ff_previous_ph_pfh_iff_natural_body_steps) = S ((S (ff_i_ph_pfh_iff_natural_body_steps)) * ff_v_ph_pfh_iff_natural)) /\ exists fs_q_ph_pfh_iff_natural_body_steps_before. ff_u_ph_pfh_iff_natural = fs_q_ph_pfh_iff_natural_body_steps_before * S ((S (ff_i_ph_pfh_iff_natural_body_steps)) * ff_v_ph_pfh_iff_natural) + (ff_previous_ph_pfh_iff_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_iff_natural_body_steps_after. fs_h_ph_pfh_iff_natural_body_steps_after + S (ff_current_ph_pfh_iff_natural_body_steps) = S ((S (S ff_i_ph_pfh_iff_natural_body_steps)) * ff_v_ph_pfh_iff_natural)) /\ exists fs_q_ph_pfh_iff_natural_body_steps_after. ff_u_ph_pfh_iff_natural = fs_q_ph_pfh_iff_natural_body_steps_after * S ((S (S ff_i_ph_pfh_iff_natural_body_steps)) * ff_v_ph_pfh_iff_natural) + (ff_current_ph_pfh_iff_natural_body_steps))) /\ ff_current_ph_pfh_iff_natural_body_steps = ff_previous_ph_pfh_iff_natural_body_steps * t + ff_coefficient_ph_pfh_iff_natural_body_steps)))))) -> (((exists pfh_trace_code_iff_execution_forward pfh_trace_scale_iff_execution_forward. (((exists pfa_gap_iff_execution_forwardtracebase. pfa_gap_iff_execution_forwardtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_iff_execution_forwardtraceinitial. ff_h_pfp_iff_execution_forwardtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_iff_execution_forward)) /\ exists ff_q_pfp_iff_execution_forwardtraceinitial. pfh_trace_code_iff_execution_forward = ff_q_pfp_iff_execution_forwardtraceinitial * S ((S (0)) * pfh_trace_scale_iff_execution_forward) + (0))) /\ (((((exists ff_h_pfp_iff_execution_forwardtraceterminal. ff_h_pfp_iff_execution_forwardtraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_iff_execution_forward)) /\ exists ff_q_pfp_iff_execution_forwardtraceterminal. pfh_trace_code_iff_execution_forward = ff_q_pfp_iff_execution_forwardtraceterminal * S ((S (l)) * pfh_trace_scale_iff_execution_forward) + (r))) /\ ((forall pfh_index_iff_execution_forwardtracesteps. (exists pfa_gap_iff_execution_forwardtracestepsindex. pfa_gap_iff_execution_forwardtracestepsindex + S (pfh_index_iff_execution_forwardtracesteps) = (l)) -> (exists pfh_coefficient_iff_execution_forwardtracestepsstep pfh_before_iff_execution_forwardtracestepsstep pfh_after_iff_execution_forwardtracestepsstep pfh_product_iff_execution_forwardtracestepsstep. ((((exists ff_h_pfp_iff_execution_forwardtracestepsstepcoefficient. ff_h_pfp_iff_execution_forwardtracestepsstepcoefficient + S (pfh_coefficient_iff_execution_forwardtracestepsstep) = S ((S (pfh_index_iff_execution_forwardtracesteps)) * e)) /\ exists ff_q_pfp_iff_execution_forwardtracestepsstepcoefficient. d = ff_q_pfp_iff_execution_forwardtracestepsstepcoefficient * S ((S (pfh_index_iff_execution_forwardtracesteps)) * e) + (pfh_coefficient_iff_execution_forwardtracestepsstep))) /\ (((((exists ff_h_pfp_iff_execution_forwardtracestepsstepbefore. ff_h_pfp_iff_execution_forwardtracestepsstepbefore + S (pfh_before_iff_execution_forwardtracestepsstep) = S ((S (pfh_index_iff_execution_forwardtracesteps)) * pfh_trace_scale_iff_execution_forward)) /\ exists ff_q_pfp_iff_execution_forwardtracestepsstepbefore. pfh_trace_code_iff_execution_forward = ff_q_pfp_iff_execution_forwardtracestepsstepbefore * S ((S (pfh_index_iff_execution_forwardtracesteps)) * pfh_trace_scale_iff_execution_forward) + (pfh_before_iff_execution_forwardtracestepsstep))) /\ (((((exists ff_h_pfp_iff_execution_forwardtracestepsstepafter. ff_h_pfp_iff_execution_forwardtracestepsstepafter + S (pfh_after_iff_execution_forwardtracestepsstep) = S ((S (S (pfh_index_iff_execution_forwardtracesteps))) * pfh_trace_scale_iff_execution_forward)) /\ exists ff_q_pfp_iff_execution_forwardtracestepsstepafter. pfh_trace_code_iff_execution_forward = ff_q_pfp_iff_execution_forwardtracestepsstepafter * S ((S (S (pfh_index_iff_execution_forwardtracesteps))) * pfh_trace_scale_iff_execution_forward) + (pfh_after_iff_execution_forwardtracestepsstep))) /\ (((((exists pfa_gap_iff_execution_forwardtracestepsstepmultiplyleft. pfa_gap_iff_execution_forwardtracestepsstepmultiplyleft + S (pfh_before_iff_execution_forwardtracestepsstep) = (p)) /\ (((exists pfa_gap_iff_execution_forwardtracestepsstepmultiplyright. pfa_gap_iff_execution_forwardtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_iff_execution_forwardtracestepsstepmultiplyresultbound. pfa_gap_iff_execution_forwardtracestepsstepmultiplyresultbound + S (pfh_product_iff_execution_forwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_iff_execution_forwardtracestepsstepmultiplyresultcongruence pfa_offset_right_iff_execution_forwardtracestepsstepmultiplyresultcongruence. ((pfh_before_iff_execution_forwardtracestepsstep) * (t)) + (p) * pfa_offset_left_iff_execution_forwardtracestepsstepmultiplyresultcongruence = (pfh_product_iff_execution_forwardtracestepsstep) + (p) * pfa_offset_right_iff_execution_forwardtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_iff_execution_forwardtracestepsstepaddleft. pfa_gap_iff_execution_forwardtracestepsstepaddleft + S (pfh_product_iff_execution_forwardtracestepsstep) = (p)) /\ (((exists pfa_gap_iff_execution_forwardtracestepsstepaddright. pfa_gap_iff_execution_forwardtracestepsstepaddright + S (pfh_coefficient_iff_execution_forwardtracestepsstep) = (p)) /\ ((((exists pfa_gap_iff_execution_forwardtracestepsstepaddresultbound. pfa_gap_iff_execution_forwardtracestepsstepaddresultbound + S (pfh_after_iff_execution_forwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_iff_execution_forwardtracestepsstepaddresultcongruence pfa_offset_right_iff_execution_forwardtracestepsstepaddresultcongruence. ((pfh_product_iff_execution_forwardtracestepsstep) + (pfh_coefficient_iff_execution_forwardtracestepsstep)) + (p) * pfa_offset_left_iff_execution_forwardtracestepsstepaddresultcongruence = (pfh_after_iff_execution_forwardtracestepsstep) + (p) * pfa_offset_right_iff_execution_forwardtracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> (((exists pfa_gap_iff_residue_forwardbound. pfa_gap_iff_residue_forwardbound + S (r) = (p)) /\ ((exists pfa_offset_left_iff_residue_forwardcongruence pfa_offset_right_iff_residue_forwardcongruence. (n) + (p) * pfa_offset_left_iff_residue_forwardcongruence = (r) + (p) * pfa_offset_right_iff_residue_forwardcongruence))))) /\ (((((exists pfa_gap_iff_residue_backwardbound. pfa_gap_iff_residue_backwardbound + S (r) = (p)) /\ ((exists pfa_offset_left_iff_residue_backwardcongruence pfa_offset_right_iff_residue_backwardcongruence. (n) + (p) * pfa_offset_left_iff_residue_backwardcongruence = (r) + (p) * pfa_offset_right_iff_residue_backwardcongruence)))) -> (exists pfh_trace_code_iff_execution_backward pfh_trace_scale_iff_execution_backward. (((exists pfa_gap_iff_execution_backwardtracebase. pfa_gap_iff_execution_backwardtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_iff_execution_backwardtraceinitial. ff_h_pfp_iff_execution_backwardtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_iff_execution_backward)) /\ exists ff_q_pfp_iff_execution_backwardtraceinitial. pfh_trace_code_iff_execution_backward = ff_q_pfp_iff_execution_backwardtraceinitial * S ((S (0)) * pfh_trace_scale_iff_execution_backward) + (0))) /\ (((((exists ff_h_pfp_iff_execution_backwardtraceterminal. ff_h_pfp_iff_execution_backwardtraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_iff_execution_backward)) /\ exists ff_q_pfp_iff_execution_backwardtraceterminal. pfh_trace_code_iff_execution_backward = ff_q_pfp_iff_execution_backwardtraceterminal * S ((S (l)) * pfh_trace_scale_iff_execution_backward) + (r))) /\ ((forall pfh_index_iff_execution_backwardtracesteps. (exists pfa_gap_iff_execution_backwardtracestepsindex. pfa_gap_iff_execution_backwardtracestepsindex + S (pfh_index_iff_execution_backwardtracesteps) = (l)) -> (exists pfh_coefficient_iff_execution_backwardtracestepsstep pfh_before_iff_execution_backwardtracestepsstep pfh_after_iff_execution_backwardtracestepsstep pfh_product_iff_execution_backwardtracestepsstep. ((((exists ff_h_pfp_iff_execution_backwardtracestepsstepcoefficient. ff_h_pfp_iff_execution_backwardtracestepsstepcoefficient + S (pfh_coefficient_iff_execution_backwardtracestepsstep) = S ((S (pfh_index_iff_execution_backwardtracesteps)) * e)) /\ exists ff_q_pfp_iff_execution_backwardtracestepsstepcoefficient. d = ff_q_pfp_iff_execution_backwardtracestepsstepcoefficient * S ((S (pfh_index_iff_execution_backwardtracesteps)) * e) + (pfh_coefficient_iff_execution_backwardtracestepsstep))) /\ (((((exists ff_h_pfp_iff_execution_backwardtracestepsstepbefore. ff_h_pfp_iff_execution_backwardtracestepsstepbefore + S (pfh_before_iff_execution_backwardtracestepsstep) = S ((S (pfh_index_iff_execution_backwardtracesteps)) * pfh_trace_scale_iff_execution_backward)) /\ exists ff_q_pfp_iff_execution_backwardtracestepsstepbefore. pfh_trace_code_iff_execution_backward = ff_q_pfp_iff_execution_backwardtracestepsstepbefore * S ((S (pfh_index_iff_execution_backwardtracesteps)) * pfh_trace_scale_iff_execution_backward) + (pfh_before_iff_execution_backwardtracestepsstep))) /\ (((((exists ff_h_pfp_iff_execution_backwardtracestepsstepafter. ff_h_pfp_iff_execution_backwardtracestepsstepafter + S (pfh_after_iff_execution_backwardtracestepsstep) = S ((S (S (pfh_index_iff_execution_backwardtracesteps))) * pfh_trace_scale_iff_execution_backward)) /\ exists ff_q_pfp_iff_execution_backwardtracestepsstepafter. pfh_trace_code_iff_execution_backward = ff_q_pfp_iff_execution_backwardtracestepsstepafter * S ((S (S (pfh_index_iff_execution_backwardtracesteps))) * pfh_trace_scale_iff_execution_backward) + (pfh_after_iff_execution_backwardtracestepsstep))) /\ (((((exists pfa_gap_iff_execution_backwardtracestepsstepmultiplyleft. pfa_gap_iff_execution_backwardtracestepsstepmultiplyleft + S (pfh_before_iff_execution_backwardtracestepsstep) = (p)) /\ (((exists pfa_gap_iff_execution_backwardtracestepsstepmultiplyright. pfa_gap_iff_execution_backwardtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_iff_execution_backwardtracestepsstepmultiplyresultbound. pfa_gap_iff_execution_backwardtracestepsstepmultiplyresultbound + S (pfh_product_iff_execution_backwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_iff_execution_backwardtracestepsstepmultiplyresultcongruence pfa_offset_right_iff_execution_backwardtracestepsstepmultiplyresultcongruence. ((pfh_before_iff_execution_backwardtracestepsstep) * (t)) + (p) * pfa_offset_left_iff_execution_backwardtracestepsstepmultiplyresultcongruence = (pfh_product_iff_execution_backwardtracestepsstep) + (p) * pfa_offset_right_iff_execution_backwardtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_iff_execution_backwardtracestepsstepaddleft. pfa_gap_iff_execution_backwardtracestepsstepaddleft + S (pfh_product_iff_execution_backwardtracestepsstep) = (p)) /\ (((exists pfa_gap_iff_execution_backwardtracestepsstepaddright. pfa_gap_iff_execution_backwardtracestepsstepaddright + S (pfh_coefficient_iff_execution_backwardtracestepsstep) = (p)) /\ ((((exists pfa_gap_iff_execution_backwardtracestepsstepaddresultbound. pfa_gap_iff_execution_backwardtracestepsstepaddresultbound + S (pfh_after_iff_execution_backwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_iff_execution_backwardtracestepsstepaddresultcongruence pfa_offset_right_iff_execution_backwardtracestepsstepaddresultcongruence. ((pfh_product_iff_execution_backwardtracestepsstep) + (pfh_coefficient_iff_execution_backwardtracestepsstep)) + (p) * pfa_offset_left_iff_execution_backwardtracestepsstepaddresultcongruence = (pfh_after_iff_execution_backwardtracestepsstep) + (p) * pfa_offset_right_iff_execution_backwardtracestepsstepaddresultcongruence))))))))))))))))))))))))))))))