prime_field_polynomial_convolution_left_unit_equivalent

Exact expanded first-order arithmetic statement

forall p ub uc ab ac L cb cc. (((exists ff_h_pfp_unit_equal_unit. ff_h_pfp_unit_equal_unit + S (1) = S ((S (0)) * uc)) /\ exists ff_q_pfp_unit_equal_unit. ub = ff_q_pfp_unit_equal_unit * S ((S (0)) * uc) + (1))) -> (((forall fom_index_pfp_unit_equal_actualleft. (exists fom_gap_pfp_unit_equal_actualleft_index_bound. fom_gap_pfp_unit_equal_actualleft_index_bound + S (fom_index_pfp_unit_equal_actualleft) = 1) -> exists fom_value_pfp_unit_equal_actualleft. ((((exists fom_beta_height_pfp_unit_equal_actualleft_entry. fom_beta_height_pfp_unit_equal_actualleft_entry + S (fom_value_pfp_unit_equal_actualleft) = S ((S (fom_index_pfp_unit_equal_actualleft)) * uc)) /\ exists fom_beta_quotient_pfp_unit_equal_actualleft_entry. ub = fom_beta_quotient_pfp_unit_equal_actualleft_entry * S ((S (fom_index_pfp_unit_equal_actualleft)) * uc) + (fom_value_pfp_unit_equal_actualleft))) /\ (exists fom_gap_pfp_unit_equal_actualleft_value_bound. fom_gap_pfp_unit_equal_actualleft_value_bound + S (fom_value_pfp_unit_equal_actualleft) = p))) /\ (((forall fom_index_pfp_unit_equal_actualright. (exists fom_gap_pfp_unit_equal_actualright_index_bound. fom_gap_pfp_unit_equal_actualright_index_bound + S (fom_index_pfp_unit_equal_actualright) = L) -> exists fom_value_pfp_unit_equal_actualright. ((((exists fom_beta_height_pfp_unit_equal_actualright_entry. fom_beta_height_pfp_unit_equal_actualright_entry + S (fom_value_pfp_unit_equal_actualright) = S ((S (fom_index_pfp_unit_equal_actualright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_equal_actualright_entry. ab = fom_beta_quotient_pfp_unit_equal_actualright_entry * S ((S (fom_index_pfp_unit_equal_actualright)) * ac) + (fom_value_pfp_unit_equal_actualright))) /\ (exists fom_gap_pfp_unit_equal_actualright_value_bound. fom_gap_pfp_unit_equal_actualright_value_bound + S (fom_value_pfp_unit_equal_actualright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_unit_equal_actualcoefficients. (exists pfa_gap_unit_equal_actualcoefficientsbound. pfa_gap_unit_equal_actualcoefficientsbound + S (pfc_index_unit_equal_actualcoefficients) = (L)) -> exists pfc_value_unit_equal_actualcoefficients. ((((exists ff_h_pfp_unit_equal_actualcoefficientsentry. ff_h_pfp_unit_equal_actualcoefficientsentry + S (pfc_value_unit_equal_actualcoefficients) = S ((S (pfc_index_unit_equal_actualcoefficients)) * cc)) /\ exists ff_q_pfp_unit_equal_actualcoefficientsentry. cb = ff_q_pfp_unit_equal_actualcoefficientsentry * S ((S (pfc_index_unit_equal_actualcoefficients)) * cc) + (pfc_value_unit_equal_actualcoefficients))) /\ ((exists pfc_terms_code_unit_equal_actualcoefficientscoefficient pfc_terms_scale_unit_equal_actualcoefficientscoefficient pfc_natural_sum_unit_equal_actualcoefficientscoefficient. ((forall pfc_index_unit_equal_actualcoefficientscoefficientdiagonal. (exists pfa_gap_unit_equal_actualcoefficientscoefficientdiagonalbound. pfa_gap_unit_equal_actualcoefficientscoefficientdiagonalbound + S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal) = (S (pfc_index_unit_equal_actualcoefficients))) -> exists pfc_value_unit_equal_actualcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry. ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry + S (pfc_value_unit_equal_actualcoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient)) /\ exists ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry. pfc_terms_code_unit_equal_actualcoefficientscoefficient = ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient) + (pfc_value_unit_equal_actualcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm. (((pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)+pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm=(pfc_index_unit_equal_actualcoefficients)) /\ ((((((exists pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) * uc) + (pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_unit_equal_actualcoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_equal_actualcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_equal_actualcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_equal_actualcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_equal_actualcoefficientscoefficientdiagonal)=pfc_left_unit_equal_actualcoefficientscoefficientdiagonalterm*pfc_right_unit_equal_actualcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_equal_actualcoefficientscoefficientsum fs_v_pfc_unit_equal_actualcoefficientscoefficientsum. ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_start. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_start. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_equal_actualcoefficientscoefficient) = S ((S (S (pfc_index_unit_equal_actualcoefficients))) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_equal_actualcoefficients))) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (pfc_natural_sum_unit_equal_actualcoefficientscoefficient))) /\ forall fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps = S (pfc_index_unit_equal_actualcoefficients)) -> exists fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_equal_actualcoefficientscoefficient = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_equal_actualcoefficientscoefficient) + (fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_equal_actualcoefficientscoefficientsum = fs_q_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_equal_actualcoefficientscoefficientsum) + (fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps = fs_r_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps + fs_a_pfc_unit_equal_actualcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_equal_actualcoefficientscoefficientresiduebound. pfa_gap_unit_equal_actualcoefficientscoefficientresiduebound + S (pfc_value_unit_equal_actualcoefficients) = (p)) /\ ((exists pfa_offset_left_unit_equal_actualcoefficientscoefficientresiduecongruence pfa_offset_right_unit_equal_actualcoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_equal_actualcoefficientscoefficient) + (p) * pfa_offset_left_unit_equal_actualcoefficientscoefficientresiduecongruence = (pfc_value_unit_equal_actualcoefficients) + (p) * pfa_offset_right_unit_equal_actualcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_unit_equivalent_result pfrep_left_unit_equivalent_result pfrep_right_unit_equivalent_result. ((exists pfrep_position_unit_equivalent_resultfirst. ((pfrep_position_unit_equivalent_resultfirst+S (pfrep_power_unit_equivalent_result)=(L)) /\ ((((exists ff_h_pfp_unit_equivalent_resultfirstentry. ff_h_pfp_unit_equivalent_resultfirstentry + S (pfrep_left_unit_equivalent_result) = S ((S (pfrep_position_unit_equivalent_resultfirst)) * cc)) /\ exists ff_q_pfp_unit_equivalent_resultfirstentry. cb = ff_q_pfp_unit_equivalent_resultfirstentry * S ((S (pfrep_position_unit_equivalent_resultfirst)) * cc) + (pfrep_left_unit_equivalent_result)))))) \/ (((exists pfrep_gap_unit_equivalent_resultfirstoutside. pfrep_gap_unit_equivalent_resultfirstoutside+(L)=(pfrep_power_unit_equivalent_result)) /\ (((pfrep_left_unit_equivalent_result)=0))))) -> ((exists pfrep_position_unit_equivalent_resultsecond. ((pfrep_position_unit_equivalent_resultsecond+S (pfrep_power_unit_equivalent_result)=(L)) /\ ((((exists ff_h_pfp_unit_equivalent_resultsecondentry. ff_h_pfp_unit_equivalent_resultsecondentry + S (pfrep_right_unit_equivalent_result) = S ((S (pfrep_position_unit_equivalent_resultsecond)) * ac)) /\ exists ff_q_pfp_unit_equivalent_resultsecondentry. ab = ff_q_pfp_unit_equivalent_resultsecondentry * S ((S (pfrep_position_unit_equivalent_resultsecond)) * ac) + (pfrep_right_unit_equivalent_result)))))) \/ (((exists pfrep_gap_unit_equivalent_resultsecondoutside. pfrep_gap_unit_equivalent_resultsecondoutside+(L)=(pfrep_power_unit_equivalent_result)) /\ (((pfrep_right_unit_equivalent_result)=0))))) -> pfrep_left_unit_equivalent_result=pfrep_right_unit_equivalent_result)