prime_field_polynomial_monic_normalization_functional

Exact expanded first-order arithmetic statement

forall p k j ab ac bb bc cb cc L. (((~((L) = 0)) /\ (((exists pfm_leading_normalization_function_first. ((((exists ff_h_pfp_normalization_function_firstsource. ff_h_pfp_normalization_function_firstsource + S (pfm_leading_normalization_function_first) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_function_firstsource. ab = ff_q_pfp_normalization_function_firstsource * S ((S (0)) * ac) + (pfm_leading_normalization_function_first))) /\ ((((~((pfm_leading_normalization_function_first) = 0)) /\ ((((exists pfa_gap_normalization_function_firstinversemultiplicationleft. pfa_gap_normalization_function_firstinversemultiplicationleft + S (pfm_leading_normalization_function_first) = (p)) /\ (((exists pfa_gap_normalization_function_firstinversemultiplicationright. pfa_gap_normalization_function_firstinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_function_firstinversemultiplicationresultbound. pfa_gap_normalization_function_firstinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_function_firstinversemultiplicationresultcongruence pfa_offset_right_normalization_function_firstinversemultiplicationresultcongruence. ((pfm_leading_normalization_function_first) * (k)) + (p) * pfa_offset_left_normalization_function_firstinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_function_firstinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_function_firstscalescalar. pfa_gap_normalization_function_firstscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_function_firstscale. (exists pfa_gap_normalization_function_firstscaleindex. pfa_gap_normalization_function_firstscaleindex + S (pfp_index_normalization_function_firstscale) = (L)) -> exists pfp_source_normalization_function_firstscale pfp_value_normalization_function_firstscale. ((((exists ff_h_pfp_normalization_function_firstscalesource. ff_h_pfp_normalization_function_firstscalesource + S (pfp_source_normalization_function_firstscale) = S ((S (pfp_index_normalization_function_firstscale)) * ac)) /\ exists ff_q_pfp_normalization_function_firstscalesource. ab = ff_q_pfp_normalization_function_firstscalesource * S ((S (pfp_index_normalization_function_firstscale)) * ac) + (pfp_source_normalization_function_firstscale))) /\ (((((exists ff_h_pfp_normalization_function_firstscaletarget. ff_h_pfp_normalization_function_firstscaletarget + S (pfp_value_normalization_function_firstscale) = S ((S (pfp_index_normalization_function_firstscale)) * bc)) /\ exists ff_q_pfp_normalization_function_firstscaletarget. bb = ff_q_pfp_normalization_function_firstscaletarget * S ((S (pfp_index_normalization_function_firstscale)) * bc) + (pfp_value_normalization_function_firstscale))) /\ ((((exists pfa_gap_normalization_function_firstscaleoperationleft. pfa_gap_normalization_function_firstscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_function_firstscaleoperationright. pfa_gap_normalization_function_firstscaleoperationright + S (pfp_source_normalization_function_firstscale) = (p)) /\ ((((exists pfa_gap_normalization_function_firstscaleoperationresultbound. pfa_gap_normalization_function_firstscaleoperationresultbound + S (pfp_value_normalization_function_firstscale) = (p)) /\ ((exists pfa_offset_left_normalization_function_firstscaleoperationresultcongruence pfa_offset_right_normalization_function_firstscaleoperationresultcongruence. ((k) * (pfp_source_normalization_function_firstscale)) + (p) * pfa_offset_left_normalization_function_firstscaleoperationresultcongruence = (pfp_value_normalization_function_firstscale) + (p) * pfa_offset_right_normalization_function_firstscaleoperationresultcongruence)))))))))))))))))))))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_function_second. ((((exists ff_h_pfp_normalization_function_secondsource. ff_h_pfp_normalization_function_secondsource + S (pfm_leading_normalization_function_second) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_function_secondsource. ab = ff_q_pfp_normalization_function_secondsource * S ((S (0)) * ac) + (pfm_leading_normalization_function_second))) /\ ((((~((pfm_leading_normalization_function_second) = 0)) /\ ((((exists pfa_gap_normalization_function_secondinversemultiplicationleft. pfa_gap_normalization_function_secondinversemultiplicationleft + S (pfm_leading_normalization_function_second) = (p)) /\ (((exists pfa_gap_normalization_function_secondinversemultiplicationright. pfa_gap_normalization_function_secondinversemultiplicationright + S (j) = (p)) /\ ((((exists pfa_gap_normalization_function_secondinversemultiplicationresultbound. pfa_gap_normalization_function_secondinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_function_secondinversemultiplicationresultcongruence pfa_offset_right_normalization_function_secondinversemultiplicationresultcongruence. ((pfm_leading_normalization_function_second) * (j)) + (p) * pfa_offset_left_normalization_function_secondinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_function_secondinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_function_secondscalescalar. pfa_gap_normalization_function_secondscalescalar + S (j) = (p)) /\ ((forall pfp_index_normalization_function_secondscale. (exists pfa_gap_normalization_function_secondscaleindex. pfa_gap_normalization_function_secondscaleindex + S (pfp_index_normalization_function_secondscale) = (L)) -> exists pfp_source_normalization_function_secondscale pfp_value_normalization_function_secondscale. ((((exists ff_h_pfp_normalization_function_secondscalesource. ff_h_pfp_normalization_function_secondscalesource + S (pfp_source_normalization_function_secondscale) = S ((S (pfp_index_normalization_function_secondscale)) * ac)) /\ exists ff_q_pfp_normalization_function_secondscalesource. ab = ff_q_pfp_normalization_function_secondscalesource * S ((S (pfp_index_normalization_function_secondscale)) * ac) + (pfp_source_normalization_function_secondscale))) /\ (((((exists ff_h_pfp_normalization_function_secondscaletarget. ff_h_pfp_normalization_function_secondscaletarget + S (pfp_value_normalization_function_secondscale) = S ((S (pfp_index_normalization_function_secondscale)) * cc)) /\ exists ff_q_pfp_normalization_function_secondscaletarget. cb = ff_q_pfp_normalization_function_secondscaletarget * S ((S (pfp_index_normalization_function_secondscale)) * cc) + (pfp_value_normalization_function_secondscale))) /\ ((((exists pfa_gap_normalization_function_secondscaleoperationleft. pfa_gap_normalization_function_secondscaleoperationleft + S (j) = (p)) /\ (((exists pfa_gap_normalization_function_secondscaleoperationright. pfa_gap_normalization_function_secondscaleoperationright + S (pfp_source_normalization_function_secondscale) = (p)) /\ ((((exists pfa_gap_normalization_function_secondscaleoperationresultbound. pfa_gap_normalization_function_secondscaleoperationresultbound + S (pfp_value_normalization_function_secondscale) = (p)) /\ ((exists pfa_offset_left_normalization_function_secondscaleoperationresultcongruence pfa_offset_right_normalization_function_secondscaleoperationresultcongruence. ((j) * (pfp_source_normalization_function_secondscale)) + (p) * pfa_offset_left_normalization_function_secondscaleoperationresultcongruence = (pfp_value_normalization_function_secondscale) + (p) * pfa_offset_right_normalization_function_secondscaleoperationresultcongruence)))))))))))))))))))))) -> (forall mdr_i_pfp_normalization_function_result mdr_a_pfp_normalization_function_result. (exists mdr_gap_pfp_normalization_function_resultb. mdr_gap_pfp_normalization_function_resultb + S (mdr_i_pfp_normalization_function_result) = (L)) -> (((exists ff_h_mdr_pfp_normalization_function_resulto. ff_h_mdr_pfp_normalization_function_resulto + S (mdr_a_pfp_normalization_function_result) = S ((S (mdr_i_pfp_normalization_function_result)) * bc)) /\ exists ff_q_mdr_pfp_normalization_function_resulto. bb = ff_q_mdr_pfp_normalization_function_resulto * S ((S (mdr_i_pfp_normalization_function_result)) * bc) + (mdr_a_pfp_normalization_function_result))) -> (((exists ff_h_mdr_pfp_normalization_function_resultn. ff_h_mdr_pfp_normalization_function_resultn + S (mdr_a_pfp_normalization_function_result) = S ((S (mdr_i_pfp_normalization_function_result)) * cc)) /\ exists ff_q_mdr_pfp_normalization_function_resultn. cb = ff_q_mdr_pfp_normalization_function_resultn * S ((S (mdr_i_pfp_normalization_function_result)) * cc) + (mdr_a_pfp_normalization_function_result))))