prime_field_polynomial_synthetic_final_coefficient

Exact expanded first-order arithmetic statement

forall p b c a n qb qc r h v. (~((p) = 1) /\ forall pfa_factor_left_final_prime pfa_factor_right_final_prime. (p) = pfa_factor_left_final_prime * pfa_factor_right_final_prime -> pfa_factor_left_final_prime = 1 \/ pfa_factor_right_final_prime = 1) -> (exists pfs_history_code_final_division pfs_history_scale_final_division. ((((exists pfa_gap_final_divisiontracebase. pfa_gap_final_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_final_divisiontraceinitial. ff_h_pfp_final_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontraceinitial. pfs_history_code_final_division = ff_q_pfp_final_divisiontraceinitial * S ((S (0)) * pfs_history_scale_final_division) + (0))) /\ (((((exists ff_h_pfp_final_divisiontraceterminal. ff_h_pfp_final_divisiontraceterminal + S (r) = S ((S (S (S n))) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontraceterminal. pfs_history_code_final_division = ff_q_pfp_final_divisiontraceterminal * S ((S (S (S n))) * pfs_history_scale_final_division) + (r))) /\ ((forall pfh_index_final_divisiontracesteps. (exists pfa_gap_final_divisiontracestepsindex. pfa_gap_final_divisiontracestepsindex + S (pfh_index_final_divisiontracesteps) = (S (S n))) -> (exists pfh_coefficient_final_divisiontracestepsstep pfh_before_final_divisiontracestepsstep pfh_after_final_divisiontracestepsstep pfh_product_final_divisiontracestepsstep. ((((exists ff_h_pfp_final_divisiontracestepsstepcoefficient. ff_h_pfp_final_divisiontracestepsstepcoefficient + S (pfh_coefficient_final_divisiontracestepsstep) = S ((S (pfh_index_final_divisiontracesteps)) * c)) /\ exists ff_q_pfp_final_divisiontracestepsstepcoefficient. b = ff_q_pfp_final_divisiontracestepsstepcoefficient * S ((S (pfh_index_final_divisiontracesteps)) * c) + (pfh_coefficient_final_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_final_divisiontracestepsstepbefore. ff_h_pfp_final_divisiontracestepsstepbefore + S (pfh_before_final_divisiontracestepsstep) = S ((S (pfh_index_final_divisiontracesteps)) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontracestepsstepbefore. pfs_history_code_final_division = ff_q_pfp_final_divisiontracestepsstepbefore * S ((S (pfh_index_final_divisiontracesteps)) * pfs_history_scale_final_division) + (pfh_before_final_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_final_divisiontracestepsstepafter. ff_h_pfp_final_divisiontracestepsstepafter + S (pfh_after_final_divisiontracestepsstep) = S ((S (S (pfh_index_final_divisiontracesteps))) * pfs_history_scale_final_division)) /\ exists ff_q_pfp_final_divisiontracestepsstepafter. pfs_history_code_final_division = ff_q_pfp_final_divisiontracestepsstepafter * S ((S (S (pfh_index_final_divisiontracesteps))) * pfs_history_scale_final_division) + (pfh_after_final_divisiontracestepsstep))) /\ (((((exists pfa_gap_final_divisiontracestepsstepmultiplyleft. pfa_gap_final_divisiontracestepsstepmultiplyleft + S (pfh_before_final_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_final_divisiontracestepsstepmultiplyright. pfa_gap_final_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_final_divisiontracestepsstepmultiplyresultbound. pfa_gap_final_divisiontracestepsstepmultiplyresultbound + S (pfh_product_final_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_final_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_final_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_final_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_final_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_final_divisiontracestepsstep) + (p) * pfa_offset_right_final_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_final_divisiontracestepsstepaddleft. pfa_gap_final_divisiontracestepsstepaddleft + S (pfh_product_final_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_final_divisiontracestepsstepaddright. pfa_gap_final_divisiontracestepsstepaddright + S (pfh_coefficient_final_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_final_divisiontracestepsstepaddresultbound. pfa_gap_final_divisiontracestepsstepaddresultbound + S (pfh_after_final_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_final_divisiontracestepsstepaddresultcongruence pfa_offset_right_final_divisiontracestepsstepaddresultcongruence. ((pfh_product_final_divisiontracestepsstep) + (pfh_coefficient_final_divisiontracestepsstep)) + (p) * pfa_offset_left_final_divisiontracestepsstepaddresultcongruence = (pfh_after_final_divisiontracestepsstep) + (p) * pfa_offset_right_final_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_final_divisionquotient ff_source_mcp_pfs_final_divisionquotient ff_target_mcp_pfs_final_divisionquotient. (exists mcp_gap_pfs_final_divisionquotient_bound. mcp_gap_pfs_final_divisionquotient_bound + S (ff_index_mcp_pfs_final_divisionquotient) = (S n)) -> (((exists fs_h_mcp_pfs_final_divisionquotient_source. fs_h_mcp_pfs_final_divisionquotient_source + S (ff_source_mcp_pfs_final_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_final_divisionquotient)) * pfs_history_scale_final_division)) /\ exists fs_q_mcp_pfs_final_divisionquotient_source. pfs_history_code_final_division = fs_q_mcp_pfs_final_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_final_divisionquotient)) * pfs_history_scale_final_division) + (ff_source_mcp_pfs_final_divisionquotient))) -> (((exists fs_h_mcp_pfs_final_divisionquotient_target. fs_h_mcp_pfs_final_divisionquotient_target + S (ff_target_mcp_pfs_final_divisionquotient) = S ((S (ff_index_mcp_pfs_final_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_final_divisionquotient_target. qb = fs_q_mcp_pfs_final_divisionquotient_target * S ((S (ff_index_mcp_pfs_final_divisionquotient)) * qc) + (ff_target_mcp_pfs_final_divisionquotient))) -> ff_target_mcp_pfs_final_divisionquotient = ff_source_mcp_pfs_final_divisionquotient)))) -> (((exists ff_h_pfp_final_quotient. ff_h_pfp_final_quotient + S (h) = S ((S (n)) * qc)) /\ exists ff_q_pfp_final_quotient. qb = ff_q_pfp_final_quotient * S ((S (n)) * qc) + (h))) -> (((exists ff_h_pfp_final_input. ff_h_pfp_final_input + S (v) = S ((S (S n)) * c)) /\ exists ff_q_pfp_final_input. b = ff_q_pfp_final_input * S ((S (S n)) * c) + (v))) -> exists k. ((((exists pfa_gap_final_productleft. pfa_gap_final_productleft + S (h) = (p)) /\ (((exists pfa_gap_final_productright. pfa_gap_final_productright + S (a) = (p)) /\ ((((exists pfa_gap_final_productresultbound. pfa_gap_final_productresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_final_productresultcongruence pfa_offset_right_final_productresultcongruence. ((h) * (a)) + (p) * pfa_offset_left_final_productresultcongruence = (k) + (p) * pfa_offset_right_final_productresultcongruence))))))))) /\ ((((exists pfa_gap_final_sumleft. pfa_gap_final_sumleft + S (k) = (p)) /\ (((exists pfa_gap_final_sumright. pfa_gap_final_sumright + S (v) = (p)) /\ ((((exists pfa_gap_final_sumresultbound. pfa_gap_final_sumresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_final_sumresultcongruence pfa_offset_right_final_sumresultcongruence. ((k) + (v)) + (p) * pfa_offset_left_final_sumresultcongruence = (r) + (p) * pfa_offset_right_final_sumresultcongruence)))))))))))