prime_field_polynomial_monic_normalization_transport

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc AB AC BB BC L. (forall mdr_i_pfp_normalization_recode_input mdr_a_pfp_normalization_recode_input. (exists mdr_gap_pfp_normalization_recode_inputb. mdr_gap_pfp_normalization_recode_inputb + S (mdr_i_pfp_normalization_recode_input) = (L)) -> (((exists ff_h_mdr_pfp_normalization_recode_inputo. ff_h_mdr_pfp_normalization_recode_inputo + S (mdr_a_pfp_normalization_recode_input) = S ((S (mdr_i_pfp_normalization_recode_input)) * ac)) /\ exists ff_q_mdr_pfp_normalization_recode_inputo. ab = ff_q_mdr_pfp_normalization_recode_inputo * S ((S (mdr_i_pfp_normalization_recode_input)) * ac) + (mdr_a_pfp_normalization_recode_input))) -> (((exists ff_h_mdr_pfp_normalization_recode_inputn. ff_h_mdr_pfp_normalization_recode_inputn + S (mdr_a_pfp_normalization_recode_input) = S ((S (mdr_i_pfp_normalization_recode_input)) * AC)) /\ exists ff_q_mdr_pfp_normalization_recode_inputn. AB = ff_q_mdr_pfp_normalization_recode_inputn * S ((S (mdr_i_pfp_normalization_recode_input)) * AC) + (mdr_a_pfp_normalization_recode_input)))) -> (forall mdr_i_pfp_normalization_recode_output mdr_a_pfp_normalization_recode_output. (exists mdr_gap_pfp_normalization_recode_outputb. mdr_gap_pfp_normalization_recode_outputb + S (mdr_i_pfp_normalization_recode_output) = (L)) -> (((exists ff_h_mdr_pfp_normalization_recode_outputo. ff_h_mdr_pfp_normalization_recode_outputo + S (mdr_a_pfp_normalization_recode_output) = S ((S (mdr_i_pfp_normalization_recode_output)) * bc)) /\ exists ff_q_mdr_pfp_normalization_recode_outputo. bb = ff_q_mdr_pfp_normalization_recode_outputo * S ((S (mdr_i_pfp_normalization_recode_output)) * bc) + (mdr_a_pfp_normalization_recode_output))) -> (((exists ff_h_mdr_pfp_normalization_recode_outputn. ff_h_mdr_pfp_normalization_recode_outputn + S (mdr_a_pfp_normalization_recode_output) = S ((S (mdr_i_pfp_normalization_recode_output)) * BC)) /\ exists ff_q_mdr_pfp_normalization_recode_outputn. BB = ff_q_mdr_pfp_normalization_recode_outputn * S ((S (mdr_i_pfp_normalization_recode_output)) * BC) + (mdr_a_pfp_normalization_recode_output)))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_recode_old. ((((exists ff_h_pfp_normalization_recode_oldsource. ff_h_pfp_normalization_recode_oldsource + S (pfm_leading_normalization_recode_old) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_recode_oldsource. ab = ff_q_pfp_normalization_recode_oldsource * S ((S (0)) * ac) + (pfm_leading_normalization_recode_old))) /\ ((((~((pfm_leading_normalization_recode_old) = 0)) /\ ((((exists pfa_gap_normalization_recode_oldinversemultiplicationleft. pfa_gap_normalization_recode_oldinversemultiplicationleft + S (pfm_leading_normalization_recode_old) = (p)) /\ (((exists pfa_gap_normalization_recode_oldinversemultiplicationright. pfa_gap_normalization_recode_oldinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_recode_oldinversemultiplicationresultbound. pfa_gap_normalization_recode_oldinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_recode_oldinversemultiplicationresultcongruence pfa_offset_right_normalization_recode_oldinversemultiplicationresultcongruence. ((pfm_leading_normalization_recode_old) * (k)) + (p) * pfa_offset_left_normalization_recode_oldinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_recode_oldinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_recode_oldscalescalar. pfa_gap_normalization_recode_oldscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_recode_oldscale. (exists pfa_gap_normalization_recode_oldscaleindex. pfa_gap_normalization_recode_oldscaleindex + S (pfp_index_normalization_recode_oldscale) = (L)) -> exists pfp_source_normalization_recode_oldscale pfp_value_normalization_recode_oldscale. ((((exists ff_h_pfp_normalization_recode_oldscalesource. ff_h_pfp_normalization_recode_oldscalesource + S (pfp_source_normalization_recode_oldscale) = S ((S (pfp_index_normalization_recode_oldscale)) * ac)) /\ exists ff_q_pfp_normalization_recode_oldscalesource. ab = ff_q_pfp_normalization_recode_oldscalesource * S ((S (pfp_index_normalization_recode_oldscale)) * ac) + (pfp_source_normalization_recode_oldscale))) /\ (((((exists ff_h_pfp_normalization_recode_oldscaletarget. ff_h_pfp_normalization_recode_oldscaletarget + S (pfp_value_normalization_recode_oldscale) = S ((S (pfp_index_normalization_recode_oldscale)) * bc)) /\ exists ff_q_pfp_normalization_recode_oldscaletarget. bb = ff_q_pfp_normalization_recode_oldscaletarget * S ((S (pfp_index_normalization_recode_oldscale)) * bc) + (pfp_value_normalization_recode_oldscale))) /\ ((((exists pfa_gap_normalization_recode_oldscaleoperationleft. pfa_gap_normalization_recode_oldscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_recode_oldscaleoperationright. pfa_gap_normalization_recode_oldscaleoperationright + S (pfp_source_normalization_recode_oldscale) = (p)) /\ ((((exists pfa_gap_normalization_recode_oldscaleoperationresultbound. pfa_gap_normalization_recode_oldscaleoperationresultbound + S (pfp_value_normalization_recode_oldscale) = (p)) /\ ((exists pfa_offset_left_normalization_recode_oldscaleoperationresultcongruence pfa_offset_right_normalization_recode_oldscaleoperationresultcongruence. ((k) * (pfp_source_normalization_recode_oldscale)) + (p) * pfa_offset_left_normalization_recode_oldscaleoperationresultcongruence = (pfp_value_normalization_recode_oldscale) + (p) * pfa_offset_right_normalization_recode_oldscaleoperationresultcongruence)))))))))))))))))))))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_recode_new. ((((exists ff_h_pfp_normalization_recode_newsource. ff_h_pfp_normalization_recode_newsource + S (pfm_leading_normalization_recode_new) = S ((S (0)) * AC)) /\ exists ff_q_pfp_normalization_recode_newsource. AB = ff_q_pfp_normalization_recode_newsource * S ((S (0)) * AC) + (pfm_leading_normalization_recode_new))) /\ ((((~((pfm_leading_normalization_recode_new) = 0)) /\ ((((exists pfa_gap_normalization_recode_newinversemultiplicationleft. pfa_gap_normalization_recode_newinversemultiplicationleft + S (pfm_leading_normalization_recode_new) = (p)) /\ (((exists pfa_gap_normalization_recode_newinversemultiplicationright. pfa_gap_normalization_recode_newinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_recode_newinversemultiplicationresultbound. pfa_gap_normalization_recode_newinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_recode_newinversemultiplicationresultcongruence pfa_offset_right_normalization_recode_newinversemultiplicationresultcongruence. ((pfm_leading_normalization_recode_new) * (k)) + (p) * pfa_offset_left_normalization_recode_newinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_recode_newinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_recode_newscalescalar. pfa_gap_normalization_recode_newscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_recode_newscale. (exists pfa_gap_normalization_recode_newscaleindex. pfa_gap_normalization_recode_newscaleindex + S (pfp_index_normalization_recode_newscale) = (L)) -> exists pfp_source_normalization_recode_newscale pfp_value_normalization_recode_newscale. ((((exists ff_h_pfp_normalization_recode_newscalesource. ff_h_pfp_normalization_recode_newscalesource + S (pfp_source_normalization_recode_newscale) = S ((S (pfp_index_normalization_recode_newscale)) * AC)) /\ exists ff_q_pfp_normalization_recode_newscalesource. AB = ff_q_pfp_normalization_recode_newscalesource * S ((S (pfp_index_normalization_recode_newscale)) * AC) + (pfp_source_normalization_recode_newscale))) /\ (((((exists ff_h_pfp_normalization_recode_newscaletarget. ff_h_pfp_normalization_recode_newscaletarget + S (pfp_value_normalization_recode_newscale) = S ((S (pfp_index_normalization_recode_newscale)) * BC)) /\ exists ff_q_pfp_normalization_recode_newscaletarget. BB = ff_q_pfp_normalization_recode_newscaletarget * S ((S (pfp_index_normalization_recode_newscale)) * BC) + (pfp_value_normalization_recode_newscale))) /\ ((((exists pfa_gap_normalization_recode_newscaleoperationleft. pfa_gap_normalization_recode_newscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_recode_newscaleoperationright. pfa_gap_normalization_recode_newscaleoperationright + S (pfp_source_normalization_recode_newscale) = (p)) /\ ((((exists pfa_gap_normalization_recode_newscaleoperationresultbound. pfa_gap_normalization_recode_newscaleoperationresultbound + S (pfp_value_normalization_recode_newscale) = (p)) /\ ((exists pfa_offset_left_normalization_recode_newscaleoperationresultcongruence pfa_offset_right_normalization_recode_newscaleoperationresultcongruence. ((k) * (pfp_source_normalization_recode_newscale)) + (p) * pfa_offset_left_normalization_recode_newscaleoperationresultcongruence = (pfp_value_normalization_recode_newscale) + (p) * pfa_offset_right_normalization_recode_newscaleoperationresultcongruence))))))))))))))))))))))