prime_field_polynomial_convolution_shift_right_nonempty

forall p ab ac L bb bc M cb cc N BB BC db dc K. (~(p=0)) -> (~(L=0)) -> (~(M=0)) -> (((forall mdr_i_pfp_shift_product_factorprefix mdr_a_pfp_shift_product_factorprefix. (exists mdr_gap_pfp_shift_product_factorprefixb. mdr_gap_pfp_shift_product_factorprefixb + S (mdr_i_pfp_shift_product_factorprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_product_factorprefixo. ff_h_mdr_pfp_shift_product_factorprefixo + S (mdr_a_pfp_shift_product_factorprefix) = S ((S (mdr_i_pfp_shift_product_factorprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_product_factorprefixo. bb = ff_q_mdr_pfp_shift_product_factorprefixo * S ((S (mdr_i_pfp_shift_product_factorprefix)) * bc) + (mdr_a_pfp_shift_product_factorprefix))) -> (((exists ff_h_mdr_pfp_shift_product_factorprefixn. ff_h_mdr_pfp_shift_product_factorprefixn + S (mdr_a_pfp_shift_product_factorprefix) = S ((S (mdr_i_pfp_shift_product_factorprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_product_factorprefixn. BB = ff_q_mdr_pfp_shift_product_factorprefixn * S ((S (mdr_i_pfp_shift_product_factorprefix)) * BC) + (mdr_a_pfp_shift_product_factorprefix)))) /\ ((((exists ff_h_pfp_shift_product_factorlast. ff_h_pfp_shift_product_factorlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_product_factorlast. BB = ff_q_pfp_shift_product_factorlast * S ((S (M)) * BC) + (0)))))) -> (((forall fom_index_pfp_shift_product_oldleft. (exists fom_gap_pfp_shift_product_oldleft_index_bound. fom_gap_pfp_shift_product_oldleft_index_bound + S (fom_index_pfp_shift_product_oldleft) = L) -> exists fom_value_pfp_shift_product_oldleft. ((((exists fom_beta_height_pfp_shift_product_oldleft_entry. fom_beta_height_pfp_shift_product_oldleft_entry + S (fom_value_pfp_shift_product_oldleft) = S ((S (fom_index_pfp_shift_product_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_product_oldleft_entry. ab = fom_beta_quotient_pfp_shift_product_oldleft_entry * S ((S (fom_index_pfp_shift_product_oldleft)) * ac) + (fom_value_pfp_shift_product_oldleft))) /\ (exists fom_gap_pfp_shift_product_oldleft_value_bound. fom_gap_pfp_shift_product_oldleft_value_bound + S (fom_value_pfp_shift_product_oldleft) = p))) /\ (((forall fom_index_pfp_shift_product_oldright. (exists fom_gap_pfp_shift_product_oldright_index_bound. fom_gap_pfp_shift_product_oldright_index_bound + S (fom_index_pfp_shift_product_oldright) = M) -> exists fom_value_pfp_shift_product_oldright. ((((exists fom_beta_height_pfp_shift_product_oldright_entry. fom_beta_height_pfp_shift_product_oldright_entry + S (fom_value_pfp_shift_product_oldright) = S ((S (fom_index_pfp_shift_product_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_shift_product_oldright_entry. bb = fom_beta_quotient_pfp_shift_product_oldright_entry * S ((S (fom_index_pfp_shift_product_oldright)) * bc) + (fom_value_pfp_shift_product_oldright))) /\ (exists fom_gap_pfp_shift_product_oldright_value_bound. fom_gap_pfp_shift_product_oldright_value_bound + S (fom_value_pfp_shift_product_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_shift_product_oldcoefficients. (exists pfa_gap_shift_product_oldcoefficientsbound. pfa_gap_shift_product_oldcoefficientsbound + S (pfc_index_shift_product_oldcoefficients) = (N)) -> exists pfc_value_shift_product_oldcoefficients. ((((exists ff_h_pfp_shift_product_oldcoefficientsentry. ff_h_pfp_shift_product_oldcoefficientsentry + S (pfc_value_shift_product_oldcoefficients) = S ((S (pfc_index_shift_product_oldcoefficients)) * cc)) /\ exists ff_q_pfp_shift_product_oldcoefficientsentry. cb = ff_q_pfp_shift_product_oldcoefficientsentry * S ((S (pfc_index_shift_product_oldcoefficients)) * cc) + (pfc_value_shift_product_oldcoefficients))) /\ ((exists pfc_terms_code_shift_product_oldcoefficientscoefficient pfc_terms_scale_shift_product_oldcoefficientscoefficient pfc_natural_sum_shift_product_oldcoefficientscoefficient. ((forall pfc_index_shift_product_oldcoefficientscoefficientdiagonal. (exists pfa_gap_shift_product_oldcoefficientscoefficientdiagonalbound. pfa_gap_shift_product_oldcoefficientscoefficientdiagonalbound + S (pfc_index_shift_product_oldcoefficientscoefficientdiagonal) = (S (pfc_index_shift_product_oldcoefficients))) -> exists pfc_value_shift_product_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_product_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_product_oldcoefficientscoefficientdiagonalentry + S (pfc_value_shift_product_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_product_oldcoefficientscoefficient)) /\ exists ff_q_pfp_shift_product_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_product_oldcoefficientscoefficient = ff_q_pfp_shift_product_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_product_oldcoefficientscoefficient) + (pfc_value_shift_product_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_product_oldcoefficientscoefficientdiagonalterm pfc_left_shift_product_oldcoefficientscoefficientdiagonalterm pfc_right_shift_product_oldcoefficientscoefficientdiagonalterm. (((pfc_index_shift_product_oldcoefficientscoefficientdiagonal)+pfc_complement_shift_product_oldcoefficientscoefficientdiagonalterm=(pfc_index_shift_product_oldcoefficients)) /\ ((((((exists pfa_gap_shift_product_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_product_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_product_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_product_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_product_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_product_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_product_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_product_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_product_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_product_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_product_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_product_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_product_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_product_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_product_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_shift_product_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_product_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_shift_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_product_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_shift_product_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_product_oldcoefficientscoefficientdiagonal)=pfc_left_shift_product_oldcoefficientscoefficientdiagonalterm*pfc_right_shift_product_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_oldcoefficientscoefficientsum fs_v_pfc_shift_product_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_start. fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_start. fs_u_pfc_shift_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_product_oldcoefficientscoefficient) = S ((S (S (pfc_index_shift_product_oldcoefficients))) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_product_oldcoefficients))) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum) + (pfc_natural_sum_shift_product_oldcoefficientscoefficient))) /\ forall fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps = S (pfc_index_shift_product_oldcoefficients)) -> exists fs_a_pfc_shift_product_oldcoefficientscoefficientsum_body_steps fs_r_pfc_shift_product_oldcoefficientscoefficientsum_body_steps fs_s_pfc_shift_product_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_product_oldcoefficientscoefficient)) /\ exists fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_product_oldcoefficientscoefficient = fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_product_oldcoefficientscoefficient) + (fs_a_pfc_shift_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum) + (fs_r_pfc_shift_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_product_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_product_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_oldcoefficientscoefficientsum) + (fs_s_pfc_shift_product_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_product_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_product_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_product_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_oldcoefficientscoefficientresiduebound. pfa_gap_shift_product_oldcoefficientscoefficientresiduebound + S (pfc_value_shift_product_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_product_oldcoefficientscoefficientresiduecongruence pfa_offset_right_shift_product_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_product_oldcoefficientscoefficient) + (p) * pfa_offset_left_shift_product_oldcoefficientscoefficientresiduecongruence = (pfc_value_shift_product_oldcoefficients) + (p) * pfa_offset_right_shift_product_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_shift_product_newleft. (exists fom_gap_pfp_shift_product_newleft_index_bound. fom_gap_pfp_shift_product_newleft_index_bound + S (fom_index_pfp_shift_product_newleft) = L) -> exists fom_value_pfp_shift_product_newleft. ((((exists fom_beta_height_pfp_shift_product_newleft_entry. fom_beta_height_pfp_shift_product_newleft_entry + S (fom_value_pfp_shift_product_newleft) = S ((S (fom_index_pfp_shift_product_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_product_newleft_entry. ab = fom_beta_quotient_pfp_shift_product_newleft_entry * S ((S (fom_index_pfp_shift_product_newleft)) * ac) + (fom_value_pfp_shift_product_newleft))) /\ (exists fom_gap_pfp_shift_product_newleft_value_bound. fom_gap_pfp_shift_product_newleft_value_bound + S (fom_value_pfp_shift_product_newleft) = p))) /\ (((forall fom_index_pfp_shift_product_newright. (exists fom_gap_pfp_shift_product_newright_index_bound. fom_gap_pfp_shift_product_newright_index_bound + S (fom_index_pfp_shift_product_newright) = S M) -> exists fom_value_pfp_shift_product_newright. ((((exists fom_beta_height_pfp_shift_product_newright_entry. fom_beta_height_pfp_shift_product_newright_entry + S (fom_value_pfp_shift_product_newright) = S ((S (fom_index_pfp_shift_product_newright)) * BC)) /\ exists fom_beta_quotient_pfp_shift_product_newright_entry. BB = fom_beta_quotient_pfp_shift_product_newright_entry * S ((S (fom_index_pfp_shift_product_newright)) * BC) + (fom_value_pfp_shift_product_newright))) /\ (exists fom_gap_pfp_shift_product_newright_value_bound. fom_gap_pfp_shift_product_newright_value_bound + S (fom_value_pfp_shift_product_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_shift_product_newcoefficients. (exists pfa_gap_shift_product_newcoefficientsbound. pfa_gap_shift_product_newcoefficientsbound + S (pfc_index_shift_product_newcoefficients) = (K)) -> exists pfc_value_shift_product_newcoefficients. ((((exists ff_h_pfp_shift_product_newcoefficientsentry. ff_h_pfp_shift_product_newcoefficientsentry + S (pfc_value_shift_product_newcoefficients) = S ((S (pfc_index_shift_product_newcoefficients)) * dc)) /\ exists ff_q_pfp_shift_product_newcoefficientsentry. db = ff_q_pfp_shift_product_newcoefficientsentry * S ((S (pfc_index_shift_product_newcoefficients)) * dc) + (pfc_value_shift_product_newcoefficients))) /\ ((exists pfc_terms_code_shift_product_newcoefficientscoefficient pfc_terms_scale_shift_product_newcoefficientscoefficient pfc_natural_sum_shift_product_newcoefficientscoefficient. ((forall pfc_index_shift_product_newcoefficientscoefficientdiagonal. (exists pfa_gap_shift_product_newcoefficientscoefficientdiagonalbound. pfa_gap_shift_product_newcoefficientscoefficientdiagonalbound + S (pfc_index_shift_product_newcoefficientscoefficientdiagonal) = (S (pfc_index_shift_product_newcoefficients))) -> exists pfc_value_shift_product_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_product_newcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_product_newcoefficientscoefficientdiagonalentry + S (pfc_value_shift_product_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_product_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_product_newcoefficientscoefficient)) /\ exists ff_q_pfp_shift_product_newcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_product_newcoefficientscoefficient = ff_q_pfp_shift_product_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_product_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_product_newcoefficientscoefficient) + (pfc_value_shift_product_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_product_newcoefficientscoefficientdiagonalterm pfc_left_shift_product_newcoefficientscoefficientdiagonalterm pfc_right_shift_product_newcoefficientscoefficientdiagonalterm. (((pfc_index_shift_product_newcoefficientscoefficientdiagonal)+pfc_complement_shift_product_newcoefficientscoefficientdiagonalterm=(pfc_index_shift_product_newcoefficients)) /\ ((((((exists pfa_gap_shift_product_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_product_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_product_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_product_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_product_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_product_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_product_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_product_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_product_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_product_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_product_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_product_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_product_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_product_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_product_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_product_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_product_newcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_newcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_product_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_product_newcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_shift_product_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_product_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_product_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_product_newcoefficientscoefficientdiagonal)=pfc_left_shift_product_newcoefficientscoefficientdiagonalterm*pfc_right_shift_product_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_newcoefficientscoefficientsum fs_v_pfc_shift_product_newcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_start. fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_start. fs_u_pfc_shift_product_newcoefficientscoefficientsum = fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_product_newcoefficientscoefficient) = S ((S (S (pfc_index_shift_product_newcoefficients))) * fs_v_pfc_shift_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_product_newcoefficientscoefficientsum = fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_product_newcoefficients))) * fs_v_pfc_shift_product_newcoefficientscoefficientsum) + (pfc_natural_sum_shift_product_newcoefficientscoefficient))) /\ forall fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_product_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_product_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps = S (pfc_index_shift_product_newcoefficients)) -> exists fs_a_pfc_shift_product_newcoefficientscoefficientsum_body_steps fs_r_pfc_shift_product_newcoefficientscoefficientsum_body_steps fs_s_pfc_shift_product_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_product_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_product_newcoefficientscoefficient)) /\ exists fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_product_newcoefficientscoefficient = fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_product_newcoefficientscoefficient) + (fs_a_pfc_shift_product_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_product_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_product_newcoefficientscoefficientsum = fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_newcoefficientscoefficientsum) + (fs_r_pfc_shift_product_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_product_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_product_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_product_newcoefficientscoefficientsum = fs_q_pfc_shift_product_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_product_newcoefficientscoefficientsum) + (fs_s_pfc_shift_product_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_product_newcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_product_newcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_product_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_newcoefficientscoefficientresiduebound. pfa_gap_shift_product_newcoefficientscoefficientresiduebound + S (pfc_value_shift_product_newcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_product_newcoefficientscoefficientresiduecongruence pfa_offset_right_shift_product_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_product_newcoefficientscoefficient) + (p) * pfa_offset_left_shift_product_newcoefficientscoefficientresiduecongruence = (pfc_value_shift_product_newcoefficients) + (p) * pfa_offset_right_shift_product_newcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((K=S N) /\ ((((forall mdr_i_pfp_shift_product_resultprefix mdr_a_pfp_shift_product_resultprefix. (exists mdr_gap_pfp_shift_product_resultprefixb. mdr_gap_pfp_shift_product_resultprefixb + S (mdr_i_pfp_shift_product_resultprefix) = (N)) -> (((exists ff_h_mdr_pfp_shift_product_resultprefixo. ff_h_mdr_pfp_shift_product_resultprefixo + S (mdr_a_pfp_shift_product_resultprefix) = S ((S (mdr_i_pfp_shift_product_resultprefix)) * cc)) /\ exists ff_q_mdr_pfp_shift_product_resultprefixo. cb = ff_q_mdr_pfp_shift_product_resultprefixo * S ((S (mdr_i_pfp_shift_product_resultprefix)) * cc) + (mdr_a_pfp_shift_product_resultprefix))) -> (((exists ff_h_mdr_pfp_shift_product_resultprefixn. ff_h_mdr_pfp_shift_product_resultprefixn + S (mdr_a_pfp_shift_product_resultprefix) = S ((S (mdr_i_pfp_shift_product_resultprefix)) * dc)) /\ exists ff_q_mdr_pfp_shift_product_resultprefixn. db = ff_q_mdr_pfp_shift_product_resultprefixn * S ((S (mdr_i_pfp_shift_product_resultprefix)) * dc) + (mdr_a_pfp_shift_product_resultprefix)))) /\ ((((exists ff_h_pfp_shift_product_resultlast. ff_h_pfp_shift_product_resultlast + S (0) = S ((S (N)) * dc)) /\ exists ff_q_pfp_shift_product_resultlast. db = ff_q_pfp_shift_product_resultlast * S ((S (N)) * dc) + (0)))))))))