Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
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)))))))))Constructive proof overview
Generated structural guide
For actual nonempty factors, the shifted product is exactly a trailing-zero extension of the original decoded product, at its proved successor length.
The unchanged tactic script uses 7 declared prerequisites and contains 156 exact native proof lines.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
PG0009 polynomial_product_length_shift_right_nonempty prime_field_convolution_prefix_entry Alpha theorem; checked-use authorized PG0008 prime_field_convolution_coefficient_shift_right_iff le_succ Alpha theorem; checked-use authorized prime_field_convolution_coefficient_functional Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized prime_field_polynomial_convolution_outside_zero Alpha theorem; checked-use authorizedDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Fix variables and assumptionsL21–21
Work with arbitrary variables or the premises of the current implication.
- L21
intro hd
04Establish hwholeL22–23
Establish this local claim before using it. It is not an additional assumption.
- L22
have hwhole : FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)Definitions: FpPolyProduct - L23
exact hc
05Separate the logical casesL24–29
06Establish hkL30–39
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length shift right nonempty.
- L30
have hk : K=S N - L31
specialize polynomial_product_length_shift_right_nonempty (L) - L32
specialize polynomial_product_length_shift_right_nonempty (M) - L33
specialize polynomial_product_length_shift_right_nonempty (N) - L34
specialize polynomial_product_length_shift_right_nonempty (K) - L35
apply polynomial_product_length_shift_right_nonempty - L36
exact hc_right_right_left - L37
exact hL - L38
exact hM - L39
exact hd_right_right_left
07Separate the logical casesL40–40
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L40
split
08Use earlier factsL41–41
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
exact hk
09Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
split
10Fix variables and assumptionsL43–46
11Establish hcaL47–56
Establish this local claim before using it. It is not an additional assumption.
- L47
have hca : FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,a)Definitions: FpConvolutionCoefficient - L48
specialize prime_field_convolution_prefix_entry (p) - L49
specialize prime_field_convolution_prefix_entry (ab) - L50
specialize prime_field_convolution_prefix_entry (ac) - L51
specialize prime_field_convolution_prefix_entry (L) - L52
specialize prime_field_convolution_prefix_entry (bb) - L53
specialize prime_field_convolution_prefix_entry (bc) - L54
specialize prime_field_convolution_prefix_entry (M) - L55
specialize prime_field_convolution_prefix_entry (cb) - L56
specialize prime_field_convolution_prefix_entry (cc)
12Use earlier factsL57–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
13Establish hdaL64–64
Establish this local claim before using it. It is not an additional assumption.
- L64
have hda : FpConvolutionCoefficient(p,ab,ac,L,BB,BC,S M,i,a)Definitions: FpConvolutionCoefficient
14Establish hiffL65–74
Establish this local claim before using it. It is not an additional assumption.
- L65
have hiff : (FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,a) → FpConvolutionCoefficient(p,ab,ac,L,BB,BC,S M,i,a)) ∧ (FpConvolutionCoefficient(p,ab,ac,L,BB,BC,S M,i,a) → FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,a))Definitions: FpConvolutionCoefficient - L66
specialize prime_field_convolution_coefficient_shift_right_iff (p) - L67
specialize prime_field_convolution_coefficient_shift_right_iff (ab) - L68
specialize prime_field_convolution_coefficient_shift_right_iff (ac) - L69
specialize prime_field_convolution_coefficient_shift_right_iff (L) - L70
specialize prime_field_convolution_coefficient_shift_right_iff (bb) - L71
specialize prime_field_convolution_coefficient_shift_right_iff (bc) - L72
specialize prime_field_convolution_coefficient_shift_right_iff (M) - L73
specialize prime_field_convolution_coefficient_shift_right_iff (BB) - L74
specialize prime_field_convolution_coefficient_shift_right_iff (BC)
15Use earlier factsL75–78
16Separate the logical casesL79–79
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L79
cases hiff
17Use earlier factsL80–81
18Establish hvL82–89
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hd right right right.
19Separate the logical casesL90–91
20Establish heqL92–101
Establish this local claim before using it. It is not an additional assumption.
- L92
have heq : a=x - L93
specialize prime_field_convolution_coefficient_functional (p) - L94
specialize prime_field_convolution_coefficient_functional (ab) - L95
specialize prime_field_convolution_coefficient_functional (ac) - L96
specialize prime_field_convolution_coefficient_functional (L) - L97
specialize prime_field_convolution_coefficient_functional (BB) - L98
specialize prime_field_convolution_coefficient_functional (BC) - L99
specialize prime_field_convolution_coefficient_functional (S M) - L100
specialize prime_field_convolution_coefficient_functional (i) - L101
specialize prime_field_convolution_coefficient_functional (a)
21Use earlier factsL102–105
22Calculate and transport equalitiesL106–107
23Use earlier factsL108–108
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L108
exact hv_witness_left
24Establish hvL109–114
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hd right right right.
25Separate the logical casesL115–116
26Establish hcoL117–117
Establish this local claim before using it. It is not an additional assumption.
- L117
have hco : FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,N,x)Definitions: FpConvolutionCoefficient
27Establish hiffL118–127
Establish this local claim before using it. It is not an additional assumption.
- L118
have hiff : (FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,N,x) → FpConvolutionCoefficient(p,ab,ac,L,BB,BC,S M,N,x)) ∧ (FpConvolutionCoefficient(p,ab,ac,L,BB,BC,S M,N,x) → FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,N,x))Definitions: FpConvolutionCoefficient - L119
specialize prime_field_convolution_coefficient_shift_right_iff (p) - L120
specialize prime_field_convolution_coefficient_shift_right_iff (ab) - L121
specialize prime_field_convolution_coefficient_shift_right_iff (ac) - L122
specialize prime_field_convolution_coefficient_shift_right_iff (L) - L123
specialize prime_field_convolution_coefficient_shift_right_iff (bb) - L124
specialize prime_field_convolution_coefficient_shift_right_iff (bc) - L125
specialize prime_field_convolution_coefficient_shift_right_iff (M) - L126
specialize prime_field_convolution_coefficient_shift_right_iff (BB) - L127
specialize prime_field_convolution_coefficient_shift_right_iff (BC)
28Use earlier factsL128–131
29Separate the logical casesL132–132
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L132
cases hiff
30Use earlier factsL133–134
31Establish hzL135–144
Establish this local claim before using it. It is not an additional assumption.
- L135
have hz : x=0 - L136
specialize prime_field_polynomial_convolution_outside_zero (p) - L137
specialize prime_field_polynomial_convolution_outside_zero (ab) - L138
specialize prime_field_polynomial_convolution_outside_zero (ac) - L139
specialize prime_field_polynomial_convolution_outside_zero (L) - L140
specialize prime_field_polynomial_convolution_outside_zero (bb) - L141
specialize prime_field_polynomial_convolution_outside_zero (bc) - L142
specialize prime_field_polynomial_convolution_outside_zero (M) - L143
specialize prime_field_polynomial_convolution_outside_zero (cb) - L144
specialize prime_field_polynomial_convolution_outside_zero (cc)
32Use earlier factsL145–153
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L145
specialize prime_field_polynomial_convolution_outside_zero (N) - L146
specialize prime_field_polynomial_convolution_outside_zero (N) - L147
specialize prime_field_polynomial_convolution_outside_zero (x) - L148
apply prime_field_polynomial_convolution_outside_zero - L149
exact hp - L150
exact hwhole - L151
specialize le_refl (N) - L152
apply le_refl - L153
exact hco
33Calculate and transport equalitiesL154–155
34Use earlier factsL156–156
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L156
exact hv_witness_left
Original exact command ledger · 156 lines
- 0001
intro p - 0002
intro ab - 0003
intro ac - 0004
intro L - 0005
intro bb - 0006
intro bc - 0007
intro M - 0008
intro cb - 0009
intro cc - 0010
intro N - 0011
intro BB - 0012
intro BC - 0013
intro db - 0014
intro dc - 0015
intro K - 0016
intro hp - 0017
intro hL - 0018
intro hM - 0019
intro hs - 0020
intro hc - 0021
intro hd - 0022
have hwhole : ((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)))))))))))))))))) - 0023
exact hc - 0024
cases hc - 0025
cases hc_right - 0026
cases hc_right_right - 0027
cases hd - 0028
cases hd_right - 0029
cases hd_right_right - 0030
have hk : K=S N - 0031
specialize polynomial_product_length_shift_right_nonempty (L) - 0032
specialize polynomial_product_length_shift_right_nonempty (M) - 0033
specialize polynomial_product_length_shift_right_nonempty (N) - 0034
specialize polynomial_product_length_shift_right_nonempty (K) - 0035
apply polynomial_product_length_shift_right_nonempty - 0036
exact hc_right_right_left - 0037
exact hL - 0038
exact hM - 0039
exact hd_right_right_left - 0040
split - 0041
exact hk - 0042
split - 0043
intro i - 0044
intro a - 0045
intro hi - 0046
intro ha - 0047
have hca : exists pfc_terms_code_shift_product_source_coefficient pfc_terms_scale_shift_product_source_coefficient pfc_natural_sum_shift_product_source_coefficient. ((forall pfc_index_shift_product_source_coefficientdiagonal. (exists pfa_gap_shift_product_source_coefficientdiagonalbound. pfa_gap_shift_product_source_coefficientdiagonalbound + S (pfc_index_shift_product_source_coefficientdiagonal) = (S (i))) -> exists pfc_value_shift_product_source_coefficientdiagonal. ((((exists ff_h_pfp_shift_product_source_coefficientdiagonalentry. ff_h_pfp_shift_product_source_coefficientdiagonalentry + S (pfc_value_shift_product_source_coefficientdiagonal) = S ((S (pfc_index_shift_product_source_coefficientdiagonal)) * pfc_terms_scale_shift_product_source_coefficient)) /\ exists ff_q_pfp_shift_product_source_coefficientdiagonalentry. pfc_terms_code_shift_product_source_coefficient = ff_q_pfp_shift_product_source_coefficientdiagonalentry * S ((S (pfc_index_shift_product_source_coefficientdiagonal)) * pfc_terms_scale_shift_product_source_coefficient) + (pfc_value_shift_product_source_coefficientdiagonal))) /\ ((exists pfc_complement_shift_product_source_coefficientdiagonalterm pfc_left_shift_product_source_coefficientdiagonalterm pfc_right_shift_product_source_coefficientdiagonalterm. (((pfc_index_shift_product_source_coefficientdiagonal)+pfc_complement_shift_product_source_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_product_source_coefficientdiagonaltermleftinside. pfa_gap_shift_product_source_coefficientdiagonaltermleftinside + S (pfc_index_shift_product_source_coefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_source_coefficientdiagonaltermleftentry. ff_h_pfp_shift_product_source_coefficientdiagonaltermleftentry + S (pfc_left_shift_product_source_coefficientdiagonalterm) = S ((S (pfc_index_shift_product_source_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_source_coefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_product_source_coefficientdiagonaltermleftentry * S ((S (pfc_index_shift_product_source_coefficientdiagonal)) * ac) + (pfc_left_shift_product_source_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_source_coefficientdiagonaltermleftoutside. pfc_gap_shift_product_source_coefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_product_source_coefficientdiagonal)) /\ (((pfc_left_shift_product_source_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_source_coefficientdiagonaltermrightinside. pfa_gap_shift_product_source_coefficientdiagonaltermrightinside + S (pfc_complement_shift_product_source_coefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_product_source_coefficientdiagonaltermrightentry. ff_h_pfp_shift_product_source_coefficientdiagonaltermrightentry + S (pfc_right_shift_product_source_coefficientdiagonalterm) = S ((S (pfc_complement_shift_product_source_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_product_source_coefficientdiagonaltermrightentry. bb = ff_q_pfp_shift_product_source_coefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_product_source_coefficientdiagonalterm)) * bc) + (pfc_right_shift_product_source_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_source_coefficientdiagonaltermrightoutside. pfc_gap_shift_product_source_coefficientdiagonaltermrightoutside+(M)=(pfc_complement_shift_product_source_coefficientdiagonalterm)) /\ (((pfc_right_shift_product_source_coefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_product_source_coefficientdiagonal)=pfc_left_shift_product_source_coefficientdiagonalterm*pfc_right_shift_product_source_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_source_coefficientsum fs_v_pfc_shift_product_source_coefficientsum. ((((exists fs_h_pfc_shift_product_source_coefficientsum_body_start. fs_h_pfc_shift_product_source_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_source_coefficientsum)) /\ exists fs_q_pfc_shift_product_source_coefficientsum_body_start. fs_u_pfc_shift_product_source_coefficientsum = fs_q_pfc_shift_product_source_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_source_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_source_coefficientsum_body_terminal. fs_h_pfc_shift_product_source_coefficientsum_body_terminal + S (pfc_natural_sum_shift_product_source_coefficient) = S ((S (S (i))) * fs_v_pfc_shift_product_source_coefficientsum)) /\ exists fs_q_pfc_shift_product_source_coefficientsum_body_terminal. fs_u_pfc_shift_product_source_coefficientsum = fs_q_pfc_shift_product_source_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_product_source_coefficientsum) + (pfc_natural_sum_shift_product_source_coefficient))) /\ forall fs_i_pfc_shift_product_source_coefficientsum_body_steps. (exists fs_lt_pfc_shift_product_source_coefficientsum_body_steps_bound. fs_lt_pfc_shift_product_source_coefficientsum_body_steps_bound + S fs_i_pfc_shift_product_source_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_shift_product_source_coefficientsum_body_steps fs_r_pfc_shift_product_source_coefficientsum_body_steps fs_s_pfc_shift_product_source_coefficientsum_body_steps. ((((exists fs_h_pfc_shift_product_source_coefficientsum_body_steps_summand. fs_h_pfc_shift_product_source_coefficientsum_body_steps_summand + S (fs_a_pfc_shift_product_source_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_source_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_source_coefficient)) /\ exists fs_q_pfc_shift_product_source_coefficientsum_body_steps_summand. pfc_terms_code_shift_product_source_coefficient = fs_q_pfc_shift_product_source_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_source_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_source_coefficient) + (fs_a_pfc_shift_product_source_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_source_coefficientsum_body_steps_partial. fs_h_pfc_shift_product_source_coefficientsum_body_steps_partial + S (fs_r_pfc_shift_product_source_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_source_coefficientsum_body_steps)) * fs_v_pfc_shift_product_source_coefficientsum)) /\ exists fs_q_pfc_shift_product_source_coefficientsum_body_steps_partial. fs_u_pfc_shift_product_source_coefficientsum = fs_q_pfc_shift_product_source_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_source_coefficientsum_body_steps)) * fs_v_pfc_shift_product_source_coefficientsum) + (fs_r_pfc_shift_product_source_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_source_coefficientsum_body_steps_successor. fs_h_pfc_shift_product_source_coefficientsum_body_steps_successor + S (fs_s_pfc_shift_product_source_coefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_product_source_coefficientsum_body_steps)) * fs_v_pfc_shift_product_source_coefficientsum)) /\ exists fs_q_pfc_shift_product_source_coefficientsum_body_steps_successor. fs_u_pfc_shift_product_source_coefficientsum = fs_q_pfc_shift_product_source_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_source_coefficientsum_body_steps)) * fs_v_pfc_shift_product_source_coefficientsum) + (fs_s_pfc_shift_product_source_coefficientsum_body_steps))) /\ fs_s_pfc_shift_product_source_coefficientsum_body_steps = fs_r_pfc_shift_product_source_coefficientsum_body_steps + fs_a_pfc_shift_product_source_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_source_coefficientresiduebound. pfa_gap_shift_product_source_coefficientresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_shift_product_source_coefficientresiduecongruence pfa_offset_right_shift_product_source_coefficientresiduecongruence. (pfc_natural_sum_shift_product_source_coefficient) + (p) * pfa_offset_left_shift_product_source_coefficientresiduecongruence = (a) + (p) * pfa_offset_right_shift_product_source_coefficientresiduecongruence)))))))) - 0048
specialize prime_field_convolution_prefix_entry (p) - 0049
specialize prime_field_convolution_prefix_entry (ab) - 0050
specialize prime_field_convolution_prefix_entry (ac) - 0051
specialize prime_field_convolution_prefix_entry (L) - 0052
specialize prime_field_convolution_prefix_entry (bb) - 0053
specialize prime_field_convolution_prefix_entry (bc) - 0054
specialize prime_field_convolution_prefix_entry (M) - 0055
specialize prime_field_convolution_prefix_entry (cb) - 0056
specialize prime_field_convolution_prefix_entry (cc) - 0057
specialize prime_field_convolution_prefix_entry (N) - 0058
specialize prime_field_convolution_prefix_entry (i) - 0059
specialize prime_field_convolution_prefix_entry (a) - 0060
apply prime_field_convolution_prefix_entry - 0061
exact hc_right_right_right - 0062
exact hi - 0063
exact ha - 0064
have hda : exists pfc_terms_code_shift_product_transported_coefficient pfc_terms_scale_shift_product_transported_coefficient pfc_natural_sum_shift_product_transported_coefficient. ((forall pfc_index_shift_product_transported_coefficientdiagonal. (exists pfa_gap_shift_product_transported_coefficientdiagonalbound. pfa_gap_shift_product_transported_coefficientdiagonalbound + S (pfc_index_shift_product_transported_coefficientdiagonal) = (S (i))) -> exists pfc_value_shift_product_transported_coefficientdiagonal. ((((exists ff_h_pfp_shift_product_transported_coefficientdiagonalentry. ff_h_pfp_shift_product_transported_coefficientdiagonalentry + S (pfc_value_shift_product_transported_coefficientdiagonal) = S ((S (pfc_index_shift_product_transported_coefficientdiagonal)) * pfc_terms_scale_shift_product_transported_coefficient)) /\ exists ff_q_pfp_shift_product_transported_coefficientdiagonalentry. pfc_terms_code_shift_product_transported_coefficient = ff_q_pfp_shift_product_transported_coefficientdiagonalentry * S ((S (pfc_index_shift_product_transported_coefficientdiagonal)) * pfc_terms_scale_shift_product_transported_coefficient) + (pfc_value_shift_product_transported_coefficientdiagonal))) /\ ((exists pfc_complement_shift_product_transported_coefficientdiagonalterm pfc_left_shift_product_transported_coefficientdiagonalterm pfc_right_shift_product_transported_coefficientdiagonalterm. (((pfc_index_shift_product_transported_coefficientdiagonal)+pfc_complement_shift_product_transported_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_product_transported_coefficientdiagonaltermleftinside. pfa_gap_shift_product_transported_coefficientdiagonaltermleftinside + S (pfc_index_shift_product_transported_coefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_transported_coefficientdiagonaltermleftentry. ff_h_pfp_shift_product_transported_coefficientdiagonaltermleftentry + S (pfc_left_shift_product_transported_coefficientdiagonalterm) = S ((S (pfc_index_shift_product_transported_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_transported_coefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_product_transported_coefficientdiagonaltermleftentry * S ((S (pfc_index_shift_product_transported_coefficientdiagonal)) * ac) + (pfc_left_shift_product_transported_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transported_coefficientdiagonaltermleftoutside. pfc_gap_shift_product_transported_coefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_product_transported_coefficientdiagonal)) /\ (((pfc_left_shift_product_transported_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_transported_coefficientdiagonaltermrightinside. pfa_gap_shift_product_transported_coefficientdiagonaltermrightinside + S (pfc_complement_shift_product_transported_coefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_transported_coefficientdiagonaltermrightentry. ff_h_pfp_shift_product_transported_coefficientdiagonaltermrightentry + S (pfc_right_shift_product_transported_coefficientdiagonalterm) = S ((S (pfc_complement_shift_product_transported_coefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_transported_coefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_product_transported_coefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_product_transported_coefficientdiagonalterm)) * BC) + (pfc_right_shift_product_transported_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transported_coefficientdiagonaltermrightoutside. pfc_gap_shift_product_transported_coefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_transported_coefficientdiagonalterm)) /\ (((pfc_right_shift_product_transported_coefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_product_transported_coefficientdiagonal)=pfc_left_shift_product_transported_coefficientdiagonalterm*pfc_right_shift_product_transported_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_transported_coefficientsum fs_v_pfc_shift_product_transported_coefficientsum. ((((exists fs_h_pfc_shift_product_transported_coefficientsum_body_start. fs_h_pfc_shift_product_transported_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_transported_coefficientsum)) /\ exists fs_q_pfc_shift_product_transported_coefficientsum_body_start. fs_u_pfc_shift_product_transported_coefficientsum = fs_q_pfc_shift_product_transported_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_transported_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_transported_coefficientsum_body_terminal. fs_h_pfc_shift_product_transported_coefficientsum_body_terminal + S (pfc_natural_sum_shift_product_transported_coefficient) = S ((S (S (i))) * fs_v_pfc_shift_product_transported_coefficientsum)) /\ exists fs_q_pfc_shift_product_transported_coefficientsum_body_terminal. fs_u_pfc_shift_product_transported_coefficientsum = fs_q_pfc_shift_product_transported_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_product_transported_coefficientsum) + (pfc_natural_sum_shift_product_transported_coefficient))) /\ forall fs_i_pfc_shift_product_transported_coefficientsum_body_steps. (exists fs_lt_pfc_shift_product_transported_coefficientsum_body_steps_bound. fs_lt_pfc_shift_product_transported_coefficientsum_body_steps_bound + S fs_i_pfc_shift_product_transported_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_shift_product_transported_coefficientsum_body_steps fs_r_pfc_shift_product_transported_coefficientsum_body_steps fs_s_pfc_shift_product_transported_coefficientsum_body_steps. ((((exists fs_h_pfc_shift_product_transported_coefficientsum_body_steps_summand. fs_h_pfc_shift_product_transported_coefficientsum_body_steps_summand + S (fs_a_pfc_shift_product_transported_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_transported_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_transported_coefficient)) /\ exists fs_q_pfc_shift_product_transported_coefficientsum_body_steps_summand. pfc_terms_code_shift_product_transported_coefficient = fs_q_pfc_shift_product_transported_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_transported_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_transported_coefficient) + (fs_a_pfc_shift_product_transported_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transported_coefficientsum_body_steps_partial. fs_h_pfc_shift_product_transported_coefficientsum_body_steps_partial + S (fs_r_pfc_shift_product_transported_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_transported_coefficientsum_body_steps)) * fs_v_pfc_shift_product_transported_coefficientsum)) /\ exists fs_q_pfc_shift_product_transported_coefficientsum_body_steps_partial. fs_u_pfc_shift_product_transported_coefficientsum = fs_q_pfc_shift_product_transported_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_transported_coefficientsum_body_steps)) * fs_v_pfc_shift_product_transported_coefficientsum) + (fs_r_pfc_shift_product_transported_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transported_coefficientsum_body_steps_successor. fs_h_pfc_shift_product_transported_coefficientsum_body_steps_successor + S (fs_s_pfc_shift_product_transported_coefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_product_transported_coefficientsum_body_steps)) * fs_v_pfc_shift_product_transported_coefficientsum)) /\ exists fs_q_pfc_shift_product_transported_coefficientsum_body_steps_successor. fs_u_pfc_shift_product_transported_coefficientsum = fs_q_pfc_shift_product_transported_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_transported_coefficientsum_body_steps)) * fs_v_pfc_shift_product_transported_coefficientsum) + (fs_s_pfc_shift_product_transported_coefficientsum_body_steps))) /\ fs_s_pfc_shift_product_transported_coefficientsum_body_steps = fs_r_pfc_shift_product_transported_coefficientsum_body_steps + fs_a_pfc_shift_product_transported_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_transported_coefficientresiduebound. pfa_gap_shift_product_transported_coefficientresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_shift_product_transported_coefficientresiduecongruence pfa_offset_right_shift_product_transported_coefficientresiduecongruence. (pfc_natural_sum_shift_product_transported_coefficient) + (p) * pfa_offset_left_shift_product_transported_coefficientresiduecongruence = (a) + (p) * pfa_offset_right_shift_product_transported_coefficientresiduecongruence)))))))) - 0065
have hiff : (((exists pfc_terms_code_shift_product_transport_old pfc_terms_scale_shift_product_transport_old pfc_natural_sum_shift_product_transport_old. ((forall pfc_index_shift_product_transport_olddiagonal. (exists pfa_gap_shift_product_transport_olddiagonalbound. pfa_gap_shift_product_transport_olddiagonalbound + S (pfc_index_shift_product_transport_olddiagonal) = (S (i))) -> exists pfc_value_shift_product_transport_olddiagonal. ((((exists ff_h_pfp_shift_product_transport_olddiagonalentry. ff_h_pfp_shift_product_transport_olddiagonalentry + S (pfc_value_shift_product_transport_olddiagonal) = S ((S (pfc_index_shift_product_transport_olddiagonal)) * pfc_terms_scale_shift_product_transport_old)) /\ exists ff_q_pfp_shift_product_transport_olddiagonalentry. pfc_terms_code_shift_product_transport_old = ff_q_pfp_shift_product_transport_olddiagonalentry * S ((S (pfc_index_shift_product_transport_olddiagonal)) * pfc_terms_scale_shift_product_transport_old) + (pfc_value_shift_product_transport_olddiagonal))) /\ ((exists pfc_complement_shift_product_transport_olddiagonalterm pfc_left_shift_product_transport_olddiagonalterm pfc_right_shift_product_transport_olddiagonalterm. (((pfc_index_shift_product_transport_olddiagonal)+pfc_complement_shift_product_transport_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_product_transport_olddiagonaltermleftinside. pfa_gap_shift_product_transport_olddiagonaltermleftinside + S (pfc_index_shift_product_transport_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_transport_olddiagonaltermleftentry. ff_h_pfp_shift_product_transport_olddiagonaltermleftentry + S (pfc_left_shift_product_transport_olddiagonalterm) = S ((S (pfc_index_shift_product_transport_olddiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_transport_olddiagonaltermleftentry. ab = ff_q_pfp_shift_product_transport_olddiagonaltermleftentry * S ((S (pfc_index_shift_product_transport_olddiagonal)) * ac) + (pfc_left_shift_product_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_olddiagonaltermleftoutside. pfc_gap_shift_product_transport_olddiagonaltermleftoutside+(L)=(pfc_index_shift_product_transport_olddiagonal)) /\ (((pfc_left_shift_product_transport_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_transport_olddiagonaltermrightinside. pfa_gap_shift_product_transport_olddiagonaltermrightinside + S (pfc_complement_shift_product_transport_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_product_transport_olddiagonaltermrightentry. ff_h_pfp_shift_product_transport_olddiagonaltermrightentry + S (pfc_right_shift_product_transport_olddiagonalterm) = S ((S (pfc_complement_shift_product_transport_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_product_transport_olddiagonaltermrightentry. bb = ff_q_pfp_shift_product_transport_olddiagonaltermrightentry * S ((S (pfc_complement_shift_product_transport_olddiagonalterm)) * bc) + (pfc_right_shift_product_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_olddiagonaltermrightoutside. pfc_gap_shift_product_transport_olddiagonaltermrightoutside+(M)=(pfc_complement_shift_product_transport_olddiagonalterm)) /\ (((pfc_right_shift_product_transport_olddiagonalterm)=0))))) /\ (((pfc_value_shift_product_transport_olddiagonal)=pfc_left_shift_product_transport_olddiagonalterm*pfc_right_shift_product_transport_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_transport_oldsum fs_v_pfc_shift_product_transport_oldsum. ((((exists fs_h_pfc_shift_product_transport_oldsum_body_start. fs_h_pfc_shift_product_transport_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_start. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_transport_oldsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_transport_oldsum_body_terminal. fs_h_pfc_shift_product_transport_oldsum_body_terminal + S (pfc_natural_sum_shift_product_transport_old) = S ((S (S (i))) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_terminal. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_product_transport_oldsum) + (pfc_natural_sum_shift_product_transport_old))) /\ forall fs_i_pfc_shift_product_transport_oldsum_body_steps. (exists fs_lt_pfc_shift_product_transport_oldsum_body_steps_bound. fs_lt_pfc_shift_product_transport_oldsum_body_steps_bound + S fs_i_pfc_shift_product_transport_oldsum_body_steps = S (i)) -> exists fs_a_pfc_shift_product_transport_oldsum_body_steps fs_r_pfc_shift_product_transport_oldsum_body_steps fs_s_pfc_shift_product_transport_oldsum_body_steps. ((((exists fs_h_pfc_shift_product_transport_oldsum_body_steps_summand. fs_h_pfc_shift_product_transport_oldsum_body_steps_summand + S (fs_a_pfc_shift_product_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_transport_old)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_steps_summand. pfc_terms_code_shift_product_transport_old = fs_q_pfc_shift_product_transport_oldsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_transport_old) + (fs_a_pfc_shift_product_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_oldsum_body_steps_partial. fs_h_pfc_shift_product_transport_oldsum_body_steps_partial + S (fs_r_pfc_shift_product_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_steps_partial. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum) + (fs_r_pfc_shift_product_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_oldsum_body_steps_successor. fs_h_pfc_shift_product_transport_oldsum_body_steps_successor + S (fs_s_pfc_shift_product_transport_oldsum_body_steps) = S ((S (S fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_steps_successor. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum) + (fs_s_pfc_shift_product_transport_oldsum_body_steps))) /\ fs_s_pfc_shift_product_transport_oldsum_body_steps = fs_r_pfc_shift_product_transport_oldsum_body_steps + fs_a_pfc_shift_product_transport_oldsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_transport_oldresiduebound. pfa_gap_shift_product_transport_oldresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_shift_product_transport_oldresiduecongruence pfa_offset_right_shift_product_transport_oldresiduecongruence. (pfc_natural_sum_shift_product_transport_old) + (p) * pfa_offset_left_shift_product_transport_oldresiduecongruence = (a) + (p) * pfa_offset_right_shift_product_transport_oldresiduecongruence))))))))) -> (exists pfc_terms_code_shift_product_transport_new pfc_terms_scale_shift_product_transport_new pfc_natural_sum_shift_product_transport_new. ((forall pfc_index_shift_product_transport_newdiagonal. (exists pfa_gap_shift_product_transport_newdiagonalbound. pfa_gap_shift_product_transport_newdiagonalbound + S (pfc_index_shift_product_transport_newdiagonal) = (S (i))) -> exists pfc_value_shift_product_transport_newdiagonal. ((((exists ff_h_pfp_shift_product_transport_newdiagonalentry. ff_h_pfp_shift_product_transport_newdiagonalentry + S (pfc_value_shift_product_transport_newdiagonal) = S ((S (pfc_index_shift_product_transport_newdiagonal)) * pfc_terms_scale_shift_product_transport_new)) /\ exists ff_q_pfp_shift_product_transport_newdiagonalentry. pfc_terms_code_shift_product_transport_new = ff_q_pfp_shift_product_transport_newdiagonalentry * S ((S (pfc_index_shift_product_transport_newdiagonal)) * pfc_terms_scale_shift_product_transport_new) + (pfc_value_shift_product_transport_newdiagonal))) /\ ((exists pfc_complement_shift_product_transport_newdiagonalterm pfc_left_shift_product_transport_newdiagonalterm pfc_right_shift_product_transport_newdiagonalterm. (((pfc_index_shift_product_transport_newdiagonal)+pfc_complement_shift_product_transport_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_product_transport_newdiagonaltermleftinside. pfa_gap_shift_product_transport_newdiagonaltermleftinside + S (pfc_index_shift_product_transport_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_transport_newdiagonaltermleftentry. ff_h_pfp_shift_product_transport_newdiagonaltermleftentry + S (pfc_left_shift_product_transport_newdiagonalterm) = S ((S (pfc_index_shift_product_transport_newdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_transport_newdiagonaltermleftentry. ab = ff_q_pfp_shift_product_transport_newdiagonaltermleftentry * S ((S (pfc_index_shift_product_transport_newdiagonal)) * ac) + (pfc_left_shift_product_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_newdiagonaltermleftoutside. pfc_gap_shift_product_transport_newdiagonaltermleftoutside+(L)=(pfc_index_shift_product_transport_newdiagonal)) /\ (((pfc_left_shift_product_transport_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_transport_newdiagonaltermrightinside. pfa_gap_shift_product_transport_newdiagonaltermrightinside + S (pfc_complement_shift_product_transport_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_transport_newdiagonaltermrightentry. ff_h_pfp_shift_product_transport_newdiagonaltermrightentry + S (pfc_right_shift_product_transport_newdiagonalterm) = S ((S (pfc_complement_shift_product_transport_newdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_transport_newdiagonaltermrightentry. BB = ff_q_pfp_shift_product_transport_newdiagonaltermrightentry * S ((S (pfc_complement_shift_product_transport_newdiagonalterm)) * BC) + (pfc_right_shift_product_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_newdiagonaltermrightoutside. pfc_gap_shift_product_transport_newdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_transport_newdiagonalterm)) /\ (((pfc_right_shift_product_transport_newdiagonalterm)=0))))) /\ (((pfc_value_shift_product_transport_newdiagonal)=pfc_left_shift_product_transport_newdiagonalterm*pfc_right_shift_product_transport_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_transport_newsum fs_v_pfc_shift_product_transport_newsum. ((((exists fs_h_pfc_shift_product_transport_newsum_body_start. fs_h_pfc_shift_product_transport_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_start. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_transport_newsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_transport_newsum_body_terminal. fs_h_pfc_shift_product_transport_newsum_body_terminal + S (pfc_natural_sum_shift_product_transport_new) = S ((S (S (i))) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_terminal. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_product_transport_newsum) + (pfc_natural_sum_shift_product_transport_new))) /\ forall fs_i_pfc_shift_product_transport_newsum_body_steps. (exists fs_lt_pfc_shift_product_transport_newsum_body_steps_bound. fs_lt_pfc_shift_product_transport_newsum_body_steps_bound + S fs_i_pfc_shift_product_transport_newsum_body_steps = S (i)) -> exists fs_a_pfc_shift_product_transport_newsum_body_steps fs_r_pfc_shift_product_transport_newsum_body_steps fs_s_pfc_shift_product_transport_newsum_body_steps. ((((exists fs_h_pfc_shift_product_transport_newsum_body_steps_summand. fs_h_pfc_shift_product_transport_newsum_body_steps_summand + S (fs_a_pfc_shift_product_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_transport_new)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_steps_summand. pfc_terms_code_shift_product_transport_new = fs_q_pfc_shift_product_transport_newsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_transport_new) + (fs_a_pfc_shift_product_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_newsum_body_steps_partial. fs_h_pfc_shift_product_transport_newsum_body_steps_partial + S (fs_r_pfc_shift_product_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_steps_partial. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum) + (fs_r_pfc_shift_product_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_newsum_body_steps_successor. fs_h_pfc_shift_product_transport_newsum_body_steps_successor + S (fs_s_pfc_shift_product_transport_newsum_body_steps) = S ((S (S fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_steps_successor. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum) + (fs_s_pfc_shift_product_transport_newsum_body_steps))) /\ fs_s_pfc_shift_product_transport_newsum_body_steps = fs_r_pfc_shift_product_transport_newsum_body_steps + fs_a_pfc_shift_product_transport_newsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_transport_newresiduebound. pfa_gap_shift_product_transport_newresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_shift_product_transport_newresiduecongruence pfa_offset_right_shift_product_transport_newresiduecongruence. (pfc_natural_sum_shift_product_transport_new) + (p) * pfa_offset_left_shift_product_transport_newresiduecongruence = (a) + (p) * pfa_offset_right_shift_product_transport_newresiduecongruence)))))))))) /\ (((exists pfc_terms_code_shift_product_transport_new pfc_terms_scale_shift_product_transport_new pfc_natural_sum_shift_product_transport_new. ((forall pfc_index_shift_product_transport_newdiagonal. (exists pfa_gap_shift_product_transport_newdiagonalbound. pfa_gap_shift_product_transport_newdiagonalbound + S (pfc_index_shift_product_transport_newdiagonal) = (S (i))) -> exists pfc_value_shift_product_transport_newdiagonal. ((((exists ff_h_pfp_shift_product_transport_newdiagonalentry. ff_h_pfp_shift_product_transport_newdiagonalentry + S (pfc_value_shift_product_transport_newdiagonal) = S ((S (pfc_index_shift_product_transport_newdiagonal)) * pfc_terms_scale_shift_product_transport_new)) /\ exists ff_q_pfp_shift_product_transport_newdiagonalentry. pfc_terms_code_shift_product_transport_new = ff_q_pfp_shift_product_transport_newdiagonalentry * S ((S (pfc_index_shift_product_transport_newdiagonal)) * pfc_terms_scale_shift_product_transport_new) + (pfc_value_shift_product_transport_newdiagonal))) /\ ((exists pfc_complement_shift_product_transport_newdiagonalterm pfc_left_shift_product_transport_newdiagonalterm pfc_right_shift_product_transport_newdiagonalterm. (((pfc_index_shift_product_transport_newdiagonal)+pfc_complement_shift_product_transport_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_product_transport_newdiagonaltermleftinside. pfa_gap_shift_product_transport_newdiagonaltermleftinside + S (pfc_index_shift_product_transport_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_transport_newdiagonaltermleftentry. ff_h_pfp_shift_product_transport_newdiagonaltermleftentry + S (pfc_left_shift_product_transport_newdiagonalterm) = S ((S (pfc_index_shift_product_transport_newdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_transport_newdiagonaltermleftentry. ab = ff_q_pfp_shift_product_transport_newdiagonaltermleftentry * S ((S (pfc_index_shift_product_transport_newdiagonal)) * ac) + (pfc_left_shift_product_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_newdiagonaltermleftoutside. pfc_gap_shift_product_transport_newdiagonaltermleftoutside+(L)=(pfc_index_shift_product_transport_newdiagonal)) /\ (((pfc_left_shift_product_transport_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_transport_newdiagonaltermrightinside. pfa_gap_shift_product_transport_newdiagonaltermrightinside + S (pfc_complement_shift_product_transport_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_transport_newdiagonaltermrightentry. ff_h_pfp_shift_product_transport_newdiagonaltermrightentry + S (pfc_right_shift_product_transport_newdiagonalterm) = S ((S (pfc_complement_shift_product_transport_newdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_transport_newdiagonaltermrightentry. BB = ff_q_pfp_shift_product_transport_newdiagonaltermrightentry * S ((S (pfc_complement_shift_product_transport_newdiagonalterm)) * BC) + (pfc_right_shift_product_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_newdiagonaltermrightoutside. pfc_gap_shift_product_transport_newdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_transport_newdiagonalterm)) /\ (((pfc_right_shift_product_transport_newdiagonalterm)=0))))) /\ (((pfc_value_shift_product_transport_newdiagonal)=pfc_left_shift_product_transport_newdiagonalterm*pfc_right_shift_product_transport_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_transport_newsum fs_v_pfc_shift_product_transport_newsum. ((((exists fs_h_pfc_shift_product_transport_newsum_body_start. fs_h_pfc_shift_product_transport_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_start. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_transport_newsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_transport_newsum_body_terminal. fs_h_pfc_shift_product_transport_newsum_body_terminal + S (pfc_natural_sum_shift_product_transport_new) = S ((S (S (i))) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_terminal. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_product_transport_newsum) + (pfc_natural_sum_shift_product_transport_new))) /\ forall fs_i_pfc_shift_product_transport_newsum_body_steps. (exists fs_lt_pfc_shift_product_transport_newsum_body_steps_bound. fs_lt_pfc_shift_product_transport_newsum_body_steps_bound + S fs_i_pfc_shift_product_transport_newsum_body_steps = S (i)) -> exists fs_a_pfc_shift_product_transport_newsum_body_steps fs_r_pfc_shift_product_transport_newsum_body_steps fs_s_pfc_shift_product_transport_newsum_body_steps. ((((exists fs_h_pfc_shift_product_transport_newsum_body_steps_summand. fs_h_pfc_shift_product_transport_newsum_body_steps_summand + S (fs_a_pfc_shift_product_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_transport_new)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_steps_summand. pfc_terms_code_shift_product_transport_new = fs_q_pfc_shift_product_transport_newsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_transport_new) + (fs_a_pfc_shift_product_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_newsum_body_steps_partial. fs_h_pfc_shift_product_transport_newsum_body_steps_partial + S (fs_r_pfc_shift_product_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_steps_partial. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum) + (fs_r_pfc_shift_product_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_newsum_body_steps_successor. fs_h_pfc_shift_product_transport_newsum_body_steps_successor + S (fs_s_pfc_shift_product_transport_newsum_body_steps) = S ((S (S fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum)) /\ exists fs_q_pfc_shift_product_transport_newsum_body_steps_successor. fs_u_pfc_shift_product_transport_newsum = fs_q_pfc_shift_product_transport_newsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_transport_newsum_body_steps)) * fs_v_pfc_shift_product_transport_newsum) + (fs_s_pfc_shift_product_transport_newsum_body_steps))) /\ fs_s_pfc_shift_product_transport_newsum_body_steps = fs_r_pfc_shift_product_transport_newsum_body_steps + fs_a_pfc_shift_product_transport_newsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_transport_newresiduebound. pfa_gap_shift_product_transport_newresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_shift_product_transport_newresiduecongruence pfa_offset_right_shift_product_transport_newresiduecongruence. (pfc_natural_sum_shift_product_transport_new) + (p) * pfa_offset_left_shift_product_transport_newresiduecongruence = (a) + (p) * pfa_offset_right_shift_product_transport_newresiduecongruence))))))))) -> (exists pfc_terms_code_shift_product_transport_old pfc_terms_scale_shift_product_transport_old pfc_natural_sum_shift_product_transport_old. ((forall pfc_index_shift_product_transport_olddiagonal. (exists pfa_gap_shift_product_transport_olddiagonalbound. pfa_gap_shift_product_transport_olddiagonalbound + S (pfc_index_shift_product_transport_olddiagonal) = (S (i))) -> exists pfc_value_shift_product_transport_olddiagonal. ((((exists ff_h_pfp_shift_product_transport_olddiagonalentry. ff_h_pfp_shift_product_transport_olddiagonalentry + S (pfc_value_shift_product_transport_olddiagonal) = S ((S (pfc_index_shift_product_transport_olddiagonal)) * pfc_terms_scale_shift_product_transport_old)) /\ exists ff_q_pfp_shift_product_transport_olddiagonalentry. pfc_terms_code_shift_product_transport_old = ff_q_pfp_shift_product_transport_olddiagonalentry * S ((S (pfc_index_shift_product_transport_olddiagonal)) * pfc_terms_scale_shift_product_transport_old) + (pfc_value_shift_product_transport_olddiagonal))) /\ ((exists pfc_complement_shift_product_transport_olddiagonalterm pfc_left_shift_product_transport_olddiagonalterm pfc_right_shift_product_transport_olddiagonalterm. (((pfc_index_shift_product_transport_olddiagonal)+pfc_complement_shift_product_transport_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_product_transport_olddiagonaltermleftinside. pfa_gap_shift_product_transport_olddiagonaltermleftinside + S (pfc_index_shift_product_transport_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_transport_olddiagonaltermleftentry. ff_h_pfp_shift_product_transport_olddiagonaltermleftentry + S (pfc_left_shift_product_transport_olddiagonalterm) = S ((S (pfc_index_shift_product_transport_olddiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_transport_olddiagonaltermleftentry. ab = ff_q_pfp_shift_product_transport_olddiagonaltermleftentry * S ((S (pfc_index_shift_product_transport_olddiagonal)) * ac) + (pfc_left_shift_product_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_olddiagonaltermleftoutside. pfc_gap_shift_product_transport_olddiagonaltermleftoutside+(L)=(pfc_index_shift_product_transport_olddiagonal)) /\ (((pfc_left_shift_product_transport_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_transport_olddiagonaltermrightinside. pfa_gap_shift_product_transport_olddiagonaltermrightinside + S (pfc_complement_shift_product_transport_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_product_transport_olddiagonaltermrightentry. ff_h_pfp_shift_product_transport_olddiagonaltermrightentry + S (pfc_right_shift_product_transport_olddiagonalterm) = S ((S (pfc_complement_shift_product_transport_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_product_transport_olddiagonaltermrightentry. bb = ff_q_pfp_shift_product_transport_olddiagonaltermrightentry * S ((S (pfc_complement_shift_product_transport_olddiagonalterm)) * bc) + (pfc_right_shift_product_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_transport_olddiagonaltermrightoutside. pfc_gap_shift_product_transport_olddiagonaltermrightoutside+(M)=(pfc_complement_shift_product_transport_olddiagonalterm)) /\ (((pfc_right_shift_product_transport_olddiagonalterm)=0))))) /\ (((pfc_value_shift_product_transport_olddiagonal)=pfc_left_shift_product_transport_olddiagonalterm*pfc_right_shift_product_transport_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_transport_oldsum fs_v_pfc_shift_product_transport_oldsum. ((((exists fs_h_pfc_shift_product_transport_oldsum_body_start. fs_h_pfc_shift_product_transport_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_start. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_transport_oldsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_transport_oldsum_body_terminal. fs_h_pfc_shift_product_transport_oldsum_body_terminal + S (pfc_natural_sum_shift_product_transport_old) = S ((S (S (i))) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_terminal. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_product_transport_oldsum) + (pfc_natural_sum_shift_product_transport_old))) /\ forall fs_i_pfc_shift_product_transport_oldsum_body_steps. (exists fs_lt_pfc_shift_product_transport_oldsum_body_steps_bound. fs_lt_pfc_shift_product_transport_oldsum_body_steps_bound + S fs_i_pfc_shift_product_transport_oldsum_body_steps = S (i)) -> exists fs_a_pfc_shift_product_transport_oldsum_body_steps fs_r_pfc_shift_product_transport_oldsum_body_steps fs_s_pfc_shift_product_transport_oldsum_body_steps. ((((exists fs_h_pfc_shift_product_transport_oldsum_body_steps_summand. fs_h_pfc_shift_product_transport_oldsum_body_steps_summand + S (fs_a_pfc_shift_product_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_transport_old)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_steps_summand. pfc_terms_code_shift_product_transport_old = fs_q_pfc_shift_product_transport_oldsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_transport_old) + (fs_a_pfc_shift_product_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_oldsum_body_steps_partial. fs_h_pfc_shift_product_transport_oldsum_body_steps_partial + S (fs_r_pfc_shift_product_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_steps_partial. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum) + (fs_r_pfc_shift_product_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_transport_oldsum_body_steps_successor. fs_h_pfc_shift_product_transport_oldsum_body_steps_successor + S (fs_s_pfc_shift_product_transport_oldsum_body_steps) = S ((S (S fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum)) /\ exists fs_q_pfc_shift_product_transport_oldsum_body_steps_successor. fs_u_pfc_shift_product_transport_oldsum = fs_q_pfc_shift_product_transport_oldsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_transport_oldsum) + (fs_s_pfc_shift_product_transport_oldsum_body_steps))) /\ fs_s_pfc_shift_product_transport_oldsum_body_steps = fs_r_pfc_shift_product_transport_oldsum_body_steps + fs_a_pfc_shift_product_transport_oldsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_transport_oldresiduebound. pfa_gap_shift_product_transport_oldresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_shift_product_transport_oldresiduecongruence pfa_offset_right_shift_product_transport_oldresiduecongruence. (pfc_natural_sum_shift_product_transport_old) + (p) * pfa_offset_left_shift_product_transport_oldresiduecongruence = (a) + (p) * pfa_offset_right_shift_product_transport_oldresiduecongruence)))))))))))) - 0066
specialize prime_field_convolution_coefficient_shift_right_iff (p) - 0067
specialize prime_field_convolution_coefficient_shift_right_iff (ab) - 0068
specialize prime_field_convolution_coefficient_shift_right_iff (ac) - 0069
specialize prime_field_convolution_coefficient_shift_right_iff (L) - 0070
specialize prime_field_convolution_coefficient_shift_right_iff (bb) - 0071
specialize prime_field_convolution_coefficient_shift_right_iff (bc) - 0072
specialize prime_field_convolution_coefficient_shift_right_iff (M) - 0073
specialize prime_field_convolution_coefficient_shift_right_iff (BB) - 0074
specialize prime_field_convolution_coefficient_shift_right_iff (BC) - 0075
specialize prime_field_convolution_coefficient_shift_right_iff (i) - 0076
specialize prime_field_convolution_coefficient_shift_right_iff (a) - 0077
apply prime_field_convolution_coefficient_shift_right_iff - 0078
exact hs - 0079
cases hiff - 0080
apply hiff_left - 0081
exact hca - 0082
have hv : exists r. ((((exists ff_h_pfp_shift_product_chosen_entry. ff_h_pfp_shift_product_chosen_entry + S (r) = S ((S (i)) * dc)) /\ exists ff_q_pfp_shift_product_chosen_entry. db = ff_q_pfp_shift_product_chosen_entry * S ((S (i)) * dc) + (r))) /\ ((exists pfc_terms_code_shift_product_chosen_coefficient pfc_terms_scale_shift_product_chosen_coefficient pfc_natural_sum_shift_product_chosen_coefficient. ((forall pfc_index_shift_product_chosen_coefficientdiagonal. (exists pfa_gap_shift_product_chosen_coefficientdiagonalbound. pfa_gap_shift_product_chosen_coefficientdiagonalbound + S (pfc_index_shift_product_chosen_coefficientdiagonal) = (S (i))) -> exists pfc_value_shift_product_chosen_coefficientdiagonal. ((((exists ff_h_pfp_shift_product_chosen_coefficientdiagonalentry. ff_h_pfp_shift_product_chosen_coefficientdiagonalentry + S (pfc_value_shift_product_chosen_coefficientdiagonal) = S ((S (pfc_index_shift_product_chosen_coefficientdiagonal)) * pfc_terms_scale_shift_product_chosen_coefficient)) /\ exists ff_q_pfp_shift_product_chosen_coefficientdiagonalentry. pfc_terms_code_shift_product_chosen_coefficient = ff_q_pfp_shift_product_chosen_coefficientdiagonalentry * S ((S (pfc_index_shift_product_chosen_coefficientdiagonal)) * pfc_terms_scale_shift_product_chosen_coefficient) + (pfc_value_shift_product_chosen_coefficientdiagonal))) /\ ((exists pfc_complement_shift_product_chosen_coefficientdiagonalterm pfc_left_shift_product_chosen_coefficientdiagonalterm pfc_right_shift_product_chosen_coefficientdiagonalterm. (((pfc_index_shift_product_chosen_coefficientdiagonal)+pfc_complement_shift_product_chosen_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_shift_product_chosen_coefficientdiagonaltermleftinside. pfa_gap_shift_product_chosen_coefficientdiagonaltermleftinside + S (pfc_index_shift_product_chosen_coefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_chosen_coefficientdiagonaltermleftentry. ff_h_pfp_shift_product_chosen_coefficientdiagonaltermleftentry + S (pfc_left_shift_product_chosen_coefficientdiagonalterm) = S ((S (pfc_index_shift_product_chosen_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_chosen_coefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_product_chosen_coefficientdiagonaltermleftentry * S ((S (pfc_index_shift_product_chosen_coefficientdiagonal)) * ac) + (pfc_left_shift_product_chosen_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_chosen_coefficientdiagonaltermleftoutside. pfc_gap_shift_product_chosen_coefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_product_chosen_coefficientdiagonal)) /\ (((pfc_left_shift_product_chosen_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_chosen_coefficientdiagonaltermrightinside. pfa_gap_shift_product_chosen_coefficientdiagonaltermrightinside + S (pfc_complement_shift_product_chosen_coefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_chosen_coefficientdiagonaltermrightentry. ff_h_pfp_shift_product_chosen_coefficientdiagonaltermrightentry + S (pfc_right_shift_product_chosen_coefficientdiagonalterm) = S ((S (pfc_complement_shift_product_chosen_coefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_chosen_coefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_product_chosen_coefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_product_chosen_coefficientdiagonalterm)) * BC) + (pfc_right_shift_product_chosen_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_chosen_coefficientdiagonaltermrightoutside. pfc_gap_shift_product_chosen_coefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_chosen_coefficientdiagonalterm)) /\ (((pfc_right_shift_product_chosen_coefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_product_chosen_coefficientdiagonal)=pfc_left_shift_product_chosen_coefficientdiagonalterm*pfc_right_shift_product_chosen_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_chosen_coefficientsum fs_v_pfc_shift_product_chosen_coefficientsum. ((((exists fs_h_pfc_shift_product_chosen_coefficientsum_body_start. fs_h_pfc_shift_product_chosen_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_chosen_coefficientsum)) /\ exists fs_q_pfc_shift_product_chosen_coefficientsum_body_start. fs_u_pfc_shift_product_chosen_coefficientsum = fs_q_pfc_shift_product_chosen_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_chosen_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_chosen_coefficientsum_body_terminal. fs_h_pfc_shift_product_chosen_coefficientsum_body_terminal + S (pfc_natural_sum_shift_product_chosen_coefficient) = S ((S (S (i))) * fs_v_pfc_shift_product_chosen_coefficientsum)) /\ exists fs_q_pfc_shift_product_chosen_coefficientsum_body_terminal. fs_u_pfc_shift_product_chosen_coefficientsum = fs_q_pfc_shift_product_chosen_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_shift_product_chosen_coefficientsum) + (pfc_natural_sum_shift_product_chosen_coefficient))) /\ forall fs_i_pfc_shift_product_chosen_coefficientsum_body_steps. (exists fs_lt_pfc_shift_product_chosen_coefficientsum_body_steps_bound. fs_lt_pfc_shift_product_chosen_coefficientsum_body_steps_bound + S fs_i_pfc_shift_product_chosen_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_shift_product_chosen_coefficientsum_body_steps fs_r_pfc_shift_product_chosen_coefficientsum_body_steps fs_s_pfc_shift_product_chosen_coefficientsum_body_steps. ((((exists fs_h_pfc_shift_product_chosen_coefficientsum_body_steps_summand. fs_h_pfc_shift_product_chosen_coefficientsum_body_steps_summand + S (fs_a_pfc_shift_product_chosen_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_chosen_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_chosen_coefficient)) /\ exists fs_q_pfc_shift_product_chosen_coefficientsum_body_steps_summand. pfc_terms_code_shift_product_chosen_coefficient = fs_q_pfc_shift_product_chosen_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_chosen_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_chosen_coefficient) + (fs_a_pfc_shift_product_chosen_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_chosen_coefficientsum_body_steps_partial. fs_h_pfc_shift_product_chosen_coefficientsum_body_steps_partial + S (fs_r_pfc_shift_product_chosen_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_chosen_coefficientsum_body_steps)) * fs_v_pfc_shift_product_chosen_coefficientsum)) /\ exists fs_q_pfc_shift_product_chosen_coefficientsum_body_steps_partial. fs_u_pfc_shift_product_chosen_coefficientsum = fs_q_pfc_shift_product_chosen_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_chosen_coefficientsum_body_steps)) * fs_v_pfc_shift_product_chosen_coefficientsum) + (fs_r_pfc_shift_product_chosen_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_chosen_coefficientsum_body_steps_successor. fs_h_pfc_shift_product_chosen_coefficientsum_body_steps_successor + S (fs_s_pfc_shift_product_chosen_coefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_product_chosen_coefficientsum_body_steps)) * fs_v_pfc_shift_product_chosen_coefficientsum)) /\ exists fs_q_pfc_shift_product_chosen_coefficientsum_body_steps_successor. fs_u_pfc_shift_product_chosen_coefficientsum = fs_q_pfc_shift_product_chosen_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_chosen_coefficientsum_body_steps)) * fs_v_pfc_shift_product_chosen_coefficientsum) + (fs_s_pfc_shift_product_chosen_coefficientsum_body_steps))) /\ fs_s_pfc_shift_product_chosen_coefficientsum_body_steps = fs_r_pfc_shift_product_chosen_coefficientsum_body_steps + fs_a_pfc_shift_product_chosen_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_chosen_coefficientresiduebound. pfa_gap_shift_product_chosen_coefficientresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_shift_product_chosen_coefficientresiduecongruence pfa_offset_right_shift_product_chosen_coefficientresiduecongruence. (pfc_natural_sum_shift_product_chosen_coefficient) + (p) * pfa_offset_left_shift_product_chosen_coefficientresiduecongruence = (r) + (p) * pfa_offset_right_shift_product_chosen_coefficientresiduecongruence))))))))))) - 0083
specialize hd_right_right_right (i) - 0084
apply hd_right_right_right - 0085
rewrite hk - 0086
specialize le_succ (S i) - 0087
specialize le_succ (N) - 0088
apply le_succ - 0089
exact hi - 0090
cases hv - 0091
cases hv_witness - 0092
have heq : a=x - 0093
specialize prime_field_convolution_coefficient_functional (p) - 0094
specialize prime_field_convolution_coefficient_functional (ab) - 0095
specialize prime_field_convolution_coefficient_functional (ac) - 0096
specialize prime_field_convolution_coefficient_functional (L) - 0097
specialize prime_field_convolution_coefficient_functional (BB) - 0098
specialize prime_field_convolution_coefficient_functional (BC) - 0099
specialize prime_field_convolution_coefficient_functional (S M) - 0100
specialize prime_field_convolution_coefficient_functional (i) - 0101
specialize prime_field_convolution_coefficient_functional (a) - 0102
specialize prime_field_convolution_coefficient_functional (x) - 0103
apply prime_field_convolution_coefficient_functional - 0104
exact hda - 0105
exact hv_witness_right - 0106
rewrite heq - 0107
rewrite heq - 0108
exact hv_witness_left - 0109
have hv : exists r. ((((exists ff_h_pfp_shift_product_last_entry. ff_h_pfp_shift_product_last_entry + S (r) = S ((S (N)) * dc)) /\ exists ff_q_pfp_shift_product_last_entry. db = ff_q_pfp_shift_product_last_entry * S ((S (N)) * dc) + (r))) /\ ((exists pfc_terms_code_shift_product_last_coefficient pfc_terms_scale_shift_product_last_coefficient pfc_natural_sum_shift_product_last_coefficient. ((forall pfc_index_shift_product_last_coefficientdiagonal. (exists pfa_gap_shift_product_last_coefficientdiagonalbound. pfa_gap_shift_product_last_coefficientdiagonalbound + S (pfc_index_shift_product_last_coefficientdiagonal) = (S (N))) -> exists pfc_value_shift_product_last_coefficientdiagonal. ((((exists ff_h_pfp_shift_product_last_coefficientdiagonalentry. ff_h_pfp_shift_product_last_coefficientdiagonalentry + S (pfc_value_shift_product_last_coefficientdiagonal) = S ((S (pfc_index_shift_product_last_coefficientdiagonal)) * pfc_terms_scale_shift_product_last_coefficient)) /\ exists ff_q_pfp_shift_product_last_coefficientdiagonalentry. pfc_terms_code_shift_product_last_coefficient = ff_q_pfp_shift_product_last_coefficientdiagonalentry * S ((S (pfc_index_shift_product_last_coefficientdiagonal)) * pfc_terms_scale_shift_product_last_coefficient) + (pfc_value_shift_product_last_coefficientdiagonal))) /\ ((exists pfc_complement_shift_product_last_coefficientdiagonalterm pfc_left_shift_product_last_coefficientdiagonalterm pfc_right_shift_product_last_coefficientdiagonalterm. (((pfc_index_shift_product_last_coefficientdiagonal)+pfc_complement_shift_product_last_coefficientdiagonalterm=(N)) /\ ((((((exists pfa_gap_shift_product_last_coefficientdiagonaltermleftinside. pfa_gap_shift_product_last_coefficientdiagonaltermleftinside + S (pfc_index_shift_product_last_coefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_last_coefficientdiagonaltermleftentry. ff_h_pfp_shift_product_last_coefficientdiagonaltermleftentry + S (pfc_left_shift_product_last_coefficientdiagonalterm) = S ((S (pfc_index_shift_product_last_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_last_coefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_product_last_coefficientdiagonaltermleftentry * S ((S (pfc_index_shift_product_last_coefficientdiagonal)) * ac) + (pfc_left_shift_product_last_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_coefficientdiagonaltermleftoutside. pfc_gap_shift_product_last_coefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_product_last_coefficientdiagonal)) /\ (((pfc_left_shift_product_last_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_last_coefficientdiagonaltermrightinside. pfa_gap_shift_product_last_coefficientdiagonaltermrightinside + S (pfc_complement_shift_product_last_coefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_last_coefficientdiagonaltermrightentry. ff_h_pfp_shift_product_last_coefficientdiagonaltermrightentry + S (pfc_right_shift_product_last_coefficientdiagonalterm) = S ((S (pfc_complement_shift_product_last_coefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_last_coefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_product_last_coefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_product_last_coefficientdiagonalterm)) * BC) + (pfc_right_shift_product_last_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_coefficientdiagonaltermrightoutside. pfc_gap_shift_product_last_coefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_last_coefficientdiagonalterm)) /\ (((pfc_right_shift_product_last_coefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_product_last_coefficientdiagonal)=pfc_left_shift_product_last_coefficientdiagonalterm*pfc_right_shift_product_last_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_last_coefficientsum fs_v_pfc_shift_product_last_coefficientsum. ((((exists fs_h_pfc_shift_product_last_coefficientsum_body_start. fs_h_pfc_shift_product_last_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_last_coefficientsum)) /\ exists fs_q_pfc_shift_product_last_coefficientsum_body_start. fs_u_pfc_shift_product_last_coefficientsum = fs_q_pfc_shift_product_last_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_last_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_last_coefficientsum_body_terminal. fs_h_pfc_shift_product_last_coefficientsum_body_terminal + S (pfc_natural_sum_shift_product_last_coefficient) = S ((S (S (N))) * fs_v_pfc_shift_product_last_coefficientsum)) /\ exists fs_q_pfc_shift_product_last_coefficientsum_body_terminal. fs_u_pfc_shift_product_last_coefficientsum = fs_q_pfc_shift_product_last_coefficientsum_body_terminal * S ((S (S (N))) * fs_v_pfc_shift_product_last_coefficientsum) + (pfc_natural_sum_shift_product_last_coefficient))) /\ forall fs_i_pfc_shift_product_last_coefficientsum_body_steps. (exists fs_lt_pfc_shift_product_last_coefficientsum_body_steps_bound. fs_lt_pfc_shift_product_last_coefficientsum_body_steps_bound + S fs_i_pfc_shift_product_last_coefficientsum_body_steps = S (N)) -> exists fs_a_pfc_shift_product_last_coefficientsum_body_steps fs_r_pfc_shift_product_last_coefficientsum_body_steps fs_s_pfc_shift_product_last_coefficientsum_body_steps. ((((exists fs_h_pfc_shift_product_last_coefficientsum_body_steps_summand. fs_h_pfc_shift_product_last_coefficientsum_body_steps_summand + S (fs_a_pfc_shift_product_last_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_last_coefficient)) /\ exists fs_q_pfc_shift_product_last_coefficientsum_body_steps_summand. pfc_terms_code_shift_product_last_coefficient = fs_q_pfc_shift_product_last_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_last_coefficientsum_body_steps)) * pfc_terms_scale_shift_product_last_coefficient) + (fs_a_pfc_shift_product_last_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_coefficientsum_body_steps_partial. fs_h_pfc_shift_product_last_coefficientsum_body_steps_partial + S (fs_r_pfc_shift_product_last_coefficientsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_coefficientsum_body_steps)) * fs_v_pfc_shift_product_last_coefficientsum)) /\ exists fs_q_pfc_shift_product_last_coefficientsum_body_steps_partial. fs_u_pfc_shift_product_last_coefficientsum = fs_q_pfc_shift_product_last_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_last_coefficientsum_body_steps)) * fs_v_pfc_shift_product_last_coefficientsum) + (fs_r_pfc_shift_product_last_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_coefficientsum_body_steps_successor. fs_h_pfc_shift_product_last_coefficientsum_body_steps_successor + S (fs_s_pfc_shift_product_last_coefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_product_last_coefficientsum_body_steps)) * fs_v_pfc_shift_product_last_coefficientsum)) /\ exists fs_q_pfc_shift_product_last_coefficientsum_body_steps_successor. fs_u_pfc_shift_product_last_coefficientsum = fs_q_pfc_shift_product_last_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_last_coefficientsum_body_steps)) * fs_v_pfc_shift_product_last_coefficientsum) + (fs_s_pfc_shift_product_last_coefficientsum_body_steps))) /\ fs_s_pfc_shift_product_last_coefficientsum_body_steps = fs_r_pfc_shift_product_last_coefficientsum_body_steps + fs_a_pfc_shift_product_last_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_last_coefficientresiduebound. pfa_gap_shift_product_last_coefficientresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_shift_product_last_coefficientresiduecongruence pfa_offset_right_shift_product_last_coefficientresiduecongruence. (pfc_natural_sum_shift_product_last_coefficient) + (p) * pfa_offset_left_shift_product_last_coefficientresiduecongruence = (r) + (p) * pfa_offset_right_shift_product_last_coefficientresiduecongruence))))))))))) - 0110
specialize hd_right_right_right (N) - 0111
apply hd_right_right_right - 0112
rewrite hk - 0113
specialize le_refl (S N) - 0114
apply le_refl - 0115
cases hv - 0116
cases hv_witness - 0117
have hco : exists pfc_terms_code_shift_product_exterior_old pfc_terms_scale_shift_product_exterior_old pfc_natural_sum_shift_product_exterior_old. ((forall pfc_index_shift_product_exterior_olddiagonal. (exists pfa_gap_shift_product_exterior_olddiagonalbound. pfa_gap_shift_product_exterior_olddiagonalbound + S (pfc_index_shift_product_exterior_olddiagonal) = (S (N))) -> exists pfc_value_shift_product_exterior_olddiagonal. ((((exists ff_h_pfp_shift_product_exterior_olddiagonalentry. ff_h_pfp_shift_product_exterior_olddiagonalentry + S (pfc_value_shift_product_exterior_olddiagonal) = S ((S (pfc_index_shift_product_exterior_olddiagonal)) * pfc_terms_scale_shift_product_exterior_old)) /\ exists ff_q_pfp_shift_product_exterior_olddiagonalentry. pfc_terms_code_shift_product_exterior_old = ff_q_pfp_shift_product_exterior_olddiagonalentry * S ((S (pfc_index_shift_product_exterior_olddiagonal)) * pfc_terms_scale_shift_product_exterior_old) + (pfc_value_shift_product_exterior_olddiagonal))) /\ ((exists pfc_complement_shift_product_exterior_olddiagonalterm pfc_left_shift_product_exterior_olddiagonalterm pfc_right_shift_product_exterior_olddiagonalterm. (((pfc_index_shift_product_exterior_olddiagonal)+pfc_complement_shift_product_exterior_olddiagonalterm=(N)) /\ ((((((exists pfa_gap_shift_product_exterior_olddiagonaltermleftinside. pfa_gap_shift_product_exterior_olddiagonaltermleftinside + S (pfc_index_shift_product_exterior_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_exterior_olddiagonaltermleftentry. ff_h_pfp_shift_product_exterior_olddiagonaltermleftentry + S (pfc_left_shift_product_exterior_olddiagonalterm) = S ((S (pfc_index_shift_product_exterior_olddiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_exterior_olddiagonaltermleftentry. ab = ff_q_pfp_shift_product_exterior_olddiagonaltermleftentry * S ((S (pfc_index_shift_product_exterior_olddiagonal)) * ac) + (pfc_left_shift_product_exterior_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_exterior_olddiagonaltermleftoutside. pfc_gap_shift_product_exterior_olddiagonaltermleftoutside+(L)=(pfc_index_shift_product_exterior_olddiagonal)) /\ (((pfc_left_shift_product_exterior_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_exterior_olddiagonaltermrightinside. pfa_gap_shift_product_exterior_olddiagonaltermrightinside + S (pfc_complement_shift_product_exterior_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_product_exterior_olddiagonaltermrightentry. ff_h_pfp_shift_product_exterior_olddiagonaltermrightentry + S (pfc_right_shift_product_exterior_olddiagonalterm) = S ((S (pfc_complement_shift_product_exterior_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_product_exterior_olddiagonaltermrightentry. bb = ff_q_pfp_shift_product_exterior_olddiagonaltermrightentry * S ((S (pfc_complement_shift_product_exterior_olddiagonalterm)) * bc) + (pfc_right_shift_product_exterior_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_exterior_olddiagonaltermrightoutside. pfc_gap_shift_product_exterior_olddiagonaltermrightoutside+(M)=(pfc_complement_shift_product_exterior_olddiagonalterm)) /\ (((pfc_right_shift_product_exterior_olddiagonalterm)=0))))) /\ (((pfc_value_shift_product_exterior_olddiagonal)=pfc_left_shift_product_exterior_olddiagonalterm*pfc_right_shift_product_exterior_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_exterior_oldsum fs_v_pfc_shift_product_exterior_oldsum. ((((exists fs_h_pfc_shift_product_exterior_oldsum_body_start. fs_h_pfc_shift_product_exterior_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_exterior_oldsum)) /\ exists fs_q_pfc_shift_product_exterior_oldsum_body_start. fs_u_pfc_shift_product_exterior_oldsum = fs_q_pfc_shift_product_exterior_oldsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_exterior_oldsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_exterior_oldsum_body_terminal. fs_h_pfc_shift_product_exterior_oldsum_body_terminal + S (pfc_natural_sum_shift_product_exterior_old) = S ((S (S (N))) * fs_v_pfc_shift_product_exterior_oldsum)) /\ exists fs_q_pfc_shift_product_exterior_oldsum_body_terminal. fs_u_pfc_shift_product_exterior_oldsum = fs_q_pfc_shift_product_exterior_oldsum_body_terminal * S ((S (S (N))) * fs_v_pfc_shift_product_exterior_oldsum) + (pfc_natural_sum_shift_product_exterior_old))) /\ forall fs_i_pfc_shift_product_exterior_oldsum_body_steps. (exists fs_lt_pfc_shift_product_exterior_oldsum_body_steps_bound. fs_lt_pfc_shift_product_exterior_oldsum_body_steps_bound + S fs_i_pfc_shift_product_exterior_oldsum_body_steps = S (N)) -> exists fs_a_pfc_shift_product_exterior_oldsum_body_steps fs_r_pfc_shift_product_exterior_oldsum_body_steps fs_s_pfc_shift_product_exterior_oldsum_body_steps. ((((exists fs_h_pfc_shift_product_exterior_oldsum_body_steps_summand. fs_h_pfc_shift_product_exterior_oldsum_body_steps_summand + S (fs_a_pfc_shift_product_exterior_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_exterior_oldsum_body_steps)) * pfc_terms_scale_shift_product_exterior_old)) /\ exists fs_q_pfc_shift_product_exterior_oldsum_body_steps_summand. pfc_terms_code_shift_product_exterior_old = fs_q_pfc_shift_product_exterior_oldsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_exterior_oldsum_body_steps)) * pfc_terms_scale_shift_product_exterior_old) + (fs_a_pfc_shift_product_exterior_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_exterior_oldsum_body_steps_partial. fs_h_pfc_shift_product_exterior_oldsum_body_steps_partial + S (fs_r_pfc_shift_product_exterior_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_exterior_oldsum_body_steps)) * fs_v_pfc_shift_product_exterior_oldsum)) /\ exists fs_q_pfc_shift_product_exterior_oldsum_body_steps_partial. fs_u_pfc_shift_product_exterior_oldsum = fs_q_pfc_shift_product_exterior_oldsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_exterior_oldsum_body_steps)) * fs_v_pfc_shift_product_exterior_oldsum) + (fs_r_pfc_shift_product_exterior_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_exterior_oldsum_body_steps_successor. fs_h_pfc_shift_product_exterior_oldsum_body_steps_successor + S (fs_s_pfc_shift_product_exterior_oldsum_body_steps) = S ((S (S fs_i_pfc_shift_product_exterior_oldsum_body_steps)) * fs_v_pfc_shift_product_exterior_oldsum)) /\ exists fs_q_pfc_shift_product_exterior_oldsum_body_steps_successor. fs_u_pfc_shift_product_exterior_oldsum = fs_q_pfc_shift_product_exterior_oldsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_exterior_oldsum_body_steps)) * fs_v_pfc_shift_product_exterior_oldsum) + (fs_s_pfc_shift_product_exterior_oldsum_body_steps))) /\ fs_s_pfc_shift_product_exterior_oldsum_body_steps = fs_r_pfc_shift_product_exterior_oldsum_body_steps + fs_a_pfc_shift_product_exterior_oldsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_exterior_oldresiduebound. pfa_gap_shift_product_exterior_oldresiduebound + S (x) = (p)) /\ ((exists pfa_offset_left_shift_product_exterior_oldresiduecongruence pfa_offset_right_shift_product_exterior_oldresiduecongruence. (pfc_natural_sum_shift_product_exterior_old) + (p) * pfa_offset_left_shift_product_exterior_oldresiduecongruence = (x) + (p) * pfa_offset_right_shift_product_exterior_oldresiduecongruence)))))))) - 0118
have hiff : (((exists pfc_terms_code_shift_product_last_transport_old pfc_terms_scale_shift_product_last_transport_old pfc_natural_sum_shift_product_last_transport_old. ((forall pfc_index_shift_product_last_transport_olddiagonal. (exists pfa_gap_shift_product_last_transport_olddiagonalbound. pfa_gap_shift_product_last_transport_olddiagonalbound + S (pfc_index_shift_product_last_transport_olddiagonal) = (S (N))) -> exists pfc_value_shift_product_last_transport_olddiagonal. ((((exists ff_h_pfp_shift_product_last_transport_olddiagonalentry. ff_h_pfp_shift_product_last_transport_olddiagonalentry + S (pfc_value_shift_product_last_transport_olddiagonal) = S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * pfc_terms_scale_shift_product_last_transport_old)) /\ exists ff_q_pfp_shift_product_last_transport_olddiagonalentry. pfc_terms_code_shift_product_last_transport_old = ff_q_pfp_shift_product_last_transport_olddiagonalentry * S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * pfc_terms_scale_shift_product_last_transport_old) + (pfc_value_shift_product_last_transport_olddiagonal))) /\ ((exists pfc_complement_shift_product_last_transport_olddiagonalterm pfc_left_shift_product_last_transport_olddiagonalterm pfc_right_shift_product_last_transport_olddiagonalterm. (((pfc_index_shift_product_last_transport_olddiagonal)+pfc_complement_shift_product_last_transport_olddiagonalterm=(N)) /\ ((((((exists pfa_gap_shift_product_last_transport_olddiagonaltermleftinside. pfa_gap_shift_product_last_transport_olddiagonaltermleftinside + S (pfc_index_shift_product_last_transport_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_last_transport_olddiagonaltermleftentry. ff_h_pfp_shift_product_last_transport_olddiagonaltermleftentry + S (pfc_left_shift_product_last_transport_olddiagonalterm) = S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_last_transport_olddiagonaltermleftentry. ab = ff_q_pfp_shift_product_last_transport_olddiagonaltermleftentry * S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * ac) + (pfc_left_shift_product_last_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_olddiagonaltermleftoutside. pfc_gap_shift_product_last_transport_olddiagonaltermleftoutside+(L)=(pfc_index_shift_product_last_transport_olddiagonal)) /\ (((pfc_left_shift_product_last_transport_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_last_transport_olddiagonaltermrightinside. pfa_gap_shift_product_last_transport_olddiagonaltermrightinside + S (pfc_complement_shift_product_last_transport_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_product_last_transport_olddiagonaltermrightentry. ff_h_pfp_shift_product_last_transport_olddiagonaltermrightentry + S (pfc_right_shift_product_last_transport_olddiagonalterm) = S ((S (pfc_complement_shift_product_last_transport_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_product_last_transport_olddiagonaltermrightentry. bb = ff_q_pfp_shift_product_last_transport_olddiagonaltermrightentry * S ((S (pfc_complement_shift_product_last_transport_olddiagonalterm)) * bc) + (pfc_right_shift_product_last_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_olddiagonaltermrightoutside. pfc_gap_shift_product_last_transport_olddiagonaltermrightoutside+(M)=(pfc_complement_shift_product_last_transport_olddiagonalterm)) /\ (((pfc_right_shift_product_last_transport_olddiagonalterm)=0))))) /\ (((pfc_value_shift_product_last_transport_olddiagonal)=pfc_left_shift_product_last_transport_olddiagonalterm*pfc_right_shift_product_last_transport_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_last_transport_oldsum fs_v_pfc_shift_product_last_transport_oldsum. ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_start. fs_h_pfc_shift_product_last_transport_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_start. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_last_transport_oldsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_terminal. fs_h_pfc_shift_product_last_transport_oldsum_body_terminal + S (pfc_natural_sum_shift_product_last_transport_old) = S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_terminal. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_terminal * S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_oldsum) + (pfc_natural_sum_shift_product_last_transport_old))) /\ forall fs_i_pfc_shift_product_last_transport_oldsum_body_steps. (exists fs_lt_pfc_shift_product_last_transport_oldsum_body_steps_bound. fs_lt_pfc_shift_product_last_transport_oldsum_body_steps_bound + S fs_i_pfc_shift_product_last_transport_oldsum_body_steps = S (N)) -> exists fs_a_pfc_shift_product_last_transport_oldsum_body_steps fs_r_pfc_shift_product_last_transport_oldsum_body_steps fs_s_pfc_shift_product_last_transport_oldsum_body_steps. ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_steps_summand. fs_h_pfc_shift_product_last_transport_oldsum_body_steps_summand + S (fs_a_pfc_shift_product_last_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_old)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_steps_summand. pfc_terms_code_shift_product_last_transport_old = fs_q_pfc_shift_product_last_transport_oldsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_old) + (fs_a_pfc_shift_product_last_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_steps_partial. fs_h_pfc_shift_product_last_transport_oldsum_body_steps_partial + S (fs_r_pfc_shift_product_last_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_steps_partial. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum) + (fs_r_pfc_shift_product_last_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_steps_successor. fs_h_pfc_shift_product_last_transport_oldsum_body_steps_successor + S (fs_s_pfc_shift_product_last_transport_oldsum_body_steps) = S ((S (S fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_steps_successor. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum) + (fs_s_pfc_shift_product_last_transport_oldsum_body_steps))) /\ fs_s_pfc_shift_product_last_transport_oldsum_body_steps = fs_r_pfc_shift_product_last_transport_oldsum_body_steps + fs_a_pfc_shift_product_last_transport_oldsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_last_transport_oldresiduebound. pfa_gap_shift_product_last_transport_oldresiduebound + S (x) = (p)) /\ ((exists pfa_offset_left_shift_product_last_transport_oldresiduecongruence pfa_offset_right_shift_product_last_transport_oldresiduecongruence. (pfc_natural_sum_shift_product_last_transport_old) + (p) * pfa_offset_left_shift_product_last_transport_oldresiduecongruence = (x) + (p) * pfa_offset_right_shift_product_last_transport_oldresiduecongruence))))))))) -> (exists pfc_terms_code_shift_product_last_transport_new pfc_terms_scale_shift_product_last_transport_new pfc_natural_sum_shift_product_last_transport_new. ((forall pfc_index_shift_product_last_transport_newdiagonal. (exists pfa_gap_shift_product_last_transport_newdiagonalbound. pfa_gap_shift_product_last_transport_newdiagonalbound + S (pfc_index_shift_product_last_transport_newdiagonal) = (S (N))) -> exists pfc_value_shift_product_last_transport_newdiagonal. ((((exists ff_h_pfp_shift_product_last_transport_newdiagonalentry. ff_h_pfp_shift_product_last_transport_newdiagonalentry + S (pfc_value_shift_product_last_transport_newdiagonal) = S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * pfc_terms_scale_shift_product_last_transport_new)) /\ exists ff_q_pfp_shift_product_last_transport_newdiagonalentry. pfc_terms_code_shift_product_last_transport_new = ff_q_pfp_shift_product_last_transport_newdiagonalentry * S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * pfc_terms_scale_shift_product_last_transport_new) + (pfc_value_shift_product_last_transport_newdiagonal))) /\ ((exists pfc_complement_shift_product_last_transport_newdiagonalterm pfc_left_shift_product_last_transport_newdiagonalterm pfc_right_shift_product_last_transport_newdiagonalterm. (((pfc_index_shift_product_last_transport_newdiagonal)+pfc_complement_shift_product_last_transport_newdiagonalterm=(N)) /\ ((((((exists pfa_gap_shift_product_last_transport_newdiagonaltermleftinside. pfa_gap_shift_product_last_transport_newdiagonaltermleftinside + S (pfc_index_shift_product_last_transport_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_last_transport_newdiagonaltermleftentry. ff_h_pfp_shift_product_last_transport_newdiagonaltermleftentry + S (pfc_left_shift_product_last_transport_newdiagonalterm) = S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_last_transport_newdiagonaltermleftentry. ab = ff_q_pfp_shift_product_last_transport_newdiagonaltermleftentry * S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * ac) + (pfc_left_shift_product_last_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_newdiagonaltermleftoutside. pfc_gap_shift_product_last_transport_newdiagonaltermleftoutside+(L)=(pfc_index_shift_product_last_transport_newdiagonal)) /\ (((pfc_left_shift_product_last_transport_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_last_transport_newdiagonaltermrightinside. pfa_gap_shift_product_last_transport_newdiagonaltermrightinside + S (pfc_complement_shift_product_last_transport_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_last_transport_newdiagonaltermrightentry. ff_h_pfp_shift_product_last_transport_newdiagonaltermrightentry + S (pfc_right_shift_product_last_transport_newdiagonalterm) = S ((S (pfc_complement_shift_product_last_transport_newdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_last_transport_newdiagonaltermrightentry. BB = ff_q_pfp_shift_product_last_transport_newdiagonaltermrightentry * S ((S (pfc_complement_shift_product_last_transport_newdiagonalterm)) * BC) + (pfc_right_shift_product_last_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_newdiagonaltermrightoutside. pfc_gap_shift_product_last_transport_newdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_last_transport_newdiagonalterm)) /\ (((pfc_right_shift_product_last_transport_newdiagonalterm)=0))))) /\ (((pfc_value_shift_product_last_transport_newdiagonal)=pfc_left_shift_product_last_transport_newdiagonalterm*pfc_right_shift_product_last_transport_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_last_transport_newsum fs_v_pfc_shift_product_last_transport_newsum. ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_start. fs_h_pfc_shift_product_last_transport_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_start. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_last_transport_newsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_terminal. fs_h_pfc_shift_product_last_transport_newsum_body_terminal + S (pfc_natural_sum_shift_product_last_transport_new) = S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_terminal. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_terminal * S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_newsum) + (pfc_natural_sum_shift_product_last_transport_new))) /\ forall fs_i_pfc_shift_product_last_transport_newsum_body_steps. (exists fs_lt_pfc_shift_product_last_transport_newsum_body_steps_bound. fs_lt_pfc_shift_product_last_transport_newsum_body_steps_bound + S fs_i_pfc_shift_product_last_transport_newsum_body_steps = S (N)) -> exists fs_a_pfc_shift_product_last_transport_newsum_body_steps fs_r_pfc_shift_product_last_transport_newsum_body_steps fs_s_pfc_shift_product_last_transport_newsum_body_steps. ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_steps_summand. fs_h_pfc_shift_product_last_transport_newsum_body_steps_summand + S (fs_a_pfc_shift_product_last_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_new)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_steps_summand. pfc_terms_code_shift_product_last_transport_new = fs_q_pfc_shift_product_last_transport_newsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_new) + (fs_a_pfc_shift_product_last_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_steps_partial. fs_h_pfc_shift_product_last_transport_newsum_body_steps_partial + S (fs_r_pfc_shift_product_last_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_steps_partial. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum) + (fs_r_pfc_shift_product_last_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_steps_successor. fs_h_pfc_shift_product_last_transport_newsum_body_steps_successor + S (fs_s_pfc_shift_product_last_transport_newsum_body_steps) = S ((S (S fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_steps_successor. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum) + (fs_s_pfc_shift_product_last_transport_newsum_body_steps))) /\ fs_s_pfc_shift_product_last_transport_newsum_body_steps = fs_r_pfc_shift_product_last_transport_newsum_body_steps + fs_a_pfc_shift_product_last_transport_newsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_last_transport_newresiduebound. pfa_gap_shift_product_last_transport_newresiduebound + S (x) = (p)) /\ ((exists pfa_offset_left_shift_product_last_transport_newresiduecongruence pfa_offset_right_shift_product_last_transport_newresiduecongruence. (pfc_natural_sum_shift_product_last_transport_new) + (p) * pfa_offset_left_shift_product_last_transport_newresiduecongruence = (x) + (p) * pfa_offset_right_shift_product_last_transport_newresiduecongruence)))))))))) /\ (((exists pfc_terms_code_shift_product_last_transport_new pfc_terms_scale_shift_product_last_transport_new pfc_natural_sum_shift_product_last_transport_new. ((forall pfc_index_shift_product_last_transport_newdiagonal. (exists pfa_gap_shift_product_last_transport_newdiagonalbound. pfa_gap_shift_product_last_transport_newdiagonalbound + S (pfc_index_shift_product_last_transport_newdiagonal) = (S (N))) -> exists pfc_value_shift_product_last_transport_newdiagonal. ((((exists ff_h_pfp_shift_product_last_transport_newdiagonalentry. ff_h_pfp_shift_product_last_transport_newdiagonalentry + S (pfc_value_shift_product_last_transport_newdiagonal) = S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * pfc_terms_scale_shift_product_last_transport_new)) /\ exists ff_q_pfp_shift_product_last_transport_newdiagonalentry. pfc_terms_code_shift_product_last_transport_new = ff_q_pfp_shift_product_last_transport_newdiagonalentry * S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * pfc_terms_scale_shift_product_last_transport_new) + (pfc_value_shift_product_last_transport_newdiagonal))) /\ ((exists pfc_complement_shift_product_last_transport_newdiagonalterm pfc_left_shift_product_last_transport_newdiagonalterm pfc_right_shift_product_last_transport_newdiagonalterm. (((pfc_index_shift_product_last_transport_newdiagonal)+pfc_complement_shift_product_last_transport_newdiagonalterm=(N)) /\ ((((((exists pfa_gap_shift_product_last_transport_newdiagonaltermleftinside. pfa_gap_shift_product_last_transport_newdiagonaltermleftinside + S (pfc_index_shift_product_last_transport_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_last_transport_newdiagonaltermleftentry. ff_h_pfp_shift_product_last_transport_newdiagonaltermleftentry + S (pfc_left_shift_product_last_transport_newdiagonalterm) = S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_last_transport_newdiagonaltermleftentry. ab = ff_q_pfp_shift_product_last_transport_newdiagonaltermleftentry * S ((S (pfc_index_shift_product_last_transport_newdiagonal)) * ac) + (pfc_left_shift_product_last_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_newdiagonaltermleftoutside. pfc_gap_shift_product_last_transport_newdiagonaltermleftoutside+(L)=(pfc_index_shift_product_last_transport_newdiagonal)) /\ (((pfc_left_shift_product_last_transport_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_last_transport_newdiagonaltermrightinside. pfa_gap_shift_product_last_transport_newdiagonaltermrightinside + S (pfc_complement_shift_product_last_transport_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_product_last_transport_newdiagonaltermrightentry. ff_h_pfp_shift_product_last_transport_newdiagonaltermrightentry + S (pfc_right_shift_product_last_transport_newdiagonalterm) = S ((S (pfc_complement_shift_product_last_transport_newdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_product_last_transport_newdiagonaltermrightentry. BB = ff_q_pfp_shift_product_last_transport_newdiagonaltermrightentry * S ((S (pfc_complement_shift_product_last_transport_newdiagonalterm)) * BC) + (pfc_right_shift_product_last_transport_newdiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_newdiagonaltermrightoutside. pfc_gap_shift_product_last_transport_newdiagonaltermrightoutside+(S M)=(pfc_complement_shift_product_last_transport_newdiagonalterm)) /\ (((pfc_right_shift_product_last_transport_newdiagonalterm)=0))))) /\ (((pfc_value_shift_product_last_transport_newdiagonal)=pfc_left_shift_product_last_transport_newdiagonalterm*pfc_right_shift_product_last_transport_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_last_transport_newsum fs_v_pfc_shift_product_last_transport_newsum. ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_start. fs_h_pfc_shift_product_last_transport_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_start. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_last_transport_newsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_terminal. fs_h_pfc_shift_product_last_transport_newsum_body_terminal + S (pfc_natural_sum_shift_product_last_transport_new) = S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_terminal. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_terminal * S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_newsum) + (pfc_natural_sum_shift_product_last_transport_new))) /\ forall fs_i_pfc_shift_product_last_transport_newsum_body_steps. (exists fs_lt_pfc_shift_product_last_transport_newsum_body_steps_bound. fs_lt_pfc_shift_product_last_transport_newsum_body_steps_bound + S fs_i_pfc_shift_product_last_transport_newsum_body_steps = S (N)) -> exists fs_a_pfc_shift_product_last_transport_newsum_body_steps fs_r_pfc_shift_product_last_transport_newsum_body_steps fs_s_pfc_shift_product_last_transport_newsum_body_steps. ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_steps_summand. fs_h_pfc_shift_product_last_transport_newsum_body_steps_summand + S (fs_a_pfc_shift_product_last_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_new)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_steps_summand. pfc_terms_code_shift_product_last_transport_new = fs_q_pfc_shift_product_last_transport_newsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_new) + (fs_a_pfc_shift_product_last_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_steps_partial. fs_h_pfc_shift_product_last_transport_newsum_body_steps_partial + S (fs_r_pfc_shift_product_last_transport_newsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_steps_partial. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum) + (fs_r_pfc_shift_product_last_transport_newsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_newsum_body_steps_successor. fs_h_pfc_shift_product_last_transport_newsum_body_steps_successor + S (fs_s_pfc_shift_product_last_transport_newsum_body_steps) = S ((S (S fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum)) /\ exists fs_q_pfc_shift_product_last_transport_newsum_body_steps_successor. fs_u_pfc_shift_product_last_transport_newsum = fs_q_pfc_shift_product_last_transport_newsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_last_transport_newsum_body_steps)) * fs_v_pfc_shift_product_last_transport_newsum) + (fs_s_pfc_shift_product_last_transport_newsum_body_steps))) /\ fs_s_pfc_shift_product_last_transport_newsum_body_steps = fs_r_pfc_shift_product_last_transport_newsum_body_steps + fs_a_pfc_shift_product_last_transport_newsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_last_transport_newresiduebound. pfa_gap_shift_product_last_transport_newresiduebound + S (x) = (p)) /\ ((exists pfa_offset_left_shift_product_last_transport_newresiduecongruence pfa_offset_right_shift_product_last_transport_newresiduecongruence. (pfc_natural_sum_shift_product_last_transport_new) + (p) * pfa_offset_left_shift_product_last_transport_newresiduecongruence = (x) + (p) * pfa_offset_right_shift_product_last_transport_newresiduecongruence))))))))) -> (exists pfc_terms_code_shift_product_last_transport_old pfc_terms_scale_shift_product_last_transport_old pfc_natural_sum_shift_product_last_transport_old. ((forall pfc_index_shift_product_last_transport_olddiagonal. (exists pfa_gap_shift_product_last_transport_olddiagonalbound. pfa_gap_shift_product_last_transport_olddiagonalbound + S (pfc_index_shift_product_last_transport_olddiagonal) = (S (N))) -> exists pfc_value_shift_product_last_transport_olddiagonal. ((((exists ff_h_pfp_shift_product_last_transport_olddiagonalentry. ff_h_pfp_shift_product_last_transport_olddiagonalentry + S (pfc_value_shift_product_last_transport_olddiagonal) = S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * pfc_terms_scale_shift_product_last_transport_old)) /\ exists ff_q_pfp_shift_product_last_transport_olddiagonalentry. pfc_terms_code_shift_product_last_transport_old = ff_q_pfp_shift_product_last_transport_olddiagonalentry * S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * pfc_terms_scale_shift_product_last_transport_old) + (pfc_value_shift_product_last_transport_olddiagonal))) /\ ((exists pfc_complement_shift_product_last_transport_olddiagonalterm pfc_left_shift_product_last_transport_olddiagonalterm pfc_right_shift_product_last_transport_olddiagonalterm. (((pfc_index_shift_product_last_transport_olddiagonal)+pfc_complement_shift_product_last_transport_olddiagonalterm=(N)) /\ ((((((exists pfa_gap_shift_product_last_transport_olddiagonaltermleftinside. pfa_gap_shift_product_last_transport_olddiagonaltermleftinside + S (pfc_index_shift_product_last_transport_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_product_last_transport_olddiagonaltermleftentry. ff_h_pfp_shift_product_last_transport_olddiagonaltermleftentry + S (pfc_left_shift_product_last_transport_olddiagonalterm) = S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * ac)) /\ exists ff_q_pfp_shift_product_last_transport_olddiagonaltermleftentry. ab = ff_q_pfp_shift_product_last_transport_olddiagonaltermleftentry * S ((S (pfc_index_shift_product_last_transport_olddiagonal)) * ac) + (pfc_left_shift_product_last_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_olddiagonaltermleftoutside. pfc_gap_shift_product_last_transport_olddiagonaltermleftoutside+(L)=(pfc_index_shift_product_last_transport_olddiagonal)) /\ (((pfc_left_shift_product_last_transport_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_product_last_transport_olddiagonaltermrightinside. pfa_gap_shift_product_last_transport_olddiagonaltermrightinside + S (pfc_complement_shift_product_last_transport_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_product_last_transport_olddiagonaltermrightentry. ff_h_pfp_shift_product_last_transport_olddiagonaltermrightentry + S (pfc_right_shift_product_last_transport_olddiagonalterm) = S ((S (pfc_complement_shift_product_last_transport_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_product_last_transport_olddiagonaltermrightentry. bb = ff_q_pfp_shift_product_last_transport_olddiagonaltermrightentry * S ((S (pfc_complement_shift_product_last_transport_olddiagonalterm)) * bc) + (pfc_right_shift_product_last_transport_olddiagonalterm)))))) \/ (((exists pfc_gap_shift_product_last_transport_olddiagonaltermrightoutside. pfc_gap_shift_product_last_transport_olddiagonaltermrightoutside+(M)=(pfc_complement_shift_product_last_transport_olddiagonalterm)) /\ (((pfc_right_shift_product_last_transport_olddiagonalterm)=0))))) /\ (((pfc_value_shift_product_last_transport_olddiagonal)=pfc_left_shift_product_last_transport_olddiagonalterm*pfc_right_shift_product_last_transport_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_product_last_transport_oldsum fs_v_pfc_shift_product_last_transport_oldsum. ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_start. fs_h_pfc_shift_product_last_transport_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_start. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_start * S ((S (0)) * fs_v_pfc_shift_product_last_transport_oldsum) + (0))) /\ ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_terminal. fs_h_pfc_shift_product_last_transport_oldsum_body_terminal + S (pfc_natural_sum_shift_product_last_transport_old) = S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_terminal. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_terminal * S ((S (S (N))) * fs_v_pfc_shift_product_last_transport_oldsum) + (pfc_natural_sum_shift_product_last_transport_old))) /\ forall fs_i_pfc_shift_product_last_transport_oldsum_body_steps. (exists fs_lt_pfc_shift_product_last_transport_oldsum_body_steps_bound. fs_lt_pfc_shift_product_last_transport_oldsum_body_steps_bound + S fs_i_pfc_shift_product_last_transport_oldsum_body_steps = S (N)) -> exists fs_a_pfc_shift_product_last_transport_oldsum_body_steps fs_r_pfc_shift_product_last_transport_oldsum_body_steps fs_s_pfc_shift_product_last_transport_oldsum_body_steps. ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_steps_summand. fs_h_pfc_shift_product_last_transport_oldsum_body_steps_summand + S (fs_a_pfc_shift_product_last_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_old)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_steps_summand. pfc_terms_code_shift_product_last_transport_old = fs_q_pfc_shift_product_last_transport_oldsum_body_steps_summand * S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * pfc_terms_scale_shift_product_last_transport_old) + (fs_a_pfc_shift_product_last_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_steps_partial. fs_h_pfc_shift_product_last_transport_oldsum_body_steps_partial + S (fs_r_pfc_shift_product_last_transport_oldsum_body_steps) = S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_steps_partial. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_steps_partial * S ((S (fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum) + (fs_r_pfc_shift_product_last_transport_oldsum_body_steps))) /\ ((((exists fs_h_pfc_shift_product_last_transport_oldsum_body_steps_successor. fs_h_pfc_shift_product_last_transport_oldsum_body_steps_successor + S (fs_s_pfc_shift_product_last_transport_oldsum_body_steps) = S ((S (S fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum)) /\ exists fs_q_pfc_shift_product_last_transport_oldsum_body_steps_successor. fs_u_pfc_shift_product_last_transport_oldsum = fs_q_pfc_shift_product_last_transport_oldsum_body_steps_successor * S ((S (S fs_i_pfc_shift_product_last_transport_oldsum_body_steps)) * fs_v_pfc_shift_product_last_transport_oldsum) + (fs_s_pfc_shift_product_last_transport_oldsum_body_steps))) /\ fs_s_pfc_shift_product_last_transport_oldsum_body_steps = fs_r_pfc_shift_product_last_transport_oldsum_body_steps + fs_a_pfc_shift_product_last_transport_oldsum_body_steps)))))) /\ ((((exists pfa_gap_shift_product_last_transport_oldresiduebound. pfa_gap_shift_product_last_transport_oldresiduebound + S (x) = (p)) /\ ((exists pfa_offset_left_shift_product_last_transport_oldresiduecongruence pfa_offset_right_shift_product_last_transport_oldresiduecongruence. (pfc_natural_sum_shift_product_last_transport_old) + (p) * pfa_offset_left_shift_product_last_transport_oldresiduecongruence = (x) + (p) * pfa_offset_right_shift_product_last_transport_oldresiduecongruence)))))))))))) - 0119
specialize prime_field_convolution_coefficient_shift_right_iff (p) - 0120
specialize prime_field_convolution_coefficient_shift_right_iff (ab) - 0121
specialize prime_field_convolution_coefficient_shift_right_iff (ac) - 0122
specialize prime_field_convolution_coefficient_shift_right_iff (L) - 0123
specialize prime_field_convolution_coefficient_shift_right_iff (bb) - 0124
specialize prime_field_convolution_coefficient_shift_right_iff (bc) - 0125
specialize prime_field_convolution_coefficient_shift_right_iff (M) - 0126
specialize prime_field_convolution_coefficient_shift_right_iff (BB) - 0127
specialize prime_field_convolution_coefficient_shift_right_iff (BC) - 0128
specialize prime_field_convolution_coefficient_shift_right_iff (N) - 0129
specialize prime_field_convolution_coefficient_shift_right_iff (x) - 0130
apply prime_field_convolution_coefficient_shift_right_iff - 0131
exact hs - 0132
cases hiff - 0133
apply hiff_right - 0134
exact hv_witness_right - 0135
have hz : x=0 - 0136
specialize prime_field_polynomial_convolution_outside_zero (p) - 0137
specialize prime_field_polynomial_convolution_outside_zero (ab) - 0138
specialize prime_field_polynomial_convolution_outside_zero (ac) - 0139
specialize prime_field_polynomial_convolution_outside_zero (L) - 0140
specialize prime_field_polynomial_convolution_outside_zero (bb) - 0141
specialize prime_field_polynomial_convolution_outside_zero (bc) - 0142
specialize prime_field_polynomial_convolution_outside_zero (M) - 0143
specialize prime_field_polynomial_convolution_outside_zero (cb) - 0144
specialize prime_field_polynomial_convolution_outside_zero (cc) - 0145
specialize prime_field_polynomial_convolution_outside_zero (N) - 0146
specialize prime_field_polynomial_convolution_outside_zero (N) - 0147
specialize prime_field_polynomial_convolution_outside_zero (x) - 0148
apply prime_field_polynomial_convolution_outside_zero - 0149
exact hp - 0150
exact hwhole - 0151
specialize le_refl (N) - 0152
apply le_refl - 0153
exact hco - 0154
rewrite hz at hv_witness_left - 0155
rewrite hz at hv_witness_left - 0156
exact hv_witness_left