prime_field_polynomial_convolution_right_scale_zero

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M sb sc db dc N. (~(p=0)) -> (((exists pfa_gap_scalar_zero_product_inputscalar. pfa_gap_scalar_zero_product_inputscalar + S (0) = (p)) /\ ((forall pfp_index_scalar_zero_product_input. (exists pfa_gap_scalar_zero_product_inputindex. pfa_gap_scalar_zero_product_inputindex + S (pfp_index_scalar_zero_product_input) = (M)) -> exists pfp_source_scalar_zero_product_input pfp_value_scalar_zero_product_input. ((((exists ff_h_pfp_scalar_zero_product_inputsource. ff_h_pfp_scalar_zero_product_inputsource + S (pfp_source_scalar_zero_product_input) = S ((S (pfp_index_scalar_zero_product_input)) * bc)) /\ exists ff_q_pfp_scalar_zero_product_inputsource. bb = ff_q_pfp_scalar_zero_product_inputsource * S ((S (pfp_index_scalar_zero_product_input)) * bc) + (pfp_source_scalar_zero_product_input))) /\ (((((exists ff_h_pfp_scalar_zero_product_inputtarget. ff_h_pfp_scalar_zero_product_inputtarget + S (pfp_value_scalar_zero_product_input) = S ((S (pfp_index_scalar_zero_product_input)) * sc)) /\ exists ff_q_pfp_scalar_zero_product_inputtarget. sb = ff_q_pfp_scalar_zero_product_inputtarget * S ((S (pfp_index_scalar_zero_product_input)) * sc) + (pfp_value_scalar_zero_product_input))) /\ ((((exists pfa_gap_scalar_zero_product_inputoperationleft. pfa_gap_scalar_zero_product_inputoperationleft + S (0) = (p)) /\ (((exists pfa_gap_scalar_zero_product_inputoperationright. pfa_gap_scalar_zero_product_inputoperationright + S (pfp_source_scalar_zero_product_input) = (p)) /\ ((((exists pfa_gap_scalar_zero_product_inputoperationresultbound. pfa_gap_scalar_zero_product_inputoperationresultbound + S (pfp_value_scalar_zero_product_input) = (p)) /\ ((exists pfa_offset_left_scalar_zero_product_inputoperationresultcongruence pfa_offset_right_scalar_zero_product_inputoperationresultcongruence. ((0) * (pfp_source_scalar_zero_product_input)) + (p) * pfa_offset_left_scalar_zero_product_inputoperationresultcongruence = (pfp_value_scalar_zero_product_input) + (p) * pfa_offset_right_scalar_zero_product_inputoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_scalar_zero_product_actualleft. (exists fom_gap_pfp_scalar_zero_product_actualleft_index_bound. fom_gap_pfp_scalar_zero_product_actualleft_index_bound + S (fom_index_pfp_scalar_zero_product_actualleft) = L) -> exists fom_value_pfp_scalar_zero_product_actualleft. ((((exists fom_beta_height_pfp_scalar_zero_product_actualleft_entry. fom_beta_height_pfp_scalar_zero_product_actualleft_entry + S (fom_value_pfp_scalar_zero_product_actualleft) = S ((S (fom_index_pfp_scalar_zero_product_actualleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_zero_product_actualleft_entry. ab = fom_beta_quotient_pfp_scalar_zero_product_actualleft_entry * S ((S (fom_index_pfp_scalar_zero_product_actualleft)) * ac) + (fom_value_pfp_scalar_zero_product_actualleft))) /\ (exists fom_gap_pfp_scalar_zero_product_actualleft_value_bound. fom_gap_pfp_scalar_zero_product_actualleft_value_bound + S (fom_value_pfp_scalar_zero_product_actualleft) = p))) /\ (((forall fom_index_pfp_scalar_zero_product_actualright. (exists fom_gap_pfp_scalar_zero_product_actualright_index_bound. fom_gap_pfp_scalar_zero_product_actualright_index_bound + S (fom_index_pfp_scalar_zero_product_actualright) = M) -> exists fom_value_pfp_scalar_zero_product_actualright. ((((exists fom_beta_height_pfp_scalar_zero_product_actualright_entry. fom_beta_height_pfp_scalar_zero_product_actualright_entry + S (fom_value_pfp_scalar_zero_product_actualright) = S ((S (fom_index_pfp_scalar_zero_product_actualright)) * sc)) /\ exists fom_beta_quotient_pfp_scalar_zero_product_actualright_entry. sb = fom_beta_quotient_pfp_scalar_zero_product_actualright_entry * S ((S (fom_index_pfp_scalar_zero_product_actualright)) * sc) + (fom_value_pfp_scalar_zero_product_actualright))) /\ (exists fom_gap_pfp_scalar_zero_product_actualright_value_bound. fom_gap_pfp_scalar_zero_product_actualright_value_bound + S (fom_value_pfp_scalar_zero_product_actualright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_zero_product_actualcoefficients. (exists pfa_gap_scalar_zero_product_actualcoefficientsbound. pfa_gap_scalar_zero_product_actualcoefficientsbound + S (pfc_index_scalar_zero_product_actualcoefficients) = (N)) -> exists pfc_value_scalar_zero_product_actualcoefficients. ((((exists ff_h_pfp_scalar_zero_product_actualcoefficientsentry. ff_h_pfp_scalar_zero_product_actualcoefficientsentry + S (pfc_value_scalar_zero_product_actualcoefficients) = S ((S (pfc_index_scalar_zero_product_actualcoefficients)) * dc)) /\ exists ff_q_pfp_scalar_zero_product_actualcoefficientsentry. db = ff_q_pfp_scalar_zero_product_actualcoefficientsentry * S ((S (pfc_index_scalar_zero_product_actualcoefficients)) * dc) + (pfc_value_scalar_zero_product_actualcoefficients))) /\ ((exists pfc_terms_code_scalar_zero_product_actualcoefficientscoefficient pfc_terms_scale_scalar_zero_product_actualcoefficientscoefficient pfc_natural_sum_scalar_zero_product_actualcoefficientscoefficient. ((forall pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_zero_product_actualcoefficientscoefficientdiagonalbound. pfa_gap_scalar_zero_product_actualcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_zero_product_actualcoefficients))) -> exists pfc_value_scalar_zero_product_actualcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_zero_product_actualcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_zero_product_actualcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_zero_product_actualcoefficientscoefficient = ff_q_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_zero_product_actualcoefficientscoefficient) + (pfc_value_scalar_zero_product_actualcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_zero_product_actualcoefficientscoefficientdiagonalterm pfc_left_scalar_zero_product_actualcoefficientscoefficientdiagonalterm pfc_right_scalar_zero_product_actualcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal)+pfc_complement_scalar_zero_product_actualcoefficientscoefficientdiagonalterm=(pfc_index_scalar_zero_product_actualcoefficients)) /\ ((((((exists pfa_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_zero_product_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_zero_product_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_zero_product_actualcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_zero_product_actualcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_zero_product_actualcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_zero_product_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_zero_product_actualcoefficientscoefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_zero_product_actualcoefficientscoefficientdiagonalterm)) * sc) + (pfc_right_scalar_zero_product_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_zero_product_actualcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_zero_product_actualcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_zero_product_actualcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_zero_product_actualcoefficientscoefficientdiagonal)=pfc_left_scalar_zero_product_actualcoefficientscoefficientdiagonalterm*pfc_right_scalar_zero_product_actualcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_zero_product_actualcoefficientscoefficientsum fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_zero_product_actualcoefficientscoefficientsum = fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_zero_product_actualcoefficientscoefficient) = S ((S (S (pfc_index_scalar_zero_product_actualcoefficients))) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_zero_product_actualcoefficientscoefficientsum = fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_zero_product_actualcoefficients))) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum) + (pfc_natural_sum_scalar_zero_product_actualcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_zero_product_actualcoefficients)) -> exists fs_a_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_zero_product_actualcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_zero_product_actualcoefficientscoefficient = fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_zero_product_actualcoefficientscoefficient) + (fs_a_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_zero_product_actualcoefficientscoefficientsum = fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum) + (fs_r_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_zero_product_actualcoefficientscoefficientsum = fs_q_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_zero_product_actualcoefficientscoefficientsum) + (fs_s_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_zero_product_actualcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_zero_product_actualcoefficientscoefficientresiduebound. pfa_gap_scalar_zero_product_actualcoefficientscoefficientresiduebound + S (pfc_value_scalar_zero_product_actualcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_zero_product_actualcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_zero_product_actualcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_zero_product_actualcoefficientscoefficient) + (p) * pfa_offset_left_scalar_zero_product_actualcoefficientscoefficientresiduecongruence = (pfc_value_scalar_zero_product_actualcoefficients) + (p) * pfa_offset_right_scalar_zero_product_actualcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfp_repeat_index_scalar_zero_product_result. (exists pfa_gap_scalar_zero_product_resultindex. pfa_gap_scalar_zero_product_resultindex + S (pfp_repeat_index_scalar_zero_product_result) = (N)) -> (((exists ff_h_pfp_scalar_zero_product_resultentry. ff_h_pfp_scalar_zero_product_resultentry + S (0) = S ((S (pfp_repeat_index_scalar_zero_product_result)) * dc)) /\ exists ff_q_pfp_scalar_zero_product_resultentry. db = ff_q_pfp_scalar_zero_product_resultentry * S ((S (pfp_repeat_index_scalar_zero_product_result)) * dc) + (0))))