prime_field_polynomial_synthetic_exists_unique

Exact expanded first-order arithmetic statement

forall p b c a n. (~((p) = 1) /\ forall pfa_factor_left_unique_prime pfa_factor_right_unique_prime. (p) = pfa_factor_left_unique_prime * pfa_factor_right_unique_prime -> pfa_factor_left_unique_prime = 1 \/ pfa_factor_right_unique_prime = 1) -> (forall fom_index_pfp_unique_coefficients. (exists fom_gap_pfp_unique_coefficients_index_bound. fom_gap_pfp_unique_coefficients_index_bound + S (fom_index_pfp_unique_coefficients) = S n) -> exists fom_value_pfp_unique_coefficients. ((((exists fom_beta_height_pfp_unique_coefficients_entry. fom_beta_height_pfp_unique_coefficients_entry + S (fom_value_pfp_unique_coefficients) = S ((S (fom_index_pfp_unique_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_unique_coefficients_entry. b = fom_beta_quotient_pfp_unique_coefficients_entry * S ((S (fom_index_pfp_unique_coefficients)) * c) + (fom_value_pfp_unique_coefficients))) /\ (exists fom_gap_pfp_unique_coefficients_value_bound. fom_gap_pfp_unique_coefficients_value_bound + S (fom_value_pfp_unique_coefficients) = p))) -> (exists pfa_gap_unique_base. pfa_gap_unique_base + S (a) = (p)) -> exists qb qc r. ((exists pfs_history_code_unique_execution pfs_history_scale_unique_execution. ((((exists pfa_gap_unique_executiontracebase. pfa_gap_unique_executiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_unique_executiontraceinitial. ff_h_pfp_unique_executiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_unique_execution)) /\ exists ff_q_pfp_unique_executiontraceinitial. pfs_history_code_unique_execution = ff_q_pfp_unique_executiontraceinitial * S ((S (0)) * pfs_history_scale_unique_execution) + (0))) /\ (((((exists ff_h_pfp_unique_executiontraceterminal. ff_h_pfp_unique_executiontraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_unique_execution)) /\ exists ff_q_pfp_unique_executiontraceterminal. pfs_history_code_unique_execution = ff_q_pfp_unique_executiontraceterminal * S ((S (S (n))) * pfs_history_scale_unique_execution) + (r))) /\ ((forall pfh_index_unique_executiontracesteps. (exists pfa_gap_unique_executiontracestepsindex. pfa_gap_unique_executiontracestepsindex + S (pfh_index_unique_executiontracesteps) = (S (n))) -> (exists pfh_coefficient_unique_executiontracestepsstep pfh_before_unique_executiontracestepsstep pfh_after_unique_executiontracestepsstep pfh_product_unique_executiontracestepsstep. ((((exists ff_h_pfp_unique_executiontracestepsstepcoefficient. ff_h_pfp_unique_executiontracestepsstepcoefficient + S (pfh_coefficient_unique_executiontracestepsstep) = S ((S (pfh_index_unique_executiontracesteps)) * c)) /\ exists ff_q_pfp_unique_executiontracestepsstepcoefficient. b = ff_q_pfp_unique_executiontracestepsstepcoefficient * S ((S (pfh_index_unique_executiontracesteps)) * c) + (pfh_coefficient_unique_executiontracestepsstep))) /\ (((((exists ff_h_pfp_unique_executiontracestepsstepbefore. ff_h_pfp_unique_executiontracestepsstepbefore + S (pfh_before_unique_executiontracestepsstep) = S ((S (pfh_index_unique_executiontracesteps)) * pfs_history_scale_unique_execution)) /\ exists ff_q_pfp_unique_executiontracestepsstepbefore. pfs_history_code_unique_execution = ff_q_pfp_unique_executiontracestepsstepbefore * S ((S (pfh_index_unique_executiontracesteps)) * pfs_history_scale_unique_execution) + (pfh_before_unique_executiontracestepsstep))) /\ (((((exists ff_h_pfp_unique_executiontracestepsstepafter. ff_h_pfp_unique_executiontracestepsstepafter + S (pfh_after_unique_executiontracestepsstep) = S ((S (S (pfh_index_unique_executiontracesteps))) * pfs_history_scale_unique_execution)) /\ exists ff_q_pfp_unique_executiontracestepsstepafter. pfs_history_code_unique_execution = ff_q_pfp_unique_executiontracestepsstepafter * S ((S (S (pfh_index_unique_executiontracesteps))) * pfs_history_scale_unique_execution) + (pfh_after_unique_executiontracestepsstep))) /\ (((((exists pfa_gap_unique_executiontracestepsstepmultiplyleft. pfa_gap_unique_executiontracestepsstepmultiplyleft + S (pfh_before_unique_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_unique_executiontracestepsstepmultiplyright. pfa_gap_unique_executiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_unique_executiontracestepsstepmultiplyresultbound. pfa_gap_unique_executiontracestepsstepmultiplyresultbound + S (pfh_product_unique_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_unique_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_unique_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_unique_executiontracestepsstep) * (a)) + (p) * pfa_offset_left_unique_executiontracestepsstepmultiplyresultcongruence = (pfh_product_unique_executiontracestepsstep) + (p) * pfa_offset_right_unique_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_unique_executiontracestepsstepaddleft. pfa_gap_unique_executiontracestepsstepaddleft + S (pfh_product_unique_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_unique_executiontracestepsstepaddright. pfa_gap_unique_executiontracestepsstepaddright + S (pfh_coefficient_unique_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_unique_executiontracestepsstepaddresultbound. pfa_gap_unique_executiontracestepsstepaddresultbound + S (pfh_after_unique_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_unique_executiontracestepsstepaddresultcongruence pfa_offset_right_unique_executiontracestepsstepaddresultcongruence. ((pfh_product_unique_executiontracestepsstep) + (pfh_coefficient_unique_executiontracestepsstep)) + (p) * pfa_offset_left_unique_executiontracestepsstepaddresultcongruence = (pfh_after_unique_executiontracestepsstep) + (p) * pfa_offset_right_unique_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_unique_executionquotient ff_source_mcp_pfs_unique_executionquotient ff_target_mcp_pfs_unique_executionquotient. (exists mcp_gap_pfs_unique_executionquotient_bound. mcp_gap_pfs_unique_executionquotient_bound + S (ff_index_mcp_pfs_unique_executionquotient) = (n)) -> (((exists fs_h_mcp_pfs_unique_executionquotient_source. fs_h_mcp_pfs_unique_executionquotient_source + S (ff_source_mcp_pfs_unique_executionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_unique_executionquotient)) * pfs_history_scale_unique_execution)) /\ exists fs_q_mcp_pfs_unique_executionquotient_source. pfs_history_code_unique_execution = fs_q_mcp_pfs_unique_executionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_unique_executionquotient)) * pfs_history_scale_unique_execution) + (ff_source_mcp_pfs_unique_executionquotient))) -> (((exists fs_h_mcp_pfs_unique_executionquotient_target. fs_h_mcp_pfs_unique_executionquotient_target + S (ff_target_mcp_pfs_unique_executionquotient) = S ((S (ff_index_mcp_pfs_unique_executionquotient)) * qc)) /\ exists fs_q_mcp_pfs_unique_executionquotient_target. qb = fs_q_mcp_pfs_unique_executionquotient_target * S ((S (ff_index_mcp_pfs_unique_executionquotient)) * qc) + (ff_target_mcp_pfs_unique_executionquotient))) -> ff_target_mcp_pfs_unique_executionquotient = ff_source_mcp_pfs_unique_executionquotient)))) /\ ((forall Qb Qc s. (exists pfs_history_code_unique_other pfs_history_scale_unique_other. ((((exists pfa_gap_unique_othertracebase. pfa_gap_unique_othertracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_unique_othertraceinitial. ff_h_pfp_unique_othertraceinitial + S (0) = S ((S (0)) * pfs_history_scale_unique_other)) /\ exists ff_q_pfp_unique_othertraceinitial. pfs_history_code_unique_other = ff_q_pfp_unique_othertraceinitial * S ((S (0)) * pfs_history_scale_unique_other) + (0))) /\ (((((exists ff_h_pfp_unique_othertraceterminal. ff_h_pfp_unique_othertraceterminal + S (s) = S ((S (S (n))) * pfs_history_scale_unique_other)) /\ exists ff_q_pfp_unique_othertraceterminal. pfs_history_code_unique_other = ff_q_pfp_unique_othertraceterminal * S ((S (S (n))) * pfs_history_scale_unique_other) + (s))) /\ ((forall pfh_index_unique_othertracesteps. (exists pfa_gap_unique_othertracestepsindex. pfa_gap_unique_othertracestepsindex + S (pfh_index_unique_othertracesteps) = (S (n))) -> (exists pfh_coefficient_unique_othertracestepsstep pfh_before_unique_othertracestepsstep pfh_after_unique_othertracestepsstep pfh_product_unique_othertracestepsstep. ((((exists ff_h_pfp_unique_othertracestepsstepcoefficient. ff_h_pfp_unique_othertracestepsstepcoefficient + S (pfh_coefficient_unique_othertracestepsstep) = S ((S (pfh_index_unique_othertracesteps)) * c)) /\ exists ff_q_pfp_unique_othertracestepsstepcoefficient. b = ff_q_pfp_unique_othertracestepsstepcoefficient * S ((S (pfh_index_unique_othertracesteps)) * c) + (pfh_coefficient_unique_othertracestepsstep))) /\ (((((exists ff_h_pfp_unique_othertracestepsstepbefore. ff_h_pfp_unique_othertracestepsstepbefore + S (pfh_before_unique_othertracestepsstep) = S ((S (pfh_index_unique_othertracesteps)) * pfs_history_scale_unique_other)) /\ exists ff_q_pfp_unique_othertracestepsstepbefore. pfs_history_code_unique_other = ff_q_pfp_unique_othertracestepsstepbefore * S ((S (pfh_index_unique_othertracesteps)) * pfs_history_scale_unique_other) + (pfh_before_unique_othertracestepsstep))) /\ (((((exists ff_h_pfp_unique_othertracestepsstepafter. ff_h_pfp_unique_othertracestepsstepafter + S (pfh_after_unique_othertracestepsstep) = S ((S (S (pfh_index_unique_othertracesteps))) * pfs_history_scale_unique_other)) /\ exists ff_q_pfp_unique_othertracestepsstepafter. pfs_history_code_unique_other = ff_q_pfp_unique_othertracestepsstepafter * S ((S (S (pfh_index_unique_othertracesteps))) * pfs_history_scale_unique_other) + (pfh_after_unique_othertracestepsstep))) /\ (((((exists pfa_gap_unique_othertracestepsstepmultiplyleft. pfa_gap_unique_othertracestepsstepmultiplyleft + S (pfh_before_unique_othertracestepsstep) = (p)) /\ (((exists pfa_gap_unique_othertracestepsstepmultiplyright. pfa_gap_unique_othertracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_unique_othertracestepsstepmultiplyresultbound. pfa_gap_unique_othertracestepsstepmultiplyresultbound + S (pfh_product_unique_othertracestepsstep) = (p)) /\ ((exists pfa_offset_left_unique_othertracestepsstepmultiplyresultcongruence pfa_offset_right_unique_othertracestepsstepmultiplyresultcongruence. ((pfh_before_unique_othertracestepsstep) * (a)) + (p) * pfa_offset_left_unique_othertracestepsstepmultiplyresultcongruence = (pfh_product_unique_othertracestepsstep) + (p) * pfa_offset_right_unique_othertracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_unique_othertracestepsstepaddleft. pfa_gap_unique_othertracestepsstepaddleft + S (pfh_product_unique_othertracestepsstep) = (p)) /\ (((exists pfa_gap_unique_othertracestepsstepaddright. pfa_gap_unique_othertracestepsstepaddright + S (pfh_coefficient_unique_othertracestepsstep) = (p)) /\ ((((exists pfa_gap_unique_othertracestepsstepaddresultbound. pfa_gap_unique_othertracestepsstepaddresultbound + S (pfh_after_unique_othertracestepsstep) = (p)) /\ ((exists pfa_offset_left_unique_othertracestepsstepaddresultcongruence pfa_offset_right_unique_othertracestepsstepaddresultcongruence. ((pfh_product_unique_othertracestepsstep) + (pfh_coefficient_unique_othertracestepsstep)) + (p) * pfa_offset_left_unique_othertracestepsstepaddresultcongruence = (pfh_after_unique_othertracestepsstep) + (p) * pfa_offset_right_unique_othertracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_unique_otherquotient ff_source_mcp_pfs_unique_otherquotient ff_target_mcp_pfs_unique_otherquotient. (exists mcp_gap_pfs_unique_otherquotient_bound. mcp_gap_pfs_unique_otherquotient_bound + S (ff_index_mcp_pfs_unique_otherquotient) = (n)) -> (((exists fs_h_mcp_pfs_unique_otherquotient_source. fs_h_mcp_pfs_unique_otherquotient_source + S (ff_source_mcp_pfs_unique_otherquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_unique_otherquotient)) * pfs_history_scale_unique_other)) /\ exists fs_q_mcp_pfs_unique_otherquotient_source. pfs_history_code_unique_other = fs_q_mcp_pfs_unique_otherquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_unique_otherquotient)) * pfs_history_scale_unique_other) + (ff_source_mcp_pfs_unique_otherquotient))) -> (((exists fs_h_mcp_pfs_unique_otherquotient_target. fs_h_mcp_pfs_unique_otherquotient_target + S (ff_target_mcp_pfs_unique_otherquotient) = S ((S (ff_index_mcp_pfs_unique_otherquotient)) * Qc)) /\ exists fs_q_mcp_pfs_unique_otherquotient_target. Qb = fs_q_mcp_pfs_unique_otherquotient_target * S ((S (ff_index_mcp_pfs_unique_otherquotient)) * Qc) + (ff_target_mcp_pfs_unique_otherquotient))) -> ff_target_mcp_pfs_unique_otherquotient = ff_source_mcp_pfs_unique_otherquotient)))) -> (((s=r) /\ ((forall mdr_i_pfp_unique_values mdr_a_pfp_unique_values. (exists mdr_gap_pfp_unique_valuesb. mdr_gap_pfp_unique_valuesb + S (mdr_i_pfp_unique_values) = (n)) -> (((exists ff_h_mdr_pfp_unique_valueso. ff_h_mdr_pfp_unique_valueso + S (mdr_a_pfp_unique_values) = S ((S (mdr_i_pfp_unique_values)) * Qc)) /\ exists ff_q_mdr_pfp_unique_valueso. Qb = ff_q_mdr_pfp_unique_valueso * S ((S (mdr_i_pfp_unique_values)) * Qc) + (mdr_a_pfp_unique_values))) -> (((exists ff_h_mdr_pfp_unique_valuesn. ff_h_mdr_pfp_unique_valuesn + S (mdr_a_pfp_unique_values) = S ((S (mdr_i_pfp_unique_values)) * qc)) /\ exists ff_q_mdr_pfp_unique_valuesn. qb = ff_q_mdr_pfp_unique_valuesn * S ((S (mdr_i_pfp_unique_values)) * qc) + (mdr_a_pfp_unique_values))))))))))