prime_field_polynomial_monic_normalization_represented_degree

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc L d. ((((L)=S (d)) /\ (((forall fom_index_pfp_normalization_degree_inputcoefficients. (exists fom_gap_pfp_normalization_degree_inputcoefficients_index_bound. fom_gap_pfp_normalization_degree_inputcoefficients_index_bound + S (fom_index_pfp_normalization_degree_inputcoefficients) = L) -> exists fom_value_pfp_normalization_degree_inputcoefficients. ((((exists fom_beta_height_pfp_normalization_degree_inputcoefficients_entry. fom_beta_height_pfp_normalization_degree_inputcoefficients_entry + S (fom_value_pfp_normalization_degree_inputcoefficients) = S ((S (fom_index_pfp_normalization_degree_inputcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_degree_inputcoefficients_entry. ab = fom_beta_quotient_pfp_normalization_degree_inputcoefficients_entry * S ((S (fom_index_pfp_normalization_degree_inputcoefficients)) * ac) + (fom_value_pfp_normalization_degree_inputcoefficients))) /\ (exists fom_gap_pfp_normalization_degree_inputcoefficients_value_bound. fom_gap_pfp_normalization_degree_inputcoefficients_value_bound + S (fom_value_pfp_normalization_degree_inputcoefficients) = p))) /\ ((exists pfd_leading_normalization_degree_input. ((((exists ff_h_pfp_normalization_degree_inputentry. ff_h_pfp_normalization_degree_inputentry + S (pfd_leading_normalization_degree_input) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_degree_inputentry. ab = ff_q_pfp_normalization_degree_inputentry * S ((S (0)) * ac) + (pfd_leading_normalization_degree_input))) /\ ((~(pfd_leading_normalization_degree_input=0)))))))))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_degree_source. ((((exists ff_h_pfp_normalization_degree_sourcesource. ff_h_pfp_normalization_degree_sourcesource + S (pfm_leading_normalization_degree_source) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_degree_sourcesource. ab = ff_q_pfp_normalization_degree_sourcesource * S ((S (0)) * ac) + (pfm_leading_normalization_degree_source))) /\ ((((~((pfm_leading_normalization_degree_source) = 0)) /\ ((((exists pfa_gap_normalization_degree_sourceinversemultiplicationleft. pfa_gap_normalization_degree_sourceinversemultiplicationleft + S (pfm_leading_normalization_degree_source) = (p)) /\ (((exists pfa_gap_normalization_degree_sourceinversemultiplicationright. pfa_gap_normalization_degree_sourceinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_degree_sourceinversemultiplicationresultbound. pfa_gap_normalization_degree_sourceinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_degree_sourceinversemultiplicationresultcongruence pfa_offset_right_normalization_degree_sourceinversemultiplicationresultcongruence. ((pfm_leading_normalization_degree_source) * (k)) + (p) * pfa_offset_left_normalization_degree_sourceinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_degree_sourceinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_degree_sourcescalescalar. pfa_gap_normalization_degree_sourcescalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_degree_sourcescale. (exists pfa_gap_normalization_degree_sourcescaleindex. pfa_gap_normalization_degree_sourcescaleindex + S (pfp_index_normalization_degree_sourcescale) = (L)) -> exists pfp_source_normalization_degree_sourcescale pfp_value_normalization_degree_sourcescale. ((((exists ff_h_pfp_normalization_degree_sourcescalesource. ff_h_pfp_normalization_degree_sourcescalesource + S (pfp_source_normalization_degree_sourcescale) = S ((S (pfp_index_normalization_degree_sourcescale)) * ac)) /\ exists ff_q_pfp_normalization_degree_sourcescalesource. ab = ff_q_pfp_normalization_degree_sourcescalesource * S ((S (pfp_index_normalization_degree_sourcescale)) * ac) + (pfp_source_normalization_degree_sourcescale))) /\ (((((exists ff_h_pfp_normalization_degree_sourcescaletarget. ff_h_pfp_normalization_degree_sourcescaletarget + S (pfp_value_normalization_degree_sourcescale) = S ((S (pfp_index_normalization_degree_sourcescale)) * bc)) /\ exists ff_q_pfp_normalization_degree_sourcescaletarget. bb = ff_q_pfp_normalization_degree_sourcescaletarget * S ((S (pfp_index_normalization_degree_sourcescale)) * bc) + (pfp_value_normalization_degree_sourcescale))) /\ ((((exists pfa_gap_normalization_degree_sourcescaleoperationleft. pfa_gap_normalization_degree_sourcescaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_degree_sourcescaleoperationright. pfa_gap_normalization_degree_sourcescaleoperationright + S (pfp_source_normalization_degree_sourcescale) = (p)) /\ ((((exists pfa_gap_normalization_degree_sourcescaleoperationresultbound. pfa_gap_normalization_degree_sourcescaleoperationresultbound + S (pfp_value_normalization_degree_sourcescale) = (p)) /\ ((exists pfa_offset_left_normalization_degree_sourcescaleoperationresultcongruence pfa_offset_right_normalization_degree_sourcescaleoperationresultcongruence. ((k) * (pfp_source_normalization_degree_sourcescale)) + (p) * pfa_offset_left_normalization_degree_sourcescaleoperationresultcongruence = (pfp_value_normalization_degree_sourcescale) + (p) * pfa_offset_right_normalization_degree_sourcescaleoperationresultcongruence)))))))))))))))))))))) -> ((((L)=S (d)) /\ (((forall fom_index_pfp_normalization_degree_resultcoefficients. (exists fom_gap_pfp_normalization_degree_resultcoefficients_index_bound. fom_gap_pfp_normalization_degree_resultcoefficients_index_bound + S (fom_index_pfp_normalization_degree_resultcoefficients) = L) -> exists fom_value_pfp_normalization_degree_resultcoefficients. ((((exists fom_beta_height_pfp_normalization_degree_resultcoefficients_entry. fom_beta_height_pfp_normalization_degree_resultcoefficients_entry + S (fom_value_pfp_normalization_degree_resultcoefficients) = S ((S (fom_index_pfp_normalization_degree_resultcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_degree_resultcoefficients_entry. bb = fom_beta_quotient_pfp_normalization_degree_resultcoefficients_entry * S ((S (fom_index_pfp_normalization_degree_resultcoefficients)) * bc) + (fom_value_pfp_normalization_degree_resultcoefficients))) /\ (exists fom_gap_pfp_normalization_degree_resultcoefficients_value_bound. fom_gap_pfp_normalization_degree_resultcoefficients_value_bound + S (fom_value_pfp_normalization_degree_resultcoefficients) = p))) /\ ((exists pfd_leading_normalization_degree_result. ((((exists ff_h_pfp_normalization_degree_resultentry. ff_h_pfp_normalization_degree_resultentry + S (pfd_leading_normalization_degree_result) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_degree_resultentry. bb = ff_q_pfp_normalization_degree_resultentry * S ((S (0)) * bc) + (pfd_leading_normalization_degree_result))) /\ ((~(pfd_leading_normalization_degree_result=0))))))))))