prime_field_convolution_coefficient_left_add

Exact expanded first-order arithmetic statement

forall p ab ac bb bc cb cc L db dc M i u v w. (forall pfp_index_coefficient_add_left_source. (exists pfa_gap_coefficient_add_left_sourceindex. pfa_gap_coefficient_add_left_sourceindex + S (pfp_index_coefficient_add_left_source) = (L)) -> exists pfp_left_coefficient_add_left_source pfp_right_coefficient_add_left_source pfp_value_coefficient_add_left_source. ((((exists ff_h_pfp_coefficient_add_left_sourceleft. ff_h_pfp_coefficient_add_left_sourceleft + S (pfp_left_coefficient_add_left_source) = S ((S (pfp_index_coefficient_add_left_source)) * ac)) /\ exists ff_q_pfp_coefficient_add_left_sourceleft. ab = ff_q_pfp_coefficient_add_left_sourceleft * S ((S (pfp_index_coefficient_add_left_source)) * ac) + (pfp_left_coefficient_add_left_source))) /\ (((((exists ff_h_pfp_coefficient_add_left_sourceright. ff_h_pfp_coefficient_add_left_sourceright + S (pfp_right_coefficient_add_left_source) = S ((S (pfp_index_coefficient_add_left_source)) * bc)) /\ exists ff_q_pfp_coefficient_add_left_sourceright. bb = ff_q_pfp_coefficient_add_left_sourceright * S ((S (pfp_index_coefficient_add_left_source)) * bc) + (pfp_right_coefficient_add_left_source))) /\ (((((exists ff_h_pfp_coefficient_add_left_sourcetarget. ff_h_pfp_coefficient_add_left_sourcetarget + S (pfp_value_coefficient_add_left_source) = S ((S (pfp_index_coefficient_add_left_source)) * cc)) /\ exists ff_q_pfp_coefficient_add_left_sourcetarget. cb = ff_q_pfp_coefficient_add_left_sourcetarget * S ((S (pfp_index_coefficient_add_left_source)) * cc) + (pfp_value_coefficient_add_left_source))) /\ ((((exists pfa_gap_coefficient_add_left_sourceoperationleft. pfa_gap_coefficient_add_left_sourceoperationleft + S (pfp_left_coefficient_add_left_source) = (p)) /\ (((exists pfa_gap_coefficient_add_left_sourceoperationright. pfa_gap_coefficient_add_left_sourceoperationright + S (pfp_right_coefficient_add_left_source) = (p)) /\ ((((exists pfa_gap_coefficient_add_left_sourceoperationresultbound. pfa_gap_coefficient_add_left_sourceoperationresultbound + S (pfp_value_coefficient_add_left_source) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_sourceoperationresultcongruence pfa_offset_right_coefficient_add_left_sourceoperationresultcongruence. ((pfp_left_coefficient_add_left_source) + (pfp_right_coefficient_add_left_source)) + (p) * pfa_offset_left_coefficient_add_left_sourceoperationresultcongruence = (pfp_value_coefficient_add_left_source) + (p) * pfa_offset_right_coefficient_add_left_sourceoperationresultcongruence)))))))))))))))) -> (exists pfc_terms_code_coefficient_add_left_u pfc_terms_scale_coefficient_add_left_u pfc_natural_sum_coefficient_add_left_u. ((forall pfc_index_coefficient_add_left_udiagonal. (exists pfa_gap_coefficient_add_left_udiagonalbound. pfa_gap_coefficient_add_left_udiagonalbound + S (pfc_index_coefficient_add_left_udiagonal) = (S (i))) -> exists pfc_value_coefficient_add_left_udiagonal. ((((exists ff_h_pfp_coefficient_add_left_udiagonalentry. ff_h_pfp_coefficient_add_left_udiagonalentry + S (pfc_value_coefficient_add_left_udiagonal) = S ((S (pfc_index_coefficient_add_left_udiagonal)) * pfc_terms_scale_coefficient_add_left_u)) /\ exists ff_q_pfp_coefficient_add_left_udiagonalentry. pfc_terms_code_coefficient_add_left_u = ff_q_pfp_coefficient_add_left_udiagonalentry * S ((S (pfc_index_coefficient_add_left_udiagonal)) * pfc_terms_scale_coefficient_add_left_u) + (pfc_value_coefficient_add_left_udiagonal))) /\ ((exists pfc_complement_coefficient_add_left_udiagonalterm pfc_left_coefficient_add_left_udiagonalterm pfc_right_coefficient_add_left_udiagonalterm. (((pfc_index_coefficient_add_left_udiagonal)+pfc_complement_coefficient_add_left_udiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_add_left_udiagonaltermleftinside. pfa_gap_coefficient_add_left_udiagonaltermleftinside + S (pfc_index_coefficient_add_left_udiagonal) = (M)) /\ ((((exists ff_h_pfp_coefficient_add_left_udiagonaltermleftentry. ff_h_pfp_coefficient_add_left_udiagonaltermleftentry + S (pfc_left_coefficient_add_left_udiagonalterm) = S ((S (pfc_index_coefficient_add_left_udiagonal)) * dc)) /\ exists ff_q_pfp_coefficient_add_left_udiagonaltermleftentry. db = ff_q_pfp_coefficient_add_left_udiagonaltermleftentry * S ((S (pfc_index_coefficient_add_left_udiagonal)) * dc) + (pfc_left_coefficient_add_left_udiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_udiagonaltermleftoutside. pfc_gap_coefficient_add_left_udiagonaltermleftoutside+(M)=(pfc_index_coefficient_add_left_udiagonal)) /\ (((pfc_left_coefficient_add_left_udiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_add_left_udiagonaltermrightinside. pfa_gap_coefficient_add_left_udiagonaltermrightinside + S (pfc_complement_coefficient_add_left_udiagonalterm) = (L)) /\ ((((exists ff_h_pfp_coefficient_add_left_udiagonaltermrightentry. ff_h_pfp_coefficient_add_left_udiagonaltermrightentry + S (pfc_right_coefficient_add_left_udiagonalterm) = S ((S (pfc_complement_coefficient_add_left_udiagonalterm)) * ac)) /\ exists ff_q_pfp_coefficient_add_left_udiagonaltermrightentry. ab = ff_q_pfp_coefficient_add_left_udiagonaltermrightentry * S ((S (pfc_complement_coefficient_add_left_udiagonalterm)) * ac) + (pfc_right_coefficient_add_left_udiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_udiagonaltermrightoutside. pfc_gap_coefficient_add_left_udiagonaltermrightoutside+(L)=(pfc_complement_coefficient_add_left_udiagonalterm)) /\ (((pfc_right_coefficient_add_left_udiagonalterm)=0))))) /\ (((pfc_value_coefficient_add_left_udiagonal)=pfc_left_coefficient_add_left_udiagonalterm*pfc_right_coefficient_add_left_udiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_add_left_usum fs_v_pfc_coefficient_add_left_usum. ((((exists fs_h_pfc_coefficient_add_left_usum_body_start. fs_h_pfc_coefficient_add_left_usum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_start. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_start * S ((S (0)) * fs_v_pfc_coefficient_add_left_usum) + (0))) /\ ((((exists fs_h_pfc_coefficient_add_left_usum_body_terminal. fs_h_pfc_coefficient_add_left_usum_body_terminal + S (pfc_natural_sum_coefficient_add_left_u) = S ((S (S (i))) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_terminal. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_add_left_usum) + (pfc_natural_sum_coefficient_add_left_u))) /\ forall fs_i_pfc_coefficient_add_left_usum_body_steps. (exists fs_lt_pfc_coefficient_add_left_usum_body_steps_bound. fs_lt_pfc_coefficient_add_left_usum_body_steps_bound + S fs_i_pfc_coefficient_add_left_usum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_add_left_usum_body_steps fs_r_pfc_coefficient_add_left_usum_body_steps fs_s_pfc_coefficient_add_left_usum_body_steps. ((((exists fs_h_pfc_coefficient_add_left_usum_body_steps_summand. fs_h_pfc_coefficient_add_left_usum_body_steps_summand + S (fs_a_pfc_coefficient_add_left_usum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * pfc_terms_scale_coefficient_add_left_u)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_steps_summand. pfc_terms_code_coefficient_add_left_u = fs_q_pfc_coefficient_add_left_usum_body_steps_summand * S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * pfc_terms_scale_coefficient_add_left_u) + (fs_a_pfc_coefficient_add_left_usum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_usum_body_steps_partial. fs_h_pfc_coefficient_add_left_usum_body_steps_partial + S (fs_r_pfc_coefficient_add_left_usum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_steps_partial. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_steps_partial * S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum) + (fs_r_pfc_coefficient_add_left_usum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_usum_body_steps_successor. fs_h_pfc_coefficient_add_left_usum_body_steps_successor + S (fs_s_pfc_coefficient_add_left_usum_body_steps) = S ((S (S fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_steps_successor. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum) + (fs_s_pfc_coefficient_add_left_usum_body_steps))) /\ fs_s_pfc_coefficient_add_left_usum_body_steps = fs_r_pfc_coefficient_add_left_usum_body_steps + fs_a_pfc_coefficient_add_left_usum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_add_left_uresiduebound. pfa_gap_coefficient_add_left_uresiduebound + S (u) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_uresiduecongruence pfa_offset_right_coefficient_add_left_uresiduecongruence. (pfc_natural_sum_coefficient_add_left_u) + (p) * pfa_offset_left_coefficient_add_left_uresiduecongruence = (u) + (p) * pfa_offset_right_coefficient_add_left_uresiduecongruence))))))))) -> (exists pfc_terms_code_coefficient_add_left_v pfc_terms_scale_coefficient_add_left_v pfc_natural_sum_coefficient_add_left_v. ((forall pfc_index_coefficient_add_left_vdiagonal. (exists pfa_gap_coefficient_add_left_vdiagonalbound. pfa_gap_coefficient_add_left_vdiagonalbound + S (pfc_index_coefficient_add_left_vdiagonal) = (S (i))) -> exists pfc_value_coefficient_add_left_vdiagonal. ((((exists ff_h_pfp_coefficient_add_left_vdiagonalentry. ff_h_pfp_coefficient_add_left_vdiagonalentry + S (pfc_value_coefficient_add_left_vdiagonal) = S ((S (pfc_index_coefficient_add_left_vdiagonal)) * pfc_terms_scale_coefficient_add_left_v)) /\ exists ff_q_pfp_coefficient_add_left_vdiagonalentry. pfc_terms_code_coefficient_add_left_v = ff_q_pfp_coefficient_add_left_vdiagonalentry * S ((S (pfc_index_coefficient_add_left_vdiagonal)) * pfc_terms_scale_coefficient_add_left_v) + (pfc_value_coefficient_add_left_vdiagonal))) /\ ((exists pfc_complement_coefficient_add_left_vdiagonalterm pfc_left_coefficient_add_left_vdiagonalterm pfc_right_coefficient_add_left_vdiagonalterm. (((pfc_index_coefficient_add_left_vdiagonal)+pfc_complement_coefficient_add_left_vdiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_add_left_vdiagonaltermleftinside. pfa_gap_coefficient_add_left_vdiagonaltermleftinside + S (pfc_index_coefficient_add_left_vdiagonal) = (M)) /\ ((((exists ff_h_pfp_coefficient_add_left_vdiagonaltermleftentry. ff_h_pfp_coefficient_add_left_vdiagonaltermleftentry + S (pfc_left_coefficient_add_left_vdiagonalterm) = S ((S (pfc_index_coefficient_add_left_vdiagonal)) * dc)) /\ exists ff_q_pfp_coefficient_add_left_vdiagonaltermleftentry. db = ff_q_pfp_coefficient_add_left_vdiagonaltermleftentry * S ((S (pfc_index_coefficient_add_left_vdiagonal)) * dc) + (pfc_left_coefficient_add_left_vdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_vdiagonaltermleftoutside. pfc_gap_coefficient_add_left_vdiagonaltermleftoutside+(M)=(pfc_index_coefficient_add_left_vdiagonal)) /\ (((pfc_left_coefficient_add_left_vdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_add_left_vdiagonaltermrightinside. pfa_gap_coefficient_add_left_vdiagonaltermrightinside + S (pfc_complement_coefficient_add_left_vdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_coefficient_add_left_vdiagonaltermrightentry. ff_h_pfp_coefficient_add_left_vdiagonaltermrightentry + S (pfc_right_coefficient_add_left_vdiagonalterm) = S ((S (pfc_complement_coefficient_add_left_vdiagonalterm)) * bc)) /\ exists ff_q_pfp_coefficient_add_left_vdiagonaltermrightentry. bb = ff_q_pfp_coefficient_add_left_vdiagonaltermrightentry * S ((S (pfc_complement_coefficient_add_left_vdiagonalterm)) * bc) + (pfc_right_coefficient_add_left_vdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_vdiagonaltermrightoutside. pfc_gap_coefficient_add_left_vdiagonaltermrightoutside+(L)=(pfc_complement_coefficient_add_left_vdiagonalterm)) /\ (((pfc_right_coefficient_add_left_vdiagonalterm)=0))))) /\ (((pfc_value_coefficient_add_left_vdiagonal)=pfc_left_coefficient_add_left_vdiagonalterm*pfc_right_coefficient_add_left_vdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_add_left_vsum fs_v_pfc_coefficient_add_left_vsum. ((((exists fs_h_pfc_coefficient_add_left_vsum_body_start. fs_h_pfc_coefficient_add_left_vsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_start. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_add_left_vsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_add_left_vsum_body_terminal. fs_h_pfc_coefficient_add_left_vsum_body_terminal + S (pfc_natural_sum_coefficient_add_left_v) = S ((S (S (i))) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_terminal. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_add_left_vsum) + (pfc_natural_sum_coefficient_add_left_v))) /\ forall fs_i_pfc_coefficient_add_left_vsum_body_steps. (exists fs_lt_pfc_coefficient_add_left_vsum_body_steps_bound. fs_lt_pfc_coefficient_add_left_vsum_body_steps_bound + S fs_i_pfc_coefficient_add_left_vsum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_add_left_vsum_body_steps fs_r_pfc_coefficient_add_left_vsum_body_steps fs_s_pfc_coefficient_add_left_vsum_body_steps. ((((exists fs_h_pfc_coefficient_add_left_vsum_body_steps_summand. fs_h_pfc_coefficient_add_left_vsum_body_steps_summand + S (fs_a_pfc_coefficient_add_left_vsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * pfc_terms_scale_coefficient_add_left_v)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_steps_summand. pfc_terms_code_coefficient_add_left_v = fs_q_pfc_coefficient_add_left_vsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * pfc_terms_scale_coefficient_add_left_v) + (fs_a_pfc_coefficient_add_left_vsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_vsum_body_steps_partial. fs_h_pfc_coefficient_add_left_vsum_body_steps_partial + S (fs_r_pfc_coefficient_add_left_vsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_steps_partial. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum) + (fs_r_pfc_coefficient_add_left_vsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_vsum_body_steps_successor. fs_h_pfc_coefficient_add_left_vsum_body_steps_successor + S (fs_s_pfc_coefficient_add_left_vsum_body_steps) = S ((S (S fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_steps_successor. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum) + (fs_s_pfc_coefficient_add_left_vsum_body_steps))) /\ fs_s_pfc_coefficient_add_left_vsum_body_steps = fs_r_pfc_coefficient_add_left_vsum_body_steps + fs_a_pfc_coefficient_add_left_vsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_add_left_vresiduebound. pfa_gap_coefficient_add_left_vresiduebound + S (v) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_vresiduecongruence pfa_offset_right_coefficient_add_left_vresiduecongruence. (pfc_natural_sum_coefficient_add_left_v) + (p) * pfa_offset_left_coefficient_add_left_vresiduecongruence = (v) + (p) * pfa_offset_right_coefficient_add_left_vresiduecongruence))))))))) -> (exists pfc_terms_code_coefficient_add_left_w pfc_terms_scale_coefficient_add_left_w pfc_natural_sum_coefficient_add_left_w. ((forall pfc_index_coefficient_add_left_wdiagonal. (exists pfa_gap_coefficient_add_left_wdiagonalbound. pfa_gap_coefficient_add_left_wdiagonalbound + S (pfc_index_coefficient_add_left_wdiagonal) = (S (i))) -> exists pfc_value_coefficient_add_left_wdiagonal. ((((exists ff_h_pfp_coefficient_add_left_wdiagonalentry. ff_h_pfp_coefficient_add_left_wdiagonalentry + S (pfc_value_coefficient_add_left_wdiagonal) = S ((S (pfc_index_coefficient_add_left_wdiagonal)) * pfc_terms_scale_coefficient_add_left_w)) /\ exists ff_q_pfp_coefficient_add_left_wdiagonalentry. pfc_terms_code_coefficient_add_left_w = ff_q_pfp_coefficient_add_left_wdiagonalentry * S ((S (pfc_index_coefficient_add_left_wdiagonal)) * pfc_terms_scale_coefficient_add_left_w) + (pfc_value_coefficient_add_left_wdiagonal))) /\ ((exists pfc_complement_coefficient_add_left_wdiagonalterm pfc_left_coefficient_add_left_wdiagonalterm pfc_right_coefficient_add_left_wdiagonalterm. (((pfc_index_coefficient_add_left_wdiagonal)+pfc_complement_coefficient_add_left_wdiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_add_left_wdiagonaltermleftinside. pfa_gap_coefficient_add_left_wdiagonaltermleftinside + S (pfc_index_coefficient_add_left_wdiagonal) = (M)) /\ ((((exists ff_h_pfp_coefficient_add_left_wdiagonaltermleftentry. ff_h_pfp_coefficient_add_left_wdiagonaltermleftentry + S (pfc_left_coefficient_add_left_wdiagonalterm) = S ((S (pfc_index_coefficient_add_left_wdiagonal)) * dc)) /\ exists ff_q_pfp_coefficient_add_left_wdiagonaltermleftentry. db = ff_q_pfp_coefficient_add_left_wdiagonaltermleftentry * S ((S (pfc_index_coefficient_add_left_wdiagonal)) * dc) + (pfc_left_coefficient_add_left_wdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_wdiagonaltermleftoutside. pfc_gap_coefficient_add_left_wdiagonaltermleftoutside+(M)=(pfc_index_coefficient_add_left_wdiagonal)) /\ (((pfc_left_coefficient_add_left_wdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_add_left_wdiagonaltermrightinside. pfa_gap_coefficient_add_left_wdiagonaltermrightinside + S (pfc_complement_coefficient_add_left_wdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_coefficient_add_left_wdiagonaltermrightentry. ff_h_pfp_coefficient_add_left_wdiagonaltermrightentry + S (pfc_right_coefficient_add_left_wdiagonalterm) = S ((S (pfc_complement_coefficient_add_left_wdiagonalterm)) * cc)) /\ exists ff_q_pfp_coefficient_add_left_wdiagonaltermrightentry. cb = ff_q_pfp_coefficient_add_left_wdiagonaltermrightentry * S ((S (pfc_complement_coefficient_add_left_wdiagonalterm)) * cc) + (pfc_right_coefficient_add_left_wdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_wdiagonaltermrightoutside. pfc_gap_coefficient_add_left_wdiagonaltermrightoutside+(L)=(pfc_complement_coefficient_add_left_wdiagonalterm)) /\ (((pfc_right_coefficient_add_left_wdiagonalterm)=0))))) /\ (((pfc_value_coefficient_add_left_wdiagonal)=pfc_left_coefficient_add_left_wdiagonalterm*pfc_right_coefficient_add_left_wdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_add_left_wsum fs_v_pfc_coefficient_add_left_wsum. ((((exists fs_h_pfc_coefficient_add_left_wsum_body_start. fs_h_pfc_coefficient_add_left_wsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_start. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_add_left_wsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_add_left_wsum_body_terminal. fs_h_pfc_coefficient_add_left_wsum_body_terminal + S (pfc_natural_sum_coefficient_add_left_w) = S ((S (S (i))) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_terminal. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_add_left_wsum) + (pfc_natural_sum_coefficient_add_left_w))) /\ forall fs_i_pfc_coefficient_add_left_wsum_body_steps. (exists fs_lt_pfc_coefficient_add_left_wsum_body_steps_bound. fs_lt_pfc_coefficient_add_left_wsum_body_steps_bound + S fs_i_pfc_coefficient_add_left_wsum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_add_left_wsum_body_steps fs_r_pfc_coefficient_add_left_wsum_body_steps fs_s_pfc_coefficient_add_left_wsum_body_steps. ((((exists fs_h_pfc_coefficient_add_left_wsum_body_steps_summand. fs_h_pfc_coefficient_add_left_wsum_body_steps_summand + S (fs_a_pfc_coefficient_add_left_wsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * pfc_terms_scale_coefficient_add_left_w)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_steps_summand. pfc_terms_code_coefficient_add_left_w = fs_q_pfc_coefficient_add_left_wsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * pfc_terms_scale_coefficient_add_left_w) + (fs_a_pfc_coefficient_add_left_wsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_wsum_body_steps_partial. fs_h_pfc_coefficient_add_left_wsum_body_steps_partial + S (fs_r_pfc_coefficient_add_left_wsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_steps_partial. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum) + (fs_r_pfc_coefficient_add_left_wsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_wsum_body_steps_successor. fs_h_pfc_coefficient_add_left_wsum_body_steps_successor + S (fs_s_pfc_coefficient_add_left_wsum_body_steps) = S ((S (S fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_steps_successor. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum) + (fs_s_pfc_coefficient_add_left_wsum_body_steps))) /\ fs_s_pfc_coefficient_add_left_wsum_body_steps = fs_r_pfc_coefficient_add_left_wsum_body_steps + fs_a_pfc_coefficient_add_left_wsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_add_left_wresiduebound. pfa_gap_coefficient_add_left_wresiduebound + S (w) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_wresiduecongruence pfa_offset_right_coefficient_add_left_wresiduecongruence. (pfc_natural_sum_coefficient_add_left_w) + (p) * pfa_offset_left_coefficient_add_left_wresiduecongruence = (w) + (p) * pfa_offset_right_coefficient_add_left_wresiduecongruence))))))))) -> (((exists pfa_gap_coefficient_add_left_resultleft. pfa_gap_coefficient_add_left_resultleft + S (u) = (p)) /\ (((exists pfa_gap_coefficient_add_left_resultright. pfa_gap_coefficient_add_left_resultright + S (v) = (p)) /\ ((((exists pfa_gap_coefficient_add_left_resultresultbound. pfa_gap_coefficient_add_left_resultresultbound + S (w) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_resultresultcongruence pfa_offset_right_coefficient_add_left_resultresultcongruence. ((u) + (v)) + (p) * pfa_offset_left_coefficient_add_left_resultresultcongruence = (w) + (p) * pfa_offset_right_coefficient_add_left_resultresultcongruence)))))))))