prime_field_polynomial_convolution_shift_right_empty

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M cb cc N BB BC db dc K. (~(p=0)) -> (((forall mdr_i_pfp_shift_empty_factorprefix mdr_a_pfp_shift_empty_factorprefix. (exists mdr_gap_pfp_shift_empty_factorprefixb. mdr_gap_pfp_shift_empty_factorprefixb + S (mdr_i_pfp_shift_empty_factorprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_empty_factorprefixo. ff_h_mdr_pfp_shift_empty_factorprefixo + S (mdr_a_pfp_shift_empty_factorprefix) = S ((S (mdr_i_pfp_shift_empty_factorprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_empty_factorprefixo. bb = ff_q_mdr_pfp_shift_empty_factorprefixo * S ((S (mdr_i_pfp_shift_empty_factorprefix)) * bc) + (mdr_a_pfp_shift_empty_factorprefix))) -> (((exists ff_h_mdr_pfp_shift_empty_factorprefixn. ff_h_mdr_pfp_shift_empty_factorprefixn + S (mdr_a_pfp_shift_empty_factorprefix) = S ((S (mdr_i_pfp_shift_empty_factorprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_empty_factorprefixn. BB = ff_q_mdr_pfp_shift_empty_factorprefixn * S ((S (mdr_i_pfp_shift_empty_factorprefix)) * BC) + (mdr_a_pfp_shift_empty_factorprefix)))) /\ ((((exists ff_h_pfp_shift_empty_factorlast. ff_h_pfp_shift_empty_factorlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_empty_factorlast. BB = ff_q_pfp_shift_empty_factorlast * S ((S (M)) * BC) + (0)))))) -> (((forall fom_index_pfp_shift_empty_oldleft. (exists fom_gap_pfp_shift_empty_oldleft_index_bound. fom_gap_pfp_shift_empty_oldleft_index_bound + S (fom_index_pfp_shift_empty_oldleft) = L) -> exists fom_value_pfp_shift_empty_oldleft. ((((exists fom_beta_height_pfp_shift_empty_oldleft_entry. fom_beta_height_pfp_shift_empty_oldleft_entry + S (fom_value_pfp_shift_empty_oldleft) = S ((S (fom_index_pfp_shift_empty_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_empty_oldleft_entry. ab = fom_beta_quotient_pfp_shift_empty_oldleft_entry * S ((S (fom_index_pfp_shift_empty_oldleft)) * ac) + (fom_value_pfp_shift_empty_oldleft))) /\ (exists fom_gap_pfp_shift_empty_oldleft_value_bound. fom_gap_pfp_shift_empty_oldleft_value_bound + S (fom_value_pfp_shift_empty_oldleft) = p))) /\ (((forall fom_index_pfp_shift_empty_oldright. (exists fom_gap_pfp_shift_empty_oldright_index_bound. fom_gap_pfp_shift_empty_oldright_index_bound + S (fom_index_pfp_shift_empty_oldright) = M) -> exists fom_value_pfp_shift_empty_oldright. ((((exists fom_beta_height_pfp_shift_empty_oldright_entry. fom_beta_height_pfp_shift_empty_oldright_entry + S (fom_value_pfp_shift_empty_oldright) = S ((S (fom_index_pfp_shift_empty_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_shift_empty_oldright_entry. bb = fom_beta_quotient_pfp_shift_empty_oldright_entry * S ((S (fom_index_pfp_shift_empty_oldright)) * bc) + (fom_value_pfp_shift_empty_oldright))) /\ (exists fom_gap_pfp_shift_empty_oldright_value_bound. fom_gap_pfp_shift_empty_oldright_value_bound + S (fom_value_pfp_shift_empty_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_shift_empty_oldcoefficients. (exists pfa_gap_shift_empty_oldcoefficientsbound. pfa_gap_shift_empty_oldcoefficientsbound + S (pfc_index_shift_empty_oldcoefficients) = (N)) -> exists pfc_value_shift_empty_oldcoefficients. ((((exists ff_h_pfp_shift_empty_oldcoefficientsentry. ff_h_pfp_shift_empty_oldcoefficientsentry + S (pfc_value_shift_empty_oldcoefficients) = S ((S (pfc_index_shift_empty_oldcoefficients)) * cc)) /\ exists ff_q_pfp_shift_empty_oldcoefficientsentry. cb = ff_q_pfp_shift_empty_oldcoefficientsentry * S ((S (pfc_index_shift_empty_oldcoefficients)) * cc) + (pfc_value_shift_empty_oldcoefficients))) /\ ((exists pfc_terms_code_shift_empty_oldcoefficientscoefficient pfc_terms_scale_shift_empty_oldcoefficientscoefficient pfc_natural_sum_shift_empty_oldcoefficientscoefficient. ((forall pfc_index_shift_empty_oldcoefficientscoefficientdiagonal. (exists pfa_gap_shift_empty_oldcoefficientscoefficientdiagonalbound. pfa_gap_shift_empty_oldcoefficientscoefficientdiagonalbound + S (pfc_index_shift_empty_oldcoefficientscoefficientdiagonal) = (S (pfc_index_shift_empty_oldcoefficients))) -> exists pfc_value_shift_empty_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_empty_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_empty_oldcoefficientscoefficientdiagonalentry + S (pfc_value_shift_empty_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_empty_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_empty_oldcoefficientscoefficient)) /\ exists ff_q_pfp_shift_empty_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_empty_oldcoefficientscoefficient = ff_q_pfp_shift_empty_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_empty_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_empty_oldcoefficientscoefficient) + (pfc_value_shift_empty_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_empty_oldcoefficientscoefficientdiagonalterm pfc_left_shift_empty_oldcoefficientscoefficientdiagonalterm pfc_right_shift_empty_oldcoefficientscoefficientdiagonalterm. (((pfc_index_shift_empty_oldcoefficientscoefficientdiagonal)+pfc_complement_shift_empty_oldcoefficientscoefficientdiagonalterm=(pfc_index_shift_empty_oldcoefficients)) /\ ((((((exists pfa_gap_shift_empty_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_empty_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_empty_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_empty_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_empty_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_empty_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_empty_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_empty_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_empty_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_empty_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_empty_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_empty_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_empty_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_empty_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_empty_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_empty_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_shift_empty_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_empty_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_shift_empty_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_empty_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_empty_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_shift_empty_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_empty_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_empty_oldcoefficientscoefficientdiagonal)=pfc_left_shift_empty_oldcoefficientscoefficientdiagonalterm*pfc_right_shift_empty_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_empty_oldcoefficientscoefficientsum fs_v_pfc_shift_empty_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_start. fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_start. fs_u_pfc_shift_empty_oldcoefficientscoefficientsum = fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_empty_oldcoefficientscoefficient) = S ((S (S (pfc_index_shift_empty_oldcoefficients))) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_empty_oldcoefficientscoefficientsum = fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_empty_oldcoefficients))) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum) + (pfc_natural_sum_shift_empty_oldcoefficientscoefficient))) /\ forall fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps = S (pfc_index_shift_empty_oldcoefficients)) -> exists fs_a_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps fs_r_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps fs_s_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_empty_oldcoefficientscoefficient)) /\ exists fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_empty_oldcoefficientscoefficient = fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_empty_oldcoefficientscoefficient) + (fs_a_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_empty_oldcoefficientscoefficientsum = fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum) + (fs_r_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_empty_oldcoefficientscoefficientsum = fs_q_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_oldcoefficientscoefficientsum) + (fs_s_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_empty_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_empty_oldcoefficientscoefficientresiduebound. pfa_gap_shift_empty_oldcoefficientscoefficientresiduebound + S (pfc_value_shift_empty_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_empty_oldcoefficientscoefficientresiduecongruence pfa_offset_right_shift_empty_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_empty_oldcoefficientscoefficient) + (p) * pfa_offset_left_shift_empty_oldcoefficientscoefficientresiduecongruence = (pfc_value_shift_empty_oldcoefficients) + (p) * pfa_offset_right_shift_empty_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_shift_empty_newleft. (exists fom_gap_pfp_shift_empty_newleft_index_bound. fom_gap_pfp_shift_empty_newleft_index_bound + S (fom_index_pfp_shift_empty_newleft) = L) -> exists fom_value_pfp_shift_empty_newleft. ((((exists fom_beta_height_pfp_shift_empty_newleft_entry. fom_beta_height_pfp_shift_empty_newleft_entry + S (fom_value_pfp_shift_empty_newleft) = S ((S (fom_index_pfp_shift_empty_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_empty_newleft_entry. ab = fom_beta_quotient_pfp_shift_empty_newleft_entry * S ((S (fom_index_pfp_shift_empty_newleft)) * ac) + (fom_value_pfp_shift_empty_newleft))) /\ (exists fom_gap_pfp_shift_empty_newleft_value_bound. fom_gap_pfp_shift_empty_newleft_value_bound + S (fom_value_pfp_shift_empty_newleft) = p))) /\ (((forall fom_index_pfp_shift_empty_newright. (exists fom_gap_pfp_shift_empty_newright_index_bound. fom_gap_pfp_shift_empty_newright_index_bound + S (fom_index_pfp_shift_empty_newright) = S M) -> exists fom_value_pfp_shift_empty_newright. ((((exists fom_beta_height_pfp_shift_empty_newright_entry. fom_beta_height_pfp_shift_empty_newright_entry + S (fom_value_pfp_shift_empty_newright) = S ((S (fom_index_pfp_shift_empty_newright)) * BC)) /\ exists fom_beta_quotient_pfp_shift_empty_newright_entry. BB = fom_beta_quotient_pfp_shift_empty_newright_entry * S ((S (fom_index_pfp_shift_empty_newright)) * BC) + (fom_value_pfp_shift_empty_newright))) /\ (exists fom_gap_pfp_shift_empty_newright_value_bound. fom_gap_pfp_shift_empty_newright_value_bound + S (fom_value_pfp_shift_empty_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_shift_empty_newcoefficients. (exists pfa_gap_shift_empty_newcoefficientsbound. pfa_gap_shift_empty_newcoefficientsbound + S (pfc_index_shift_empty_newcoefficients) = (K)) -> exists pfc_value_shift_empty_newcoefficients. ((((exists ff_h_pfp_shift_empty_newcoefficientsentry. ff_h_pfp_shift_empty_newcoefficientsentry + S (pfc_value_shift_empty_newcoefficients) = S ((S (pfc_index_shift_empty_newcoefficients)) * dc)) /\ exists ff_q_pfp_shift_empty_newcoefficientsentry. db = ff_q_pfp_shift_empty_newcoefficientsentry * S ((S (pfc_index_shift_empty_newcoefficients)) * dc) + (pfc_value_shift_empty_newcoefficients))) /\ ((exists pfc_terms_code_shift_empty_newcoefficientscoefficient pfc_terms_scale_shift_empty_newcoefficientscoefficient pfc_natural_sum_shift_empty_newcoefficientscoefficient. ((forall pfc_index_shift_empty_newcoefficientscoefficientdiagonal. (exists pfa_gap_shift_empty_newcoefficientscoefficientdiagonalbound. pfa_gap_shift_empty_newcoefficientscoefficientdiagonalbound + S (pfc_index_shift_empty_newcoefficientscoefficientdiagonal) = (S (pfc_index_shift_empty_newcoefficients))) -> exists pfc_value_shift_empty_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_empty_newcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_empty_newcoefficientscoefficientdiagonalentry + S (pfc_value_shift_empty_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_empty_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_empty_newcoefficientscoefficient)) /\ exists ff_q_pfp_shift_empty_newcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_empty_newcoefficientscoefficient = ff_q_pfp_shift_empty_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_empty_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_empty_newcoefficientscoefficient) + (pfc_value_shift_empty_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_empty_newcoefficientscoefficientdiagonalterm pfc_left_shift_empty_newcoefficientscoefficientdiagonalterm pfc_right_shift_empty_newcoefficientscoefficientdiagonalterm. (((pfc_index_shift_empty_newcoefficientscoefficientdiagonal)+pfc_complement_shift_empty_newcoefficientscoefficientdiagonalterm=(pfc_index_shift_empty_newcoefficients)) /\ ((((((exists pfa_gap_shift_empty_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_empty_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_empty_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_empty_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_empty_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_empty_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_empty_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_empty_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_empty_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_empty_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_empty_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_empty_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_empty_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_empty_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_empty_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_empty_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_empty_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_empty_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_empty_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_empty_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_empty_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_empty_newcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_empty_newcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_empty_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_empty_newcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_shift_empty_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_empty_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_empty_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_empty_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_empty_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_empty_newcoefficientscoefficientdiagonal)=pfc_left_shift_empty_newcoefficientscoefficientdiagonalterm*pfc_right_shift_empty_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_empty_newcoefficientscoefficientsum fs_v_pfc_shift_empty_newcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_start. fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_start. fs_u_pfc_shift_empty_newcoefficientscoefficientsum = fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_empty_newcoefficientscoefficient) = S ((S (S (pfc_index_shift_empty_newcoefficients))) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_empty_newcoefficientscoefficientsum = fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_empty_newcoefficients))) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum) + (pfc_natural_sum_shift_empty_newcoefficientscoefficient))) /\ forall fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps = S (pfc_index_shift_empty_newcoefficients)) -> exists fs_a_pfc_shift_empty_newcoefficientscoefficientsum_body_steps fs_r_pfc_shift_empty_newcoefficientscoefficientsum_body_steps fs_s_pfc_shift_empty_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_empty_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_empty_newcoefficientscoefficient)) /\ exists fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_empty_newcoefficientscoefficient = fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_empty_newcoefficientscoefficient) + (fs_a_pfc_shift_empty_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_empty_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_empty_newcoefficientscoefficientsum = fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum) + (fs_r_pfc_shift_empty_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_empty_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_empty_newcoefficientscoefficientsum = fs_q_pfc_shift_empty_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_empty_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_empty_newcoefficientscoefficientsum) + (fs_s_pfc_shift_empty_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_empty_newcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_empty_newcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_empty_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_empty_newcoefficientscoefficientresiduebound. pfa_gap_shift_empty_newcoefficientscoefficientresiduebound + S (pfc_value_shift_empty_newcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_empty_newcoefficientscoefficientresiduecongruence pfa_offset_right_shift_empty_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_empty_newcoefficientscoefficient) + (p) * pfa_offset_left_shift_empty_newcoefficientscoefficientresiduecongruence = (pfc_value_shift_empty_newcoefficients) + (p) * pfa_offset_right_shift_empty_newcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (L=0 \/ M=0) -> (((forall pfp_repeat_index_shift_empty_old_zero. (exists pfa_gap_shift_empty_old_zeroindex. pfa_gap_shift_empty_old_zeroindex + S (pfp_repeat_index_shift_empty_old_zero) = (N)) -> (((exists ff_h_pfp_shift_empty_old_zeroentry. ff_h_pfp_shift_empty_old_zeroentry + S (0) = S ((S (pfp_repeat_index_shift_empty_old_zero)) * cc)) /\ exists ff_q_pfp_shift_empty_old_zeroentry. cb = ff_q_pfp_shift_empty_old_zeroentry * S ((S (pfp_repeat_index_shift_empty_old_zero)) * cc) + (0)))) /\ ((forall pfp_repeat_index_shift_empty_new_zero. (exists pfa_gap_shift_empty_new_zeroindex. pfa_gap_shift_empty_new_zeroindex + S (pfp_repeat_index_shift_empty_new_zero) = (K)) -> (((exists ff_h_pfp_shift_empty_new_zeroentry. ff_h_pfp_shift_empty_new_zeroentry + S (0) = S ((S (pfp_repeat_index_shift_empty_new_zero)) * dc)) /\ exists ff_q_pfp_shift_empty_new_zeroentry. db = ff_q_pfp_shift_empty_new_zeroentry * S ((S (pfp_repeat_index_shift_empty_new_zero)) * dc) + (0)))))))