PX006D

prime_field_polynomial_convolution_left_padding_nonempty_right

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

Two actual nonempty-factor products are related by exact leading-zero output padding and its proved length equation; no raw beta-code equality is asserted.

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 t CB CC K. (~(p=0)) -> (~(L=0)) -> (~(M=0)) -> (((forall pfp_repeat_index_nonempty_factor_padding_rightzeros. (exists pfa_gap_nonempty_factor_padding_rightzerosindex. pfa_gap_nonempty_factor_padding_rightzerosindex + S (pfp_repeat_index_nonempty_factor_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_nonempty_factor_padding_rightzerosentry. ff_h_pfp_nonempty_factor_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_nonempty_factor_padding_rightzeros)) * BC)) /\ exists ff_q_pfp_nonempty_factor_padding_rightzerosentry. BB = ff_q_pfp_nonempty_factor_padding_rightzerosentry * S ((S (pfp_repeat_index_nonempty_factor_padding_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_nonempty_factor_padding_right pfrep_value_nonempty_factor_padding_right. (exists pfa_gap_nonempty_factor_padding_rightbound. pfa_gap_nonempty_factor_padding_rightbound + S (pfrep_index_nonempty_factor_padding_right) = (M)) -> (((exists ff_h_pfp_nonempty_factor_padding_rightinput. ff_h_pfp_nonempty_factor_padding_rightinput + S (pfrep_value_nonempty_factor_padding_right) = S ((S (pfrep_index_nonempty_factor_padding_right)) * bc)) /\ exists ff_q_pfp_nonempty_factor_padding_rightinput. bb = ff_q_pfp_nonempty_factor_padding_rightinput * S ((S (pfrep_index_nonempty_factor_padding_right)) * bc) + (pfrep_value_nonempty_factor_padding_right))) -> (((exists ff_h_pfp_nonempty_factor_padding_rightoutput. ff_h_pfp_nonempty_factor_padding_rightoutput + S (pfrep_value_nonempty_factor_padding_right) = S ((S ((t)+pfrep_index_nonempty_factor_padding_right)) * BC)) /\ exists ff_q_pfp_nonempty_factor_padding_rightoutput. BB = ff_q_pfp_nonempty_factor_padding_rightoutput * S ((S ((t)+pfrep_index_nonempty_factor_padding_right)) * BC) + (pfrep_value_nonempty_factor_padding_right))))))) -> (((forall fom_index_pfp_nonempty_old_rightleft. (exists fom_gap_pfp_nonempty_old_rightleft_index_bound. fom_gap_pfp_nonempty_old_rightleft_index_bound + S (fom_index_pfp_nonempty_old_rightleft) = L) -> exists fom_value_pfp_nonempty_old_rightleft. ((((exists fom_beta_height_pfp_nonempty_old_rightleft_entry. fom_beta_height_pfp_nonempty_old_rightleft_entry + S (fom_value_pfp_nonempty_old_rightleft) = S ((S (fom_index_pfp_nonempty_old_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_nonempty_old_rightleft_entry. ab = fom_beta_quotient_pfp_nonempty_old_rightleft_entry * S ((S (fom_index_pfp_nonempty_old_rightleft)) * ac) + (fom_value_pfp_nonempty_old_rightleft))) /\ (exists fom_gap_pfp_nonempty_old_rightleft_value_bound. fom_gap_pfp_nonempty_old_rightleft_value_bound + S (fom_value_pfp_nonempty_old_rightleft) = p))) /\ (((forall fom_index_pfp_nonempty_old_rightright. (exists fom_gap_pfp_nonempty_old_rightright_index_bound. fom_gap_pfp_nonempty_old_rightright_index_bound + S (fom_index_pfp_nonempty_old_rightright) = M) -> exists fom_value_pfp_nonempty_old_rightright. ((((exists fom_beta_height_pfp_nonempty_old_rightright_entry. fom_beta_height_pfp_nonempty_old_rightright_entry + S (fom_value_pfp_nonempty_old_rightright) = S ((S (fom_index_pfp_nonempty_old_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_nonempty_old_rightright_entry. bb = fom_beta_quotient_pfp_nonempty_old_rightright_entry * S ((S (fom_index_pfp_nonempty_old_rightright)) * bc) + (fom_value_pfp_nonempty_old_rightright))) /\ (exists fom_gap_pfp_nonempty_old_rightright_value_bound. fom_gap_pfp_nonempty_old_rightright_value_bound + S (fom_value_pfp_nonempty_old_rightright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_nonempty_old_rightcoefficients. (exists pfa_gap_nonempty_old_rightcoefficientsbound. pfa_gap_nonempty_old_rightcoefficientsbound + S (pfc_index_nonempty_old_rightcoefficients) = (N)) -> exists pfc_value_nonempty_old_rightcoefficients. ((((exists ff_h_pfp_nonempty_old_rightcoefficientsentry. ff_h_pfp_nonempty_old_rightcoefficientsentry + S (pfc_value_nonempty_old_rightcoefficients) = S ((S (pfc_index_nonempty_old_rightcoefficients)) * cc)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientsentry. cb = ff_q_pfp_nonempty_old_rightcoefficientsentry * S ((S (pfc_index_nonempty_old_rightcoefficients)) * cc) + (pfc_value_nonempty_old_rightcoefficients))) /\ ((exists pfc_terms_code_nonempty_old_rightcoefficientscoefficient pfc_terms_scale_nonempty_old_rightcoefficientscoefficient pfc_natural_sum_nonempty_old_rightcoefficientscoefficient. ((forall pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_old_rightcoefficients))) -> exists pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_old_rightcoefficientscoefficient = ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient) + (pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)+pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_old_rightcoefficients)) /\ ((((((exists pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_nonempty_old_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_nonempty_old_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_old_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_nonempty_old_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_old_rightcoefficientscoefficientdiagonal)=pfc_left_nonempty_old_rightcoefficientscoefficientdiagonalterm*pfc_right_nonempty_old_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_old_rightcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_old_rightcoefficients))) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_old_rightcoefficients))) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_old_rightcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_old_rightcoefficients)) -> exists fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_old_rightcoefficientscoefficient = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_old_rightcoefficientscoefficient) + (fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_old_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_old_rightcoefficientscoefficientsum) + (fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_old_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_old_rightcoefficientscoefficientresiduebound. pfa_gap_nonempty_old_rightcoefficientscoefficientresiduebound + S (pfc_value_nonempty_old_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_old_rightcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_old_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_old_rightcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_old_rightcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_old_rightcoefficients) + (p) * pfa_offset_right_nonempty_old_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_nonempty_new_rightleft. (exists fom_gap_pfp_nonempty_new_rightleft_index_bound. fom_gap_pfp_nonempty_new_rightleft_index_bound + S (fom_index_pfp_nonempty_new_rightleft) = L) -> exists fom_value_pfp_nonempty_new_rightleft. ((((exists fom_beta_height_pfp_nonempty_new_rightleft_entry. fom_beta_height_pfp_nonempty_new_rightleft_entry + S (fom_value_pfp_nonempty_new_rightleft) = S ((S (fom_index_pfp_nonempty_new_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_nonempty_new_rightleft_entry. ab = fom_beta_quotient_pfp_nonempty_new_rightleft_entry * S ((S (fom_index_pfp_nonempty_new_rightleft)) * ac) + (fom_value_pfp_nonempty_new_rightleft))) /\ (exists fom_gap_pfp_nonempty_new_rightleft_value_bound. fom_gap_pfp_nonempty_new_rightleft_value_bound + S (fom_value_pfp_nonempty_new_rightleft) = p))) /\ (((forall fom_index_pfp_nonempty_new_rightright. (exists fom_gap_pfp_nonempty_new_rightright_index_bound. fom_gap_pfp_nonempty_new_rightright_index_bound + S (fom_index_pfp_nonempty_new_rightright) = t+M) -> exists fom_value_pfp_nonempty_new_rightright. ((((exists fom_beta_height_pfp_nonempty_new_rightright_entry. fom_beta_height_pfp_nonempty_new_rightright_entry + S (fom_value_pfp_nonempty_new_rightright) = S ((S (fom_index_pfp_nonempty_new_rightright)) * BC)) /\ exists fom_beta_quotient_pfp_nonempty_new_rightright_entry. BB = fom_beta_quotient_pfp_nonempty_new_rightright_entry * S ((S (fom_index_pfp_nonempty_new_rightright)) * BC) + (fom_value_pfp_nonempty_new_rightright))) /\ (exists fom_gap_pfp_nonempty_new_rightright_value_bound. fom_gap_pfp_nonempty_new_rightright_value_bound + S (fom_value_pfp_nonempty_new_rightright) = p))) /\ (((((((L)=0 \/ (t+M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((t+M)=0)) /\ (((L)+(t+M)=S (K)))))))) /\ ((forall pfc_index_nonempty_new_rightcoefficients. (exists pfa_gap_nonempty_new_rightcoefficientsbound. pfa_gap_nonempty_new_rightcoefficientsbound + S (pfc_index_nonempty_new_rightcoefficients) = (K)) -> exists pfc_value_nonempty_new_rightcoefficients. ((((exists ff_h_pfp_nonempty_new_rightcoefficientsentry. ff_h_pfp_nonempty_new_rightcoefficientsentry + S (pfc_value_nonempty_new_rightcoefficients) = S ((S (pfc_index_nonempty_new_rightcoefficients)) * CC)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientsentry. CB = ff_q_pfp_nonempty_new_rightcoefficientsentry * S ((S (pfc_index_nonempty_new_rightcoefficients)) * CC) + (pfc_value_nonempty_new_rightcoefficients))) /\ ((exists pfc_terms_code_nonempty_new_rightcoefficientscoefficient pfc_terms_scale_nonempty_new_rightcoefficientscoefficient pfc_natural_sum_nonempty_new_rightcoefficientscoefficient. ((forall pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_new_rightcoefficients))) -> exists pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_new_rightcoefficientscoefficient = ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient) + (pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)+pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_new_rightcoefficients)) /\ ((((((exists pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_nonempty_new_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_nonempty_new_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_new_rightcoefficientscoefficientdiagonaltermrightoutside+(t+M)=(pfc_complement_nonempty_new_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_new_rightcoefficientscoefficientdiagonal)=pfc_left_nonempty_new_rightcoefficientscoefficientdiagonalterm*pfc_right_nonempty_new_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_new_rightcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_new_rightcoefficients))) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_new_rightcoefficients))) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_new_rightcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_new_rightcoefficients)) -> exists fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_new_rightcoefficientscoefficient = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_new_rightcoefficientscoefficient) + (fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_new_rightcoefficientscoefficientsum = fs_q_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_new_rightcoefficientscoefficientsum) + (fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_new_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_new_rightcoefficientscoefficientresiduebound. pfa_gap_nonempty_new_rightcoefficientscoefficientresiduebound + S (pfc_value_nonempty_new_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_new_rightcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_new_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_new_rightcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_new_rightcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_new_rightcoefficients) + (p) * pfa_offset_right_nonempty_new_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((K=t+N) /\ ((((forall pfp_repeat_index_nonempty_product_padding_rightzeros. (exists pfa_gap_nonempty_product_padding_rightzerosindex. pfa_gap_nonempty_product_padding_rightzerosindex + S (pfp_repeat_index_nonempty_product_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_nonempty_product_padding_rightzerosentry. ff_h_pfp_nonempty_product_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_nonempty_product_padding_rightzeros)) * CC)) /\ exists ff_q_pfp_nonempty_product_padding_rightzerosentry. CB = ff_q_pfp_nonempty_product_padding_rightzerosentry * S ((S (pfp_repeat_index_nonempty_product_padding_rightzeros)) * CC) + (0)))) /\ ((forall pfrep_index_nonempty_product_padding_right pfrep_value_nonempty_product_padding_right. (exists pfa_gap_nonempty_product_padding_rightbound. pfa_gap_nonempty_product_padding_rightbound + S (pfrep_index_nonempty_product_padding_right) = (N)) -> (((exists ff_h_pfp_nonempty_product_padding_rightinput. ff_h_pfp_nonempty_product_padding_rightinput + S (pfrep_value_nonempty_product_padding_right) = S ((S (pfrep_index_nonempty_product_padding_right)) * cc)) /\ exists ff_q_pfp_nonempty_product_padding_rightinput. cb = ff_q_pfp_nonempty_product_padding_rightinput * S ((S (pfrep_index_nonempty_product_padding_right)) * cc) + (pfrep_value_nonempty_product_padding_right))) -> (((exists ff_h_pfp_nonempty_product_padding_rightoutput. ff_h_pfp_nonempty_product_padding_rightoutput + S (pfrep_value_nonempty_product_padding_right) = S ((S ((t)+pfrep_index_nonempty_product_padding_right)) * CC)) /\ exists ff_q_pfp_nonempty_product_padding_rightoutput. CB = ff_q_pfp_nonempty_product_padding_rightoutput * S ((S ((t)+pfrep_index_nonempty_product_padding_right)) * CC) + (pfrep_value_nonempty_product_padding_right))))))))))

Constructive proof overview

Generated structural guide

Two actual nonempty-factor products are related by exact leading-zero output padding and its proved length equation; no raw beta-code equality is asserted.

The unchanged tactic script uses 8 declared prerequisites and contains 142 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PX006B polynomial_product_length_left_padding_right le_trans Alpha theorem; checked-use authorized le_add_right Alpha theorem; checked-use authorized PX0069 prime_field_convolution_coefficient_before_left_padding_right prime_field_convolution_prefix_entry Alpha theorem; checked-use authorized matrix_recursive_lt_add_left Alpha theorem; checked-use authorized prime_field_convolution_coefficient_functional Alpha theorem; checked-use authorized PX0067 prime_field_convolution_coefficient_left_padding_right

Direct dependents

PX006F prime_field_polynomial_convolution_left_padding_equivalent_right

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

142 script commands · 27 reading checkpoints · 6 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)
polynomial product length left padding rightprime field convolution coefficient before left padding rightprime field convolution coefficient left padding 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 BB
  2. L12
    intro BC
  3. L13
    intro t
  4. L14
    intro CB
  5. L15
    intro CC
  6. L16
    intro K
  7. L17
    intro hp
  8. L18
    intro hL
  9. L19
    intro hM
  10. L20
    intro hpad
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hc
  2. L22
    intro hn
04Separate the logical casesL23–28

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

  1. L23
    cases hc
  2. L24
    cases hc_right
  3. L25
    cases hc_right_right
  4. L26
    cases hn
  5. L27
    cases hn_right
  6. L28
    cases hn_right_right
05Establish hlengthL29–38

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

  1. L29
    have hlength : K=t+N
  2. L30
    specialize polynomial_product_length_left_padding_right (L)
  3. L31
    specialize polynomial_product_length_left_padding_right (M)
  4. L32
    specialize polynomial_product_length_left_padding_right (N)
  5. L33
    specialize polynomial_product_length_left_padding_right (t)
  6. L34
    specialize polynomial_product_length_left_padding_right (K)
  7. L35
    apply polynomial_product_length_left_padding_right
  8. L36
    exact hc_right_right_left
  9. L37
    exact hL
  10. L38
    exact hM
06Use earlier factsL39–39

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

  1. L39
    exact hn_right_right_left
07Separate the logical casesL40–40

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

  1. L40
    split
08Use earlier factsL41–41

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

  1. L41
    exact hlength
09Separate the logical casesL42–42

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

  1. L42
    split
10Fix variables and assumptionsL43–44

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

  1. L43
    intro i
  2. L44
    intro hi
11Establish hvL45–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hn right right right.

  1. L45
    have hv : ∃ r. BetaAt(CB,CC,i,r) ∧ FpConvolutionCoefficient(p,ab,ac,L,BB,BC,t + M,i,r)Definitions: FpConvolutionCoefficientBetaAt
  2. L46
    specialize hn_right_right_right (i)
  3. L47
    apply hn_right_right_right
  4. L48
    specialize le_trans (S i)
  5. L49
    specialize le_trans (t)
  6. L50
    specialize le_trans (K)
  7. L51
    apply le_trans
  8. L52
    exact hi
  9. L53
    rewrite hlength
  10. L54
    specialize le_add_right (t)
12Use earlier factsL55–56

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

  1. L55
    specialize le_add_right (N)
  2. L56
    apply le_add_right
13Separate the logical casesL57–58

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

  1. L57
    cases hv
  2. L58
    cases hv_witness
14Establish hzeroL59–68

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

  1. L59
    have hzero : x=0
  2. L60
    specialize prime_field_convolution_coefficient_before_left_padding_right (p)
  3. L61
    specialize prime_field_convolution_coefficient_before_left_padding_right (ab)
  4. L62
    specialize prime_field_convolution_coefficient_before_left_padding_right (ac)
  5. L63
    specialize prime_field_convolution_coefficient_before_left_padding_right (L)
  6. L64
    specialize prime_field_convolution_coefficient_before_left_padding_right (bb)
  7. L65
    specialize prime_field_convolution_coefficient_before_left_padding_right (bc)
  8. L66
    specialize prime_field_convolution_coefficient_before_left_padding_right (M)
  9. L67
    specialize prime_field_convolution_coefficient_before_left_padding_right (BB)
  10. L68
    specialize prime_field_convolution_coefficient_before_left_padding_right (BC)
15Use earlier factsL69–76

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

  1. L69
    specialize prime_field_convolution_coefficient_before_left_padding_right (t)
  2. L70
    specialize prime_field_convolution_coefficient_before_left_padding_right (i)
  3. L71
    specialize prime_field_convolution_coefficient_before_left_padding_right (x)
  4. L72
    apply prime_field_convolution_coefficient_before_left_padding_right
  5. L73
    exact hp
  6. L74
    exact hpad
  7. L75
    exact hi
  8. L76
    exact hv_witness_right
16Calculate and transport equalitiesL77–78

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L77
    rewrite hzero at hv_witness_left
  2. L78
    rewrite hzero at hv_witness_left
17Use earlier factsL79–79

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

  1. L79
    exact hv_witness_left
18Fix variables and assumptionsL80–83

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

  1. L80
    intro i
  2. L81
    intro a
  3. L82
    intro hi
  4. L83
    intro ha
19Establish hcoefficientL84–93

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

  1. L84
    have hcoefficient : FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,a)Definitions: FpConvolutionCoefficient
  2. L85
    specialize prime_field_convolution_prefix_entry (p)
  3. L86
    specialize prime_field_convolution_prefix_entry (ab)
  4. L87
    specialize prime_field_convolution_prefix_entry (ac)
  5. L88
    specialize prime_field_convolution_prefix_entry (L)
  6. L89
    specialize prime_field_convolution_prefix_entry (bb)
  7. L90
    specialize prime_field_convolution_prefix_entry (bc)
  8. L91
    specialize prime_field_convolution_prefix_entry (M)
  9. L92
    specialize prime_field_convolution_prefix_entry (cb)
  10. L93
    specialize prime_field_convolution_prefix_entry (cc)
20Use earlier factsL94–100

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

  1. L94
    specialize prime_field_convolution_prefix_entry (N)
  2. L95
    specialize prime_field_convolution_prefix_entry (i)
  3. L96
    specialize prime_field_convolution_prefix_entry (a)
  4. L97
    apply prime_field_convolution_prefix_entry
  5. L98
    exact hc_right_right_right
  6. L99
    exact hi
  7. L100
    exact ha
21Establish hvL101–109

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hn right right right.

  1. L101
    have hv : ∃ r. BetaAt(CB,CC,t + i,r) ∧ FpConvolutionCoefficient(p,ab,ac,L,BB,BC,t + M,t + i,r)Definitions: FpConvolutionCoefficientBetaAt
  2. L102
    specialize hn_right_right_right (t+i)
  3. L103
    apply hn_right_right_right
  4. L104
    rewrite hlength
  5. L105
    specialize matrix_recursive_lt_add_left (i)
  6. L106
    specialize matrix_recursive_lt_add_left (N)
  7. L107
    specialize matrix_recursive_lt_add_left (t)
  8. L108
    apply matrix_recursive_lt_add_left
  9. L109
    exact hi
22Separate the logical casesL110–111

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

  1. L110
    cases hv
  2. L111
    cases hv_witness
23Establish heqL112–121

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

  1. L112
    have heq : x=a
  2. L113
    specialize prime_field_convolution_coefficient_functional (p)
  3. L114
    specialize prime_field_convolution_coefficient_functional (ab)
  4. L115
    specialize prime_field_convolution_coefficient_functional (ac)
  5. L116
    specialize prime_field_convolution_coefficient_functional (L)
  6. L117
    specialize prime_field_convolution_coefficient_functional (BB)
  7. L118
    specialize prime_field_convolution_coefficient_functional (BC)
  8. L119
    specialize prime_field_convolution_coefficient_functional (t+M)
  9. L120
    specialize prime_field_convolution_coefficient_functional (t+i)
  10. L121
    specialize prime_field_convolution_coefficient_functional (x)
24Use earlier factsL122–131

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

  1. L122
    specialize prime_field_convolution_coefficient_functional (a)
  2. L123
    apply prime_field_convolution_coefficient_functional
  3. L124
    exact hv_witness_right
  4. L125
    specialize prime_field_convolution_coefficient_left_padding_right (p)
  5. L126
    specialize prime_field_convolution_coefficient_left_padding_right (ab)
  6. L127
    specialize prime_field_convolution_coefficient_left_padding_right (ac)
  7. L128
    specialize prime_field_convolution_coefficient_left_padding_right (L)
  8. L129
    specialize prime_field_convolution_coefficient_left_padding_right (bb)
  9. L130
    specialize prime_field_convolution_coefficient_left_padding_right (bc)
  10. L131
    specialize prime_field_convolution_coefficient_left_padding_right (M)
25Use earlier factsL132–139

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

  1. L132
    specialize prime_field_convolution_coefficient_left_padding_right (BB)
  2. L133
    specialize prime_field_convolution_coefficient_left_padding_right (BC)
  3. L134
    specialize prime_field_convolution_coefficient_left_padding_right (t)
  4. L135
    specialize prime_field_convolution_coefficient_left_padding_right (i)
  5. L136
    specialize prime_field_convolution_coefficient_left_padding_right (a)
  6. L137
    apply prime_field_convolution_coefficient_left_padding_right
  7. L138
    exact hpad
  8. L139
    exact hcoefficient
26Calculate and transport equalitiesL140–141

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L140
    rewrite heq at hv_witness_left
  2. L141
    rewrite heq at hv_witness_left
27Use earlier factsL142–142

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

  1. L142
    exact hv_witness_left

Library-wide reading audit

Original exact command ledger · 142 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 BB
  12. 0012intro BC
  13. 0013intro t
  14. 0014intro CB
  15. 0015intro CC
  16. 0016intro K
  17. 0017intro hp
  18. 0018intro hL
  19. 0019intro hM
  20. 0020intro hpad
  21. 0021intro hc
  22. 0022intro hn
  23. 0023cases hc
  24. 0024cases hc_right
  25. 0025cases hc_right_right
  26. 0026cases hn
  27. 0027cases hn_right
  28. 0028cases hn_right_right
  29. 0029have hlength : K=t+N
  30. 0030specialize polynomial_product_length_left_padding_right (L)
  31. 0031specialize polynomial_product_length_left_padding_right (M)
  32. 0032specialize polynomial_product_length_left_padding_right (N)
  33. 0033specialize polynomial_product_length_left_padding_right (t)
  34. 0034specialize polynomial_product_length_left_padding_right (K)
  35. 0035apply polynomial_product_length_left_padding_right
  36. 0036exact hc_right_right_left
  37. 0037exact hL
  38. 0038exact hM
  39. 0039exact hn_right_right_left
  40. 0040split
  41. 0041exact hlength
  42. 0042split
  43. 0043intro i
  44. 0044intro hi
  45. 0045have hv : exists r. ((((exists ff_h_pfp_nonempty_zero_entry_right. ff_h_pfp_nonempty_zero_entry_right + S (r) = S ((S (i)) * CC)) /\ exists ff_q_pfp_nonempty_zero_entry_right. CB = ff_q_pfp_nonempty_zero_entry_right * S ((S (i)) * CC) + (r))) /\ ((exists pfc_terms_code_nonempty_zero_coefficient_right pfc_terms_scale_nonempty_zero_coefficient_right pfc_natural_sum_nonempty_zero_coefficient_right. ((forall pfc_index_nonempty_zero_coefficient_rightdiagonal. (exists pfa_gap_nonempty_zero_coefficient_rightdiagonalbound. pfa_gap_nonempty_zero_coefficient_rightdiagonalbound + S (pfc_index_nonempty_zero_coefficient_rightdiagonal) = (S (i))) -> exists pfc_value_nonempty_zero_coefficient_rightdiagonal. ((((exists ff_h_pfp_nonempty_zero_coefficient_rightdiagonalentry. ff_h_pfp_nonempty_zero_coefficient_rightdiagonalentry + S (pfc_value_nonempty_zero_coefficient_rightdiagonal) = S ((S (pfc_index_nonempty_zero_coefficient_rightdiagonal)) * pfc_terms_scale_nonempty_zero_coefficient_right)) /\ exists ff_q_pfp_nonempty_zero_coefficient_rightdiagonalentry. pfc_terms_code_nonempty_zero_coefficient_right = ff_q_pfp_nonempty_zero_coefficient_rightdiagonalentry * S ((S (pfc_index_nonempty_zero_coefficient_rightdiagonal)) * pfc_terms_scale_nonempty_zero_coefficient_right) + (pfc_value_nonempty_zero_coefficient_rightdiagonal))) /\ ((exists pfc_complement_nonempty_zero_coefficient_rightdiagonalterm pfc_left_nonempty_zero_coefficient_rightdiagonalterm pfc_right_nonempty_zero_coefficient_rightdiagonalterm. (((pfc_index_nonempty_zero_coefficient_rightdiagonal)+pfc_complement_nonempty_zero_coefficient_rightdiagonalterm=(i)) /\ ((((((exists pfa_gap_nonempty_zero_coefficient_rightdiagonaltermleftinside. pfa_gap_nonempty_zero_coefficient_rightdiagonaltermleftinside + S (pfc_index_nonempty_zero_coefficient_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_zero_coefficient_rightdiagonaltermleftentry. ff_h_pfp_nonempty_zero_coefficient_rightdiagonaltermleftentry + S (pfc_left_nonempty_zero_coefficient_rightdiagonalterm) = S ((S (pfc_index_nonempty_zero_coefficient_rightdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_zero_coefficient_rightdiagonaltermleftentry. ab = ff_q_pfp_nonempty_zero_coefficient_rightdiagonaltermleftentry * S ((S (pfc_index_nonempty_zero_coefficient_rightdiagonal)) * ac) + (pfc_left_nonempty_zero_coefficient_rightdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_zero_coefficient_rightdiagonaltermleftoutside. pfc_gap_nonempty_zero_coefficient_rightdiagonaltermleftoutside+(L)=(pfc_index_nonempty_zero_coefficient_rightdiagonal)) /\ (((pfc_left_nonempty_zero_coefficient_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_zero_coefficient_rightdiagonaltermrightinside. pfa_gap_nonempty_zero_coefficient_rightdiagonaltermrightinside + S (pfc_complement_nonempty_zero_coefficient_rightdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_nonempty_zero_coefficient_rightdiagonaltermrightentry. ff_h_pfp_nonempty_zero_coefficient_rightdiagonaltermrightentry + S (pfc_right_nonempty_zero_coefficient_rightdiagonalterm) = S ((S (pfc_complement_nonempty_zero_coefficient_rightdiagonalterm)) * BC)) /\ exists ff_q_pfp_nonempty_zero_coefficient_rightdiagonaltermrightentry. BB = ff_q_pfp_nonempty_zero_coefficient_rightdiagonaltermrightentry * S ((S (pfc_complement_nonempty_zero_coefficient_rightdiagonalterm)) * BC) + (pfc_right_nonempty_zero_coefficient_rightdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_zero_coefficient_rightdiagonaltermrightoutside. pfc_gap_nonempty_zero_coefficient_rightdiagonaltermrightoutside+(t+M)=(pfc_complement_nonempty_zero_coefficient_rightdiagonalterm)) /\ (((pfc_right_nonempty_zero_coefficient_rightdiagonalterm)=0))))) /\ (((pfc_value_nonempty_zero_coefficient_rightdiagonal)=pfc_left_nonempty_zero_coefficient_rightdiagonalterm*pfc_right_nonempty_zero_coefficient_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_zero_coefficient_rightsum fs_v_pfc_nonempty_zero_coefficient_rightsum. ((((exists fs_h_pfc_nonempty_zero_coefficient_rightsum_body_start. fs_h_pfc_nonempty_zero_coefficient_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_zero_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_zero_coefficient_rightsum_body_start. fs_u_pfc_nonempty_zero_coefficient_rightsum = fs_q_pfc_nonempty_zero_coefficient_rightsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_zero_coefficient_rightsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_zero_coefficient_rightsum_body_terminal. fs_h_pfc_nonempty_zero_coefficient_rightsum_body_terminal + S (pfc_natural_sum_nonempty_zero_coefficient_right) = S ((S (S (i))) * fs_v_pfc_nonempty_zero_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_zero_coefficient_rightsum_body_terminal. fs_u_pfc_nonempty_zero_coefficient_rightsum = fs_q_pfc_nonempty_zero_coefficient_rightsum_body_terminal * S ((S (S (i))) * fs_v_pfc_nonempty_zero_coefficient_rightsum) + (pfc_natural_sum_nonempty_zero_coefficient_right))) /\ forall fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps. (exists fs_lt_pfc_nonempty_zero_coefficient_rightsum_body_steps_bound. fs_lt_pfc_nonempty_zero_coefficient_rightsum_body_steps_bound + S fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps = S (i)) -> exists fs_a_pfc_nonempty_zero_coefficient_rightsum_body_steps fs_r_pfc_nonempty_zero_coefficient_rightsum_body_steps fs_s_pfc_nonempty_zero_coefficient_rightsum_body_steps. ((((exists fs_h_pfc_nonempty_zero_coefficient_rightsum_body_steps_summand. fs_h_pfc_nonempty_zero_coefficient_rightsum_body_steps_summand + S (fs_a_pfc_nonempty_zero_coefficient_rightsum_body_steps) = S ((S (fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps)) * pfc_terms_scale_nonempty_zero_coefficient_right)) /\ exists fs_q_pfc_nonempty_zero_coefficient_rightsum_body_steps_summand. pfc_terms_code_nonempty_zero_coefficient_right = fs_q_pfc_nonempty_zero_coefficient_rightsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps)) * pfc_terms_scale_nonempty_zero_coefficient_right) + (fs_a_pfc_nonempty_zero_coefficient_rightsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_zero_coefficient_rightsum_body_steps_partial. fs_h_pfc_nonempty_zero_coefficient_rightsum_body_steps_partial + S (fs_r_pfc_nonempty_zero_coefficient_rightsum_body_steps) = S ((S (fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_zero_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_zero_coefficient_rightsum_body_steps_partial. fs_u_pfc_nonempty_zero_coefficient_rightsum = fs_q_pfc_nonempty_zero_coefficient_rightsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_zero_coefficient_rightsum) + (fs_r_pfc_nonempty_zero_coefficient_rightsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_zero_coefficient_rightsum_body_steps_successor. fs_h_pfc_nonempty_zero_coefficient_rightsum_body_steps_successor + S (fs_s_pfc_nonempty_zero_coefficient_rightsum_body_steps) = S ((S (S fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_zero_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_zero_coefficient_rightsum_body_steps_successor. fs_u_pfc_nonempty_zero_coefficient_rightsum = fs_q_pfc_nonempty_zero_coefficient_rightsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_zero_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_zero_coefficient_rightsum) + (fs_s_pfc_nonempty_zero_coefficient_rightsum_body_steps))) /\ fs_s_pfc_nonempty_zero_coefficient_rightsum_body_steps = fs_r_pfc_nonempty_zero_coefficient_rightsum_body_steps + fs_a_pfc_nonempty_zero_coefficient_rightsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_zero_coefficient_rightresiduebound. pfa_gap_nonempty_zero_coefficient_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_nonempty_zero_coefficient_rightresiduecongruence pfa_offset_right_nonempty_zero_coefficient_rightresiduecongruence. (pfc_natural_sum_nonempty_zero_coefficient_right) + (p) * pfa_offset_left_nonempty_zero_coefficient_rightresiduecongruence = (r) + (p) * pfa_offset_right_nonempty_zero_coefficient_rightresiduecongruence)))))))))))
  46. 0046specialize hn_right_right_right (i)
  47. 0047apply hn_right_right_right
  48. 0048specialize le_trans (S i)
  49. 0049specialize le_trans (t)
  50. 0050specialize le_trans (K)
  51. 0051apply le_trans
  52. 0052exact hi
  53. 0053rewrite hlength
  54. 0054specialize le_add_right (t)
  55. 0055specialize le_add_right (N)
  56. 0056apply le_add_right
  57. 0057cases hv
  58. 0058cases hv_witness
  59. 0059have hzero : x=0
  60. 0060specialize prime_field_convolution_coefficient_before_left_padding_right (p)
  61. 0061specialize prime_field_convolution_coefficient_before_left_padding_right (ab)
  62. 0062specialize prime_field_convolution_coefficient_before_left_padding_right (ac)
  63. 0063specialize prime_field_convolution_coefficient_before_left_padding_right (L)
  64. 0064specialize prime_field_convolution_coefficient_before_left_padding_right (bb)
  65. 0065specialize prime_field_convolution_coefficient_before_left_padding_right (bc)
  66. 0066specialize prime_field_convolution_coefficient_before_left_padding_right (M)
  67. 0067specialize prime_field_convolution_coefficient_before_left_padding_right (BB)
  68. 0068specialize prime_field_convolution_coefficient_before_left_padding_right (BC)
  69. 0069specialize prime_field_convolution_coefficient_before_left_padding_right (t)
  70. 0070specialize prime_field_convolution_coefficient_before_left_padding_right (i)
  71. 0071specialize prime_field_convolution_coefficient_before_left_padding_right (x)
  72. 0072apply prime_field_convolution_coefficient_before_left_padding_right
  73. 0073exact hp
  74. 0074exact hpad
  75. 0075exact hi
  76. 0076exact hv_witness_right
  77. 0077rewrite hzero at hv_witness_left
  78. 0078rewrite hzero at hv_witness_left
  79. 0079exact hv_witness_left
  80. 0080intro i
  81. 0081intro a
  82. 0082intro hi
  83. 0083intro ha
  84. 0084have hcoefficient : exists pfc_terms_code_nonempty_original_coefficient_right pfc_terms_scale_nonempty_original_coefficient_right pfc_natural_sum_nonempty_original_coefficient_right. ((forall pfc_index_nonempty_original_coefficient_rightdiagonal. (exists pfa_gap_nonempty_original_coefficient_rightdiagonalbound. pfa_gap_nonempty_original_coefficient_rightdiagonalbound + S (pfc_index_nonempty_original_coefficient_rightdiagonal) = (S (i))) -> exists pfc_value_nonempty_original_coefficient_rightdiagonal. ((((exists ff_h_pfp_nonempty_original_coefficient_rightdiagonalentry. ff_h_pfp_nonempty_original_coefficient_rightdiagonalentry + S (pfc_value_nonempty_original_coefficient_rightdiagonal) = S ((S (pfc_index_nonempty_original_coefficient_rightdiagonal)) * pfc_terms_scale_nonempty_original_coefficient_right)) /\ exists ff_q_pfp_nonempty_original_coefficient_rightdiagonalentry. pfc_terms_code_nonempty_original_coefficient_right = ff_q_pfp_nonempty_original_coefficient_rightdiagonalentry * S ((S (pfc_index_nonempty_original_coefficient_rightdiagonal)) * pfc_terms_scale_nonempty_original_coefficient_right) + (pfc_value_nonempty_original_coefficient_rightdiagonal))) /\ ((exists pfc_complement_nonempty_original_coefficient_rightdiagonalterm pfc_left_nonempty_original_coefficient_rightdiagonalterm pfc_right_nonempty_original_coefficient_rightdiagonalterm. (((pfc_index_nonempty_original_coefficient_rightdiagonal)+pfc_complement_nonempty_original_coefficient_rightdiagonalterm=(i)) /\ ((((((exists pfa_gap_nonempty_original_coefficient_rightdiagonaltermleftinside. pfa_gap_nonempty_original_coefficient_rightdiagonaltermleftinside + S (pfc_index_nonempty_original_coefficient_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_original_coefficient_rightdiagonaltermleftentry. ff_h_pfp_nonempty_original_coefficient_rightdiagonaltermleftentry + S (pfc_left_nonempty_original_coefficient_rightdiagonalterm) = S ((S (pfc_index_nonempty_original_coefficient_rightdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_original_coefficient_rightdiagonaltermleftentry. ab = ff_q_pfp_nonempty_original_coefficient_rightdiagonaltermleftentry * S ((S (pfc_index_nonempty_original_coefficient_rightdiagonal)) * ac) + (pfc_left_nonempty_original_coefficient_rightdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_original_coefficient_rightdiagonaltermleftoutside. pfc_gap_nonempty_original_coefficient_rightdiagonaltermleftoutside+(L)=(pfc_index_nonempty_original_coefficient_rightdiagonal)) /\ (((pfc_left_nonempty_original_coefficient_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_original_coefficient_rightdiagonaltermrightinside. pfa_gap_nonempty_original_coefficient_rightdiagonaltermrightinside + S (pfc_complement_nonempty_original_coefficient_rightdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_nonempty_original_coefficient_rightdiagonaltermrightentry. ff_h_pfp_nonempty_original_coefficient_rightdiagonaltermrightentry + S (pfc_right_nonempty_original_coefficient_rightdiagonalterm) = S ((S (pfc_complement_nonempty_original_coefficient_rightdiagonalterm)) * bc)) /\ exists ff_q_pfp_nonempty_original_coefficient_rightdiagonaltermrightentry. bb = ff_q_pfp_nonempty_original_coefficient_rightdiagonaltermrightentry * S ((S (pfc_complement_nonempty_original_coefficient_rightdiagonalterm)) * bc) + (pfc_right_nonempty_original_coefficient_rightdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_original_coefficient_rightdiagonaltermrightoutside. pfc_gap_nonempty_original_coefficient_rightdiagonaltermrightoutside+(M)=(pfc_complement_nonempty_original_coefficient_rightdiagonalterm)) /\ (((pfc_right_nonempty_original_coefficient_rightdiagonalterm)=0))))) /\ (((pfc_value_nonempty_original_coefficient_rightdiagonal)=pfc_left_nonempty_original_coefficient_rightdiagonalterm*pfc_right_nonempty_original_coefficient_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_original_coefficient_rightsum fs_v_pfc_nonempty_original_coefficient_rightsum. ((((exists fs_h_pfc_nonempty_original_coefficient_rightsum_body_start. fs_h_pfc_nonempty_original_coefficient_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_original_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_original_coefficient_rightsum_body_start. fs_u_pfc_nonempty_original_coefficient_rightsum = fs_q_pfc_nonempty_original_coefficient_rightsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_original_coefficient_rightsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_original_coefficient_rightsum_body_terminal. fs_h_pfc_nonempty_original_coefficient_rightsum_body_terminal + S (pfc_natural_sum_nonempty_original_coefficient_right) = S ((S (S (i))) * fs_v_pfc_nonempty_original_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_original_coefficient_rightsum_body_terminal. fs_u_pfc_nonempty_original_coefficient_rightsum = fs_q_pfc_nonempty_original_coefficient_rightsum_body_terminal * S ((S (S (i))) * fs_v_pfc_nonempty_original_coefficient_rightsum) + (pfc_natural_sum_nonempty_original_coefficient_right))) /\ forall fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps. (exists fs_lt_pfc_nonempty_original_coefficient_rightsum_body_steps_bound. fs_lt_pfc_nonempty_original_coefficient_rightsum_body_steps_bound + S fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps = S (i)) -> exists fs_a_pfc_nonempty_original_coefficient_rightsum_body_steps fs_r_pfc_nonempty_original_coefficient_rightsum_body_steps fs_s_pfc_nonempty_original_coefficient_rightsum_body_steps. ((((exists fs_h_pfc_nonempty_original_coefficient_rightsum_body_steps_summand. fs_h_pfc_nonempty_original_coefficient_rightsum_body_steps_summand + S (fs_a_pfc_nonempty_original_coefficient_rightsum_body_steps) = S ((S (fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps)) * pfc_terms_scale_nonempty_original_coefficient_right)) /\ exists fs_q_pfc_nonempty_original_coefficient_rightsum_body_steps_summand. pfc_terms_code_nonempty_original_coefficient_right = fs_q_pfc_nonempty_original_coefficient_rightsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps)) * pfc_terms_scale_nonempty_original_coefficient_right) + (fs_a_pfc_nonempty_original_coefficient_rightsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_original_coefficient_rightsum_body_steps_partial. fs_h_pfc_nonempty_original_coefficient_rightsum_body_steps_partial + S (fs_r_pfc_nonempty_original_coefficient_rightsum_body_steps) = S ((S (fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_original_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_original_coefficient_rightsum_body_steps_partial. fs_u_pfc_nonempty_original_coefficient_rightsum = fs_q_pfc_nonempty_original_coefficient_rightsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_original_coefficient_rightsum) + (fs_r_pfc_nonempty_original_coefficient_rightsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_original_coefficient_rightsum_body_steps_successor. fs_h_pfc_nonempty_original_coefficient_rightsum_body_steps_successor + S (fs_s_pfc_nonempty_original_coefficient_rightsum_body_steps) = S ((S (S fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_original_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_original_coefficient_rightsum_body_steps_successor. fs_u_pfc_nonempty_original_coefficient_rightsum = fs_q_pfc_nonempty_original_coefficient_rightsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_original_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_original_coefficient_rightsum) + (fs_s_pfc_nonempty_original_coefficient_rightsum_body_steps))) /\ fs_s_pfc_nonempty_original_coefficient_rightsum_body_steps = fs_r_pfc_nonempty_original_coefficient_rightsum_body_steps + fs_a_pfc_nonempty_original_coefficient_rightsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_original_coefficient_rightresiduebound. pfa_gap_nonempty_original_coefficient_rightresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_nonempty_original_coefficient_rightresiduecongruence pfa_offset_right_nonempty_original_coefficient_rightresiduecongruence. (pfc_natural_sum_nonempty_original_coefficient_right) + (p) * pfa_offset_left_nonempty_original_coefficient_rightresiduecongruence = (a) + (p) * pfa_offset_right_nonempty_original_coefficient_rightresiduecongruence))))))))
  85. 0085specialize prime_field_convolution_prefix_entry (p)
  86. 0086specialize prime_field_convolution_prefix_entry (ab)
  87. 0087specialize prime_field_convolution_prefix_entry (ac)
  88. 0088specialize prime_field_convolution_prefix_entry (L)
  89. 0089specialize prime_field_convolution_prefix_entry (bb)
  90. 0090specialize prime_field_convolution_prefix_entry (bc)
  91. 0091specialize prime_field_convolution_prefix_entry (M)
  92. 0092specialize prime_field_convolution_prefix_entry (cb)
  93. 0093specialize prime_field_convolution_prefix_entry (cc)
  94. 0094specialize prime_field_convolution_prefix_entry (N)
  95. 0095specialize prime_field_convolution_prefix_entry (i)
  96. 0096specialize prime_field_convolution_prefix_entry (a)
  97. 0097apply prime_field_convolution_prefix_entry
  98. 0098exact hc_right_right_right
  99. 0099exact hi
  100. 0100exact ha
  101. 0101have hv : exists r. ((((exists ff_h_pfp_nonempty_shifted_entry_right. ff_h_pfp_nonempty_shifted_entry_right + S (r) = S ((S (t+i)) * CC)) /\ exists ff_q_pfp_nonempty_shifted_entry_right. CB = ff_q_pfp_nonempty_shifted_entry_right * S ((S (t+i)) * CC) + (r))) /\ ((exists pfc_terms_code_nonempty_shifted_coefficient_right pfc_terms_scale_nonempty_shifted_coefficient_right pfc_natural_sum_nonempty_shifted_coefficient_right. ((forall pfc_index_nonempty_shifted_coefficient_rightdiagonal. (exists pfa_gap_nonempty_shifted_coefficient_rightdiagonalbound. pfa_gap_nonempty_shifted_coefficient_rightdiagonalbound + S (pfc_index_nonempty_shifted_coefficient_rightdiagonal) = (S (t+i))) -> exists pfc_value_nonempty_shifted_coefficient_rightdiagonal. ((((exists ff_h_pfp_nonempty_shifted_coefficient_rightdiagonalentry. ff_h_pfp_nonempty_shifted_coefficient_rightdiagonalentry + S (pfc_value_nonempty_shifted_coefficient_rightdiagonal) = S ((S (pfc_index_nonempty_shifted_coefficient_rightdiagonal)) * pfc_terms_scale_nonempty_shifted_coefficient_right)) /\ exists ff_q_pfp_nonempty_shifted_coefficient_rightdiagonalentry. pfc_terms_code_nonempty_shifted_coefficient_right = ff_q_pfp_nonempty_shifted_coefficient_rightdiagonalentry * S ((S (pfc_index_nonempty_shifted_coefficient_rightdiagonal)) * pfc_terms_scale_nonempty_shifted_coefficient_right) + (pfc_value_nonempty_shifted_coefficient_rightdiagonal))) /\ ((exists pfc_complement_nonempty_shifted_coefficient_rightdiagonalterm pfc_left_nonempty_shifted_coefficient_rightdiagonalterm pfc_right_nonempty_shifted_coefficient_rightdiagonalterm. (((pfc_index_nonempty_shifted_coefficient_rightdiagonal)+pfc_complement_nonempty_shifted_coefficient_rightdiagonalterm=(t+i)) /\ ((((((exists pfa_gap_nonempty_shifted_coefficient_rightdiagonaltermleftinside. pfa_gap_nonempty_shifted_coefficient_rightdiagonaltermleftinside + S (pfc_index_nonempty_shifted_coefficient_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_nonempty_shifted_coefficient_rightdiagonaltermleftentry. ff_h_pfp_nonempty_shifted_coefficient_rightdiagonaltermleftentry + S (pfc_left_nonempty_shifted_coefficient_rightdiagonalterm) = S ((S (pfc_index_nonempty_shifted_coefficient_rightdiagonal)) * ac)) /\ exists ff_q_pfp_nonempty_shifted_coefficient_rightdiagonaltermleftentry. ab = ff_q_pfp_nonempty_shifted_coefficient_rightdiagonaltermleftentry * S ((S (pfc_index_nonempty_shifted_coefficient_rightdiagonal)) * ac) + (pfc_left_nonempty_shifted_coefficient_rightdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_shifted_coefficient_rightdiagonaltermleftoutside. pfc_gap_nonempty_shifted_coefficient_rightdiagonaltermleftoutside+(L)=(pfc_index_nonempty_shifted_coefficient_rightdiagonal)) /\ (((pfc_left_nonempty_shifted_coefficient_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_shifted_coefficient_rightdiagonaltermrightinside. pfa_gap_nonempty_shifted_coefficient_rightdiagonaltermrightinside + S (pfc_complement_nonempty_shifted_coefficient_rightdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_nonempty_shifted_coefficient_rightdiagonaltermrightentry. ff_h_pfp_nonempty_shifted_coefficient_rightdiagonaltermrightentry + S (pfc_right_nonempty_shifted_coefficient_rightdiagonalterm) = S ((S (pfc_complement_nonempty_shifted_coefficient_rightdiagonalterm)) * BC)) /\ exists ff_q_pfp_nonempty_shifted_coefficient_rightdiagonaltermrightentry. BB = ff_q_pfp_nonempty_shifted_coefficient_rightdiagonaltermrightentry * S ((S (pfc_complement_nonempty_shifted_coefficient_rightdiagonalterm)) * BC) + (pfc_right_nonempty_shifted_coefficient_rightdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_shifted_coefficient_rightdiagonaltermrightoutside. pfc_gap_nonempty_shifted_coefficient_rightdiagonaltermrightoutside+(t+M)=(pfc_complement_nonempty_shifted_coefficient_rightdiagonalterm)) /\ (((pfc_right_nonempty_shifted_coefficient_rightdiagonalterm)=0))))) /\ (((pfc_value_nonempty_shifted_coefficient_rightdiagonal)=pfc_left_nonempty_shifted_coefficient_rightdiagonalterm*pfc_right_nonempty_shifted_coefficient_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_shifted_coefficient_rightsum fs_v_pfc_nonempty_shifted_coefficient_rightsum. ((((exists fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_start. fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_shifted_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_start. fs_u_pfc_nonempty_shifted_coefficient_rightsum = fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_shifted_coefficient_rightsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_terminal. fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_terminal + S (pfc_natural_sum_nonempty_shifted_coefficient_right) = S ((S (S (t+i))) * fs_v_pfc_nonempty_shifted_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_terminal. fs_u_pfc_nonempty_shifted_coefficient_rightsum = fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_terminal * S ((S (S (t+i))) * fs_v_pfc_nonempty_shifted_coefficient_rightsum) + (pfc_natural_sum_nonempty_shifted_coefficient_right))) /\ forall fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps. (exists fs_lt_pfc_nonempty_shifted_coefficient_rightsum_body_steps_bound. fs_lt_pfc_nonempty_shifted_coefficient_rightsum_body_steps_bound + S fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps = S (t+i)) -> exists fs_a_pfc_nonempty_shifted_coefficient_rightsum_body_steps fs_r_pfc_nonempty_shifted_coefficient_rightsum_body_steps fs_s_pfc_nonempty_shifted_coefficient_rightsum_body_steps. ((((exists fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_steps_summand. fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_steps_summand + S (fs_a_pfc_nonempty_shifted_coefficient_rightsum_body_steps) = S ((S (fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps)) * pfc_terms_scale_nonempty_shifted_coefficient_right)) /\ exists fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_steps_summand. pfc_terms_code_nonempty_shifted_coefficient_right = fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps)) * pfc_terms_scale_nonempty_shifted_coefficient_right) + (fs_a_pfc_nonempty_shifted_coefficient_rightsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_steps_partial. fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_steps_partial + S (fs_r_pfc_nonempty_shifted_coefficient_rightsum_body_steps) = S ((S (fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_shifted_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_steps_partial. fs_u_pfc_nonempty_shifted_coefficient_rightsum = fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_shifted_coefficient_rightsum) + (fs_r_pfc_nonempty_shifted_coefficient_rightsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_steps_successor. fs_h_pfc_nonempty_shifted_coefficient_rightsum_body_steps_successor + S (fs_s_pfc_nonempty_shifted_coefficient_rightsum_body_steps) = S ((S (S fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_shifted_coefficient_rightsum)) /\ exists fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_steps_successor. fs_u_pfc_nonempty_shifted_coefficient_rightsum = fs_q_pfc_nonempty_shifted_coefficient_rightsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_shifted_coefficient_rightsum_body_steps)) * fs_v_pfc_nonempty_shifted_coefficient_rightsum) + (fs_s_pfc_nonempty_shifted_coefficient_rightsum_body_steps))) /\ fs_s_pfc_nonempty_shifted_coefficient_rightsum_body_steps = fs_r_pfc_nonempty_shifted_coefficient_rightsum_body_steps + fs_a_pfc_nonempty_shifted_coefficient_rightsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_shifted_coefficient_rightresiduebound. pfa_gap_nonempty_shifted_coefficient_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_nonempty_shifted_coefficient_rightresiduecongruence pfa_offset_right_nonempty_shifted_coefficient_rightresiduecongruence. (pfc_natural_sum_nonempty_shifted_coefficient_right) + (p) * pfa_offset_left_nonempty_shifted_coefficient_rightresiduecongruence = (r) + (p) * pfa_offset_right_nonempty_shifted_coefficient_rightresiduecongruence)))))))))))
  102. 0102specialize hn_right_right_right (t+i)
  103. 0103apply hn_right_right_right
  104. 0104rewrite hlength
  105. 0105specialize matrix_recursive_lt_add_left (i)
  106. 0106specialize matrix_recursive_lt_add_left (N)
  107. 0107specialize matrix_recursive_lt_add_left (t)
  108. 0108apply matrix_recursive_lt_add_left
  109. 0109exact hi
  110. 0110cases hv
  111. 0111cases hv_witness
  112. 0112have heq : x=a
  113. 0113specialize prime_field_convolution_coefficient_functional (p)
  114. 0114specialize prime_field_convolution_coefficient_functional (ab)
  115. 0115specialize prime_field_convolution_coefficient_functional (ac)
  116. 0116specialize prime_field_convolution_coefficient_functional (L)
  117. 0117specialize prime_field_convolution_coefficient_functional (BB)
  118. 0118specialize prime_field_convolution_coefficient_functional (BC)
  119. 0119specialize prime_field_convolution_coefficient_functional (t+M)
  120. 0120specialize prime_field_convolution_coefficient_functional (t+i)
  121. 0121specialize prime_field_convolution_coefficient_functional (x)
  122. 0122specialize prime_field_convolution_coefficient_functional (a)
  123. 0123apply prime_field_convolution_coefficient_functional
  124. 0124exact hv_witness_right
  125. 0125specialize prime_field_convolution_coefficient_left_padding_right (p)
  126. 0126specialize prime_field_convolution_coefficient_left_padding_right (ab)
  127. 0127specialize prime_field_convolution_coefficient_left_padding_right (ac)
  128. 0128specialize prime_field_convolution_coefficient_left_padding_right (L)
  129. 0129specialize prime_field_convolution_coefficient_left_padding_right (bb)
  130. 0130specialize prime_field_convolution_coefficient_left_padding_right (bc)
  131. 0131specialize prime_field_convolution_coefficient_left_padding_right (M)
  132. 0132specialize prime_field_convolution_coefficient_left_padding_right (BB)
  133. 0133specialize prime_field_convolution_coefficient_left_padding_right (BC)
  134. 0134specialize prime_field_convolution_coefficient_left_padding_right (t)
  135. 0135specialize prime_field_convolution_coefficient_left_padding_right (i)
  136. 0136specialize prime_field_convolution_coefficient_left_padding_right (a)
  137. 0137apply prime_field_convolution_coefficient_left_padding_right
  138. 0138exact hpad
  139. 0139exact hcoefficient
  140. 0140rewrite heq at hv_witness_left
  141. 0141rewrite heq at hv_witness_left
  142. 0142exact hv_witness_left