polynomial_diagonal_term_left_add_congruent

forall p ab ac bb bc cb cc L db dc M i j u v w. (forall pfp_index_term_add_left_source. (exists pfa_gap_term_add_left_sourceindex. pfa_gap_term_add_left_sourceindex + S (pfp_index_term_add_left_source) = (L)) -> exists pfp_left_term_add_left_source pfp_right_term_add_left_source pfp_value_term_add_left_source. ((((exists ff_h_pfp_term_add_left_sourceleft. ff_h_pfp_term_add_left_sourceleft + S (pfp_left_term_add_left_source) = S ((S (pfp_index_term_add_left_source)) * ac)) /\ exists ff_q_pfp_term_add_left_sourceleft. ab = ff_q_pfp_term_add_left_sourceleft * S ((S (pfp_index_term_add_left_source)) * ac) + (pfp_left_term_add_left_source))) /\ (((((exists ff_h_pfp_term_add_left_sourceright. ff_h_pfp_term_add_left_sourceright + S (pfp_right_term_add_left_source) = S ((S (pfp_index_term_add_left_source)) * bc)) /\ exists ff_q_pfp_term_add_left_sourceright. bb = ff_q_pfp_term_add_left_sourceright * S ((S (pfp_index_term_add_left_source)) * bc) + (pfp_right_term_add_left_source))) /\ (((((exists ff_h_pfp_term_add_left_sourcetarget. ff_h_pfp_term_add_left_sourcetarget + S (pfp_value_term_add_left_source) = S ((S (pfp_index_term_add_left_source)) * cc)) /\ exists ff_q_pfp_term_add_left_sourcetarget. cb = ff_q_pfp_term_add_left_sourcetarget * S ((S (pfp_index_term_add_left_source)) * cc) + (pfp_value_term_add_left_source))) /\ ((((exists pfa_gap_term_add_left_sourceoperationleft. pfa_gap_term_add_left_sourceoperationleft + S (pfp_left_term_add_left_source) = (p)) /\ (((exists pfa_gap_term_add_left_sourceoperationright. pfa_gap_term_add_left_sourceoperationright + S (pfp_right_term_add_left_source) = (p)) /\ ((((exists pfa_gap_term_add_left_sourceoperationresultbound. pfa_gap_term_add_left_sourceoperationresultbound + S (pfp_value_term_add_left_source) = (p)) /\ ((exists pfa_offset_left_term_add_left_sourceoperationresultcongruence pfa_offset_right_term_add_left_sourceoperationresultcongruence. ((pfp_left_term_add_left_source) + (pfp_right_term_add_left_source)) + (p) * pfa_offset_left_term_add_left_sourceoperationresultcongruence = (pfp_value_term_add_left_source) + (p) * pfa_offset_right_term_add_left_sourceoperationresultcongruence)))))))))))))))) -> (exists pfc_complement_term_add_left_u pfc_left_term_add_left_u pfc_right_term_add_left_u. (((j)+pfc_complement_term_add_left_u=(i)) /\ ((((((exists pfa_gap_term_add_left_uleftinside. pfa_gap_term_add_left_uleftinside + S (j) = (M)) /\ ((((exists ff_h_pfp_term_add_left_uleftentry. ff_h_pfp_term_add_left_uleftentry + S (pfc_left_term_add_left_u) = S ((S (j)) * dc)) /\ exists ff_q_pfp_term_add_left_uleftentry. db = ff_q_pfp_term_add_left_uleftentry * S ((S (j)) * dc) + (pfc_left_term_add_left_u)))))) \/ (((exists pfc_gap_term_add_left_uleftoutside. pfc_gap_term_add_left_uleftoutside+(M)=(j)) /\ (((pfc_left_term_add_left_u)=0))))) /\ ((((((exists pfa_gap_term_add_left_urightinside. pfa_gap_term_add_left_urightinside + S (pfc_complement_term_add_left_u) = (L)) /\ ((((exists ff_h_pfp_term_add_left_urightentry. ff_h_pfp_term_add_left_urightentry + S (pfc_right_term_add_left_u) = S ((S (pfc_complement_term_add_left_u)) * ac)) /\ exists ff_q_pfp_term_add_left_urightentry. ab = ff_q_pfp_term_add_left_urightentry * S ((S (pfc_complement_term_add_left_u)) * ac) + (pfc_right_term_add_left_u)))))) \/ (((exists pfc_gap_term_add_left_urightoutside. pfc_gap_term_add_left_urightoutside+(L)=(pfc_complement_term_add_left_u)) /\ (((pfc_right_term_add_left_u)=0))))) /\ (((u)=pfc_left_term_add_left_u*pfc_right_term_add_left_u)))))))) -> (exists pfc_complement_term_add_left_v pfc_left_term_add_left_v pfc_right_term_add_left_v. (((j)+pfc_complement_term_add_left_v=(i)) /\ ((((((exists pfa_gap_term_add_left_vleftinside. pfa_gap_term_add_left_vleftinside + S (j) = (M)) /\ ((((exists ff_h_pfp_term_add_left_vleftentry. ff_h_pfp_term_add_left_vleftentry + S (pfc_left_term_add_left_v) = S ((S (j)) * dc)) /\ exists ff_q_pfp_term_add_left_vleftentry. db = ff_q_pfp_term_add_left_vleftentry * S ((S (j)) * dc) + (pfc_left_term_add_left_v)))))) \/ (((exists pfc_gap_term_add_left_vleftoutside. pfc_gap_term_add_left_vleftoutside+(M)=(j)) /\ (((pfc_left_term_add_left_v)=0))))) /\ ((((((exists pfa_gap_term_add_left_vrightinside. pfa_gap_term_add_left_vrightinside + S (pfc_complement_term_add_left_v) = (L)) /\ ((((exists ff_h_pfp_term_add_left_vrightentry. ff_h_pfp_term_add_left_vrightentry + S (pfc_right_term_add_left_v) = S ((S (pfc_complement_term_add_left_v)) * bc)) /\ exists ff_q_pfp_term_add_left_vrightentry. bb = ff_q_pfp_term_add_left_vrightentry * S ((S (pfc_complement_term_add_left_v)) * bc) + (pfc_right_term_add_left_v)))))) \/ (((exists pfc_gap_term_add_left_vrightoutside. pfc_gap_term_add_left_vrightoutside+(L)=(pfc_complement_term_add_left_v)) /\ (((pfc_right_term_add_left_v)=0))))) /\ (((v)=pfc_left_term_add_left_v*pfc_right_term_add_left_v)))))))) -> (exists pfc_complement_term_add_left_w pfc_left_term_add_left_w pfc_right_term_add_left_w. (((j)+pfc_complement_term_add_left_w=(i)) /\ ((((((exists pfa_gap_term_add_left_wleftinside. pfa_gap_term_add_left_wleftinside + S (j) = (M)) /\ ((((exists ff_h_pfp_term_add_left_wleftentry. ff_h_pfp_term_add_left_wleftentry + S (pfc_left_term_add_left_w) = S ((S (j)) * dc)) /\ exists ff_q_pfp_term_add_left_wleftentry. db = ff_q_pfp_term_add_left_wleftentry * S ((S (j)) * dc) + (pfc_left_term_add_left_w)))))) \/ (((exists pfc_gap_term_add_left_wleftoutside. pfc_gap_term_add_left_wleftoutside+(M)=(j)) /\ (((pfc_left_term_add_left_w)=0))))) /\ ((((((exists pfa_gap_term_add_left_wrightinside. pfa_gap_term_add_left_wrightinside + S (pfc_complement_term_add_left_w) = (L)) /\ ((((exists ff_h_pfp_term_add_left_wrightentry. ff_h_pfp_term_add_left_wrightentry + S (pfc_right_term_add_left_w) = S ((S (pfc_complement_term_add_left_w)) * cc)) /\ exists ff_q_pfp_term_add_left_wrightentry. cb = ff_q_pfp_term_add_left_wrightentry * S ((S (pfc_complement_term_add_left_w)) * cc) + (pfc_right_term_add_left_w)))))) \/ (((exists pfc_gap_term_add_left_wrightoutside. pfc_gap_term_add_left_wrightoutside+(L)=(pfc_complement_term_add_left_w)) /\ (((pfc_right_term_add_left_w)=0))))) /\ (((w)=pfc_left_term_add_left_w*pfc_right_term_add_left_w)))))))) -> (exists pfa_offset_left_term_add_left_result pfa_offset_right_term_add_left_result. (u+v) + (p) * pfa_offset_left_term_add_left_result = (w) + (p) * pfa_offset_right_term_add_left_result)