prime_field_polynomial_synthetic_functional

Exact expanded first-order arithmetic statement

forall p b c a n qb qc r Qb Qc s. (~((p) = 1) /\ forall pfa_factor_left_functional_prime pfa_factor_right_functional_prime. (p) = pfa_factor_left_functional_prime * pfa_factor_right_functional_prime -> pfa_factor_left_functional_prime = 1 \/ pfa_factor_right_functional_prime = 1) -> (exists pfs_history_code_functional_first pfs_history_scale_functional_first. ((((exists pfa_gap_functional_firsttracebase. pfa_gap_functional_firsttracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_functional_firsttraceinitial. ff_h_pfp_functional_firsttraceinitial + S (0) = S ((S (0)) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceinitial. pfs_history_code_functional_first = ff_q_pfp_functional_firsttraceinitial * S ((S (0)) * pfs_history_scale_functional_first) + (0))) /\ (((((exists ff_h_pfp_functional_firsttraceterminal. ff_h_pfp_functional_firsttraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceterminal. pfs_history_code_functional_first = ff_q_pfp_functional_firsttraceterminal * S ((S (S (n))) * pfs_history_scale_functional_first) + (r))) /\ ((forall pfh_index_functional_firsttracesteps. (exists pfa_gap_functional_firsttracestepsindex. pfa_gap_functional_firsttracestepsindex + S (pfh_index_functional_firsttracesteps) = (S (n))) -> (exists pfh_coefficient_functional_firsttracestepsstep pfh_before_functional_firsttracestepsstep pfh_after_functional_firsttracestepsstep pfh_product_functional_firsttracestepsstep. ((((exists ff_h_pfp_functional_firsttracestepsstepcoefficient. ff_h_pfp_functional_firsttracestepsstepcoefficient + S (pfh_coefficient_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * c)) /\ exists ff_q_pfp_functional_firsttracestepsstepcoefficient. b = ff_q_pfp_functional_firsttracestepsstepcoefficient * S ((S (pfh_index_functional_firsttracesteps)) * c) + (pfh_coefficient_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepbefore. ff_h_pfp_functional_firsttracestepsstepbefore + S (pfh_before_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepbefore. pfs_history_code_functional_first = ff_q_pfp_functional_firsttracestepsstepbefore * S ((S (pfh_index_functional_firsttracesteps)) * pfs_history_scale_functional_first) + (pfh_before_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepafter. ff_h_pfp_functional_firsttracestepsstepafter + S (pfh_after_functional_firsttracestepsstep) = S ((S (S (pfh_index_functional_firsttracesteps))) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepafter. pfs_history_code_functional_first = ff_q_pfp_functional_firsttracestepsstepafter * S ((S (S (pfh_index_functional_firsttracesteps))) * pfs_history_scale_functional_first) + (pfh_after_functional_firsttracestepsstep))) /\ (((((exists pfa_gap_functional_firsttracestepsstepmultiplyleft. pfa_gap_functional_firsttracestepsstepmultiplyleft + S (pfh_before_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepmultiplyright. pfa_gap_functional_firsttracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepmultiplyresultbound. pfa_gap_functional_firsttracestepsstepmultiplyresultbound + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence. ((pfh_before_functional_firsttracestepsstep) * (a)) + (p) * pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence = (pfh_product_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddleft. pfa_gap_functional_firsttracestepsstepaddleft + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepaddright. pfa_gap_functional_firsttracestepsstepaddright + S (pfh_coefficient_functional_firsttracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddresultbound. pfa_gap_functional_firsttracestepsstepaddresultbound + S (pfh_after_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepaddresultcongruence pfa_offset_right_functional_firsttracestepsstepaddresultcongruence. ((pfh_product_functional_firsttracestepsstep) + (pfh_coefficient_functional_firsttracestepsstep)) + (p) * pfa_offset_left_functional_firsttracestepsstepaddresultcongruence = (pfh_after_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_functional_firstquotient ff_source_mcp_pfs_functional_firstquotient ff_target_mcp_pfs_functional_firstquotient. (exists mcp_gap_pfs_functional_firstquotient_bound. mcp_gap_pfs_functional_firstquotient_bound + S (ff_index_mcp_pfs_functional_firstquotient) = (n)) -> (((exists fs_h_mcp_pfs_functional_firstquotient_source. fs_h_mcp_pfs_functional_firstquotient_source + S (ff_source_mcp_pfs_functional_firstquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_functional_firstquotient)) * pfs_history_scale_functional_first)) /\ exists fs_q_mcp_pfs_functional_firstquotient_source. pfs_history_code_functional_first = fs_q_mcp_pfs_functional_firstquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_functional_firstquotient)) * pfs_history_scale_functional_first) + (ff_source_mcp_pfs_functional_firstquotient))) -> (((exists fs_h_mcp_pfs_functional_firstquotient_target. fs_h_mcp_pfs_functional_firstquotient_target + S (ff_target_mcp_pfs_functional_firstquotient) = S ((S (ff_index_mcp_pfs_functional_firstquotient)) * qc)) /\ exists fs_q_mcp_pfs_functional_firstquotient_target. qb = fs_q_mcp_pfs_functional_firstquotient_target * S ((S (ff_index_mcp_pfs_functional_firstquotient)) * qc) + (ff_target_mcp_pfs_functional_firstquotient))) -> ff_target_mcp_pfs_functional_firstquotient = ff_source_mcp_pfs_functional_firstquotient)))) -> (exists pfs_history_code_functional_second pfs_history_scale_functional_second. ((((exists pfa_gap_functional_secondtracebase. pfa_gap_functional_secondtracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_functional_secondtraceinitial. ff_h_pfp_functional_secondtraceinitial + S (0) = S ((S (0)) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceinitial. pfs_history_code_functional_second = ff_q_pfp_functional_secondtraceinitial * S ((S (0)) * pfs_history_scale_functional_second) + (0))) /\ (((((exists ff_h_pfp_functional_secondtraceterminal. ff_h_pfp_functional_secondtraceterminal + S (s) = S ((S (S (n))) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceterminal. pfs_history_code_functional_second = ff_q_pfp_functional_secondtraceterminal * S ((S (S (n))) * pfs_history_scale_functional_second) + (s))) /\ ((forall pfh_index_functional_secondtracesteps. (exists pfa_gap_functional_secondtracestepsindex. pfa_gap_functional_secondtracestepsindex + S (pfh_index_functional_secondtracesteps) = (S (n))) -> (exists pfh_coefficient_functional_secondtracestepsstep pfh_before_functional_secondtracestepsstep pfh_after_functional_secondtracestepsstep pfh_product_functional_secondtracestepsstep. ((((exists ff_h_pfp_functional_secondtracestepsstepcoefficient. ff_h_pfp_functional_secondtracestepsstepcoefficient + S (pfh_coefficient_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * c)) /\ exists ff_q_pfp_functional_secondtracestepsstepcoefficient. b = ff_q_pfp_functional_secondtracestepsstepcoefficient * S ((S (pfh_index_functional_secondtracesteps)) * c) + (pfh_coefficient_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepbefore. ff_h_pfp_functional_secondtracestepsstepbefore + S (pfh_before_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepbefore. pfs_history_code_functional_second = ff_q_pfp_functional_secondtracestepsstepbefore * S ((S (pfh_index_functional_secondtracesteps)) * pfs_history_scale_functional_second) + (pfh_before_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepafter. ff_h_pfp_functional_secondtracestepsstepafter + S (pfh_after_functional_secondtracestepsstep) = S ((S (S (pfh_index_functional_secondtracesteps))) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepafter. pfs_history_code_functional_second = ff_q_pfp_functional_secondtracestepsstepafter * S ((S (S (pfh_index_functional_secondtracesteps))) * pfs_history_scale_functional_second) + (pfh_after_functional_secondtracestepsstep))) /\ (((((exists pfa_gap_functional_secondtracestepsstepmultiplyleft. pfa_gap_functional_secondtracestepsstepmultiplyleft + S (pfh_before_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepmultiplyright. pfa_gap_functional_secondtracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepmultiplyresultbound. pfa_gap_functional_secondtracestepsstepmultiplyresultbound + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence. ((pfh_before_functional_secondtracestepsstep) * (a)) + (p) * pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence = (pfh_product_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddleft. pfa_gap_functional_secondtracestepsstepaddleft + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepaddright. pfa_gap_functional_secondtracestepsstepaddright + S (pfh_coefficient_functional_secondtracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddresultbound. pfa_gap_functional_secondtracestepsstepaddresultbound + S (pfh_after_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepaddresultcongruence pfa_offset_right_functional_secondtracestepsstepaddresultcongruence. ((pfh_product_functional_secondtracestepsstep) + (pfh_coefficient_functional_secondtracestepsstep)) + (p) * pfa_offset_left_functional_secondtracestepsstepaddresultcongruence = (pfh_after_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_functional_secondquotient ff_source_mcp_pfs_functional_secondquotient ff_target_mcp_pfs_functional_secondquotient. (exists mcp_gap_pfs_functional_secondquotient_bound. mcp_gap_pfs_functional_secondquotient_bound + S (ff_index_mcp_pfs_functional_secondquotient) = (n)) -> (((exists fs_h_mcp_pfs_functional_secondquotient_source. fs_h_mcp_pfs_functional_secondquotient_source + S (ff_source_mcp_pfs_functional_secondquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_functional_secondquotient)) * pfs_history_scale_functional_second)) /\ exists fs_q_mcp_pfs_functional_secondquotient_source. pfs_history_code_functional_second = fs_q_mcp_pfs_functional_secondquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_functional_secondquotient)) * pfs_history_scale_functional_second) + (ff_source_mcp_pfs_functional_secondquotient))) -> (((exists fs_h_mcp_pfs_functional_secondquotient_target. fs_h_mcp_pfs_functional_secondquotient_target + S (ff_target_mcp_pfs_functional_secondquotient) = S ((S (ff_index_mcp_pfs_functional_secondquotient)) * Qc)) /\ exists fs_q_mcp_pfs_functional_secondquotient_target. Qb = fs_q_mcp_pfs_functional_secondquotient_target * S ((S (ff_index_mcp_pfs_functional_secondquotient)) * Qc) + (ff_target_mcp_pfs_functional_secondquotient))) -> ff_target_mcp_pfs_functional_secondquotient = ff_source_mcp_pfs_functional_secondquotient)))) -> ((r=s) /\ ((forall mdr_i_pfp_functional_values mdr_a_pfp_functional_values. (exists mdr_gap_pfp_functional_valuesb. mdr_gap_pfp_functional_valuesb + S (mdr_i_pfp_functional_values) = (n)) -> (((exists ff_h_mdr_pfp_functional_valueso. ff_h_mdr_pfp_functional_valueso + S (mdr_a_pfp_functional_values) = S ((S (mdr_i_pfp_functional_values)) * qc)) /\ exists ff_q_mdr_pfp_functional_valueso. qb = ff_q_mdr_pfp_functional_valueso * S ((S (mdr_i_pfp_functional_values)) * qc) + (mdr_a_pfp_functional_values))) -> (((exists ff_h_mdr_pfp_functional_valuesn. ff_h_mdr_pfp_functional_valuesn + S (mdr_a_pfp_functional_values) = S ((S (mdr_i_pfp_functional_values)) * Qc)) /\ exists ff_q_mdr_pfp_functional_valuesn. Qb = ff_q_mdr_pfp_functional_valuesn * S ((S (mdr_i_pfp_functional_values)) * Qc) + (mdr_a_pfp_functional_values))))))