prime_field_convolution_coefficient_left_unit

Exact expanded first-order arithmetic statement

forall p ub uc ab ac L i a r. (((exists ff_h_pfp_unit_coefficient_unit. ff_h_pfp_unit_coefficient_unit + S (1) = S ((S (0)) * uc)) /\ exists ff_q_pfp_unit_coefficient_unit. ub = ff_q_pfp_unit_coefficient_unit * S ((S (0)) * uc) + (1))) -> (exists pfa_gap_unit_coefficient_index. pfa_gap_unit_coefficient_index + S (i) = (L)) -> (((exists ff_h_pfp_unit_coefficient_A. ff_h_pfp_unit_coefficient_A + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_unit_coefficient_A. ab = ff_q_pfp_unit_coefficient_A * S ((S (i)) * ac) + (a))) -> (exists pfa_gap_unit_coefficient_bound. pfa_gap_unit_coefficient_bound + S (a) = (p)) -> (exists pfc_terms_code_unit_coefficient_actual pfc_terms_scale_unit_coefficient_actual pfc_natural_sum_unit_coefficient_actual. ((forall pfc_index_unit_coefficient_actualdiagonal. (exists pfa_gap_unit_coefficient_actualdiagonalbound. pfa_gap_unit_coefficient_actualdiagonalbound + S (pfc_index_unit_coefficient_actualdiagonal) = (S (i))) -> exists pfc_value_unit_coefficient_actualdiagonal. ((((exists ff_h_pfp_unit_coefficient_actualdiagonalentry. ff_h_pfp_unit_coefficient_actualdiagonalentry + S (pfc_value_unit_coefficient_actualdiagonal) = S ((S (pfc_index_unit_coefficient_actualdiagonal)) * pfc_terms_scale_unit_coefficient_actual)) /\ exists ff_q_pfp_unit_coefficient_actualdiagonalentry. pfc_terms_code_unit_coefficient_actual = ff_q_pfp_unit_coefficient_actualdiagonalentry * S ((S (pfc_index_unit_coefficient_actualdiagonal)) * pfc_terms_scale_unit_coefficient_actual) + (pfc_value_unit_coefficient_actualdiagonal))) /\ ((exists pfc_complement_unit_coefficient_actualdiagonalterm pfc_left_unit_coefficient_actualdiagonalterm pfc_right_unit_coefficient_actualdiagonalterm. (((pfc_index_unit_coefficient_actualdiagonal)+pfc_complement_unit_coefficient_actualdiagonalterm=(i)) /\ ((((((exists pfa_gap_unit_coefficient_actualdiagonaltermleftinside. pfa_gap_unit_coefficient_actualdiagonaltermleftinside + S (pfc_index_unit_coefficient_actualdiagonal) = (1)) /\ ((((exists ff_h_pfp_unit_coefficient_actualdiagonaltermleftentry. ff_h_pfp_unit_coefficient_actualdiagonaltermleftentry + S (pfc_left_unit_coefficient_actualdiagonalterm) = S ((S (pfc_index_unit_coefficient_actualdiagonal)) * uc)) /\ exists ff_q_pfp_unit_coefficient_actualdiagonaltermleftentry. ub = ff_q_pfp_unit_coefficient_actualdiagonaltermleftentry * S ((S (pfc_index_unit_coefficient_actualdiagonal)) * uc) + (pfc_left_unit_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_unit_coefficient_actualdiagonaltermleftoutside. pfc_gap_unit_coefficient_actualdiagonaltermleftoutside+(1)=(pfc_index_unit_coefficient_actualdiagonal)) /\ (((pfc_left_unit_coefficient_actualdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_coefficient_actualdiagonaltermrightinside. pfa_gap_unit_coefficient_actualdiagonaltermrightinside + S (pfc_complement_unit_coefficient_actualdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_coefficient_actualdiagonaltermrightentry. ff_h_pfp_unit_coefficient_actualdiagonaltermrightentry + S (pfc_right_unit_coefficient_actualdiagonalterm) = S ((S (pfc_complement_unit_coefficient_actualdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_coefficient_actualdiagonaltermrightentry. ab = ff_q_pfp_unit_coefficient_actualdiagonaltermrightentry * S ((S (pfc_complement_unit_coefficient_actualdiagonalterm)) * ac) + (pfc_right_unit_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_unit_coefficient_actualdiagonaltermrightoutside. pfc_gap_unit_coefficient_actualdiagonaltermrightoutside+(L)=(pfc_complement_unit_coefficient_actualdiagonalterm)) /\ (((pfc_right_unit_coefficient_actualdiagonalterm)=0))))) /\ (((pfc_value_unit_coefficient_actualdiagonal)=pfc_left_unit_coefficient_actualdiagonalterm*pfc_right_unit_coefficient_actualdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_coefficient_actualsum fs_v_pfc_unit_coefficient_actualsum. ((((exists fs_h_pfc_unit_coefficient_actualsum_body_start. fs_h_pfc_unit_coefficient_actualsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_coefficient_actualsum)) /\ exists fs_q_pfc_unit_coefficient_actualsum_body_start. fs_u_pfc_unit_coefficient_actualsum = fs_q_pfc_unit_coefficient_actualsum_body_start * S ((S (0)) * fs_v_pfc_unit_coefficient_actualsum) + (0))) /\ ((((exists fs_h_pfc_unit_coefficient_actualsum_body_terminal. fs_h_pfc_unit_coefficient_actualsum_body_terminal + S (pfc_natural_sum_unit_coefficient_actual) = S ((S (S (i))) * fs_v_pfc_unit_coefficient_actualsum)) /\ exists fs_q_pfc_unit_coefficient_actualsum_body_terminal. fs_u_pfc_unit_coefficient_actualsum = fs_q_pfc_unit_coefficient_actualsum_body_terminal * S ((S (S (i))) * fs_v_pfc_unit_coefficient_actualsum) + (pfc_natural_sum_unit_coefficient_actual))) /\ forall fs_i_pfc_unit_coefficient_actualsum_body_steps. (exists fs_lt_pfc_unit_coefficient_actualsum_body_steps_bound. fs_lt_pfc_unit_coefficient_actualsum_body_steps_bound + S fs_i_pfc_unit_coefficient_actualsum_body_steps = S (i)) -> exists fs_a_pfc_unit_coefficient_actualsum_body_steps fs_r_pfc_unit_coefficient_actualsum_body_steps fs_s_pfc_unit_coefficient_actualsum_body_steps. ((((exists fs_h_pfc_unit_coefficient_actualsum_body_steps_summand. fs_h_pfc_unit_coefficient_actualsum_body_steps_summand + S (fs_a_pfc_unit_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_unit_coefficient_actualsum_body_steps)) * pfc_terms_scale_unit_coefficient_actual)) /\ exists fs_q_pfc_unit_coefficient_actualsum_body_steps_summand. pfc_terms_code_unit_coefficient_actual = fs_q_pfc_unit_coefficient_actualsum_body_steps_summand * S ((S (fs_i_pfc_unit_coefficient_actualsum_body_steps)) * pfc_terms_scale_unit_coefficient_actual) + (fs_a_pfc_unit_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_unit_coefficient_actualsum_body_steps_partial. fs_h_pfc_unit_coefficient_actualsum_body_steps_partial + S (fs_r_pfc_unit_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_unit_coefficient_actualsum_body_steps)) * fs_v_pfc_unit_coefficient_actualsum)) /\ exists fs_q_pfc_unit_coefficient_actualsum_body_steps_partial. fs_u_pfc_unit_coefficient_actualsum = fs_q_pfc_unit_coefficient_actualsum_body_steps_partial * S ((S (fs_i_pfc_unit_coefficient_actualsum_body_steps)) * fs_v_pfc_unit_coefficient_actualsum) + (fs_r_pfc_unit_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_unit_coefficient_actualsum_body_steps_successor. fs_h_pfc_unit_coefficient_actualsum_body_steps_successor + S (fs_s_pfc_unit_coefficient_actualsum_body_steps) = S ((S (S fs_i_pfc_unit_coefficient_actualsum_body_steps)) * fs_v_pfc_unit_coefficient_actualsum)) /\ exists fs_q_pfc_unit_coefficient_actualsum_body_steps_successor. fs_u_pfc_unit_coefficient_actualsum = fs_q_pfc_unit_coefficient_actualsum_body_steps_successor * S ((S (S fs_i_pfc_unit_coefficient_actualsum_body_steps)) * fs_v_pfc_unit_coefficient_actualsum) + (fs_s_pfc_unit_coefficient_actualsum_body_steps))) /\ fs_s_pfc_unit_coefficient_actualsum_body_steps = fs_r_pfc_unit_coefficient_actualsum_body_steps + fs_a_pfc_unit_coefficient_actualsum_body_steps)))))) /\ ((((exists pfa_gap_unit_coefficient_actualresiduebound. pfa_gap_unit_coefficient_actualresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_unit_coefficient_actualresiduecongruence pfa_offset_right_unit_coefficient_actualresiduecongruence. (pfc_natural_sum_unit_coefficient_actual) + (p) * pfa_offset_left_unit_coefficient_actualresiduecongruence = (r) + (p) * pfa_offset_right_unit_coefficient_actualresiduecongruence))))))))) -> (r=a)