polynomial_diagonal_term_shift_right_iff

Exact expanded first-order arithmetic statement

forall ab ac L bb bc M BB BC i j t. (((forall mdr_i_pfp_shift_term_relationprefix mdr_a_pfp_shift_term_relationprefix. (exists mdr_gap_pfp_shift_term_relationprefixb. mdr_gap_pfp_shift_term_relationprefixb + S (mdr_i_pfp_shift_term_relationprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_term_relationprefixo. ff_h_mdr_pfp_shift_term_relationprefixo + S (mdr_a_pfp_shift_term_relationprefix) = S ((S (mdr_i_pfp_shift_term_relationprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_term_relationprefixo. bb = ff_q_mdr_pfp_shift_term_relationprefixo * S ((S (mdr_i_pfp_shift_term_relationprefix)) * bc) + (mdr_a_pfp_shift_term_relationprefix))) -> (((exists ff_h_mdr_pfp_shift_term_relationprefixn. ff_h_mdr_pfp_shift_term_relationprefixn + S (mdr_a_pfp_shift_term_relationprefix) = S ((S (mdr_i_pfp_shift_term_relationprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_term_relationprefixn. BB = ff_q_mdr_pfp_shift_term_relationprefixn * S ((S (mdr_i_pfp_shift_term_relationprefix)) * BC) + (mdr_a_pfp_shift_term_relationprefix)))) /\ ((((exists ff_h_pfp_shift_term_relationlast. ff_h_pfp_shift_term_relationlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_term_relationlast. BB = ff_q_pfp_shift_term_relationlast * S ((S (M)) * BC) + (0)))))) -> ((((exists pfc_complement_shift_term_old pfc_left_shift_term_old pfc_right_shift_term_old. (((j)+pfc_complement_shift_term_old=(i)) /\ ((((((exists pfa_gap_shift_term_oldleftinside. pfa_gap_shift_term_oldleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_oldleftentry. ff_h_pfp_shift_term_oldleftentry + S (pfc_left_shift_term_old) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_oldleftentry. ab = ff_q_pfp_shift_term_oldleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldleftoutside. pfc_gap_shift_term_oldleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_old)=0))))) /\ ((((((exists pfa_gap_shift_term_oldrightinside. pfa_gap_shift_term_oldrightinside + S (pfc_complement_shift_term_old) = (M)) /\ ((((exists ff_h_pfp_shift_term_oldrightentry. ff_h_pfp_shift_term_oldrightentry + S (pfc_right_shift_term_old) = S ((S (pfc_complement_shift_term_old)) * bc)) /\ exists ff_q_pfp_shift_term_oldrightentry. bb = ff_q_pfp_shift_term_oldrightentry * S ((S (pfc_complement_shift_term_old)) * bc) + (pfc_right_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldrightoutside. pfc_gap_shift_term_oldrightoutside+(M)=(pfc_complement_shift_term_old)) /\ (((pfc_right_shift_term_old)=0))))) /\ (((t)=pfc_left_shift_term_old*pfc_right_shift_term_old)))))))) -> (exists pfc_complement_shift_term_new pfc_left_shift_term_new pfc_right_shift_term_new. (((j)+pfc_complement_shift_term_new=(i)) /\ ((((((exists pfa_gap_shift_term_newleftinside. pfa_gap_shift_term_newleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_newleftentry. ff_h_pfp_shift_term_newleftentry + S (pfc_left_shift_term_new) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_newleftentry. ab = ff_q_pfp_shift_term_newleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newleftoutside. pfc_gap_shift_term_newleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_new)=0))))) /\ ((((((exists pfa_gap_shift_term_newrightinside. pfa_gap_shift_term_newrightinside + S (pfc_complement_shift_term_new) = (S M)) /\ ((((exists ff_h_pfp_shift_term_newrightentry. ff_h_pfp_shift_term_newrightentry + S (pfc_right_shift_term_new) = S ((S (pfc_complement_shift_term_new)) * BC)) /\ exists ff_q_pfp_shift_term_newrightentry. BB = ff_q_pfp_shift_term_newrightentry * S ((S (pfc_complement_shift_term_new)) * BC) + (pfc_right_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newrightoutside. pfc_gap_shift_term_newrightoutside+(S M)=(pfc_complement_shift_term_new)) /\ (((pfc_right_shift_term_new)=0))))) /\ (((t)=pfc_left_shift_term_new*pfc_right_shift_term_new))))))))) /\ (((exists pfc_complement_shift_term_new pfc_left_shift_term_new pfc_right_shift_term_new. (((j)+pfc_complement_shift_term_new=(i)) /\ ((((((exists pfa_gap_shift_term_newleftinside. pfa_gap_shift_term_newleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_newleftentry. ff_h_pfp_shift_term_newleftentry + S (pfc_left_shift_term_new) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_newleftentry. ab = ff_q_pfp_shift_term_newleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newleftoutside. pfc_gap_shift_term_newleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_new)=0))))) /\ ((((((exists pfa_gap_shift_term_newrightinside. pfa_gap_shift_term_newrightinside + S (pfc_complement_shift_term_new) = (S M)) /\ ((((exists ff_h_pfp_shift_term_newrightentry. ff_h_pfp_shift_term_newrightentry + S (pfc_right_shift_term_new) = S ((S (pfc_complement_shift_term_new)) * BC)) /\ exists ff_q_pfp_shift_term_newrightentry. BB = ff_q_pfp_shift_term_newrightentry * S ((S (pfc_complement_shift_term_new)) * BC) + (pfc_right_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newrightoutside. pfc_gap_shift_term_newrightoutside+(S M)=(pfc_complement_shift_term_new)) /\ (((pfc_right_shift_term_new)=0))))) /\ (((t)=pfc_left_shift_term_new*pfc_right_shift_term_new)))))))) -> (exists pfc_complement_shift_term_old pfc_left_shift_term_old pfc_right_shift_term_old. (((j)+pfc_complement_shift_term_old=(i)) /\ ((((((exists pfa_gap_shift_term_oldleftinside. pfa_gap_shift_term_oldleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_oldleftentry. ff_h_pfp_shift_term_oldleftentry + S (pfc_left_shift_term_old) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_oldleftentry. ab = ff_q_pfp_shift_term_oldleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldleftoutside. pfc_gap_shift_term_oldleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_old)=0))))) /\ ((((((exists pfa_gap_shift_term_oldrightinside. pfa_gap_shift_term_oldrightinside + S (pfc_complement_shift_term_old) = (M)) /\ ((((exists ff_h_pfp_shift_term_oldrightentry. ff_h_pfp_shift_term_oldrightentry + S (pfc_right_shift_term_old) = S ((S (pfc_complement_shift_term_old)) * bc)) /\ exists ff_q_pfp_shift_term_oldrightentry. bb = ff_q_pfp_shift_term_oldrightentry * S ((S (pfc_complement_shift_term_old)) * bc) + (pfc_right_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldrightoutside. pfc_gap_shift_term_oldrightoutside+(M)=(pfc_complement_shift_term_old)) /\ (((pfc_right_shift_term_old)=0))))) /\ (((t)=pfc_left_shift_term_old*pfc_right_shift_term_old))))))))))))