polynomial_diagonal_term_right_add_congruent

Exact expanded first-order arithmetic statement

forall p ab ac bb bc cb cc L db dc M i j u v w. (forall pfp_index_term_add_right_source. (exists pfa_gap_term_add_right_sourceindex. pfa_gap_term_add_right_sourceindex + S (pfp_index_term_add_right_source) = (L)) -> exists pfp_left_term_add_right_source pfp_right_term_add_right_source pfp_value_term_add_right_source. ((((exists ff_h_pfp_term_add_right_sourceleft. ff_h_pfp_term_add_right_sourceleft + S (pfp_left_term_add_right_source) = S ((S (pfp_index_term_add_right_source)) * ac)) /\ exists ff_q_pfp_term_add_right_sourceleft. ab = ff_q_pfp_term_add_right_sourceleft * S ((S (pfp_index_term_add_right_source)) * ac) + (pfp_left_term_add_right_source))) /\ (((((exists ff_h_pfp_term_add_right_sourceright. ff_h_pfp_term_add_right_sourceright + S (pfp_right_term_add_right_source) = S ((S (pfp_index_term_add_right_source)) * bc)) /\ exists ff_q_pfp_term_add_right_sourceright. bb = ff_q_pfp_term_add_right_sourceright * S ((S (pfp_index_term_add_right_source)) * bc) + (pfp_right_term_add_right_source))) /\ (((((exists ff_h_pfp_term_add_right_sourcetarget. ff_h_pfp_term_add_right_sourcetarget + S (pfp_value_term_add_right_source) = S ((S (pfp_index_term_add_right_source)) * cc)) /\ exists ff_q_pfp_term_add_right_sourcetarget. cb = ff_q_pfp_term_add_right_sourcetarget * S ((S (pfp_index_term_add_right_source)) * cc) + (pfp_value_term_add_right_source))) /\ ((((exists pfa_gap_term_add_right_sourceoperationleft. pfa_gap_term_add_right_sourceoperationleft + S (pfp_left_term_add_right_source) = (p)) /\ (((exists pfa_gap_term_add_right_sourceoperationright. pfa_gap_term_add_right_sourceoperationright + S (pfp_right_term_add_right_source) = (p)) /\ ((((exists pfa_gap_term_add_right_sourceoperationresultbound. pfa_gap_term_add_right_sourceoperationresultbound + S (pfp_value_term_add_right_source) = (p)) /\ ((exists pfa_offset_left_term_add_right_sourceoperationresultcongruence pfa_offset_right_term_add_right_sourceoperationresultcongruence. ((pfp_left_term_add_right_source) + (pfp_right_term_add_right_source)) + (p) * pfa_offset_left_term_add_right_sourceoperationresultcongruence = (pfp_value_term_add_right_source) + (p) * pfa_offset_right_term_add_right_sourceoperationresultcongruence)))))))))))))))) -> (exists pfc_complement_term_add_right_u pfc_left_term_add_right_u pfc_right_term_add_right_u. (((j)+pfc_complement_term_add_right_u=(i)) /\ ((((((exists pfa_gap_term_add_right_uleftinside. pfa_gap_term_add_right_uleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_term_add_right_uleftentry. ff_h_pfp_term_add_right_uleftentry + S (pfc_left_term_add_right_u) = S ((S (j)) * ac)) /\ exists ff_q_pfp_term_add_right_uleftentry. ab = ff_q_pfp_term_add_right_uleftentry * S ((S (j)) * ac) + (pfc_left_term_add_right_u)))))) \/ (((exists pfc_gap_term_add_right_uleftoutside. pfc_gap_term_add_right_uleftoutside+(L)=(j)) /\ (((pfc_left_term_add_right_u)=0))))) /\ ((((((exists pfa_gap_term_add_right_urightinside. pfa_gap_term_add_right_urightinside + S (pfc_complement_term_add_right_u) = (M)) /\ ((((exists ff_h_pfp_term_add_right_urightentry. ff_h_pfp_term_add_right_urightentry + S (pfc_right_term_add_right_u) = S ((S (pfc_complement_term_add_right_u)) * dc)) /\ exists ff_q_pfp_term_add_right_urightentry. db = ff_q_pfp_term_add_right_urightentry * S ((S (pfc_complement_term_add_right_u)) * dc) + (pfc_right_term_add_right_u)))))) \/ (((exists pfc_gap_term_add_right_urightoutside. pfc_gap_term_add_right_urightoutside+(M)=(pfc_complement_term_add_right_u)) /\ (((pfc_right_term_add_right_u)=0))))) /\ (((u)=pfc_left_term_add_right_u*pfc_right_term_add_right_u)))))))) -> (exists pfc_complement_term_add_right_v pfc_left_term_add_right_v pfc_right_term_add_right_v. (((j)+pfc_complement_term_add_right_v=(i)) /\ ((((((exists pfa_gap_term_add_right_vleftinside. pfa_gap_term_add_right_vleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_term_add_right_vleftentry. ff_h_pfp_term_add_right_vleftentry + S (pfc_left_term_add_right_v) = S ((S (j)) * bc)) /\ exists ff_q_pfp_term_add_right_vleftentry. bb = ff_q_pfp_term_add_right_vleftentry * S ((S (j)) * bc) + (pfc_left_term_add_right_v)))))) \/ (((exists pfc_gap_term_add_right_vleftoutside. pfc_gap_term_add_right_vleftoutside+(L)=(j)) /\ (((pfc_left_term_add_right_v)=0))))) /\ ((((((exists pfa_gap_term_add_right_vrightinside. pfa_gap_term_add_right_vrightinside + S (pfc_complement_term_add_right_v) = (M)) /\ ((((exists ff_h_pfp_term_add_right_vrightentry. ff_h_pfp_term_add_right_vrightentry + S (pfc_right_term_add_right_v) = S ((S (pfc_complement_term_add_right_v)) * dc)) /\ exists ff_q_pfp_term_add_right_vrightentry. db = ff_q_pfp_term_add_right_vrightentry * S ((S (pfc_complement_term_add_right_v)) * dc) + (pfc_right_term_add_right_v)))))) \/ (((exists pfc_gap_term_add_right_vrightoutside. pfc_gap_term_add_right_vrightoutside+(M)=(pfc_complement_term_add_right_v)) /\ (((pfc_right_term_add_right_v)=0))))) /\ (((v)=pfc_left_term_add_right_v*pfc_right_term_add_right_v)))))))) -> (exists pfc_complement_term_add_right_w pfc_left_term_add_right_w pfc_right_term_add_right_w. (((j)+pfc_complement_term_add_right_w=(i)) /\ ((((((exists pfa_gap_term_add_right_wleftinside. pfa_gap_term_add_right_wleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_term_add_right_wleftentry. ff_h_pfp_term_add_right_wleftentry + S (pfc_left_term_add_right_w) = S ((S (j)) * cc)) /\ exists ff_q_pfp_term_add_right_wleftentry. cb = ff_q_pfp_term_add_right_wleftentry * S ((S (j)) * cc) + (pfc_left_term_add_right_w)))))) \/ (((exists pfc_gap_term_add_right_wleftoutside. pfc_gap_term_add_right_wleftoutside+(L)=(j)) /\ (((pfc_left_term_add_right_w)=0))))) /\ ((((((exists pfa_gap_term_add_right_wrightinside. pfa_gap_term_add_right_wrightinside + S (pfc_complement_term_add_right_w) = (M)) /\ ((((exists ff_h_pfp_term_add_right_wrightentry. ff_h_pfp_term_add_right_wrightentry + S (pfc_right_term_add_right_w) = S ((S (pfc_complement_term_add_right_w)) * dc)) /\ exists ff_q_pfp_term_add_right_wrightentry. db = ff_q_pfp_term_add_right_wrightentry * S ((S (pfc_complement_term_add_right_w)) * dc) + (pfc_right_term_add_right_w)))))) \/ (((exists pfc_gap_term_add_right_wrightoutside. pfc_gap_term_add_right_wrightoutside+(M)=(pfc_complement_term_add_right_w)) /\ (((pfc_right_term_add_right_w)=0))))) /\ (((w)=pfc_left_term_add_right_w*pfc_right_term_add_right_w)))))))) -> (exists pfa_offset_left_term_add_right_result pfa_offset_right_term_add_right_result. (u+v) + (p) * pfa_offset_left_term_add_right_result = (w) + (p) * pfa_offset_right_term_add_right_result)