prime_field_convolution_coefficient_left_constant

Exact expanded first-order arithmetic statement

forall p k kb kc ab ac L i a r. (((exists ff_h_pfp_left_constant_coefficient_K. ff_h_pfp_left_constant_coefficient_K + S (k) = S ((S (0)) * kc)) /\ exists ff_q_pfp_left_constant_coefficient_K. kb = ff_q_pfp_left_constant_coefficient_K * S ((S (0)) * kc) + (k))) -> (exists pfa_gap_left_constant_coefficient_index. pfa_gap_left_constant_coefficient_index + S (i) = (L)) -> (((exists ff_h_pfp_left_constant_coefficient_A. ff_h_pfp_left_constant_coefficient_A + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_left_constant_coefficient_A. ab = ff_q_pfp_left_constant_coefficient_A * S ((S (i)) * ac) + (a))) -> (exists pfa_gap_left_constant_coefficient_k_bound. pfa_gap_left_constant_coefficient_k_bound + S (k) = (p)) -> (exists pfa_gap_left_constant_coefficient_a_bound. pfa_gap_left_constant_coefficient_a_bound + S (a) = (p)) -> (exists pfc_terms_code_left_constant_coefficient_actual pfc_terms_scale_left_constant_coefficient_actual pfc_natural_sum_left_constant_coefficient_actual. ((forall pfc_index_left_constant_coefficient_actualdiagonal. (exists pfa_gap_left_constant_coefficient_actualdiagonalbound. pfa_gap_left_constant_coefficient_actualdiagonalbound + S (pfc_index_left_constant_coefficient_actualdiagonal) = (S (i))) -> exists pfc_value_left_constant_coefficient_actualdiagonal. ((((exists ff_h_pfp_left_constant_coefficient_actualdiagonalentry. ff_h_pfp_left_constant_coefficient_actualdiagonalentry + S (pfc_value_left_constant_coefficient_actualdiagonal) = S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * pfc_terms_scale_left_constant_coefficient_actual)) /\ exists ff_q_pfp_left_constant_coefficient_actualdiagonalentry. pfc_terms_code_left_constant_coefficient_actual = ff_q_pfp_left_constant_coefficient_actualdiagonalentry * S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * pfc_terms_scale_left_constant_coefficient_actual) + (pfc_value_left_constant_coefficient_actualdiagonal))) /\ ((exists pfc_complement_left_constant_coefficient_actualdiagonalterm pfc_left_left_constant_coefficient_actualdiagonalterm pfc_right_left_constant_coefficient_actualdiagonalterm. (((pfc_index_left_constant_coefficient_actualdiagonal)+pfc_complement_left_constant_coefficient_actualdiagonalterm=(i)) /\ ((((((exists pfa_gap_left_constant_coefficient_actualdiagonaltermleftinside. pfa_gap_left_constant_coefficient_actualdiagonaltermleftinside + S (pfc_index_left_constant_coefficient_actualdiagonal) = (1)) /\ ((((exists ff_h_pfp_left_constant_coefficient_actualdiagonaltermleftentry. ff_h_pfp_left_constant_coefficient_actualdiagonaltermleftentry + S (pfc_left_left_constant_coefficient_actualdiagonalterm) = S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * kc)) /\ exists ff_q_pfp_left_constant_coefficient_actualdiagonaltermleftentry. kb = ff_q_pfp_left_constant_coefficient_actualdiagonaltermleftentry * S ((S (pfc_index_left_constant_coefficient_actualdiagonal)) * kc) + (pfc_left_left_constant_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_coefficient_actualdiagonaltermleftoutside. pfc_gap_left_constant_coefficient_actualdiagonaltermleftoutside+(1)=(pfc_index_left_constant_coefficient_actualdiagonal)) /\ (((pfc_left_left_constant_coefficient_actualdiagonalterm)=0))))) /\ ((((((exists pfa_gap_left_constant_coefficient_actualdiagonaltermrightinside. pfa_gap_left_constant_coefficient_actualdiagonaltermrightinside + S (pfc_complement_left_constant_coefficient_actualdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_left_constant_coefficient_actualdiagonaltermrightentry. ff_h_pfp_left_constant_coefficient_actualdiagonaltermrightentry + S (pfc_right_left_constant_coefficient_actualdiagonalterm) = S ((S (pfc_complement_left_constant_coefficient_actualdiagonalterm)) * ac)) /\ exists ff_q_pfp_left_constant_coefficient_actualdiagonaltermrightentry. ab = ff_q_pfp_left_constant_coefficient_actualdiagonaltermrightentry * S ((S (pfc_complement_left_constant_coefficient_actualdiagonalterm)) * ac) + (pfc_right_left_constant_coefficient_actualdiagonalterm)))))) \/ (((exists pfc_gap_left_constant_coefficient_actualdiagonaltermrightoutside. pfc_gap_left_constant_coefficient_actualdiagonaltermrightoutside+(L)=(pfc_complement_left_constant_coefficient_actualdiagonalterm)) /\ (((pfc_right_left_constant_coefficient_actualdiagonalterm)=0))))) /\ (((pfc_value_left_constant_coefficient_actualdiagonal)=pfc_left_left_constant_coefficient_actualdiagonalterm*pfc_right_left_constant_coefficient_actualdiagonalterm))))))))))) /\ (((exists fs_u_pfc_left_constant_coefficient_actualsum fs_v_pfc_left_constant_coefficient_actualsum. ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_start. fs_h_pfc_left_constant_coefficient_actualsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_start. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_start * S ((S (0)) * fs_v_pfc_left_constant_coefficient_actualsum) + (0))) /\ ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_terminal. fs_h_pfc_left_constant_coefficient_actualsum_body_terminal + S (pfc_natural_sum_left_constant_coefficient_actual) = S ((S (S (i))) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_terminal. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_terminal * S ((S (S (i))) * fs_v_pfc_left_constant_coefficient_actualsum) + (pfc_natural_sum_left_constant_coefficient_actual))) /\ forall fs_i_pfc_left_constant_coefficient_actualsum_body_steps. (exists fs_lt_pfc_left_constant_coefficient_actualsum_body_steps_bound. fs_lt_pfc_left_constant_coefficient_actualsum_body_steps_bound + S fs_i_pfc_left_constant_coefficient_actualsum_body_steps = S (i)) -> exists fs_a_pfc_left_constant_coefficient_actualsum_body_steps fs_r_pfc_left_constant_coefficient_actualsum_body_steps fs_s_pfc_left_constant_coefficient_actualsum_body_steps. ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_steps_summand. fs_h_pfc_left_constant_coefficient_actualsum_body_steps_summand + S (fs_a_pfc_left_constant_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * pfc_terms_scale_left_constant_coefficient_actual)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_steps_summand. pfc_terms_code_left_constant_coefficient_actual = fs_q_pfc_left_constant_coefficient_actualsum_body_steps_summand * S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * pfc_terms_scale_left_constant_coefficient_actual) + (fs_a_pfc_left_constant_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_steps_partial. fs_h_pfc_left_constant_coefficient_actualsum_body_steps_partial + S (fs_r_pfc_left_constant_coefficient_actualsum_body_steps) = S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_steps_partial. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_steps_partial * S ((S (fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum) + (fs_r_pfc_left_constant_coefficient_actualsum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_coefficient_actualsum_body_steps_successor. fs_h_pfc_left_constant_coefficient_actualsum_body_steps_successor + S (fs_s_pfc_left_constant_coefficient_actualsum_body_steps) = S ((S (S fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum)) /\ exists fs_q_pfc_left_constant_coefficient_actualsum_body_steps_successor. fs_u_pfc_left_constant_coefficient_actualsum = fs_q_pfc_left_constant_coefficient_actualsum_body_steps_successor * S ((S (S fs_i_pfc_left_constant_coefficient_actualsum_body_steps)) * fs_v_pfc_left_constant_coefficient_actualsum) + (fs_s_pfc_left_constant_coefficient_actualsum_body_steps))) /\ fs_s_pfc_left_constant_coefficient_actualsum_body_steps = fs_r_pfc_left_constant_coefficient_actualsum_body_steps + fs_a_pfc_left_constant_coefficient_actualsum_body_steps)))))) /\ ((((exists pfa_gap_left_constant_coefficient_actualresiduebound. pfa_gap_left_constant_coefficient_actualresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_left_constant_coefficient_actualresiduecongruence pfa_offset_right_left_constant_coefficient_actualresiduecongruence. (pfc_natural_sum_left_constant_coefficient_actual) + (p) * pfa_offset_left_left_constant_coefficient_actualresiduecongruence = (r) + (p) * pfa_offset_right_left_constant_coefficient_actualresiduecongruence))))))))) -> (((exists pfa_gap_left_constant_coefficient_resultleft. pfa_gap_left_constant_coefficient_resultleft + S (k) = (p)) /\ (((exists pfa_gap_left_constant_coefficient_resultright. pfa_gap_left_constant_coefficient_resultright + S (a) = (p)) /\ ((((exists pfa_gap_left_constant_coefficient_resultresultbound. pfa_gap_left_constant_coefficient_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_left_constant_coefficient_resultresultcongruence pfa_offset_right_left_constant_coefficient_resultresultcongruence. ((k) * (a)) + (p) * pfa_offset_left_left_constant_coefficient_resultresultcongruence = (r) + (p) * pfa_offset_right_left_constant_coefficient_resultresultcongruence)))))))))