prime_field_polynomial_synthetic_represented_degree

Exact expanded first-order arithmetic statement

forall p b c a n qb qc r. (~((p) = 1) /\ forall pfa_factor_left_degree_prime pfa_factor_right_degree_prime. (p) = pfa_factor_left_degree_prime * pfa_factor_right_degree_prime -> pfa_factor_left_degree_prime = 1 \/ pfa_factor_right_degree_prime = 1) -> ((((S (S n))=S (S n)) /\ (((forall fom_index_pfp_degree_inputcoefficients. (exists fom_gap_pfp_degree_inputcoefficients_index_bound. fom_gap_pfp_degree_inputcoefficients_index_bound + S (fom_index_pfp_degree_inputcoefficients) = S (S n)) -> exists fom_value_pfp_degree_inputcoefficients. ((((exists fom_beta_height_pfp_degree_inputcoefficients_entry. fom_beta_height_pfp_degree_inputcoefficients_entry + S (fom_value_pfp_degree_inputcoefficients) = S ((S (fom_index_pfp_degree_inputcoefficients)) * c)) /\ exists fom_beta_quotient_pfp_degree_inputcoefficients_entry. b = fom_beta_quotient_pfp_degree_inputcoefficients_entry * S ((S (fom_index_pfp_degree_inputcoefficients)) * c) + (fom_value_pfp_degree_inputcoefficients))) /\ (exists fom_gap_pfp_degree_inputcoefficients_value_bound. fom_gap_pfp_degree_inputcoefficients_value_bound + S (fom_value_pfp_degree_inputcoefficients) = p))) /\ ((exists pfd_leading_degree_input. ((((exists ff_h_pfp_degree_inputentry. ff_h_pfp_degree_inputentry + S (pfd_leading_degree_input) = S ((S (0)) * c)) /\ exists ff_q_pfp_degree_inputentry. b = ff_q_pfp_degree_inputentry * S ((S (0)) * c) + (pfd_leading_degree_input))) /\ ((~(pfd_leading_degree_input=0)))))))))) -> (exists pfs_history_code_degree_division pfs_history_scale_degree_division. ((((exists pfa_gap_degree_divisiontracebase. pfa_gap_degree_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_degree_divisiontraceinitial. ff_h_pfp_degree_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_degree_division)) /\ exists ff_q_pfp_degree_divisiontraceinitial. pfs_history_code_degree_division = ff_q_pfp_degree_divisiontraceinitial * S ((S (0)) * pfs_history_scale_degree_division) + (0))) /\ (((((exists ff_h_pfp_degree_divisiontraceterminal. ff_h_pfp_degree_divisiontraceterminal + S (r) = S ((S (S (S n))) * pfs_history_scale_degree_division)) /\ exists ff_q_pfp_degree_divisiontraceterminal. pfs_history_code_degree_division = ff_q_pfp_degree_divisiontraceterminal * S ((S (S (S n))) * pfs_history_scale_degree_division) + (r))) /\ ((forall pfh_index_degree_divisiontracesteps. (exists pfa_gap_degree_divisiontracestepsindex. pfa_gap_degree_divisiontracestepsindex + S (pfh_index_degree_divisiontracesteps) = (S (S n))) -> (exists pfh_coefficient_degree_divisiontracestepsstep pfh_before_degree_divisiontracestepsstep pfh_after_degree_divisiontracestepsstep pfh_product_degree_divisiontracestepsstep. ((((exists ff_h_pfp_degree_divisiontracestepsstepcoefficient. ff_h_pfp_degree_divisiontracestepsstepcoefficient + S (pfh_coefficient_degree_divisiontracestepsstep) = S ((S (pfh_index_degree_divisiontracesteps)) * c)) /\ exists ff_q_pfp_degree_divisiontracestepsstepcoefficient. b = ff_q_pfp_degree_divisiontracestepsstepcoefficient * S ((S (pfh_index_degree_divisiontracesteps)) * c) + (pfh_coefficient_degree_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_degree_divisiontracestepsstepbefore. ff_h_pfp_degree_divisiontracestepsstepbefore + S (pfh_before_degree_divisiontracestepsstep) = S ((S (pfh_index_degree_divisiontracesteps)) * pfs_history_scale_degree_division)) /\ exists ff_q_pfp_degree_divisiontracestepsstepbefore. pfs_history_code_degree_division = ff_q_pfp_degree_divisiontracestepsstepbefore * S ((S (pfh_index_degree_divisiontracesteps)) * pfs_history_scale_degree_division) + (pfh_before_degree_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_degree_divisiontracestepsstepafter. ff_h_pfp_degree_divisiontracestepsstepafter + S (pfh_after_degree_divisiontracestepsstep) = S ((S (S (pfh_index_degree_divisiontracesteps))) * pfs_history_scale_degree_division)) /\ exists ff_q_pfp_degree_divisiontracestepsstepafter. pfs_history_code_degree_division = ff_q_pfp_degree_divisiontracestepsstepafter * S ((S (S (pfh_index_degree_divisiontracesteps))) * pfs_history_scale_degree_division) + (pfh_after_degree_divisiontracestepsstep))) /\ (((((exists pfa_gap_degree_divisiontracestepsstepmultiplyleft. pfa_gap_degree_divisiontracestepsstepmultiplyleft + S (pfh_before_degree_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_degree_divisiontracestepsstepmultiplyright. pfa_gap_degree_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_degree_divisiontracestepsstepmultiplyresultbound. pfa_gap_degree_divisiontracestepsstepmultiplyresultbound + S (pfh_product_degree_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_degree_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_degree_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_degree_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_degree_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_degree_divisiontracestepsstep) + (p) * pfa_offset_right_degree_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_degree_divisiontracestepsstepaddleft. pfa_gap_degree_divisiontracestepsstepaddleft + S (pfh_product_degree_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_degree_divisiontracestepsstepaddright. pfa_gap_degree_divisiontracestepsstepaddright + S (pfh_coefficient_degree_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_degree_divisiontracestepsstepaddresultbound. pfa_gap_degree_divisiontracestepsstepaddresultbound + S (pfh_after_degree_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_degree_divisiontracestepsstepaddresultcongruence pfa_offset_right_degree_divisiontracestepsstepaddresultcongruence. ((pfh_product_degree_divisiontracestepsstep) + (pfh_coefficient_degree_divisiontracestepsstep)) + (p) * pfa_offset_left_degree_divisiontracestepsstepaddresultcongruence = (pfh_after_degree_divisiontracestepsstep) + (p) * pfa_offset_right_degree_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_degree_divisionquotient ff_source_mcp_pfs_degree_divisionquotient ff_target_mcp_pfs_degree_divisionquotient. (exists mcp_gap_pfs_degree_divisionquotient_bound. mcp_gap_pfs_degree_divisionquotient_bound + S (ff_index_mcp_pfs_degree_divisionquotient) = (S n)) -> (((exists fs_h_mcp_pfs_degree_divisionquotient_source. fs_h_mcp_pfs_degree_divisionquotient_source + S (ff_source_mcp_pfs_degree_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_degree_divisionquotient)) * pfs_history_scale_degree_division)) /\ exists fs_q_mcp_pfs_degree_divisionquotient_source. pfs_history_code_degree_division = fs_q_mcp_pfs_degree_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_degree_divisionquotient)) * pfs_history_scale_degree_division) + (ff_source_mcp_pfs_degree_divisionquotient))) -> (((exists fs_h_mcp_pfs_degree_divisionquotient_target. fs_h_mcp_pfs_degree_divisionquotient_target + S (ff_target_mcp_pfs_degree_divisionquotient) = S ((S (ff_index_mcp_pfs_degree_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_degree_divisionquotient_target. qb = fs_q_mcp_pfs_degree_divisionquotient_target * S ((S (ff_index_mcp_pfs_degree_divisionquotient)) * qc) + (ff_target_mcp_pfs_degree_divisionquotient))) -> ff_target_mcp_pfs_degree_divisionquotient = ff_source_mcp_pfs_degree_divisionquotient)))) -> ((((S n)=S (n)) /\ (((forall fom_index_pfp_degree_quotientcoefficients. (exists fom_gap_pfp_degree_quotientcoefficients_index_bound. fom_gap_pfp_degree_quotientcoefficients_index_bound + S (fom_index_pfp_degree_quotientcoefficients) = S n) -> exists fom_value_pfp_degree_quotientcoefficients. ((((exists fom_beta_height_pfp_degree_quotientcoefficients_entry. fom_beta_height_pfp_degree_quotientcoefficients_entry + S (fom_value_pfp_degree_quotientcoefficients) = S ((S (fom_index_pfp_degree_quotientcoefficients)) * qc)) /\ exists fom_beta_quotient_pfp_degree_quotientcoefficients_entry. qb = fom_beta_quotient_pfp_degree_quotientcoefficients_entry * S ((S (fom_index_pfp_degree_quotientcoefficients)) * qc) + (fom_value_pfp_degree_quotientcoefficients))) /\ (exists fom_gap_pfp_degree_quotientcoefficients_value_bound. fom_gap_pfp_degree_quotientcoefficients_value_bound + S (fom_value_pfp_degree_quotientcoefficients) = p))) /\ ((exists pfd_leading_degree_quotient. ((((exists ff_h_pfp_degree_quotiententry. ff_h_pfp_degree_quotiententry + S (pfd_leading_degree_quotient) = S ((S (0)) * qc)) /\ exists ff_q_pfp_degree_quotiententry. qb = ff_q_pfp_degree_quotiententry * S ((S (0)) * qc) + (pfd_leading_degree_quotient))) /\ ((~(pfd_leading_degree_quotient=0))))))))))