prime_field_convolution_coefficient_append

Exact expanded first-order arithmetic statement

forall p ab ac AB AC bb bc d N a b c t r. (forall mdr_i_pfp_tri_append_prefix mdr_a_pfp_tri_append_prefix. (exists mdr_gap_pfp_tri_append_prefixb. mdr_gap_pfp_tri_append_prefixb + S (mdr_i_pfp_tri_append_prefix) = (N)) -> (((exists ff_h_mdr_pfp_tri_append_prefixo. ff_h_mdr_pfp_tri_append_prefixo + S (mdr_a_pfp_tri_append_prefix) = S ((S (mdr_i_pfp_tri_append_prefix)) * ac)) /\ exists ff_q_mdr_pfp_tri_append_prefixo. ab = ff_q_mdr_pfp_tri_append_prefixo * S ((S (mdr_i_pfp_tri_append_prefix)) * ac) + (mdr_a_pfp_tri_append_prefix))) -> (((exists ff_h_mdr_pfp_tri_append_prefixn. ff_h_mdr_pfp_tri_append_prefixn + S (mdr_a_pfp_tri_append_prefix) = S ((S (mdr_i_pfp_tri_append_prefix)) * AC)) /\ exists ff_q_mdr_pfp_tri_append_prefixn. AB = ff_q_mdr_pfp_tri_append_prefixn * S ((S (mdr_i_pfp_tri_append_prefix)) * AC) + (mdr_a_pfp_tri_append_prefix)))) -> (((exists ff_h_pfp_tri_append_actual_entry. ff_h_pfp_tri_append_actual_entry + S (a) = S ((S (N)) * AC)) /\ exists ff_q_pfp_tri_append_actual_entry. AB = ff_q_pfp_tri_append_actual_entry * S ((S (N)) * AC) + (a))) -> (((exists ff_h_pfp_tri_append_actual_head. ff_h_pfp_tri_append_actual_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_tri_append_actual_head. bb = ff_q_pfp_tri_append_actual_head * S ((S (0)) * bc) + (b))) -> (exists pfc_terms_code_tri_append_previous_coefficient pfc_terms_scale_tri_append_previous_coefficient pfc_natural_sum_tri_append_previous_coefficient. ((forall pfc_index_tri_append_previous_coefficientdiagonal. (exists pfa_gap_tri_append_previous_coefficientdiagonalbound. pfa_gap_tri_append_previous_coefficientdiagonalbound + S (pfc_index_tri_append_previous_coefficientdiagonal) = (S (N))) -> exists pfc_value_tri_append_previous_coefficientdiagonal. ((((exists ff_h_pfp_tri_append_previous_coefficientdiagonalentry. ff_h_pfp_tri_append_previous_coefficientdiagonalentry + S (pfc_value_tri_append_previous_coefficientdiagonal) = S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * pfc_terms_scale_tri_append_previous_coefficient)) /\ exists ff_q_pfp_tri_append_previous_coefficientdiagonalentry. pfc_terms_code_tri_append_previous_coefficient = ff_q_pfp_tri_append_previous_coefficientdiagonalentry * S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * pfc_terms_scale_tri_append_previous_coefficient) + (pfc_value_tri_append_previous_coefficientdiagonal))) /\ ((exists pfc_complement_tri_append_previous_coefficientdiagonalterm pfc_left_tri_append_previous_coefficientdiagonalterm pfc_right_tri_append_previous_coefficientdiagonalterm. (((pfc_index_tri_append_previous_coefficientdiagonal)+pfc_complement_tri_append_previous_coefficientdiagonalterm=(N)) /\ ((((((exists pfa_gap_tri_append_previous_coefficientdiagonaltermleftinside. pfa_gap_tri_append_previous_coefficientdiagonaltermleftinside + S (pfc_index_tri_append_previous_coefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_tri_append_previous_coefficientdiagonaltermleftentry. ff_h_pfp_tri_append_previous_coefficientdiagonaltermleftentry + S (pfc_left_tri_append_previous_coefficientdiagonalterm) = S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_tri_append_previous_coefficientdiagonaltermleftentry. ab = ff_q_pfp_tri_append_previous_coefficientdiagonaltermleftentry * S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * ac) + (pfc_left_tri_append_previous_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_previous_coefficientdiagonaltermleftoutside. pfc_gap_tri_append_previous_coefficientdiagonaltermleftoutside+(N)=(pfc_index_tri_append_previous_coefficientdiagonal)) /\ (((pfc_left_tri_append_previous_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_previous_coefficientdiagonaltermrightinside. pfa_gap_tri_append_previous_coefficientdiagonaltermrightinside + S (pfc_complement_tri_append_previous_coefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_tri_append_previous_coefficientdiagonaltermrightentry. ff_h_pfp_tri_append_previous_coefficientdiagonaltermrightentry + S (pfc_right_tri_append_previous_coefficientdiagonalterm) = S ((S (pfc_complement_tri_append_previous_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_previous_coefficientdiagonaltermrightentry. bb = ff_q_pfp_tri_append_previous_coefficientdiagonaltermrightentry * S ((S (pfc_complement_tri_append_previous_coefficientdiagonalterm)) * bc) + (pfc_right_tri_append_previous_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_previous_coefficientdiagonaltermrightoutside. pfc_gap_tri_append_previous_coefficientdiagonaltermrightoutside+(S d)=(pfc_complement_tri_append_previous_coefficientdiagonalterm)) /\ (((pfc_right_tri_append_previous_coefficientdiagonalterm)=0))))) /\ (((pfc_value_tri_append_previous_coefficientdiagonal)=pfc_left_tri_append_previous_coefficientdiagonalterm*pfc_right_tri_append_previous_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_previous_coefficientsum fs_v_pfc_tri_append_previous_coefficientsum. ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_start. fs_h_pfc_tri_append_previous_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_start. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_previous_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_terminal. fs_h_pfc_tri_append_previous_coefficientsum_body_terminal + S (pfc_natural_sum_tri_append_previous_coefficient) = S ((S (S (N))) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_terminal. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_terminal * S ((S (S (N))) * fs_v_pfc_tri_append_previous_coefficientsum) + (pfc_natural_sum_tri_append_previous_coefficient))) /\ forall fs_i_pfc_tri_append_previous_coefficientsum_body_steps. (exists fs_lt_pfc_tri_append_previous_coefficientsum_body_steps_bound. fs_lt_pfc_tri_append_previous_coefficientsum_body_steps_bound + S fs_i_pfc_tri_append_previous_coefficientsum_body_steps = S (N)) -> exists fs_a_pfc_tri_append_previous_coefficientsum_body_steps fs_r_pfc_tri_append_previous_coefficientsum_body_steps fs_s_pfc_tri_append_previous_coefficientsum_body_steps. ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_steps_summand. fs_h_pfc_tri_append_previous_coefficientsum_body_steps_summand + S (fs_a_pfc_tri_append_previous_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_previous_coefficient)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_steps_summand. pfc_terms_code_tri_append_previous_coefficient = fs_q_pfc_tri_append_previous_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_previous_coefficient) + (fs_a_pfc_tri_append_previous_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_steps_partial. fs_h_pfc_tri_append_previous_coefficientsum_body_steps_partial + S (fs_r_pfc_tri_append_previous_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_steps_partial. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum) + (fs_r_pfc_tri_append_previous_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_steps_successor. fs_h_pfc_tri_append_previous_coefficientsum_body_steps_successor + S (fs_s_pfc_tri_append_previous_coefficientsum_body_steps) = S ((S (S fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_steps_successor. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum) + (fs_s_pfc_tri_append_previous_coefficientsum_body_steps))) /\ fs_s_pfc_tri_append_previous_coefficientsum_body_steps = fs_r_pfc_tri_append_previous_coefficientsum_body_steps + fs_a_pfc_tri_append_previous_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_previous_coefficientresiduebound. pfa_gap_tri_append_previous_coefficientresiduebound + S (c) = (p)) /\ ((exists pfa_offset_left_tri_append_previous_coefficientresiduecongruence pfa_offset_right_tri_append_previous_coefficientresiduecongruence. (pfc_natural_sum_tri_append_previous_coefficient) + (p) * pfa_offset_left_tri_append_previous_coefficientresiduecongruence = (c) + (p) * pfa_offset_right_tri_append_previous_coefficientresiduecongruence))))))))) -> (exists pfc_terms_code_tri_append_actual_coefficient pfc_terms_scale_tri_append_actual_coefficient pfc_natural_sum_tri_append_actual_coefficient. ((forall pfc_index_tri_append_actual_coefficientdiagonal. (exists pfa_gap_tri_append_actual_coefficientdiagonalbound. pfa_gap_tri_append_actual_coefficientdiagonalbound + S (pfc_index_tri_append_actual_coefficientdiagonal) = (S (N))) -> exists pfc_value_tri_append_actual_coefficientdiagonal. ((((exists ff_h_pfp_tri_append_actual_coefficientdiagonalentry. ff_h_pfp_tri_append_actual_coefficientdiagonalentry + S (pfc_value_tri_append_actual_coefficientdiagonal) = S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * pfc_terms_scale_tri_append_actual_coefficient)) /\ exists ff_q_pfp_tri_append_actual_coefficientdiagonalentry. pfc_terms_code_tri_append_actual_coefficient = ff_q_pfp_tri_append_actual_coefficientdiagonalentry * S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * pfc_terms_scale_tri_append_actual_coefficient) + (pfc_value_tri_append_actual_coefficientdiagonal))) /\ ((exists pfc_complement_tri_append_actual_coefficientdiagonalterm pfc_left_tri_append_actual_coefficientdiagonalterm pfc_right_tri_append_actual_coefficientdiagonalterm. (((pfc_index_tri_append_actual_coefficientdiagonal)+pfc_complement_tri_append_actual_coefficientdiagonalterm=(N)) /\ ((((((exists pfa_gap_tri_append_actual_coefficientdiagonaltermleftinside. pfa_gap_tri_append_actual_coefficientdiagonaltermleftinside + S (pfc_index_tri_append_actual_coefficientdiagonal) = (S N)) /\ ((((exists ff_h_pfp_tri_append_actual_coefficientdiagonaltermleftentry. ff_h_pfp_tri_append_actual_coefficientdiagonaltermleftentry + S (pfc_left_tri_append_actual_coefficientdiagonalterm) = S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * AC)) /\ exists ff_q_pfp_tri_append_actual_coefficientdiagonaltermleftentry. AB = ff_q_pfp_tri_append_actual_coefficientdiagonaltermleftentry * S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * AC) + (pfc_left_tri_append_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_actual_coefficientdiagonaltermleftoutside. pfc_gap_tri_append_actual_coefficientdiagonaltermleftoutside+(S N)=(pfc_index_tri_append_actual_coefficientdiagonal)) /\ (((pfc_left_tri_append_actual_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_actual_coefficientdiagonaltermrightinside. pfa_gap_tri_append_actual_coefficientdiagonaltermrightinside + S (pfc_complement_tri_append_actual_coefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_tri_append_actual_coefficientdiagonaltermrightentry. ff_h_pfp_tri_append_actual_coefficientdiagonaltermrightentry + S (pfc_right_tri_append_actual_coefficientdiagonalterm) = S ((S (pfc_complement_tri_append_actual_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_actual_coefficientdiagonaltermrightentry. bb = ff_q_pfp_tri_append_actual_coefficientdiagonaltermrightentry * S ((S (pfc_complement_tri_append_actual_coefficientdiagonalterm)) * bc) + (pfc_right_tri_append_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_actual_coefficientdiagonaltermrightoutside. pfc_gap_tri_append_actual_coefficientdiagonaltermrightoutside+(S d)=(pfc_complement_tri_append_actual_coefficientdiagonalterm)) /\ (((pfc_right_tri_append_actual_coefficientdiagonalterm)=0))))) /\ (((pfc_value_tri_append_actual_coefficientdiagonal)=pfc_left_tri_append_actual_coefficientdiagonalterm*pfc_right_tri_append_actual_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_actual_coefficientsum fs_v_pfc_tri_append_actual_coefficientsum. ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_start. fs_h_pfc_tri_append_actual_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_start. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_actual_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_terminal. fs_h_pfc_tri_append_actual_coefficientsum_body_terminal + S (pfc_natural_sum_tri_append_actual_coefficient) = S ((S (S (N))) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_terminal. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_terminal * S ((S (S (N))) * fs_v_pfc_tri_append_actual_coefficientsum) + (pfc_natural_sum_tri_append_actual_coefficient))) /\ forall fs_i_pfc_tri_append_actual_coefficientsum_body_steps. (exists fs_lt_pfc_tri_append_actual_coefficientsum_body_steps_bound. fs_lt_pfc_tri_append_actual_coefficientsum_body_steps_bound + S fs_i_pfc_tri_append_actual_coefficientsum_body_steps = S (N)) -> exists fs_a_pfc_tri_append_actual_coefficientsum_body_steps fs_r_pfc_tri_append_actual_coefficientsum_body_steps fs_s_pfc_tri_append_actual_coefficientsum_body_steps. ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_steps_summand. fs_h_pfc_tri_append_actual_coefficientsum_body_steps_summand + S (fs_a_pfc_tri_append_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_actual_coefficient)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_steps_summand. pfc_terms_code_tri_append_actual_coefficient = fs_q_pfc_tri_append_actual_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_actual_coefficient) + (fs_a_pfc_tri_append_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_steps_partial. fs_h_pfc_tri_append_actual_coefficientsum_body_steps_partial + S (fs_r_pfc_tri_append_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_steps_partial. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum) + (fs_r_pfc_tri_append_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_steps_successor. fs_h_pfc_tri_append_actual_coefficientsum_body_steps_successor + S (fs_s_pfc_tri_append_actual_coefficientsum_body_steps) = S ((S (S fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_steps_successor. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum) + (fs_s_pfc_tri_append_actual_coefficientsum_body_steps))) /\ fs_s_pfc_tri_append_actual_coefficientsum_body_steps = fs_r_pfc_tri_append_actual_coefficientsum_body_steps + fs_a_pfc_tri_append_actual_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_actual_coefficientresiduebound. pfa_gap_tri_append_actual_coefficientresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_actual_coefficientresiduecongruence pfa_offset_right_tri_append_actual_coefficientresiduecongruence. (pfc_natural_sum_tri_append_actual_coefficient) + (p) * pfa_offset_left_tri_append_actual_coefficientresiduecongruence = (r) + (p) * pfa_offset_right_tri_append_actual_coefficientresiduecongruence))))))))) -> (((exists pfa_gap_tri_append_actual_productleft. pfa_gap_tri_append_actual_productleft + S (a) = (p)) /\ (((exists pfa_gap_tri_append_actual_productright. pfa_gap_tri_append_actual_productright + S (b) = (p)) /\ ((((exists pfa_gap_tri_append_actual_productresultbound. pfa_gap_tri_append_actual_productresultbound + S (t) = (p)) /\ ((exists pfa_offset_left_tri_append_actual_productresultcongruence pfa_offset_right_tri_append_actual_productresultcongruence. ((a) * (b)) + (p) * pfa_offset_left_tri_append_actual_productresultcongruence = (t) + (p) * pfa_offset_right_tri_append_actual_productresultcongruence))))))))) -> (((exists pfa_gap_tri_append_resultleft. pfa_gap_tri_append_resultleft + S (c) = (p)) /\ (((exists pfa_gap_tri_append_resultright. pfa_gap_tri_append_resultright + S (t) = (p)) /\ ((((exists pfa_gap_tri_append_resultresultbound. pfa_gap_tri_append_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_resultresultcongruence pfa_offset_right_tri_append_resultresultcongruence. ((c) + (t)) + (p) * pfa_offset_left_tri_append_resultresultcongruence = (r) + (p) * pfa_offset_right_tri_append_resultresultcongruence)))))))))