prime_field_convolution_coefficient_shift_right_iff

forall p ab ac L bb bc M BB BC i r. (((forall mdr_i_pfp_shift_coefficient_relationprefix mdr_a_pfp_shift_coefficient_relationprefix. (exists mdr_gap_pfp_shift_coefficient_relationprefixb. mdr_gap_pfp_shift_coefficient_relationprefixb + S (mdr_i_pfp_shift_coefficient_relationprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_coefficient_relationprefixo. ff_h_mdr_pfp_shift_coefficient_relationprefixo + S (mdr_a_pfp_shift_coefficient_relationprefix) = S ((S (mdr_i_pfp_shift_coefficient_relationprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_coefficient_relationprefixo. bb = ff_q_mdr_pfp_shift_coefficient_relationprefixo * S ((S (mdr_i_pfp_shift_coefficient_relationprefix)) * bc) + (mdr_a_pfp_shift_coefficient_relationprefix))) -> (((exists ff_h_mdr_pfp_shift_coefficient_relationprefixn. ff_h_mdr_pfp_shift_coefficient_relationprefixn + S (mdr_a_pfp_shift_coefficient_relationprefix) = S ((S (mdr_i_pfp_shift_coefficient_relationprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_coefficient_relationprefixn. BB = ff_q_mdr_pfp_shift_coefficient_relationprefixn * S ((S (mdr_i_pfp_shift_coefficient_relationprefix)) * BC) + (mdr_a_pfp_shift_coefficient_relationprefix)))) /\ ((((exists ff_h_pfp_shift_coefficient_relationlast. ff_h_pfp_shift_coefficient_relationlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_coefficient_relationlast. BB = ff_q_pfp_shift_coefficient_relationlast * S ((S (M)) * BC) + (0)))))) -> ((((exists pfc_terms_code_shift_coefficient_old pfc_terms_scale_shift_coefficient_old pfc_natural_sum_shift_coefficient_old. ((forall pfc_index_shift_coefficient_olddiagonal. (exists pfa_gap_shift_coefficient_olddiagonalbound. pfa_gap_shift_coefficient_olddiagonalbound + S (pfc_index_shift_coefficient_olddiagonal) = (S (i))) -> exists pfc_value_shift_coefficient_olddiagonal. ((((exists ff_h_pfp_shift_coefficient_olddiagonalentry. ff_h_pfp_shift_coefficient_olddiagonalentry + S (pfc_value_shift_coefficient_olddiagonal) = S ((S (pfc_index_shift_coefficient_olddiagonal)) * pfc_terms_scale_shift_coefficient_old)) /\ exists ff_q_pfp_shift_coefficient_olddiagonalentry. pfc_terms_code_shift_coefficient_old = ff_q_pfp_shift_coefficient_olddiagonalentry * S ((S (pfc_index_shift_coefficient_olddiagonal)) * pfc_terms_scale_shift_coefficient_old) + (pfc_value_shift_coefficient_olddiagonal))) /\ ((exists pfc_complement_shift_coefficient_olddiagonalterm pfc_left_shift_coefficient_olddiagonalterm pfc_right_shift_coefficient_olddiagonalterm. (((pfc_index_shift_coefficient_olddiagonal)+pfc_complement_shift_coefficient_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_coefficient_olddiagonaltermleftinside. pfa_gap_shift_coefficient_olddiagonaltermleftinside + S (pfc_index_shift_coefficient_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_coefficient_olddiagonaltermleftentry. ff_h_pfp_shift_coefficient_olddiagonaltermleftentry + S (pfc_left_shift_coefficient_olddiagonalterm) = S ((S (pfc_index_shift_coefficient_olddiagonal)) * ac)) /\ exists ff_q_pfp_shift_coefficient_olddiagonaltermleftentry. ab = ff_q_pfp_shift_coefficient_olddiagonaltermleftentry * S ((S (pfc_index_shift_coefficient_olddiagonal)) * ac) + (pfc_left_shift_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_olddiagonaltermleftoutside. pfc_gap_shift_coefficient_olddiagonaltermleftoutside+(L)=(pfc_index_shift_coefficient_olddiagonal)) /\ (((pfc_left_shift_coefficient_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_coefficient_olddiagonaltermrightinside. pfa_gap_shift_coefficient_olddiagonaltermrightinside + S (pfc_complement_shift_coefficient_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_coefficient_olddiagonaltermrightentry. ff_h_pfp_shift_coefficient_olddiagonaltermrightentry + S (pfc_right_shift_coefficient_olddiagonalterm) = S ((S (pfc_complement_shift_coefficient_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_coefficient_olddiagonaltermrightentry. bb = ff_q_pfp_shift_coefficient_olddiagonaltermrightentry * S ((S (pfc_complement_shift_coefficient_olddiagonalterm)) * bc) + (pfc_right_shift_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_olddiagonaltermrightoutside. pfc_gap_shift_coefficient_olddiagonaltermrightoutside+(M)=(pfc_complement_shift_coefficient_olddiagonalterm)) /\ (((pfc_right_shift_coefficient_olddiagonalterm)=0))))) /\ (((pfc_value_shift_coefficient_olddiagonal)=pfc_left_shift_coefficient_olddiagonalterm*pfc_right_shift_coefficient_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_coefficient_oldsum fs_v_pfc_shift_coefficient_oldsum. ((((exists fs_h_pfc_shift_coefficient_oldsum_body_start. fs_h_pfc_shift_coefficient_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_start. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_start * S ((S (0)) * fs_v_pfc_shift_coefficient_oldsum) + (0))) /\ ((((exists fs_h_pfc_shift_coefficient_oldsum_body_terminal. fs_h_pfc_shift_coefficient_oldsum_body_terminal + S (pfc_natural_sum_shift_coefficient_old) = S ((S (S (i))) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_terminal. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_coefficient_oldsum) + (pfc_natural_sum_shift_coefficient_old))) /\ forall fs_i_pfc_shift_coefficient_oldsum_body_steps. (exists fs_lt_pfc_shift_coefficient_oldsum_body_steps_bound. fs_lt_pfc_shift_coefficient_oldsum_body_steps_bound + S fs_i_pfc_shift_coefficient_oldsum_body_steps = S (i)) -> exists fs_a_pfc_shift_coefficient_oldsum_body_steps fs_r_pfc_shift_coefficient_oldsum_body_steps fs_s_pfc_shift_coefficient_oldsum_body_steps. ((((exists fs_h_pfc_shift_coefficient_oldsum_body_steps_summand. fs_h_pfc_shift_coefficient_oldsum_body_steps_summand + S (fs_a_pfc_shift_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * pfc_terms_scale_shift_coefficient_old)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_steps_summand. pfc_terms_code_shift_coefficient_old = fs_q_pfc_shift_coefficient_oldsum_body_steps_summand * S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * pfc_terms_scale_shift_coefficient_old) + (fs_a_pfc_shift_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_oldsum_body_steps_partial. fs_h_pfc_shift_coefficient_oldsum_body_steps_partial + S (fs_r_pfc_shift_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_steps_partial. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_steps_partial * S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum) + (fs_r_pfc_shift_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_oldsum_body_steps_successor. fs_h_pfc_shift_coefficient_oldsum_body_steps_successor + S (fs_s_pfc_shift_coefficient_oldsum_body_steps) = S ((S (S fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_steps_successor. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_steps_successor * S ((S (S fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum) + (fs_s_pfc_shift_coefficient_oldsum_body_steps))) /\ fs_s_pfc_shift_coefficient_oldsum_body_steps = fs_r_pfc_shift_coefficient_oldsum_body_steps + fs_a_pfc_shift_coefficient_oldsum_body_steps)))))) /\ ((((exists pfa_gap_shift_coefficient_oldresiduebound. pfa_gap_shift_coefficient_oldresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_shift_coefficient_oldresiduecongruence pfa_offset_right_shift_coefficient_oldresiduecongruence. (pfc_natural_sum_shift_coefficient_old) + (p) * pfa_offset_left_shift_coefficient_oldresiduecongruence = (r) + (p) * pfa_offset_right_shift_coefficient_oldresiduecongruence))))))))) -> (exists pfc_terms_code_shift_coefficient_new pfc_terms_scale_shift_coefficient_new pfc_natural_sum_shift_coefficient_new. ((forall pfc_index_shift_coefficient_newdiagonal. (exists pfa_gap_shift_coefficient_newdiagonalbound. pfa_gap_shift_coefficient_newdiagonalbound + S (pfc_index_shift_coefficient_newdiagonal) = (S (i))) -> exists pfc_value_shift_coefficient_newdiagonal. ((((exists ff_h_pfp_shift_coefficient_newdiagonalentry. ff_h_pfp_shift_coefficient_newdiagonalentry + S (pfc_value_shift_coefficient_newdiagonal) = S ((S (pfc_index_shift_coefficient_newdiagonal)) * pfc_terms_scale_shift_coefficient_new)) /\ exists ff_q_pfp_shift_coefficient_newdiagonalentry. pfc_terms_code_shift_coefficient_new = ff_q_pfp_shift_coefficient_newdiagonalentry * S ((S (pfc_index_shift_coefficient_newdiagonal)) * pfc_terms_scale_shift_coefficient_new) + (pfc_value_shift_coefficient_newdiagonal))) /\ ((exists pfc_complement_shift_coefficient_newdiagonalterm pfc_left_shift_coefficient_newdiagonalterm pfc_right_shift_coefficient_newdiagonalterm. (((pfc_index_shift_coefficient_newdiagonal)+pfc_complement_shift_coefficient_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_coefficient_newdiagonaltermleftinside. pfa_gap_shift_coefficient_newdiagonaltermleftinside + S (pfc_index_shift_coefficient_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_coefficient_newdiagonaltermleftentry. ff_h_pfp_shift_coefficient_newdiagonaltermleftentry + S (pfc_left_shift_coefficient_newdiagonalterm) = S ((S (pfc_index_shift_coefficient_newdiagonal)) * ac)) /\ exists ff_q_pfp_shift_coefficient_newdiagonaltermleftentry. ab = ff_q_pfp_shift_coefficient_newdiagonaltermleftentry * S ((S (pfc_index_shift_coefficient_newdiagonal)) * ac) + (pfc_left_shift_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_newdiagonaltermleftoutside. pfc_gap_shift_coefficient_newdiagonaltermleftoutside+(L)=(pfc_index_shift_coefficient_newdiagonal)) /\ (((pfc_left_shift_coefficient_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_coefficient_newdiagonaltermrightinside. pfa_gap_shift_coefficient_newdiagonaltermrightinside + S (pfc_complement_shift_coefficient_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_coefficient_newdiagonaltermrightentry. ff_h_pfp_shift_coefficient_newdiagonaltermrightentry + S (pfc_right_shift_coefficient_newdiagonalterm) = S ((S (pfc_complement_shift_coefficient_newdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_coefficient_newdiagonaltermrightentry. BB = ff_q_pfp_shift_coefficient_newdiagonaltermrightentry * S ((S (pfc_complement_shift_coefficient_newdiagonalterm)) * BC) + (pfc_right_shift_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_newdiagonaltermrightoutside. pfc_gap_shift_coefficient_newdiagonaltermrightoutside+(S M)=(pfc_complement_shift_coefficient_newdiagonalterm)) /\ (((pfc_right_shift_coefficient_newdiagonalterm)=0))))) /\ (((pfc_value_shift_coefficient_newdiagonal)=pfc_left_shift_coefficient_newdiagonalterm*pfc_right_shift_coefficient_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_coefficient_newsum fs_v_pfc_shift_coefficient_newsum. ((((exists fs_h_pfc_shift_coefficient_newsum_body_start. fs_h_pfc_shift_coefficient_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_start. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_start * S ((S (0)) * fs_v_pfc_shift_coefficient_newsum) + (0))) /\ ((((exists fs_h_pfc_shift_coefficient_newsum_body_terminal. fs_h_pfc_shift_coefficient_newsum_body_terminal + S (pfc_natural_sum_shift_coefficient_new) = S ((S (S (i))) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_terminal. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_coefficient_newsum) + (pfc_natural_sum_shift_coefficient_new))) /\ forall fs_i_pfc_shift_coefficient_newsum_body_steps. (exists fs_lt_pfc_shift_coefficient_newsum_body_steps_bound. fs_lt_pfc_shift_coefficient_newsum_body_steps_bound + S fs_i_pfc_shift_coefficient_newsum_body_steps = S (i)) -> exists fs_a_pfc_shift_coefficient_newsum_body_steps fs_r_pfc_shift_coefficient_newsum_body_steps fs_s_pfc_shift_coefficient_newsum_body_steps. ((((exists fs_h_pfc_shift_coefficient_newsum_body_steps_summand. fs_h_pfc_shift_coefficient_newsum_body_steps_summand + S (fs_a_pfc_shift_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * pfc_terms_scale_shift_coefficient_new)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_steps_summand. pfc_terms_code_shift_coefficient_new = fs_q_pfc_shift_coefficient_newsum_body_steps_summand * S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * pfc_terms_scale_shift_coefficient_new) + (fs_a_pfc_shift_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_newsum_body_steps_partial. fs_h_pfc_shift_coefficient_newsum_body_steps_partial + S (fs_r_pfc_shift_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_steps_partial. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_steps_partial * S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum) + (fs_r_pfc_shift_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_newsum_body_steps_successor. fs_h_pfc_shift_coefficient_newsum_body_steps_successor + S (fs_s_pfc_shift_coefficient_newsum_body_steps) = S ((S (S fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_steps_successor. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_steps_successor * S ((S (S fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum) + (fs_s_pfc_shift_coefficient_newsum_body_steps))) /\ fs_s_pfc_shift_coefficient_newsum_body_steps = fs_r_pfc_shift_coefficient_newsum_body_steps + fs_a_pfc_shift_coefficient_newsum_body_steps)))))) /\ ((((exists pfa_gap_shift_coefficient_newresiduebound. pfa_gap_shift_coefficient_newresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_shift_coefficient_newresiduecongruence pfa_offset_right_shift_coefficient_newresiduecongruence. (pfc_natural_sum_shift_coefficient_new) + (p) * pfa_offset_left_shift_coefficient_newresiduecongruence = (r) + (p) * pfa_offset_right_shift_coefficient_newresiduecongruence)))))))))) /\ (((exists pfc_terms_code_shift_coefficient_new pfc_terms_scale_shift_coefficient_new pfc_natural_sum_shift_coefficient_new. ((forall pfc_index_shift_coefficient_newdiagonal. (exists pfa_gap_shift_coefficient_newdiagonalbound. pfa_gap_shift_coefficient_newdiagonalbound + S (pfc_index_shift_coefficient_newdiagonal) = (S (i))) -> exists pfc_value_shift_coefficient_newdiagonal. ((((exists ff_h_pfp_shift_coefficient_newdiagonalentry. ff_h_pfp_shift_coefficient_newdiagonalentry + S (pfc_value_shift_coefficient_newdiagonal) = S ((S (pfc_index_shift_coefficient_newdiagonal)) * pfc_terms_scale_shift_coefficient_new)) /\ exists ff_q_pfp_shift_coefficient_newdiagonalentry. pfc_terms_code_shift_coefficient_new = ff_q_pfp_shift_coefficient_newdiagonalentry * S ((S (pfc_index_shift_coefficient_newdiagonal)) * pfc_terms_scale_shift_coefficient_new) + (pfc_value_shift_coefficient_newdiagonal))) /\ ((exists pfc_complement_shift_coefficient_newdiagonalterm pfc_left_shift_coefficient_newdiagonalterm pfc_right_shift_coefficient_newdiagonalterm. (((pfc_index_shift_coefficient_newdiagonal)+pfc_complement_shift_coefficient_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_coefficient_newdiagonaltermleftinside. pfa_gap_shift_coefficient_newdiagonaltermleftinside + S (pfc_index_shift_coefficient_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_coefficient_newdiagonaltermleftentry. ff_h_pfp_shift_coefficient_newdiagonaltermleftentry + S (pfc_left_shift_coefficient_newdiagonalterm) = S ((S (pfc_index_shift_coefficient_newdiagonal)) * ac)) /\ exists ff_q_pfp_shift_coefficient_newdiagonaltermleftentry. ab = ff_q_pfp_shift_coefficient_newdiagonaltermleftentry * S ((S (pfc_index_shift_coefficient_newdiagonal)) * ac) + (pfc_left_shift_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_newdiagonaltermleftoutside. pfc_gap_shift_coefficient_newdiagonaltermleftoutside+(L)=(pfc_index_shift_coefficient_newdiagonal)) /\ (((pfc_left_shift_coefficient_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_coefficient_newdiagonaltermrightinside. pfa_gap_shift_coefficient_newdiagonaltermrightinside + S (pfc_complement_shift_coefficient_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_coefficient_newdiagonaltermrightentry. ff_h_pfp_shift_coefficient_newdiagonaltermrightentry + S (pfc_right_shift_coefficient_newdiagonalterm) = S ((S (pfc_complement_shift_coefficient_newdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_coefficient_newdiagonaltermrightentry. BB = ff_q_pfp_shift_coefficient_newdiagonaltermrightentry * S ((S (pfc_complement_shift_coefficient_newdiagonalterm)) * BC) + (pfc_right_shift_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_newdiagonaltermrightoutside. pfc_gap_shift_coefficient_newdiagonaltermrightoutside+(S M)=(pfc_complement_shift_coefficient_newdiagonalterm)) /\ (((pfc_right_shift_coefficient_newdiagonalterm)=0))))) /\ (((pfc_value_shift_coefficient_newdiagonal)=pfc_left_shift_coefficient_newdiagonalterm*pfc_right_shift_coefficient_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_coefficient_newsum fs_v_pfc_shift_coefficient_newsum. ((((exists fs_h_pfc_shift_coefficient_newsum_body_start. fs_h_pfc_shift_coefficient_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_start. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_start * S ((S (0)) * fs_v_pfc_shift_coefficient_newsum) + (0))) /\ ((((exists fs_h_pfc_shift_coefficient_newsum_body_terminal. fs_h_pfc_shift_coefficient_newsum_body_terminal + S (pfc_natural_sum_shift_coefficient_new) = S ((S (S (i))) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_terminal. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_coefficient_newsum) + (pfc_natural_sum_shift_coefficient_new))) /\ forall fs_i_pfc_shift_coefficient_newsum_body_steps. (exists fs_lt_pfc_shift_coefficient_newsum_body_steps_bound. fs_lt_pfc_shift_coefficient_newsum_body_steps_bound + S fs_i_pfc_shift_coefficient_newsum_body_steps = S (i)) -> exists fs_a_pfc_shift_coefficient_newsum_body_steps fs_r_pfc_shift_coefficient_newsum_body_steps fs_s_pfc_shift_coefficient_newsum_body_steps. ((((exists fs_h_pfc_shift_coefficient_newsum_body_steps_summand. fs_h_pfc_shift_coefficient_newsum_body_steps_summand + S (fs_a_pfc_shift_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * pfc_terms_scale_shift_coefficient_new)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_steps_summand. pfc_terms_code_shift_coefficient_new = fs_q_pfc_shift_coefficient_newsum_body_steps_summand * S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * pfc_terms_scale_shift_coefficient_new) + (fs_a_pfc_shift_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_newsum_body_steps_partial. fs_h_pfc_shift_coefficient_newsum_body_steps_partial + S (fs_r_pfc_shift_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_steps_partial. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_steps_partial * S ((S (fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum) + (fs_r_pfc_shift_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_newsum_body_steps_successor. fs_h_pfc_shift_coefficient_newsum_body_steps_successor + S (fs_s_pfc_shift_coefficient_newsum_body_steps) = S ((S (S fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum)) /\ exists fs_q_pfc_shift_coefficient_newsum_body_steps_successor. fs_u_pfc_shift_coefficient_newsum = fs_q_pfc_shift_coefficient_newsum_body_steps_successor * S ((S (S fs_i_pfc_shift_coefficient_newsum_body_steps)) * fs_v_pfc_shift_coefficient_newsum) + (fs_s_pfc_shift_coefficient_newsum_body_steps))) /\ fs_s_pfc_shift_coefficient_newsum_body_steps = fs_r_pfc_shift_coefficient_newsum_body_steps + fs_a_pfc_shift_coefficient_newsum_body_steps)))))) /\ ((((exists pfa_gap_shift_coefficient_newresiduebound. pfa_gap_shift_coefficient_newresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_shift_coefficient_newresiduecongruence pfa_offset_right_shift_coefficient_newresiduecongruence. (pfc_natural_sum_shift_coefficient_new) + (p) * pfa_offset_left_shift_coefficient_newresiduecongruence = (r) + (p) * pfa_offset_right_shift_coefficient_newresiduecongruence))))))))) -> (exists pfc_terms_code_shift_coefficient_old pfc_terms_scale_shift_coefficient_old pfc_natural_sum_shift_coefficient_old. ((forall pfc_index_shift_coefficient_olddiagonal. (exists pfa_gap_shift_coefficient_olddiagonalbound. pfa_gap_shift_coefficient_olddiagonalbound + S (pfc_index_shift_coefficient_olddiagonal) = (S (i))) -> exists pfc_value_shift_coefficient_olddiagonal. ((((exists ff_h_pfp_shift_coefficient_olddiagonalentry. ff_h_pfp_shift_coefficient_olddiagonalentry + S (pfc_value_shift_coefficient_olddiagonal) = S ((S (pfc_index_shift_coefficient_olddiagonal)) * pfc_terms_scale_shift_coefficient_old)) /\ exists ff_q_pfp_shift_coefficient_olddiagonalentry. pfc_terms_code_shift_coefficient_old = ff_q_pfp_shift_coefficient_olddiagonalentry * S ((S (pfc_index_shift_coefficient_olddiagonal)) * pfc_terms_scale_shift_coefficient_old) + (pfc_value_shift_coefficient_olddiagonal))) /\ ((exists pfc_complement_shift_coefficient_olddiagonalterm pfc_left_shift_coefficient_olddiagonalterm pfc_right_shift_coefficient_olddiagonalterm. (((pfc_index_shift_coefficient_olddiagonal)+pfc_complement_shift_coefficient_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_coefficient_olddiagonaltermleftinside. pfa_gap_shift_coefficient_olddiagonaltermleftinside + S (pfc_index_shift_coefficient_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_coefficient_olddiagonaltermleftentry. ff_h_pfp_shift_coefficient_olddiagonaltermleftentry + S (pfc_left_shift_coefficient_olddiagonalterm) = S ((S (pfc_index_shift_coefficient_olddiagonal)) * ac)) /\ exists ff_q_pfp_shift_coefficient_olddiagonaltermleftentry. ab = ff_q_pfp_shift_coefficient_olddiagonaltermleftentry * S ((S (pfc_index_shift_coefficient_olddiagonal)) * ac) + (pfc_left_shift_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_olddiagonaltermleftoutside. pfc_gap_shift_coefficient_olddiagonaltermleftoutside+(L)=(pfc_index_shift_coefficient_olddiagonal)) /\ (((pfc_left_shift_coefficient_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_coefficient_olddiagonaltermrightinside. pfa_gap_shift_coefficient_olddiagonaltermrightinside + S (pfc_complement_shift_coefficient_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_coefficient_olddiagonaltermrightentry. ff_h_pfp_shift_coefficient_olddiagonaltermrightentry + S (pfc_right_shift_coefficient_olddiagonalterm) = S ((S (pfc_complement_shift_coefficient_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_coefficient_olddiagonaltermrightentry. bb = ff_q_pfp_shift_coefficient_olddiagonaltermrightentry * S ((S (pfc_complement_shift_coefficient_olddiagonalterm)) * bc) + (pfc_right_shift_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_coefficient_olddiagonaltermrightoutside. pfc_gap_shift_coefficient_olddiagonaltermrightoutside+(M)=(pfc_complement_shift_coefficient_olddiagonalterm)) /\ (((pfc_right_shift_coefficient_olddiagonalterm)=0))))) /\ (((pfc_value_shift_coefficient_olddiagonal)=pfc_left_shift_coefficient_olddiagonalterm*pfc_right_shift_coefficient_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_coefficient_oldsum fs_v_pfc_shift_coefficient_oldsum. ((((exists fs_h_pfc_shift_coefficient_oldsum_body_start. fs_h_pfc_shift_coefficient_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_start. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_start * S ((S (0)) * fs_v_pfc_shift_coefficient_oldsum) + (0))) /\ ((((exists fs_h_pfc_shift_coefficient_oldsum_body_terminal. fs_h_pfc_shift_coefficient_oldsum_body_terminal + S (pfc_natural_sum_shift_coefficient_old) = S ((S (S (i))) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_terminal. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_coefficient_oldsum) + (pfc_natural_sum_shift_coefficient_old))) /\ forall fs_i_pfc_shift_coefficient_oldsum_body_steps. (exists fs_lt_pfc_shift_coefficient_oldsum_body_steps_bound. fs_lt_pfc_shift_coefficient_oldsum_body_steps_bound + S fs_i_pfc_shift_coefficient_oldsum_body_steps = S (i)) -> exists fs_a_pfc_shift_coefficient_oldsum_body_steps fs_r_pfc_shift_coefficient_oldsum_body_steps fs_s_pfc_shift_coefficient_oldsum_body_steps. ((((exists fs_h_pfc_shift_coefficient_oldsum_body_steps_summand. fs_h_pfc_shift_coefficient_oldsum_body_steps_summand + S (fs_a_pfc_shift_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * pfc_terms_scale_shift_coefficient_old)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_steps_summand. pfc_terms_code_shift_coefficient_old = fs_q_pfc_shift_coefficient_oldsum_body_steps_summand * S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * pfc_terms_scale_shift_coefficient_old) + (fs_a_pfc_shift_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_oldsum_body_steps_partial. fs_h_pfc_shift_coefficient_oldsum_body_steps_partial + S (fs_r_pfc_shift_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_steps_partial. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_steps_partial * S ((S (fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum) + (fs_r_pfc_shift_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_coefficient_oldsum_body_steps_successor. fs_h_pfc_shift_coefficient_oldsum_body_steps_successor + S (fs_s_pfc_shift_coefficient_oldsum_body_steps) = S ((S (S fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum)) /\ exists fs_q_pfc_shift_coefficient_oldsum_body_steps_successor. fs_u_pfc_shift_coefficient_oldsum = fs_q_pfc_shift_coefficient_oldsum_body_steps_successor * S ((S (S fs_i_pfc_shift_coefficient_oldsum_body_steps)) * fs_v_pfc_shift_coefficient_oldsum) + (fs_s_pfc_shift_coefficient_oldsum_body_steps))) /\ fs_s_pfc_shift_coefficient_oldsum_body_steps = fs_r_pfc_shift_coefficient_oldsum_body_steps + fs_a_pfc_shift_coefficient_oldsum_body_steps)))))) /\ ((((exists pfa_gap_shift_coefficient_oldresiduebound. pfa_gap_shift_coefficient_oldresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_shift_coefficient_oldresiduecongruence pfa_offset_right_shift_coefficient_oldresiduecongruence. (pfc_natural_sum_shift_coefficient_old) + (p) * pfa_offset_left_shift_coefficient_oldresiduecongruence = (r) + (p) * pfa_offset_right_shift_coefficient_oldresiduecongruence)))))))))))))