PX0070

prime_field_polynomial_convolution_both_left_paddings_equivalent

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Construct an actual intermediate product and compose the two proved factor-padding compatibilities; both empty and nonempty factors are covered.

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 AB AC t BB BC s CB CC K. (~(p=0)) -> (((forall pfp_repeat_index_both_left_paddingzeros. (exists pfa_gap_both_left_paddingzerosindex. pfa_gap_both_left_paddingzerosindex + S (pfp_repeat_index_both_left_paddingzeros) = (t)) -> (((exists ff_h_pfp_both_left_paddingzerosentry. ff_h_pfp_both_left_paddingzerosentry + S (0) = S ((S (pfp_repeat_index_both_left_paddingzeros)) * AC)) /\ exists ff_q_pfp_both_left_paddingzerosentry. AB = ff_q_pfp_both_left_paddingzerosentry * S ((S (pfp_repeat_index_both_left_paddingzeros)) * AC) + (0)))) /\ ((forall pfrep_index_both_left_padding pfrep_value_both_left_padding. (exists pfa_gap_both_left_paddingbound. pfa_gap_both_left_paddingbound + S (pfrep_index_both_left_padding) = (L)) -> (((exists ff_h_pfp_both_left_paddinginput. ff_h_pfp_both_left_paddinginput + S (pfrep_value_both_left_padding) = S ((S (pfrep_index_both_left_padding)) * ac)) /\ exists ff_q_pfp_both_left_paddinginput. ab = ff_q_pfp_both_left_paddinginput * S ((S (pfrep_index_both_left_padding)) * ac) + (pfrep_value_both_left_padding))) -> (((exists ff_h_pfp_both_left_paddingoutput. ff_h_pfp_both_left_paddingoutput + S (pfrep_value_both_left_padding) = S ((S ((t)+pfrep_index_both_left_padding)) * AC)) /\ exists ff_q_pfp_both_left_paddingoutput. AB = ff_q_pfp_both_left_paddingoutput * S ((S ((t)+pfrep_index_both_left_padding)) * AC) + (pfrep_value_both_left_padding))))))) -> (((forall pfp_repeat_index_both_right_paddingzeros. (exists pfa_gap_both_right_paddingzerosindex. pfa_gap_both_right_paddingzerosindex + S (pfp_repeat_index_both_right_paddingzeros) = (s)) -> (((exists ff_h_pfp_both_right_paddingzerosentry. ff_h_pfp_both_right_paddingzerosentry + S (0) = S ((S (pfp_repeat_index_both_right_paddingzeros)) * BC)) /\ exists ff_q_pfp_both_right_paddingzerosentry. BB = ff_q_pfp_both_right_paddingzerosentry * S ((S (pfp_repeat_index_both_right_paddingzeros)) * BC) + (0)))) /\ ((forall pfrep_index_both_right_padding pfrep_value_both_right_padding. (exists pfa_gap_both_right_paddingbound. pfa_gap_both_right_paddingbound + S (pfrep_index_both_right_padding) = (M)) -> (((exists ff_h_pfp_both_right_paddinginput. ff_h_pfp_both_right_paddinginput + S (pfrep_value_both_right_padding) = S ((S (pfrep_index_both_right_padding)) * bc)) /\ exists ff_q_pfp_both_right_paddinginput. bb = ff_q_pfp_both_right_paddinginput * S ((S (pfrep_index_both_right_padding)) * bc) + (pfrep_value_both_right_padding))) -> (((exists ff_h_pfp_both_right_paddingoutput. ff_h_pfp_both_right_paddingoutput + S (pfrep_value_both_right_padding) = S ((S ((s)+pfrep_index_both_right_padding)) * BC)) /\ exists ff_q_pfp_both_right_paddingoutput. BB = ff_q_pfp_both_right_paddingoutput * S ((S ((s)+pfrep_index_both_right_padding)) * BC) + (pfrep_value_both_right_padding))))))) -> (((forall fom_index_pfp_both_original_productleft. (exists fom_gap_pfp_both_original_productleft_index_bound. fom_gap_pfp_both_original_productleft_index_bound + S (fom_index_pfp_both_original_productleft) = L) -> exists fom_value_pfp_both_original_productleft. ((((exists fom_beta_height_pfp_both_original_productleft_entry. fom_beta_height_pfp_both_original_productleft_entry + S (fom_value_pfp_both_original_productleft) = S ((S (fom_index_pfp_both_original_productleft)) * ac)) /\ exists fom_beta_quotient_pfp_both_original_productleft_entry. ab = fom_beta_quotient_pfp_both_original_productleft_entry * S ((S (fom_index_pfp_both_original_productleft)) * ac) + (fom_value_pfp_both_original_productleft))) /\ (exists fom_gap_pfp_both_original_productleft_value_bound. fom_gap_pfp_both_original_productleft_value_bound + S (fom_value_pfp_both_original_productleft) = p))) /\ (((forall fom_index_pfp_both_original_productright. (exists fom_gap_pfp_both_original_productright_index_bound. fom_gap_pfp_both_original_productright_index_bound + S (fom_index_pfp_both_original_productright) = M) -> exists fom_value_pfp_both_original_productright. ((((exists fom_beta_height_pfp_both_original_productright_entry. fom_beta_height_pfp_both_original_productright_entry + S (fom_value_pfp_both_original_productright) = S ((S (fom_index_pfp_both_original_productright)) * bc)) /\ exists fom_beta_quotient_pfp_both_original_productright_entry. bb = fom_beta_quotient_pfp_both_original_productright_entry * S ((S (fom_index_pfp_both_original_productright)) * bc) + (fom_value_pfp_both_original_productright))) /\ (exists fom_gap_pfp_both_original_productright_value_bound. fom_gap_pfp_both_original_productright_value_bound + S (fom_value_pfp_both_original_productright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_both_original_productcoefficients. (exists pfa_gap_both_original_productcoefficientsbound. pfa_gap_both_original_productcoefficientsbound + S (pfc_index_both_original_productcoefficients) = (N)) -> exists pfc_value_both_original_productcoefficients. ((((exists ff_h_pfp_both_original_productcoefficientsentry. ff_h_pfp_both_original_productcoefficientsentry + S (pfc_value_both_original_productcoefficients) = S ((S (pfc_index_both_original_productcoefficients)) * cc)) /\ exists ff_q_pfp_both_original_productcoefficientsentry. cb = ff_q_pfp_both_original_productcoefficientsentry * S ((S (pfc_index_both_original_productcoefficients)) * cc) + (pfc_value_both_original_productcoefficients))) /\ ((exists pfc_terms_code_both_original_productcoefficientscoefficient pfc_terms_scale_both_original_productcoefficientscoefficient pfc_natural_sum_both_original_productcoefficientscoefficient. ((forall pfc_index_both_original_productcoefficientscoefficientdiagonal. (exists pfa_gap_both_original_productcoefficientscoefficientdiagonalbound. pfa_gap_both_original_productcoefficientscoefficientdiagonalbound + S (pfc_index_both_original_productcoefficientscoefficientdiagonal) = (S (pfc_index_both_original_productcoefficients))) -> exists pfc_value_both_original_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_both_original_productcoefficientscoefficientdiagonalentry. ff_h_pfp_both_original_productcoefficientscoefficientdiagonalentry + S (pfc_value_both_original_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_original_productcoefficientscoefficient)) /\ exists ff_q_pfp_both_original_productcoefficientscoefficientdiagonalentry. pfc_terms_code_both_original_productcoefficientscoefficient = ff_q_pfp_both_original_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_original_productcoefficientscoefficient) + (pfc_value_both_original_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_both_original_productcoefficientscoefficientdiagonalterm pfc_left_both_original_productcoefficientscoefficientdiagonalterm pfc_right_both_original_productcoefficientscoefficientdiagonalterm. (((pfc_index_both_original_productcoefficientscoefficientdiagonal)+pfc_complement_both_original_productcoefficientscoefficientdiagonalterm=(pfc_index_both_original_productcoefficients)) /\ ((((((exists pfa_gap_both_original_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_both_original_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_both_original_productcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_both_original_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * ac) + (pfc_left_both_original_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_original_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_both_original_productcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_both_original_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_both_original_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_both_original_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_both_original_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_both_original_productcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_both_original_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_both_original_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_both_original_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_both_original_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_original_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_both_original_productcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_both_original_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_both_original_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_both_original_productcoefficientscoefficientdiagonal)=pfc_left_both_original_productcoefficientscoefficientdiagonalterm*pfc_right_both_original_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_both_original_productcoefficientscoefficientsum fs_v_pfc_both_original_productcoefficientscoefficientsum. ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_start. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_start. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_both_original_productcoefficientscoefficient) = S ((S (S (pfc_index_both_original_productcoefficients))) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_both_original_productcoefficients))) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (pfc_natural_sum_both_original_productcoefficientscoefficient))) /\ forall fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_both_original_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_both_original_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps = S (pfc_index_both_original_productcoefficients)) -> exists fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_original_productcoefficientscoefficient)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_both_original_productcoefficientscoefficient = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_original_productcoefficientscoefficient) + (fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps = fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps + fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_both_original_productcoefficientscoefficientresiduebound. pfa_gap_both_original_productcoefficientscoefficientresiduebound + S (pfc_value_both_original_productcoefficients) = (p)) /\ ((exists pfa_offset_left_both_original_productcoefficientscoefficientresiduecongruence pfa_offset_right_both_original_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_both_original_productcoefficientscoefficient) + (p) * pfa_offset_left_both_original_productcoefficientscoefficientresiduecongruence = (pfc_value_both_original_productcoefficients) + (p) * pfa_offset_right_both_original_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_both_padded_productleft. (exists fom_gap_pfp_both_padded_productleft_index_bound. fom_gap_pfp_both_padded_productleft_index_bound + S (fom_index_pfp_both_padded_productleft) = t+L) -> exists fom_value_pfp_both_padded_productleft. ((((exists fom_beta_height_pfp_both_padded_productleft_entry. fom_beta_height_pfp_both_padded_productleft_entry + S (fom_value_pfp_both_padded_productleft) = S ((S (fom_index_pfp_both_padded_productleft)) * AC)) /\ exists fom_beta_quotient_pfp_both_padded_productleft_entry. AB = fom_beta_quotient_pfp_both_padded_productleft_entry * S ((S (fom_index_pfp_both_padded_productleft)) * AC) + (fom_value_pfp_both_padded_productleft))) /\ (exists fom_gap_pfp_both_padded_productleft_value_bound. fom_gap_pfp_both_padded_productleft_value_bound + S (fom_value_pfp_both_padded_productleft) = p))) /\ (((forall fom_index_pfp_both_padded_productright. (exists fom_gap_pfp_both_padded_productright_index_bound. fom_gap_pfp_both_padded_productright_index_bound + S (fom_index_pfp_both_padded_productright) = s+M) -> exists fom_value_pfp_both_padded_productright. ((((exists fom_beta_height_pfp_both_padded_productright_entry. fom_beta_height_pfp_both_padded_productright_entry + S (fom_value_pfp_both_padded_productright) = S ((S (fom_index_pfp_both_padded_productright)) * BC)) /\ exists fom_beta_quotient_pfp_both_padded_productright_entry. BB = fom_beta_quotient_pfp_both_padded_productright_entry * S ((S (fom_index_pfp_both_padded_productright)) * BC) + (fom_value_pfp_both_padded_productright))) /\ (exists fom_gap_pfp_both_padded_productright_value_bound. fom_gap_pfp_both_padded_productright_value_bound + S (fom_value_pfp_both_padded_productright) = p))) /\ (((((((t+L)=0 \/ (s+M)=0) /\ (((K)=0)))) \/ (((~((t+L)=0)) /\ (((~((s+M)=0)) /\ (((t+L)+(s+M)=S (K)))))))) /\ ((forall pfc_index_both_padded_productcoefficients. (exists pfa_gap_both_padded_productcoefficientsbound. pfa_gap_both_padded_productcoefficientsbound + S (pfc_index_both_padded_productcoefficients) = (K)) -> exists pfc_value_both_padded_productcoefficients. ((((exists ff_h_pfp_both_padded_productcoefficientsentry. ff_h_pfp_both_padded_productcoefficientsentry + S (pfc_value_both_padded_productcoefficients) = S ((S (pfc_index_both_padded_productcoefficients)) * CC)) /\ exists ff_q_pfp_both_padded_productcoefficientsentry. CB = ff_q_pfp_both_padded_productcoefficientsentry * S ((S (pfc_index_both_padded_productcoefficients)) * CC) + (pfc_value_both_padded_productcoefficients))) /\ ((exists pfc_terms_code_both_padded_productcoefficientscoefficient pfc_terms_scale_both_padded_productcoefficientscoefficient pfc_natural_sum_both_padded_productcoefficientscoefficient. ((forall pfc_index_both_padded_productcoefficientscoefficientdiagonal. (exists pfa_gap_both_padded_productcoefficientscoefficientdiagonalbound. pfa_gap_both_padded_productcoefficientscoefficientdiagonalbound + S (pfc_index_both_padded_productcoefficientscoefficientdiagonal) = (S (pfc_index_both_padded_productcoefficients))) -> exists pfc_value_both_padded_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_both_padded_productcoefficientscoefficientdiagonalentry. ff_h_pfp_both_padded_productcoefficientscoefficientdiagonalentry + S (pfc_value_both_padded_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_padded_productcoefficientscoefficient)) /\ exists ff_q_pfp_both_padded_productcoefficientscoefficientdiagonalentry. pfc_terms_code_both_padded_productcoefficientscoefficient = ff_q_pfp_both_padded_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_padded_productcoefficientscoefficient) + (pfc_value_both_padded_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm pfc_left_both_padded_productcoefficientscoefficientdiagonalterm pfc_right_both_padded_productcoefficientscoefficientdiagonalterm. (((pfc_index_both_padded_productcoefficientscoefficientdiagonal)+pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm=(pfc_index_both_padded_productcoefficients)) /\ ((((((exists pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_both_padded_productcoefficientscoefficientdiagonal) = (t+L)) /\ ((((exists ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_both_padded_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * AC) + (pfc_left_both_padded_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermleftoutside+(t+L)=(pfc_index_both_padded_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_both_padded_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm) = (s+M)) /\ ((((exists ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_both_padded_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_both_padded_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermrightoutside+(s+M)=(pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_both_padded_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_both_padded_productcoefficientscoefficientdiagonal)=pfc_left_both_padded_productcoefficientscoefficientdiagonalterm*pfc_right_both_padded_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_both_padded_productcoefficientscoefficientsum fs_v_pfc_both_padded_productcoefficientscoefficientsum. ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_start. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_start. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_both_padded_productcoefficientscoefficient) = S ((S (S (pfc_index_both_padded_productcoefficients))) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_both_padded_productcoefficients))) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (pfc_natural_sum_both_padded_productcoefficientscoefficient))) /\ forall fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_both_padded_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_both_padded_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps = S (pfc_index_both_padded_productcoefficients)) -> exists fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_padded_productcoefficientscoefficient)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_both_padded_productcoefficientscoefficient = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_padded_productcoefficientscoefficient) + (fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps = fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps + fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_both_padded_productcoefficientscoefficientresiduebound. pfa_gap_both_padded_productcoefficientscoefficientresiduebound + S (pfc_value_both_padded_productcoefficients) = (p)) /\ ((exists pfa_offset_left_both_padded_productcoefficientscoefficientresiduecongruence pfa_offset_right_both_padded_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_both_padded_productcoefficientscoefficient) + (p) * pfa_offset_left_both_padded_productcoefficientscoefficientresiduecongruence = (pfc_value_both_padded_productcoefficients) + (p) * pfa_offset_right_both_padded_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_both_equivalent_result pfrep_left_both_equivalent_result pfrep_right_both_equivalent_result. ((exists pfrep_position_both_equivalent_resultfirst. ((pfrep_position_both_equivalent_resultfirst+S (pfrep_power_both_equivalent_result)=(N)) /\ ((((exists ff_h_pfp_both_equivalent_resultfirstentry. ff_h_pfp_both_equivalent_resultfirstentry + S (pfrep_left_both_equivalent_result) = S ((S (pfrep_position_both_equivalent_resultfirst)) * cc)) /\ exists ff_q_pfp_both_equivalent_resultfirstentry. cb = ff_q_pfp_both_equivalent_resultfirstentry * S ((S (pfrep_position_both_equivalent_resultfirst)) * cc) + (pfrep_left_both_equivalent_result)))))) \/ (((exists pfrep_gap_both_equivalent_resultfirstoutside. pfrep_gap_both_equivalent_resultfirstoutside+(N)=(pfrep_power_both_equivalent_result)) /\ (((pfrep_left_both_equivalent_result)=0))))) -> ((exists pfrep_position_both_equivalent_resultsecond. ((pfrep_position_both_equivalent_resultsecond+S (pfrep_power_both_equivalent_result)=(K)) /\ ((((exists ff_h_pfp_both_equivalent_resultsecondentry. ff_h_pfp_both_equivalent_resultsecondentry + S (pfrep_right_both_equivalent_result) = S ((S (pfrep_position_both_equivalent_resultsecond)) * CC)) /\ exists ff_q_pfp_both_equivalent_resultsecondentry. CB = ff_q_pfp_both_equivalent_resultsecondentry * S ((S (pfrep_position_both_equivalent_resultsecond)) * CC) + (pfrep_right_both_equivalent_result)))))) \/ (((exists pfrep_gap_both_equivalent_resultsecondoutside. pfrep_gap_both_equivalent_resultsecondoutside+(K)=(pfrep_power_both_equivalent_result)) /\ (((pfrep_right_both_equivalent_result)=0))))) -> pfrep_left_both_equivalent_result=pfrep_right_both_equivalent_result)

Constructive proof overview

Generated structural guide

Construct an actual intermediate product and compose the two proved factor-padding compatibilities; both empty and nonempty factors are covered.

The unchanged tactic script uses 5 declared prerequisites and contains 107 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

polynomial_product_length_exists Alpha theorem; checked-use authorized prime_field_polynomial_convolution_at_length_exists Alpha theorem; checked-use authorized PX0010 prime_field_polynomial_equivalent_transitive PX006E prime_field_polynomial_convolution_left_padding_equivalent_left PX006F prime_field_polynomial_convolution_left_padding_equivalent_right

Direct dependents

PX0071 prime_field_polynomial_convolution_both_left_paddings_exists

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

107 script commands · 17 reading checkpoints · 4 local claims

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 (3)
prime field polynomial equivalent transitiveprime field polynomial convolution left padding equivalent leftprime field polynomial convolution left padding equivalent right

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro cb
  9. L9
    intro cc
  10. L10
    intro N
02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro AB
  2. L12
    intro AC
  3. L13
    intro t
  4. L14
    intro BB
  5. L15
    intro BC
  6. L16
    intro s
  7. L17
    intro CB
  8. L18
    intro CC
  9. L19
    intro K
  10. L20
    intro hp
03Fix variables and assumptionsL21–24

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro hA
  2. L22
    intro hB
  3. L23
    intro hc
  4. L24
    intro hn
04Establish hcopyL25–26

Establish this local claim before using it. It is not an additional assumption.

  1. L25
    have hcopy : FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)Definitions: FpPolyProduct
  2. L26
    exact hc
05Establish hnewcopyL27–28

Establish this local claim before using it. It is not an additional assumption.

  1. L27
    have hnewcopy : FpPolyProduct(p,AB,AC,t + L,BB,BC,s + M,CB,CC,K)Definitions: FpPolyProduct
  2. L28
    exact hn
06Separate the logical casesL29–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases hcopy
  2. L30
    cases hcopy_right
  3. L31
    cases hcopy_right_right
  4. L32
    cases hnewcopy
  5. L33
    cases hnewcopy_right
  6. L34
    cases hnewcopy_right_right
07Establish hlengthL35–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.

  1. L35
    have hlength : exists J. ((((t+L)=0 \/ (M)=0) /\ (((J)=0)))) \/ (((~((t+L)=0)) /\ (((~((M)=0)) /\ (((t+L)+(M)=S (J)))))))
  2. L36
    specialize polynomial_product_length_exists (t+L)
  3. L37
    specialize polynomial_product_length_exists (M)
  4. L38
    apply polynomial_product_length_exists
08Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hlength
09Establish hmiddleL40–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.

  1. L40
    have hmiddle : ∃ db. ∃ dc. FpPolyProduct(p,AB,AC,t + L,bb,bc,M,db,dc,x)Definitions: FpPolyProduct
  2. L41
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L42
    specialize prime_field_polynomial_convolution_at_length_exists (AB)
  4. L43
    specialize prime_field_polynomial_convolution_at_length_exists (AC)
  5. L44
    specialize prime_field_polynomial_convolution_at_length_exists (t+L)
  6. L45
    specialize prime_field_polynomial_convolution_at_length_exists (bb)
  7. L46
    specialize prime_field_polynomial_convolution_at_length_exists (bc)
  8. L47
    specialize prime_field_polynomial_convolution_at_length_exists (M)
  9. L48
    specialize prime_field_polynomial_convolution_at_length_exists (x)
  10. L49
    apply prime_field_polynomial_convolution_at_length_exists
10Use earlier factsL50–53

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    exact hp
  2. L51
    exact hnewcopy_left
  3. L52
    exact hcopy_right_left
  4. L53
    exact hlength_witness
11Separate the logical casesL54–55

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hmiddle
  2. L55
    cases hmiddle_witness
12Use earlier factsL56–65

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L56
    specialize prime_field_polynomial_equivalent_transitive (cb)
  2. L57
    specialize prime_field_polynomial_equivalent_transitive (cc)
  3. L58
    specialize prime_field_polynomial_equivalent_transitive (N)
  4. L59
    specialize prime_field_polynomial_equivalent_transitive (x1)
  5. L60
    specialize prime_field_polynomial_equivalent_transitive (x2)
  6. L61
    specialize prime_field_polynomial_equivalent_transitive (x)
  7. L62
    specialize prime_field_polynomial_equivalent_transitive (CB)
  8. L63
    specialize prime_field_polynomial_equivalent_transitive (CC)
  9. L64
    specialize prime_field_polynomial_equivalent_transitive (K)
  10. L65
    apply prime_field_polynomial_equivalent_transitive
13Use earlier factsL66–75

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L66
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (p)
  2. L67
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (ab)
  3. L68
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (ac)
  4. L69
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (L)
  5. L70
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (bb)
  6. L71
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (bc)
  7. L72
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (M)
  8. L73
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (cb)
  9. L74
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (cc)
  10. L75
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (N)
14Use earlier factsL76–85

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L76
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (AB)
  2. L77
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (AC)
  3. L78
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (t)
  4. L79
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (x1)
  5. L80
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (x2)
  6. L81
    specialize prime_field_polynomial_convolution_left_padding_equivalent_left (x)
  7. L82
    apply prime_field_polynomial_convolution_left_padding_equivalent_left
  8. L83
    exact hp
  9. L84
    exact hA
  10. L85
    exact hc
15Use earlier factsL86–95

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L86
    exact hmiddle_witness_witness
  2. L87
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (p)
  3. L88
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (AB)
  4. L89
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (AC)
  5. L90
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (t+L)
  6. L91
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (bb)
  7. L92
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (bc)
  8. L93
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (M)
  9. L94
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (x1)
  10. L95
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (x2)
16Use earlier factsL96–105

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L96
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (x)
  2. L97
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (BB)
  3. L98
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (BC)
  4. L99
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (s)
  5. L100
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (CB)
  6. L101
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (CC)
  7. L102
    specialize prime_field_polynomial_convolution_left_padding_equivalent_right (K)
  8. L103
    apply prime_field_polynomial_convolution_left_padding_equivalent_right
  9. L104
    exact hp
  10. L105
    exact hB
17Use earlier factsL106–107

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L106
    exact hmiddle_witness_witness
  2. L107
    exact hn

Library-wide reading audit

Original exact command ledger · 107 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro cb
  9. 0009intro cc
  10. 0010intro N
  11. 0011intro AB
  12. 0012intro AC
  13. 0013intro t
  14. 0014intro BB
  15. 0015intro BC
  16. 0016intro s
  17. 0017intro CB
  18. 0018intro CC
  19. 0019intro K
  20. 0020intro hp
  21. 0021intro hA
  22. 0022intro hB
  23. 0023intro hc
  24. 0024intro hn
  25. 0025have hcopy : ((forall fom_index_pfp_both_original_productleft. (exists fom_gap_pfp_both_original_productleft_index_bound. fom_gap_pfp_both_original_productleft_index_bound + S (fom_index_pfp_both_original_productleft) = L) -> exists fom_value_pfp_both_original_productleft. ((((exists fom_beta_height_pfp_both_original_productleft_entry. fom_beta_height_pfp_both_original_productleft_entry + S (fom_value_pfp_both_original_productleft) = S ((S (fom_index_pfp_both_original_productleft)) * ac)) /\ exists fom_beta_quotient_pfp_both_original_productleft_entry. ab = fom_beta_quotient_pfp_both_original_productleft_entry * S ((S (fom_index_pfp_both_original_productleft)) * ac) + (fom_value_pfp_both_original_productleft))) /\ (exists fom_gap_pfp_both_original_productleft_value_bound. fom_gap_pfp_both_original_productleft_value_bound + S (fom_value_pfp_both_original_productleft) = p))) /\ (((forall fom_index_pfp_both_original_productright. (exists fom_gap_pfp_both_original_productright_index_bound. fom_gap_pfp_both_original_productright_index_bound + S (fom_index_pfp_both_original_productright) = M) -> exists fom_value_pfp_both_original_productright. ((((exists fom_beta_height_pfp_both_original_productright_entry. fom_beta_height_pfp_both_original_productright_entry + S (fom_value_pfp_both_original_productright) = S ((S (fom_index_pfp_both_original_productright)) * bc)) /\ exists fom_beta_quotient_pfp_both_original_productright_entry. bb = fom_beta_quotient_pfp_both_original_productright_entry * S ((S (fom_index_pfp_both_original_productright)) * bc) + (fom_value_pfp_both_original_productright))) /\ (exists fom_gap_pfp_both_original_productright_value_bound. fom_gap_pfp_both_original_productright_value_bound + S (fom_value_pfp_both_original_productright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_both_original_productcoefficients. (exists pfa_gap_both_original_productcoefficientsbound. pfa_gap_both_original_productcoefficientsbound + S (pfc_index_both_original_productcoefficients) = (N)) -> exists pfc_value_both_original_productcoefficients. ((((exists ff_h_pfp_both_original_productcoefficientsentry. ff_h_pfp_both_original_productcoefficientsentry + S (pfc_value_both_original_productcoefficients) = S ((S (pfc_index_both_original_productcoefficients)) * cc)) /\ exists ff_q_pfp_both_original_productcoefficientsentry. cb = ff_q_pfp_both_original_productcoefficientsentry * S ((S (pfc_index_both_original_productcoefficients)) * cc) + (pfc_value_both_original_productcoefficients))) /\ ((exists pfc_terms_code_both_original_productcoefficientscoefficient pfc_terms_scale_both_original_productcoefficientscoefficient pfc_natural_sum_both_original_productcoefficientscoefficient. ((forall pfc_index_both_original_productcoefficientscoefficientdiagonal. (exists pfa_gap_both_original_productcoefficientscoefficientdiagonalbound. pfa_gap_both_original_productcoefficientscoefficientdiagonalbound + S (pfc_index_both_original_productcoefficientscoefficientdiagonal) = (S (pfc_index_both_original_productcoefficients))) -> exists pfc_value_both_original_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_both_original_productcoefficientscoefficientdiagonalentry. ff_h_pfp_both_original_productcoefficientscoefficientdiagonalentry + S (pfc_value_both_original_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_original_productcoefficientscoefficient)) /\ exists ff_q_pfp_both_original_productcoefficientscoefficientdiagonalentry. pfc_terms_code_both_original_productcoefficientscoefficient = ff_q_pfp_both_original_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_original_productcoefficientscoefficient) + (pfc_value_both_original_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_both_original_productcoefficientscoefficientdiagonalterm pfc_left_both_original_productcoefficientscoefficientdiagonalterm pfc_right_both_original_productcoefficientscoefficientdiagonalterm. (((pfc_index_both_original_productcoefficientscoefficientdiagonal)+pfc_complement_both_original_productcoefficientscoefficientdiagonalterm=(pfc_index_both_original_productcoefficients)) /\ ((((((exists pfa_gap_both_original_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_both_original_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_both_original_productcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_both_original_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_both_original_productcoefficientscoefficientdiagonal)) * ac) + (pfc_left_both_original_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_original_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_both_original_productcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_both_original_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_both_original_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_both_original_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_both_original_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_both_original_productcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_both_original_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_both_original_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_both_original_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_both_original_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_both_original_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_original_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_both_original_productcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_both_original_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_both_original_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_both_original_productcoefficientscoefficientdiagonal)=pfc_left_both_original_productcoefficientscoefficientdiagonalterm*pfc_right_both_original_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_both_original_productcoefficientscoefficientsum fs_v_pfc_both_original_productcoefficientscoefficientsum. ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_start. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_start. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_both_original_productcoefficientscoefficient) = S ((S (S (pfc_index_both_original_productcoefficients))) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_both_original_productcoefficients))) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (pfc_natural_sum_both_original_productcoefficientscoefficient))) /\ forall fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_both_original_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_both_original_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps = S (pfc_index_both_original_productcoefficients)) -> exists fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_original_productcoefficientscoefficient)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_both_original_productcoefficientscoefficient = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_original_productcoefficientscoefficient) + (fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_both_original_productcoefficientscoefficientsum = fs_q_pfc_both_original_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_both_original_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_original_productcoefficientscoefficientsum) + (fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_both_original_productcoefficientscoefficientsum_body_steps = fs_r_pfc_both_original_productcoefficientscoefficientsum_body_steps + fs_a_pfc_both_original_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_both_original_productcoefficientscoefficientresiduebound. pfa_gap_both_original_productcoefficientscoefficientresiduebound + S (pfc_value_both_original_productcoefficients) = (p)) /\ ((exists pfa_offset_left_both_original_productcoefficientscoefficientresiduecongruence pfa_offset_right_both_original_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_both_original_productcoefficientscoefficient) + (p) * pfa_offset_left_both_original_productcoefficientscoefficientresiduecongruence = (pfc_value_both_original_productcoefficients) + (p) * pfa_offset_right_both_original_productcoefficientscoefficientresiduecongruence))))))))))))))))))
  26. 0026exact hc
  27. 0027have hnewcopy : ((forall fom_index_pfp_both_padded_productleft. (exists fom_gap_pfp_both_padded_productleft_index_bound. fom_gap_pfp_both_padded_productleft_index_bound + S (fom_index_pfp_both_padded_productleft) = t+L) -> exists fom_value_pfp_both_padded_productleft. ((((exists fom_beta_height_pfp_both_padded_productleft_entry. fom_beta_height_pfp_both_padded_productleft_entry + S (fom_value_pfp_both_padded_productleft) = S ((S (fom_index_pfp_both_padded_productleft)) * AC)) /\ exists fom_beta_quotient_pfp_both_padded_productleft_entry. AB = fom_beta_quotient_pfp_both_padded_productleft_entry * S ((S (fom_index_pfp_both_padded_productleft)) * AC) + (fom_value_pfp_both_padded_productleft))) /\ (exists fom_gap_pfp_both_padded_productleft_value_bound. fom_gap_pfp_both_padded_productleft_value_bound + S (fom_value_pfp_both_padded_productleft) = p))) /\ (((forall fom_index_pfp_both_padded_productright. (exists fom_gap_pfp_both_padded_productright_index_bound. fom_gap_pfp_both_padded_productright_index_bound + S (fom_index_pfp_both_padded_productright) = s+M) -> exists fom_value_pfp_both_padded_productright. ((((exists fom_beta_height_pfp_both_padded_productright_entry. fom_beta_height_pfp_both_padded_productright_entry + S (fom_value_pfp_both_padded_productright) = S ((S (fom_index_pfp_both_padded_productright)) * BC)) /\ exists fom_beta_quotient_pfp_both_padded_productright_entry. BB = fom_beta_quotient_pfp_both_padded_productright_entry * S ((S (fom_index_pfp_both_padded_productright)) * BC) + (fom_value_pfp_both_padded_productright))) /\ (exists fom_gap_pfp_both_padded_productright_value_bound. fom_gap_pfp_both_padded_productright_value_bound + S (fom_value_pfp_both_padded_productright) = p))) /\ (((((((t+L)=0 \/ (s+M)=0) /\ (((K)=0)))) \/ (((~((t+L)=0)) /\ (((~((s+M)=0)) /\ (((t+L)+(s+M)=S (K)))))))) /\ ((forall pfc_index_both_padded_productcoefficients. (exists pfa_gap_both_padded_productcoefficientsbound. pfa_gap_both_padded_productcoefficientsbound + S (pfc_index_both_padded_productcoefficients) = (K)) -> exists pfc_value_both_padded_productcoefficients. ((((exists ff_h_pfp_both_padded_productcoefficientsentry. ff_h_pfp_both_padded_productcoefficientsentry + S (pfc_value_both_padded_productcoefficients) = S ((S (pfc_index_both_padded_productcoefficients)) * CC)) /\ exists ff_q_pfp_both_padded_productcoefficientsentry. CB = ff_q_pfp_both_padded_productcoefficientsentry * S ((S (pfc_index_both_padded_productcoefficients)) * CC) + (pfc_value_both_padded_productcoefficients))) /\ ((exists pfc_terms_code_both_padded_productcoefficientscoefficient pfc_terms_scale_both_padded_productcoefficientscoefficient pfc_natural_sum_both_padded_productcoefficientscoefficient. ((forall pfc_index_both_padded_productcoefficientscoefficientdiagonal. (exists pfa_gap_both_padded_productcoefficientscoefficientdiagonalbound. pfa_gap_both_padded_productcoefficientscoefficientdiagonalbound + S (pfc_index_both_padded_productcoefficientscoefficientdiagonal) = (S (pfc_index_both_padded_productcoefficients))) -> exists pfc_value_both_padded_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_both_padded_productcoefficientscoefficientdiagonalentry. ff_h_pfp_both_padded_productcoefficientscoefficientdiagonalentry + S (pfc_value_both_padded_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_padded_productcoefficientscoefficient)) /\ exists ff_q_pfp_both_padded_productcoefficientscoefficientdiagonalentry. pfc_terms_code_both_padded_productcoefficientscoefficient = ff_q_pfp_both_padded_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_padded_productcoefficientscoefficient) + (pfc_value_both_padded_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm pfc_left_both_padded_productcoefficientscoefficientdiagonalterm pfc_right_both_padded_productcoefficientscoefficientdiagonalterm. (((pfc_index_both_padded_productcoefficientscoefficientdiagonal)+pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm=(pfc_index_both_padded_productcoefficients)) /\ ((((((exists pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_both_padded_productcoefficientscoefficientdiagonal) = (t+L)) /\ ((((exists ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_both_padded_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_both_padded_productcoefficientscoefficientdiagonal)) * AC) + (pfc_left_both_padded_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermleftoutside+(t+L)=(pfc_index_both_padded_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_both_padded_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_both_padded_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm) = (s+M)) /\ ((((exists ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_both_padded_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_both_padded_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_both_padded_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_both_padded_productcoefficientscoefficientdiagonaltermrightoutside+(s+M)=(pfc_complement_both_padded_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_both_padded_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_both_padded_productcoefficientscoefficientdiagonal)=pfc_left_both_padded_productcoefficientscoefficientdiagonalterm*pfc_right_both_padded_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_both_padded_productcoefficientscoefficientsum fs_v_pfc_both_padded_productcoefficientscoefficientsum. ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_start. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_start. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_both_padded_productcoefficientscoefficient) = S ((S (S (pfc_index_both_padded_productcoefficients))) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_both_padded_productcoefficients))) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (pfc_natural_sum_both_padded_productcoefficientscoefficient))) /\ forall fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_both_padded_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_both_padded_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps = S (pfc_index_both_padded_productcoefficients)) -> exists fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_padded_productcoefficientscoefficient)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_both_padded_productcoefficientscoefficient = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_padded_productcoefficientscoefficient) + (fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_both_padded_productcoefficientscoefficientsum = fs_q_pfc_both_padded_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_both_padded_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_padded_productcoefficientscoefficientsum) + (fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_both_padded_productcoefficientscoefficientsum_body_steps = fs_r_pfc_both_padded_productcoefficientscoefficientsum_body_steps + fs_a_pfc_both_padded_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_both_padded_productcoefficientscoefficientresiduebound. pfa_gap_both_padded_productcoefficientscoefficientresiduebound + S (pfc_value_both_padded_productcoefficients) = (p)) /\ ((exists pfa_offset_left_both_padded_productcoefficientscoefficientresiduecongruence pfa_offset_right_both_padded_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_both_padded_productcoefficientscoefficient) + (p) * pfa_offset_left_both_padded_productcoefficientscoefficientresiduecongruence = (pfc_value_both_padded_productcoefficients) + (p) * pfa_offset_right_both_padded_productcoefficientscoefficientresiduecongruence))))))))))))))))))
  28. 0028exact hn
  29. 0029cases hcopy
  30. 0030cases hcopy_right
  31. 0031cases hcopy_right_right
  32. 0032cases hnewcopy
  33. 0033cases hnewcopy_right
  34. 0034cases hnewcopy_right_right
  35. 0035have hlength : exists J. ((((t+L)=0 \/ (M)=0) /\ (((J)=0)))) \/ (((~((t+L)=0)) /\ (((~((M)=0)) /\ (((t+L)+(M)=S (J)))))))
  36. 0036specialize polynomial_product_length_exists (t+L)
  37. 0037specialize polynomial_product_length_exists (M)
  38. 0038apply polynomial_product_length_exists
  39. 0039cases hlength
  40. 0040have hmiddle : exists db dc. ((forall fom_index_pfp_both_middle_productleft. (exists fom_gap_pfp_both_middle_productleft_index_bound. fom_gap_pfp_both_middle_productleft_index_bound + S (fom_index_pfp_both_middle_productleft) = t+L) -> exists fom_value_pfp_both_middle_productleft. ((((exists fom_beta_height_pfp_both_middle_productleft_entry. fom_beta_height_pfp_both_middle_productleft_entry + S (fom_value_pfp_both_middle_productleft) = S ((S (fom_index_pfp_both_middle_productleft)) * AC)) /\ exists fom_beta_quotient_pfp_both_middle_productleft_entry. AB = fom_beta_quotient_pfp_both_middle_productleft_entry * S ((S (fom_index_pfp_both_middle_productleft)) * AC) + (fom_value_pfp_both_middle_productleft))) /\ (exists fom_gap_pfp_both_middle_productleft_value_bound. fom_gap_pfp_both_middle_productleft_value_bound + S (fom_value_pfp_both_middle_productleft) = p))) /\ (((forall fom_index_pfp_both_middle_productright. (exists fom_gap_pfp_both_middle_productright_index_bound. fom_gap_pfp_both_middle_productright_index_bound + S (fom_index_pfp_both_middle_productright) = M) -> exists fom_value_pfp_both_middle_productright. ((((exists fom_beta_height_pfp_both_middle_productright_entry. fom_beta_height_pfp_both_middle_productright_entry + S (fom_value_pfp_both_middle_productright) = S ((S (fom_index_pfp_both_middle_productright)) * bc)) /\ exists fom_beta_quotient_pfp_both_middle_productright_entry. bb = fom_beta_quotient_pfp_both_middle_productright_entry * S ((S (fom_index_pfp_both_middle_productright)) * bc) + (fom_value_pfp_both_middle_productright))) /\ (exists fom_gap_pfp_both_middle_productright_value_bound. fom_gap_pfp_both_middle_productright_value_bound + S (fom_value_pfp_both_middle_productright) = p))) /\ (((((((t+L)=0 \/ (M)=0) /\ (((x)=0)))) \/ (((~((t+L)=0)) /\ (((~((M)=0)) /\ (((t+L)+(M)=S (x)))))))) /\ ((forall pfc_index_both_middle_productcoefficients. (exists pfa_gap_both_middle_productcoefficientsbound. pfa_gap_both_middle_productcoefficientsbound + S (pfc_index_both_middle_productcoefficients) = (x)) -> exists pfc_value_both_middle_productcoefficients. ((((exists ff_h_pfp_both_middle_productcoefficientsentry. ff_h_pfp_both_middle_productcoefficientsentry + S (pfc_value_both_middle_productcoefficients) = S ((S (pfc_index_both_middle_productcoefficients)) * dc)) /\ exists ff_q_pfp_both_middle_productcoefficientsentry. db = ff_q_pfp_both_middle_productcoefficientsentry * S ((S (pfc_index_both_middle_productcoefficients)) * dc) + (pfc_value_both_middle_productcoefficients))) /\ ((exists pfc_terms_code_both_middle_productcoefficientscoefficient pfc_terms_scale_both_middle_productcoefficientscoefficient pfc_natural_sum_both_middle_productcoefficientscoefficient. ((forall pfc_index_both_middle_productcoefficientscoefficientdiagonal. (exists pfa_gap_both_middle_productcoefficientscoefficientdiagonalbound. pfa_gap_both_middle_productcoefficientscoefficientdiagonalbound + S (pfc_index_both_middle_productcoefficientscoefficientdiagonal) = (S (pfc_index_both_middle_productcoefficients))) -> exists pfc_value_both_middle_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_both_middle_productcoefficientscoefficientdiagonalentry. ff_h_pfp_both_middle_productcoefficientscoefficientdiagonalentry + S (pfc_value_both_middle_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_both_middle_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_middle_productcoefficientscoefficient)) /\ exists ff_q_pfp_both_middle_productcoefficientscoefficientdiagonalentry. pfc_terms_code_both_middle_productcoefficientscoefficient = ff_q_pfp_both_middle_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_both_middle_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_both_middle_productcoefficientscoefficient) + (pfc_value_both_middle_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_both_middle_productcoefficientscoefficientdiagonalterm pfc_left_both_middle_productcoefficientscoefficientdiagonalterm pfc_right_both_middle_productcoefficientscoefficientdiagonalterm. (((pfc_index_both_middle_productcoefficientscoefficientdiagonal)+pfc_complement_both_middle_productcoefficientscoefficientdiagonalterm=(pfc_index_both_middle_productcoefficients)) /\ ((((((exists pfa_gap_both_middle_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_both_middle_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_both_middle_productcoefficientscoefficientdiagonal) = (t+L)) /\ ((((exists ff_h_pfp_both_middle_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_both_middle_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_both_middle_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_both_middle_productcoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_both_middle_productcoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_both_middle_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_both_middle_productcoefficientscoefficientdiagonal)) * AC) + (pfc_left_both_middle_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_middle_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_both_middle_productcoefficientscoefficientdiagonaltermleftoutside+(t+L)=(pfc_index_both_middle_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_both_middle_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_both_middle_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_both_middle_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_both_middle_productcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_both_middle_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_both_middle_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_both_middle_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_both_middle_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_both_middle_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_both_middle_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_both_middle_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_both_middle_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_both_middle_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_both_middle_productcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_both_middle_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_both_middle_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_both_middle_productcoefficientscoefficientdiagonal)=pfc_left_both_middle_productcoefficientscoefficientdiagonalterm*pfc_right_both_middle_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_both_middle_productcoefficientscoefficientsum fs_v_pfc_both_middle_productcoefficientscoefficientsum. ((((exists fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_start. fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_both_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_start. fs_u_pfc_both_middle_productcoefficientscoefficientsum = fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_both_middle_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_both_middle_productcoefficientscoefficient) = S ((S (S (pfc_index_both_middle_productcoefficients))) * fs_v_pfc_both_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_both_middle_productcoefficientscoefficientsum = fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_both_middle_productcoefficients))) * fs_v_pfc_both_middle_productcoefficientscoefficientsum) + (pfc_natural_sum_both_middle_productcoefficientscoefficient))) /\ forall fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_both_middle_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_both_middle_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps = S (pfc_index_both_middle_productcoefficients)) -> exists fs_a_pfc_both_middle_productcoefficientscoefficientsum_body_steps fs_r_pfc_both_middle_productcoefficientscoefficientsum_body_steps fs_s_pfc_both_middle_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_both_middle_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_middle_productcoefficientscoefficient)) /\ exists fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_both_middle_productcoefficientscoefficient = fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_both_middle_productcoefficientscoefficient) + (fs_a_pfc_both_middle_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_both_middle_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_both_middle_productcoefficientscoefficientsum = fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_middle_productcoefficientscoefficientsum) + (fs_r_pfc_both_middle_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_both_middle_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_both_middle_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_both_middle_productcoefficientscoefficientsum = fs_q_pfc_both_middle_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_both_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_both_middle_productcoefficientscoefficientsum) + (fs_s_pfc_both_middle_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_both_middle_productcoefficientscoefficientsum_body_steps = fs_r_pfc_both_middle_productcoefficientscoefficientsum_body_steps + fs_a_pfc_both_middle_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_both_middle_productcoefficientscoefficientresiduebound. pfa_gap_both_middle_productcoefficientscoefficientresiduebound + S (pfc_value_both_middle_productcoefficients) = (p)) /\ ((exists pfa_offset_left_both_middle_productcoefficientscoefficientresiduecongruence pfa_offset_right_both_middle_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_both_middle_productcoefficientscoefficient) + (p) * pfa_offset_left_both_middle_productcoefficientscoefficientresiduecongruence = (pfc_value_both_middle_productcoefficients) + (p) * pfa_offset_right_both_middle_productcoefficientscoefficientresiduecongruence))))))))))))))))))
  41. 0041specialize prime_field_polynomial_convolution_at_length_exists (p)
  42. 0042specialize prime_field_polynomial_convolution_at_length_exists (AB)
  43. 0043specialize prime_field_polynomial_convolution_at_length_exists (AC)
  44. 0044specialize prime_field_polynomial_convolution_at_length_exists (t+L)
  45. 0045specialize prime_field_polynomial_convolution_at_length_exists (bb)
  46. 0046specialize prime_field_polynomial_convolution_at_length_exists (bc)
  47. 0047specialize prime_field_polynomial_convolution_at_length_exists (M)
  48. 0048specialize prime_field_polynomial_convolution_at_length_exists (x)
  49. 0049apply prime_field_polynomial_convolution_at_length_exists
  50. 0050exact hp
  51. 0051exact hnewcopy_left
  52. 0052exact hcopy_right_left
  53. 0053exact hlength_witness
  54. 0054cases hmiddle
  55. 0055cases hmiddle_witness
  56. 0056specialize prime_field_polynomial_equivalent_transitive (cb)
  57. 0057specialize prime_field_polynomial_equivalent_transitive (cc)
  58. 0058specialize prime_field_polynomial_equivalent_transitive (N)
  59. 0059specialize prime_field_polynomial_equivalent_transitive (x1)
  60. 0060specialize prime_field_polynomial_equivalent_transitive (x2)
  61. 0061specialize prime_field_polynomial_equivalent_transitive (x)
  62. 0062specialize prime_field_polynomial_equivalent_transitive (CB)
  63. 0063specialize prime_field_polynomial_equivalent_transitive (CC)
  64. 0064specialize prime_field_polynomial_equivalent_transitive (K)
  65. 0065apply prime_field_polynomial_equivalent_transitive
  66. 0066specialize prime_field_polynomial_convolution_left_padding_equivalent_left (p)
  67. 0067specialize prime_field_polynomial_convolution_left_padding_equivalent_left (ab)
  68. 0068specialize prime_field_polynomial_convolution_left_padding_equivalent_left (ac)
  69. 0069specialize prime_field_polynomial_convolution_left_padding_equivalent_left (L)
  70. 0070specialize prime_field_polynomial_convolution_left_padding_equivalent_left (bb)
  71. 0071specialize prime_field_polynomial_convolution_left_padding_equivalent_left (bc)
  72. 0072specialize prime_field_polynomial_convolution_left_padding_equivalent_left (M)
  73. 0073specialize prime_field_polynomial_convolution_left_padding_equivalent_left (cb)
  74. 0074specialize prime_field_polynomial_convolution_left_padding_equivalent_left (cc)
  75. 0075specialize prime_field_polynomial_convolution_left_padding_equivalent_left (N)
  76. 0076specialize prime_field_polynomial_convolution_left_padding_equivalent_left (AB)
  77. 0077specialize prime_field_polynomial_convolution_left_padding_equivalent_left (AC)
  78. 0078specialize prime_field_polynomial_convolution_left_padding_equivalent_left (t)
  79. 0079specialize prime_field_polynomial_convolution_left_padding_equivalent_left (x1)
  80. 0080specialize prime_field_polynomial_convolution_left_padding_equivalent_left (x2)
  81. 0081specialize prime_field_polynomial_convolution_left_padding_equivalent_left (x)
  82. 0082apply prime_field_polynomial_convolution_left_padding_equivalent_left
  83. 0083exact hp
  84. 0084exact hA
  85. 0085exact hc
  86. 0086exact hmiddle_witness_witness
  87. 0087specialize prime_field_polynomial_convolution_left_padding_equivalent_right (p)
  88. 0088specialize prime_field_polynomial_convolution_left_padding_equivalent_right (AB)
  89. 0089specialize prime_field_polynomial_convolution_left_padding_equivalent_right (AC)
  90. 0090specialize prime_field_polynomial_convolution_left_padding_equivalent_right (t+L)
  91. 0091specialize prime_field_polynomial_convolution_left_padding_equivalent_right (bb)
  92. 0092specialize prime_field_polynomial_convolution_left_padding_equivalent_right (bc)
  93. 0093specialize prime_field_polynomial_convolution_left_padding_equivalent_right (M)
  94. 0094specialize prime_field_polynomial_convolution_left_padding_equivalent_right (x1)
  95. 0095specialize prime_field_polynomial_convolution_left_padding_equivalent_right (x2)
  96. 0096specialize prime_field_polynomial_convolution_left_padding_equivalent_right (x)
  97. 0097specialize prime_field_polynomial_convolution_left_padding_equivalent_right (BB)
  98. 0098specialize prime_field_polynomial_convolution_left_padding_equivalent_right (BC)
  99. 0099specialize prime_field_polynomial_convolution_left_padding_equivalent_right (s)
  100. 0100specialize prime_field_polynomial_convolution_left_padding_equivalent_right (CB)
  101. 0101specialize prime_field_polynomial_convolution_left_padding_equivalent_right (CC)
  102. 0102specialize prime_field_polynomial_convolution_left_padding_equivalent_right (K)
  103. 0103apply prime_field_polynomial_convolution_left_padding_equivalent_right
  104. 0104exact hp
  105. 0105exact hB
  106. 0106exact hmiddle_witness_witness
  107. 0107exact hn