prime_field_polynomial_synthetic_middle_coefficients

Exact expanded first-order arithmetic statement

forall p b c a n qb qc r i h j v. (~((p) = 1) /\ forall pfa_factor_left_middle_prime pfa_factor_right_middle_prime. (p) = pfa_factor_left_middle_prime * pfa_factor_right_middle_prime -> pfa_factor_left_middle_prime = 1 \/ pfa_factor_right_middle_prime = 1) -> (exists pfs_history_code_middle_division pfs_history_scale_middle_division. ((((exists pfa_gap_middle_divisiontracebase. pfa_gap_middle_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_middle_divisiontraceinitial. ff_h_pfp_middle_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontraceinitial. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontraceinitial * S ((S (0)) * pfs_history_scale_middle_division) + (0))) /\ (((((exists ff_h_pfp_middle_divisiontraceterminal. ff_h_pfp_middle_divisiontraceterminal + S (r) = S ((S (S (S n))) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontraceterminal. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontraceterminal * S ((S (S (S n))) * pfs_history_scale_middle_division) + (r))) /\ ((forall pfh_index_middle_divisiontracesteps. (exists pfa_gap_middle_divisiontracestepsindex. pfa_gap_middle_divisiontracestepsindex + S (pfh_index_middle_divisiontracesteps) = (S (S n))) -> (exists pfh_coefficient_middle_divisiontracestepsstep pfh_before_middle_divisiontracestepsstep pfh_after_middle_divisiontracestepsstep pfh_product_middle_divisiontracestepsstep. ((((exists ff_h_pfp_middle_divisiontracestepsstepcoefficient. ff_h_pfp_middle_divisiontracestepsstepcoefficient + S (pfh_coefficient_middle_divisiontracestepsstep) = S ((S (pfh_index_middle_divisiontracesteps)) * c)) /\ exists ff_q_pfp_middle_divisiontracestepsstepcoefficient. b = ff_q_pfp_middle_divisiontracestepsstepcoefficient * S ((S (pfh_index_middle_divisiontracesteps)) * c) + (pfh_coefficient_middle_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_middle_divisiontracestepsstepbefore. ff_h_pfp_middle_divisiontracestepsstepbefore + S (pfh_before_middle_divisiontracestepsstep) = S ((S (pfh_index_middle_divisiontracesteps)) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontracestepsstepbefore. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontracestepsstepbefore * S ((S (pfh_index_middle_divisiontracesteps)) * pfs_history_scale_middle_division) + (pfh_before_middle_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_middle_divisiontracestepsstepafter. ff_h_pfp_middle_divisiontracestepsstepafter + S (pfh_after_middle_divisiontracestepsstep) = S ((S (S (pfh_index_middle_divisiontracesteps))) * pfs_history_scale_middle_division)) /\ exists ff_q_pfp_middle_divisiontracestepsstepafter. pfs_history_code_middle_division = ff_q_pfp_middle_divisiontracestepsstepafter * S ((S (S (pfh_index_middle_divisiontracesteps))) * pfs_history_scale_middle_division) + (pfh_after_middle_divisiontracestepsstep))) /\ (((((exists pfa_gap_middle_divisiontracestepsstepmultiplyleft. pfa_gap_middle_divisiontracestepsstepmultiplyleft + S (pfh_before_middle_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_middle_divisiontracestepsstepmultiplyright. pfa_gap_middle_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_middle_divisiontracestepsstepmultiplyresultbound. pfa_gap_middle_divisiontracestepsstepmultiplyresultbound + S (pfh_product_middle_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_middle_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_middle_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_middle_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_middle_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_middle_divisiontracestepsstep) + (p) * pfa_offset_right_middle_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_middle_divisiontracestepsstepaddleft. pfa_gap_middle_divisiontracestepsstepaddleft + S (pfh_product_middle_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_middle_divisiontracestepsstepaddright. pfa_gap_middle_divisiontracestepsstepaddright + S (pfh_coefficient_middle_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_middle_divisiontracestepsstepaddresultbound. pfa_gap_middle_divisiontracestepsstepaddresultbound + S (pfh_after_middle_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_middle_divisiontracestepsstepaddresultcongruence pfa_offset_right_middle_divisiontracestepsstepaddresultcongruence. ((pfh_product_middle_divisiontracestepsstep) + (pfh_coefficient_middle_divisiontracestepsstep)) + (p) * pfa_offset_left_middle_divisiontracestepsstepaddresultcongruence = (pfh_after_middle_divisiontracestepsstep) + (p) * pfa_offset_right_middle_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_middle_divisionquotient ff_source_mcp_pfs_middle_divisionquotient ff_target_mcp_pfs_middle_divisionquotient. (exists mcp_gap_pfs_middle_divisionquotient_bound. mcp_gap_pfs_middle_divisionquotient_bound + S (ff_index_mcp_pfs_middle_divisionquotient) = (S n)) -> (((exists fs_h_mcp_pfs_middle_divisionquotient_source. fs_h_mcp_pfs_middle_divisionquotient_source + S (ff_source_mcp_pfs_middle_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_middle_divisionquotient)) * pfs_history_scale_middle_division)) /\ exists fs_q_mcp_pfs_middle_divisionquotient_source. pfs_history_code_middle_division = fs_q_mcp_pfs_middle_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_middle_divisionquotient)) * pfs_history_scale_middle_division) + (ff_source_mcp_pfs_middle_divisionquotient))) -> (((exists fs_h_mcp_pfs_middle_divisionquotient_target. fs_h_mcp_pfs_middle_divisionquotient_target + S (ff_target_mcp_pfs_middle_divisionquotient) = S ((S (ff_index_mcp_pfs_middle_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_middle_divisionquotient_target. qb = fs_q_mcp_pfs_middle_divisionquotient_target * S ((S (ff_index_mcp_pfs_middle_divisionquotient)) * qc) + (ff_target_mcp_pfs_middle_divisionquotient))) -> ff_target_mcp_pfs_middle_divisionquotient = ff_source_mcp_pfs_middle_divisionquotient)))) -> (exists pfa_gap_middle_index. pfa_gap_middle_index + S (i) = (n)) -> (((exists ff_h_pfp_middle_previous. ff_h_pfp_middle_previous + S (h) = S ((S (i)) * qc)) /\ exists ff_q_pfp_middle_previous. qb = ff_q_pfp_middle_previous * S ((S (i)) * qc) + (h))) -> (((exists ff_h_pfp_middle_next. ff_h_pfp_middle_next + S (j) = S ((S (S i)) * qc)) /\ exists ff_q_pfp_middle_next. qb = ff_q_pfp_middle_next * S ((S (S i)) * qc) + (j))) -> (((exists ff_h_pfp_middle_input. ff_h_pfp_middle_input + S (v) = S ((S (S i)) * c)) /\ exists ff_q_pfp_middle_input. b = ff_q_pfp_middle_input * S ((S (S i)) * c) + (v))) -> exists k. ((((exists pfa_gap_middle_productleft. pfa_gap_middle_productleft + S (h) = (p)) /\ (((exists pfa_gap_middle_productright. pfa_gap_middle_productright + S (a) = (p)) /\ ((((exists pfa_gap_middle_productresultbound. pfa_gap_middle_productresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_middle_productresultcongruence pfa_offset_right_middle_productresultcongruence. ((h) * (a)) + (p) * pfa_offset_left_middle_productresultcongruence = (k) + (p) * pfa_offset_right_middle_productresultcongruence))))))))) /\ ((((exists pfa_gap_middle_sumleft. pfa_gap_middle_sumleft + S (k) = (p)) /\ (((exists pfa_gap_middle_sumright. pfa_gap_middle_sumright + S (v) = (p)) /\ ((((exists pfa_gap_middle_sumresultbound. pfa_gap_middle_sumresultbound + S (j) = (p)) /\ ((exists pfa_offset_left_middle_sumresultcongruence pfa_offset_right_middle_sumresultcongruence. ((k) + (v)) + (p) * pfa_offset_left_middle_sumresultcongruence = (j) + (p) * pfa_offset_right_middle_sumresultcongruence)))))))))))