prime_field_polynomial_subtract_common_right_cancel

Exact expanded first-order arithmetic statement

forall p ab ac bb bc cb cc rb rc l. (forall pfs_index_sub_cancel_right_first. (exists pfa_gap_sub_cancel_right_firstindex. pfa_gap_sub_cancel_right_firstindex + S (pfs_index_sub_cancel_right_first) = (l)) -> exists pfs_left_sub_cancel_right_first pfs_right_sub_cancel_right_first pfs_result_sub_cancel_right_first. ((((exists ff_h_pfp_sub_cancel_right_firstleft. ff_h_pfp_sub_cancel_right_firstleft + S (pfs_left_sub_cancel_right_first) = S ((S (pfs_index_sub_cancel_right_first)) * ac)) /\ exists ff_q_pfp_sub_cancel_right_firstleft. ab = ff_q_pfp_sub_cancel_right_firstleft * S ((S (pfs_index_sub_cancel_right_first)) * ac) + (pfs_left_sub_cancel_right_first))) /\ (((((exists ff_h_pfp_sub_cancel_right_firstright. ff_h_pfp_sub_cancel_right_firstright + S (pfs_right_sub_cancel_right_first) = S ((S (pfs_index_sub_cancel_right_first)) * cc)) /\ exists ff_q_pfp_sub_cancel_right_firstright. cb = ff_q_pfp_sub_cancel_right_firstright * S ((S (pfs_index_sub_cancel_right_first)) * cc) + (pfs_right_sub_cancel_right_first))) /\ (((((exists ff_h_pfp_sub_cancel_right_firstresult. ff_h_pfp_sub_cancel_right_firstresult + S (pfs_result_sub_cancel_right_first) = S ((S (pfs_index_sub_cancel_right_first)) * rc)) /\ exists ff_q_pfp_sub_cancel_right_firstresult. rb = ff_q_pfp_sub_cancel_right_firstresult * S ((S (pfs_index_sub_cancel_right_first)) * rc) + (pfs_result_sub_cancel_right_first))) /\ ((((exists pfa_gap_sub_cancel_right_firstoperationleft. pfa_gap_sub_cancel_right_firstoperationleft + S (pfs_right_sub_cancel_right_first) = (p)) /\ (((exists pfa_gap_sub_cancel_right_firstoperationright. pfa_gap_sub_cancel_right_firstoperationright + S (pfs_result_sub_cancel_right_first) = (p)) /\ ((((exists pfa_gap_sub_cancel_right_firstoperationresultbound. pfa_gap_sub_cancel_right_firstoperationresultbound + S (pfs_left_sub_cancel_right_first) = (p)) /\ ((exists pfa_offset_left_sub_cancel_right_firstoperationresultcongruence pfa_offset_right_sub_cancel_right_firstoperationresultcongruence. ((pfs_right_sub_cancel_right_first) + (pfs_result_sub_cancel_right_first)) + (p) * pfa_offset_left_sub_cancel_right_firstoperationresultcongruence = (pfs_left_sub_cancel_right_first) + (p) * pfa_offset_right_sub_cancel_right_firstoperationresultcongruence)))))))))))))))) -> (forall pfs_index_sub_cancel_right_second. (exists pfa_gap_sub_cancel_right_secondindex. pfa_gap_sub_cancel_right_secondindex + S (pfs_index_sub_cancel_right_second) = (l)) -> exists pfs_left_sub_cancel_right_second pfs_right_sub_cancel_right_second pfs_result_sub_cancel_right_second. ((((exists ff_h_pfp_sub_cancel_right_secondleft. ff_h_pfp_sub_cancel_right_secondleft + S (pfs_left_sub_cancel_right_second) = S ((S (pfs_index_sub_cancel_right_second)) * bc)) /\ exists ff_q_pfp_sub_cancel_right_secondleft. bb = ff_q_pfp_sub_cancel_right_secondleft * S ((S (pfs_index_sub_cancel_right_second)) * bc) + (pfs_left_sub_cancel_right_second))) /\ (((((exists ff_h_pfp_sub_cancel_right_secondright. ff_h_pfp_sub_cancel_right_secondright + S (pfs_right_sub_cancel_right_second) = S ((S (pfs_index_sub_cancel_right_second)) * cc)) /\ exists ff_q_pfp_sub_cancel_right_secondright. cb = ff_q_pfp_sub_cancel_right_secondright * S ((S (pfs_index_sub_cancel_right_second)) * cc) + (pfs_right_sub_cancel_right_second))) /\ (((((exists ff_h_pfp_sub_cancel_right_secondresult. ff_h_pfp_sub_cancel_right_secondresult + S (pfs_result_sub_cancel_right_second) = S ((S (pfs_index_sub_cancel_right_second)) * rc)) /\ exists ff_q_pfp_sub_cancel_right_secondresult. rb = ff_q_pfp_sub_cancel_right_secondresult * S ((S (pfs_index_sub_cancel_right_second)) * rc) + (pfs_result_sub_cancel_right_second))) /\ ((((exists pfa_gap_sub_cancel_right_secondoperationleft. pfa_gap_sub_cancel_right_secondoperationleft + S (pfs_right_sub_cancel_right_second) = (p)) /\ (((exists pfa_gap_sub_cancel_right_secondoperationright. pfa_gap_sub_cancel_right_secondoperationright + S (pfs_result_sub_cancel_right_second) = (p)) /\ ((((exists pfa_gap_sub_cancel_right_secondoperationresultbound. pfa_gap_sub_cancel_right_secondoperationresultbound + S (pfs_left_sub_cancel_right_second) = (p)) /\ ((exists pfa_offset_left_sub_cancel_right_secondoperationresultcongruence pfa_offset_right_sub_cancel_right_secondoperationresultcongruence. ((pfs_right_sub_cancel_right_second) + (pfs_result_sub_cancel_right_second)) + (p) * pfa_offset_left_sub_cancel_right_secondoperationresultcongruence = (pfs_left_sub_cancel_right_second) + (p) * pfa_offset_right_sub_cancel_right_secondoperationresultcongruence)))))))))))))))) -> (forall mdr_i_pfp_sub_cancel_right_result mdr_a_pfp_sub_cancel_right_result. (exists mdr_gap_pfp_sub_cancel_right_resultb. mdr_gap_pfp_sub_cancel_right_resultb + S (mdr_i_pfp_sub_cancel_right_result) = (l)) -> (((exists ff_h_mdr_pfp_sub_cancel_right_resulto. ff_h_mdr_pfp_sub_cancel_right_resulto + S (mdr_a_pfp_sub_cancel_right_result) = S ((S (mdr_i_pfp_sub_cancel_right_result)) * ac)) /\ exists ff_q_mdr_pfp_sub_cancel_right_resulto. ab = ff_q_mdr_pfp_sub_cancel_right_resulto * S ((S (mdr_i_pfp_sub_cancel_right_result)) * ac) + (mdr_a_pfp_sub_cancel_right_result))) -> (((exists ff_h_mdr_pfp_sub_cancel_right_resultn. ff_h_mdr_pfp_sub_cancel_right_resultn + S (mdr_a_pfp_sub_cancel_right_result) = S ((S (mdr_i_pfp_sub_cancel_right_result)) * bc)) /\ exists ff_q_mdr_pfp_sub_cancel_right_resultn. bb = ff_q_mdr_pfp_sub_cancel_right_resultn * S ((S (mdr_i_pfp_sub_cancel_right_result)) * bc) + (mdr_a_pfp_sub_cancel_right_result))))