prime_field_convolution_coefficient_prefix_transport

Exact expanded first-order arithmetic statement

forall p ab ac L AB AC K bb bc M N i r. (exists pfc_gap_tri_coefficient_old_length. pfc_gap_tri_coefficient_old_length+(N)=(L)) -> (exists pfc_gap_tri_coefficient_new_length. pfc_gap_tri_coefficient_new_length+(N)=(K)) -> (forall mdr_i_pfp_tri_coefficient_equal mdr_a_pfp_tri_coefficient_equal. (exists mdr_gap_pfp_tri_coefficient_equalb. mdr_gap_pfp_tri_coefficient_equalb + S (mdr_i_pfp_tri_coefficient_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_coefficient_equalo. ff_h_mdr_pfp_tri_coefficient_equalo + S (mdr_a_pfp_tri_coefficient_equal) = S ((S (mdr_i_pfp_tri_coefficient_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_coefficient_equalo. ab = ff_q_mdr_pfp_tri_coefficient_equalo * S ((S (mdr_i_pfp_tri_coefficient_equal)) * ac) + (mdr_a_pfp_tri_coefficient_equal))) -> (((exists ff_h_mdr_pfp_tri_coefficient_equaln. ff_h_mdr_pfp_tri_coefficient_equaln + S (mdr_a_pfp_tri_coefficient_equal) = S ((S (mdr_i_pfp_tri_coefficient_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_coefficient_equaln. AB = ff_q_mdr_pfp_tri_coefficient_equaln * S ((S (mdr_i_pfp_tri_coefficient_equal)) * AC) + (mdr_a_pfp_tri_coefficient_equal)))) -> (exists pfa_gap_tri_coefficient_index. pfa_gap_tri_coefficient_index + S (i) = (N)) -> (exists pfc_terms_code_tri_coefficient_old pfc_terms_scale_tri_coefficient_old pfc_natural_sum_tri_coefficient_old. ((forall pfc_index_tri_coefficient_olddiagonal. (exists pfa_gap_tri_coefficient_olddiagonalbound. pfa_gap_tri_coefficient_olddiagonalbound + S (pfc_index_tri_coefficient_olddiagonal) = (S (i))) -> exists pfc_value_tri_coefficient_olddiagonal. ((((exists ff_h_pfp_tri_coefficient_olddiagonalentry. ff_h_pfp_tri_coefficient_olddiagonalentry + S (pfc_value_tri_coefficient_olddiagonal) = S ((S (pfc_index_tri_coefficient_olddiagonal)) * pfc_terms_scale_tri_coefficient_old)) /\ exists ff_q_pfp_tri_coefficient_olddiagonalentry. pfc_terms_code_tri_coefficient_old = ff_q_pfp_tri_coefficient_olddiagonalentry * S ((S (pfc_index_tri_coefficient_olddiagonal)) * pfc_terms_scale_tri_coefficient_old) + (pfc_value_tri_coefficient_olddiagonal))) /\ ((exists pfc_complement_tri_coefficient_olddiagonalterm pfc_left_tri_coefficient_olddiagonalterm pfc_right_tri_coefficient_olddiagonalterm. (((pfc_index_tri_coefficient_olddiagonal)+pfc_complement_tri_coefficient_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_coefficient_olddiagonaltermleftinside. pfa_gap_tri_coefficient_olddiagonaltermleftinside + S (pfc_index_tri_coefficient_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_tri_coefficient_olddiagonaltermleftentry. ff_h_pfp_tri_coefficient_olddiagonaltermleftentry + S (pfc_left_tri_coefficient_olddiagonalterm) = S ((S (pfc_index_tri_coefficient_olddiagonal)) * ac)) /\ exists ff_q_pfp_tri_coefficient_olddiagonaltermleftentry. ab = ff_q_pfp_tri_coefficient_olddiagonaltermleftentry * S ((S (pfc_index_tri_coefficient_olddiagonal)) * ac) + (pfc_left_tri_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_olddiagonaltermleftoutside. pfc_gap_tri_coefficient_olddiagonaltermleftoutside+(L)=(pfc_index_tri_coefficient_olddiagonal)) /\ (((pfc_left_tri_coefficient_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_coefficient_olddiagonaltermrightinside. pfa_gap_tri_coefficient_olddiagonaltermrightinside + S (pfc_complement_tri_coefficient_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_coefficient_olddiagonaltermrightentry. ff_h_pfp_tri_coefficient_olddiagonaltermrightentry + S (pfc_right_tri_coefficient_olddiagonalterm) = S ((S (pfc_complement_tri_coefficient_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_coefficient_olddiagonaltermrightentry. bb = ff_q_pfp_tri_coefficient_olddiagonaltermrightentry * S ((S (pfc_complement_tri_coefficient_olddiagonalterm)) * bc) + (pfc_right_tri_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_olddiagonaltermrightoutside. pfc_gap_tri_coefficient_olddiagonaltermrightoutside+(M)=(pfc_complement_tri_coefficient_olddiagonalterm)) /\ (((pfc_right_tri_coefficient_olddiagonalterm)=0))))) /\ (((pfc_value_tri_coefficient_olddiagonal)=pfc_left_tri_coefficient_olddiagonalterm*pfc_right_tri_coefficient_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_coefficient_oldsum fs_v_pfc_tri_coefficient_oldsum. ((((exists fs_h_pfc_tri_coefficient_oldsum_body_start. fs_h_pfc_tri_coefficient_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_start. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_start * S ((S (0)) * fs_v_pfc_tri_coefficient_oldsum) + (0))) /\ ((((exists fs_h_pfc_tri_coefficient_oldsum_body_terminal. fs_h_pfc_tri_coefficient_oldsum_body_terminal + S (pfc_natural_sum_tri_coefficient_old) = S ((S (S (i))) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_terminal. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_coefficient_oldsum) + (pfc_natural_sum_tri_coefficient_old))) /\ forall fs_i_pfc_tri_coefficient_oldsum_body_steps. (exists fs_lt_pfc_tri_coefficient_oldsum_body_steps_bound. fs_lt_pfc_tri_coefficient_oldsum_body_steps_bound + S fs_i_pfc_tri_coefficient_oldsum_body_steps = S (i)) -> exists fs_a_pfc_tri_coefficient_oldsum_body_steps fs_r_pfc_tri_coefficient_oldsum_body_steps fs_s_pfc_tri_coefficient_oldsum_body_steps. ((((exists fs_h_pfc_tri_coefficient_oldsum_body_steps_summand. fs_h_pfc_tri_coefficient_oldsum_body_steps_summand + S (fs_a_pfc_tri_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * pfc_terms_scale_tri_coefficient_old)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_steps_summand. pfc_terms_code_tri_coefficient_old = fs_q_pfc_tri_coefficient_oldsum_body_steps_summand * S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * pfc_terms_scale_tri_coefficient_old) + (fs_a_pfc_tri_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_oldsum_body_steps_partial. fs_h_pfc_tri_coefficient_oldsum_body_steps_partial + S (fs_r_pfc_tri_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_steps_partial. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_steps_partial * S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum) + (fs_r_pfc_tri_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_oldsum_body_steps_successor. fs_h_pfc_tri_coefficient_oldsum_body_steps_successor + S (fs_s_pfc_tri_coefficient_oldsum_body_steps) = S ((S (S fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_steps_successor. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_steps_successor * S ((S (S fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum) + (fs_s_pfc_tri_coefficient_oldsum_body_steps))) /\ fs_s_pfc_tri_coefficient_oldsum_body_steps = fs_r_pfc_tri_coefficient_oldsum_body_steps + fs_a_pfc_tri_coefficient_oldsum_body_steps)))))) /\ ((((exists pfa_gap_tri_coefficient_oldresiduebound. pfa_gap_tri_coefficient_oldresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_coefficient_oldresiduecongruence pfa_offset_right_tri_coefficient_oldresiduecongruence. (pfc_natural_sum_tri_coefficient_old) + (p) * pfa_offset_left_tri_coefficient_oldresiduecongruence = (r) + (p) * pfa_offset_right_tri_coefficient_oldresiduecongruence))))))))) -> (exists pfc_terms_code_tri_coefficient_new pfc_terms_scale_tri_coefficient_new pfc_natural_sum_tri_coefficient_new. ((forall pfc_index_tri_coefficient_newdiagonal. (exists pfa_gap_tri_coefficient_newdiagonalbound. pfa_gap_tri_coefficient_newdiagonalbound + S (pfc_index_tri_coefficient_newdiagonal) = (S (i))) -> exists pfc_value_tri_coefficient_newdiagonal. ((((exists ff_h_pfp_tri_coefficient_newdiagonalentry. ff_h_pfp_tri_coefficient_newdiagonalentry + S (pfc_value_tri_coefficient_newdiagonal) = S ((S (pfc_index_tri_coefficient_newdiagonal)) * pfc_terms_scale_tri_coefficient_new)) /\ exists ff_q_pfp_tri_coefficient_newdiagonalentry. pfc_terms_code_tri_coefficient_new = ff_q_pfp_tri_coefficient_newdiagonalentry * S ((S (pfc_index_tri_coefficient_newdiagonal)) * pfc_terms_scale_tri_coefficient_new) + (pfc_value_tri_coefficient_newdiagonal))) /\ ((exists pfc_complement_tri_coefficient_newdiagonalterm pfc_left_tri_coefficient_newdiagonalterm pfc_right_tri_coefficient_newdiagonalterm. (((pfc_index_tri_coefficient_newdiagonal)+pfc_complement_tri_coefficient_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_coefficient_newdiagonaltermleftinside. pfa_gap_tri_coefficient_newdiagonaltermleftinside + S (pfc_index_tri_coefficient_newdiagonal) = (K)) /\ ((((exists ff_h_pfp_tri_coefficient_newdiagonaltermleftentry. ff_h_pfp_tri_coefficient_newdiagonaltermleftentry + S (pfc_left_tri_coefficient_newdiagonalterm) = S ((S (pfc_index_tri_coefficient_newdiagonal)) * AC)) /\ exists ff_q_pfp_tri_coefficient_newdiagonaltermleftentry. AB = ff_q_pfp_tri_coefficient_newdiagonaltermleftentry * S ((S (pfc_index_tri_coefficient_newdiagonal)) * AC) + (pfc_left_tri_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_newdiagonaltermleftoutside. pfc_gap_tri_coefficient_newdiagonaltermleftoutside+(K)=(pfc_index_tri_coefficient_newdiagonal)) /\ (((pfc_left_tri_coefficient_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_coefficient_newdiagonaltermrightinside. pfa_gap_tri_coefficient_newdiagonaltermrightinside + S (pfc_complement_tri_coefficient_newdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_coefficient_newdiagonaltermrightentry. ff_h_pfp_tri_coefficient_newdiagonaltermrightentry + S (pfc_right_tri_coefficient_newdiagonalterm) = S ((S (pfc_complement_tri_coefficient_newdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_coefficient_newdiagonaltermrightentry. bb = ff_q_pfp_tri_coefficient_newdiagonaltermrightentry * S ((S (pfc_complement_tri_coefficient_newdiagonalterm)) * bc) + (pfc_right_tri_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_newdiagonaltermrightoutside. pfc_gap_tri_coefficient_newdiagonaltermrightoutside+(M)=(pfc_complement_tri_coefficient_newdiagonalterm)) /\ (((pfc_right_tri_coefficient_newdiagonalterm)=0))))) /\ (((pfc_value_tri_coefficient_newdiagonal)=pfc_left_tri_coefficient_newdiagonalterm*pfc_right_tri_coefficient_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_coefficient_newsum fs_v_pfc_tri_coefficient_newsum. ((((exists fs_h_pfc_tri_coefficient_newsum_body_start. fs_h_pfc_tri_coefficient_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_start. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_start * S ((S (0)) * fs_v_pfc_tri_coefficient_newsum) + (0))) /\ ((((exists fs_h_pfc_tri_coefficient_newsum_body_terminal. fs_h_pfc_tri_coefficient_newsum_body_terminal + S (pfc_natural_sum_tri_coefficient_new) = S ((S (S (i))) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_terminal. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_coefficient_newsum) + (pfc_natural_sum_tri_coefficient_new))) /\ forall fs_i_pfc_tri_coefficient_newsum_body_steps. (exists fs_lt_pfc_tri_coefficient_newsum_body_steps_bound. fs_lt_pfc_tri_coefficient_newsum_body_steps_bound + S fs_i_pfc_tri_coefficient_newsum_body_steps = S (i)) -> exists fs_a_pfc_tri_coefficient_newsum_body_steps fs_r_pfc_tri_coefficient_newsum_body_steps fs_s_pfc_tri_coefficient_newsum_body_steps. ((((exists fs_h_pfc_tri_coefficient_newsum_body_steps_summand. fs_h_pfc_tri_coefficient_newsum_body_steps_summand + S (fs_a_pfc_tri_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * pfc_terms_scale_tri_coefficient_new)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_steps_summand. pfc_terms_code_tri_coefficient_new = fs_q_pfc_tri_coefficient_newsum_body_steps_summand * S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * pfc_terms_scale_tri_coefficient_new) + (fs_a_pfc_tri_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_newsum_body_steps_partial. fs_h_pfc_tri_coefficient_newsum_body_steps_partial + S (fs_r_pfc_tri_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_steps_partial. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_steps_partial * S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum) + (fs_r_pfc_tri_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_newsum_body_steps_successor. fs_h_pfc_tri_coefficient_newsum_body_steps_successor + S (fs_s_pfc_tri_coefficient_newsum_body_steps) = S ((S (S fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_steps_successor. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_steps_successor * S ((S (S fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum) + (fs_s_pfc_tri_coefficient_newsum_body_steps))) /\ fs_s_pfc_tri_coefficient_newsum_body_steps = fs_r_pfc_tri_coefficient_newsum_body_steps + fs_a_pfc_tri_coefficient_newsum_body_steps)))))) /\ ((((exists pfa_gap_tri_coefficient_newresiduebound. pfa_gap_tri_coefficient_newresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_coefficient_newresiduecongruence pfa_offset_right_tri_coefficient_newresiduecongruence. (pfc_natural_sum_tri_coefficient_new) + (p) * pfa_offset_left_tri_coefficient_newresiduecongruence = (r) + (p) * pfa_offset_right_tri_coefficient_newresiduecongruence)))))))))