prime_field_convolution_prefix_left_subtract

Exact expanded first-order arithmetic statement

forall p ab ac bb bc cb cc L db dc M ub uc vb vc wb wc N. (forall pfs_index_prefix_subtract_left_source. (exists pfa_gap_prefix_subtract_left_sourceindex. pfa_gap_prefix_subtract_left_sourceindex + S (pfs_index_prefix_subtract_left_source) = (L)) -> exists pfs_left_prefix_subtract_left_source pfs_right_prefix_subtract_left_source pfs_result_prefix_subtract_left_source. ((((exists ff_h_pfp_prefix_subtract_left_sourceleft. ff_h_pfp_prefix_subtract_left_sourceleft + S (pfs_left_prefix_subtract_left_source) = S ((S (pfs_index_prefix_subtract_left_source)) * ac)) /\ exists ff_q_pfp_prefix_subtract_left_sourceleft. ab = ff_q_pfp_prefix_subtract_left_sourceleft * S ((S (pfs_index_prefix_subtract_left_source)) * ac) + (pfs_left_prefix_subtract_left_source))) /\ (((((exists ff_h_pfp_prefix_subtract_left_sourceright. ff_h_pfp_prefix_subtract_left_sourceright + S (pfs_right_prefix_subtract_left_source) = S ((S (pfs_index_prefix_subtract_left_source)) * bc)) /\ exists ff_q_pfp_prefix_subtract_left_sourceright. bb = ff_q_pfp_prefix_subtract_left_sourceright * S ((S (pfs_index_prefix_subtract_left_source)) * bc) + (pfs_right_prefix_subtract_left_source))) /\ (((((exists ff_h_pfp_prefix_subtract_left_sourceresult. ff_h_pfp_prefix_subtract_left_sourceresult + S (pfs_result_prefix_subtract_left_source) = S ((S (pfs_index_prefix_subtract_left_source)) * cc)) /\ exists ff_q_pfp_prefix_subtract_left_sourceresult. cb = ff_q_pfp_prefix_subtract_left_sourceresult * S ((S (pfs_index_prefix_subtract_left_source)) * cc) + (pfs_result_prefix_subtract_left_source))) /\ ((((exists pfa_gap_prefix_subtract_left_sourceoperationleft. pfa_gap_prefix_subtract_left_sourceoperationleft + S (pfs_right_prefix_subtract_left_source) = (p)) /\ (((exists pfa_gap_prefix_subtract_left_sourceoperationright. pfa_gap_prefix_subtract_left_sourceoperationright + S (pfs_result_prefix_subtract_left_source) = (p)) /\ ((((exists pfa_gap_prefix_subtract_left_sourceoperationresultbound. pfa_gap_prefix_subtract_left_sourceoperationresultbound + S (pfs_left_prefix_subtract_left_source) = (p)) /\ ((exists pfa_offset_left_prefix_subtract_left_sourceoperationresultcongruence pfa_offset_right_prefix_subtract_left_sourceoperationresultcongruence. ((pfs_right_prefix_subtract_left_source) + (pfs_result_prefix_subtract_left_source)) + (p) * pfa_offset_left_prefix_subtract_left_sourceoperationresultcongruence = (pfs_left_prefix_subtract_left_source) + (p) * pfa_offset_right_prefix_subtract_left_sourceoperationresultcongruence)))))))))))))))) -> (forall pfc_index_prefix_subtract_left_ub. (exists pfa_gap_prefix_subtract_left_ubbound. pfa_gap_prefix_subtract_left_ubbound + S (pfc_index_prefix_subtract_left_ub) = (N)) -> exists pfc_value_prefix_subtract_left_ub. ((((exists ff_h_pfp_prefix_subtract_left_ubentry. ff_h_pfp_prefix_subtract_left_ubentry + S (pfc_value_prefix_subtract_left_ub) = S ((S (pfc_index_prefix_subtract_left_ub)) * uc)) /\ exists ff_q_pfp_prefix_subtract_left_ubentry. ub = ff_q_pfp_prefix_subtract_left_ubentry * S ((S (pfc_index_prefix_subtract_left_ub)) * uc) + (pfc_value_prefix_subtract_left_ub))) /\ ((exists pfc_terms_code_prefix_subtract_left_ubcoefficient pfc_terms_scale_prefix_subtract_left_ubcoefficient pfc_natural_sum_prefix_subtract_left_ubcoefficient. ((forall pfc_index_prefix_subtract_left_ubcoefficientdiagonal. (exists pfa_gap_prefix_subtract_left_ubcoefficientdiagonalbound. pfa_gap_prefix_subtract_left_ubcoefficientdiagonalbound + S (pfc_index_prefix_subtract_left_ubcoefficientdiagonal) = (S (pfc_index_prefix_subtract_left_ub))) -> exists pfc_value_prefix_subtract_left_ubcoefficientdiagonal. ((((exists ff_h_pfp_prefix_subtract_left_ubcoefficientdiagonalentry. ff_h_pfp_prefix_subtract_left_ubcoefficientdiagonalentry + S (pfc_value_prefix_subtract_left_ubcoefficientdiagonal) = S ((S (pfc_index_prefix_subtract_left_ubcoefficientdiagonal)) * pfc_terms_scale_prefix_subtract_left_ubcoefficient)) /\ exists ff_q_pfp_prefix_subtract_left_ubcoefficientdiagonalentry. pfc_terms_code_prefix_subtract_left_ubcoefficient = ff_q_pfp_prefix_subtract_left_ubcoefficientdiagonalentry * S ((S (pfc_index_prefix_subtract_left_ubcoefficientdiagonal)) * pfc_terms_scale_prefix_subtract_left_ubcoefficient) + (pfc_value_prefix_subtract_left_ubcoefficientdiagonal))) /\ ((exists pfc_complement_prefix_subtract_left_ubcoefficientdiagonalterm pfc_left_prefix_subtract_left_ubcoefficientdiagonalterm pfc_right_prefix_subtract_left_ubcoefficientdiagonalterm. (((pfc_index_prefix_subtract_left_ubcoefficientdiagonal)+pfc_complement_prefix_subtract_left_ubcoefficientdiagonalterm=(pfc_index_prefix_subtract_left_ub)) /\ ((((((exists pfa_gap_prefix_subtract_left_ubcoefficientdiagonaltermleftinside. pfa_gap_prefix_subtract_left_ubcoefficientdiagonaltermleftinside + S (pfc_index_prefix_subtract_left_ubcoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_prefix_subtract_left_ubcoefficientdiagonaltermleftentry. ff_h_pfp_prefix_subtract_left_ubcoefficientdiagonaltermleftentry + S (pfc_left_prefix_subtract_left_ubcoefficientdiagonalterm) = S ((S (pfc_index_prefix_subtract_left_ubcoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_prefix_subtract_left_ubcoefficientdiagonaltermleftentry. db = ff_q_pfp_prefix_subtract_left_ubcoefficientdiagonaltermleftentry * S ((S (pfc_index_prefix_subtract_left_ubcoefficientdiagonal)) * dc) + (pfc_left_prefix_subtract_left_ubcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_prefix_subtract_left_ubcoefficientdiagonaltermleftoutside. pfc_gap_prefix_subtract_left_ubcoefficientdiagonaltermleftoutside+(M)=(pfc_index_prefix_subtract_left_ubcoefficientdiagonal)) /\ (((pfc_left_prefix_subtract_left_ubcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_subtract_left_ubcoefficientdiagonaltermrightinside. pfa_gap_prefix_subtract_left_ubcoefficientdiagonaltermrightinside + S (pfc_complement_prefix_subtract_left_ubcoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_prefix_subtract_left_ubcoefficientdiagonaltermrightentry. ff_h_pfp_prefix_subtract_left_ubcoefficientdiagonaltermrightentry + S (pfc_right_prefix_subtract_left_ubcoefficientdiagonalterm) = S ((S (pfc_complement_prefix_subtract_left_ubcoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_prefix_subtract_left_ubcoefficientdiagonaltermrightentry. ab = ff_q_pfp_prefix_subtract_left_ubcoefficientdiagonaltermrightentry * S ((S (pfc_complement_prefix_subtract_left_ubcoefficientdiagonalterm)) * ac) + (pfc_right_prefix_subtract_left_ubcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_prefix_subtract_left_ubcoefficientdiagonaltermrightoutside. pfc_gap_prefix_subtract_left_ubcoefficientdiagonaltermrightoutside+(L)=(pfc_complement_prefix_subtract_left_ubcoefficientdiagonalterm)) /\ (((pfc_right_prefix_subtract_left_ubcoefficientdiagonalterm)=0))))) /\ (((pfc_value_prefix_subtract_left_ubcoefficientdiagonal)=pfc_left_prefix_subtract_left_ubcoefficientdiagonalterm*pfc_right_prefix_subtract_left_ubcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_subtract_left_ubcoefficientsum fs_v_pfc_prefix_subtract_left_ubcoefficientsum. ((((exists fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_start. fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_start. fs_u_pfc_prefix_subtract_left_ubcoefficientsum = fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_terminal. fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_terminal + S (pfc_natural_sum_prefix_subtract_left_ubcoefficient) = S ((S (S (pfc_index_prefix_subtract_left_ub))) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_terminal. fs_u_pfc_prefix_subtract_left_ubcoefficientsum = fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_terminal * S ((S (S (pfc_index_prefix_subtract_left_ub))) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum) + (pfc_natural_sum_prefix_subtract_left_ubcoefficient))) /\ forall fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps. (exists fs_lt_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_bound. fs_lt_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_bound + S fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps = S (pfc_index_prefix_subtract_left_ub)) -> exists fs_a_pfc_prefix_subtract_left_ubcoefficientsum_body_steps fs_r_pfc_prefix_subtract_left_ubcoefficientsum_body_steps fs_s_pfc_prefix_subtract_left_ubcoefficientsum_body_steps. ((((exists fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_summand. fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_summand + S (fs_a_pfc_prefix_subtract_left_ubcoefficientsum_body_steps) = S ((S (fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps)) * pfc_terms_scale_prefix_subtract_left_ubcoefficient)) /\ exists fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_summand. pfc_terms_code_prefix_subtract_left_ubcoefficient = fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps)) * pfc_terms_scale_prefix_subtract_left_ubcoefficient) + (fs_a_pfc_prefix_subtract_left_ubcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_partial. fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_partial + S (fs_r_pfc_prefix_subtract_left_ubcoefficientsum_body_steps) = S ((S (fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_partial. fs_u_pfc_prefix_subtract_left_ubcoefficientsum = fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum) + (fs_r_pfc_prefix_subtract_left_ubcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_successor. fs_h_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_successor + S (fs_s_pfc_prefix_subtract_left_ubcoefficientsum_body_steps) = S ((S (S fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_successor. fs_u_pfc_prefix_subtract_left_ubcoefficientsum = fs_q_pfc_prefix_subtract_left_ubcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_prefix_subtract_left_ubcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_ubcoefficientsum) + (fs_s_pfc_prefix_subtract_left_ubcoefficientsum_body_steps))) /\ fs_s_pfc_prefix_subtract_left_ubcoefficientsum_body_steps = fs_r_pfc_prefix_subtract_left_ubcoefficientsum_body_steps + fs_a_pfc_prefix_subtract_left_ubcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_prefix_subtract_left_ubcoefficientresiduebound. pfa_gap_prefix_subtract_left_ubcoefficientresiduebound + S (pfc_value_prefix_subtract_left_ub) = (p)) /\ ((exists pfa_offset_left_prefix_subtract_left_ubcoefficientresiduecongruence pfa_offset_right_prefix_subtract_left_ubcoefficientresiduecongruence. (pfc_natural_sum_prefix_subtract_left_ubcoefficient) + (p) * pfa_offset_left_prefix_subtract_left_ubcoefficientresiduecongruence = (pfc_value_prefix_subtract_left_ub) + (p) * pfa_offset_right_prefix_subtract_left_ubcoefficientresiduecongruence)))))))))))) -> (forall pfc_index_prefix_subtract_left_vb. (exists pfa_gap_prefix_subtract_left_vbbound. pfa_gap_prefix_subtract_left_vbbound + S (pfc_index_prefix_subtract_left_vb) = (N)) -> exists pfc_value_prefix_subtract_left_vb. ((((exists ff_h_pfp_prefix_subtract_left_vbentry. ff_h_pfp_prefix_subtract_left_vbentry + S (pfc_value_prefix_subtract_left_vb) = S ((S (pfc_index_prefix_subtract_left_vb)) * vc)) /\ exists ff_q_pfp_prefix_subtract_left_vbentry. vb = ff_q_pfp_prefix_subtract_left_vbentry * S ((S (pfc_index_prefix_subtract_left_vb)) * vc) + (pfc_value_prefix_subtract_left_vb))) /\ ((exists pfc_terms_code_prefix_subtract_left_vbcoefficient pfc_terms_scale_prefix_subtract_left_vbcoefficient pfc_natural_sum_prefix_subtract_left_vbcoefficient. ((forall pfc_index_prefix_subtract_left_vbcoefficientdiagonal. (exists pfa_gap_prefix_subtract_left_vbcoefficientdiagonalbound. pfa_gap_prefix_subtract_left_vbcoefficientdiagonalbound + S (pfc_index_prefix_subtract_left_vbcoefficientdiagonal) = (S (pfc_index_prefix_subtract_left_vb))) -> exists pfc_value_prefix_subtract_left_vbcoefficientdiagonal. ((((exists ff_h_pfp_prefix_subtract_left_vbcoefficientdiagonalentry. ff_h_pfp_prefix_subtract_left_vbcoefficientdiagonalentry + S (pfc_value_prefix_subtract_left_vbcoefficientdiagonal) = S ((S (pfc_index_prefix_subtract_left_vbcoefficientdiagonal)) * pfc_terms_scale_prefix_subtract_left_vbcoefficient)) /\ exists ff_q_pfp_prefix_subtract_left_vbcoefficientdiagonalentry. pfc_terms_code_prefix_subtract_left_vbcoefficient = ff_q_pfp_prefix_subtract_left_vbcoefficientdiagonalentry * S ((S (pfc_index_prefix_subtract_left_vbcoefficientdiagonal)) * pfc_terms_scale_prefix_subtract_left_vbcoefficient) + (pfc_value_prefix_subtract_left_vbcoefficientdiagonal))) /\ ((exists pfc_complement_prefix_subtract_left_vbcoefficientdiagonalterm pfc_left_prefix_subtract_left_vbcoefficientdiagonalterm pfc_right_prefix_subtract_left_vbcoefficientdiagonalterm. (((pfc_index_prefix_subtract_left_vbcoefficientdiagonal)+pfc_complement_prefix_subtract_left_vbcoefficientdiagonalterm=(pfc_index_prefix_subtract_left_vb)) /\ ((((((exists pfa_gap_prefix_subtract_left_vbcoefficientdiagonaltermleftinside. pfa_gap_prefix_subtract_left_vbcoefficientdiagonaltermleftinside + S (pfc_index_prefix_subtract_left_vbcoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_prefix_subtract_left_vbcoefficientdiagonaltermleftentry. ff_h_pfp_prefix_subtract_left_vbcoefficientdiagonaltermleftentry + S (pfc_left_prefix_subtract_left_vbcoefficientdiagonalterm) = S ((S (pfc_index_prefix_subtract_left_vbcoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_prefix_subtract_left_vbcoefficientdiagonaltermleftentry. db = ff_q_pfp_prefix_subtract_left_vbcoefficientdiagonaltermleftentry * S ((S (pfc_index_prefix_subtract_left_vbcoefficientdiagonal)) * dc) + (pfc_left_prefix_subtract_left_vbcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_prefix_subtract_left_vbcoefficientdiagonaltermleftoutside. pfc_gap_prefix_subtract_left_vbcoefficientdiagonaltermleftoutside+(M)=(pfc_index_prefix_subtract_left_vbcoefficientdiagonal)) /\ (((pfc_left_prefix_subtract_left_vbcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_subtract_left_vbcoefficientdiagonaltermrightinside. pfa_gap_prefix_subtract_left_vbcoefficientdiagonaltermrightinside + S (pfc_complement_prefix_subtract_left_vbcoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_prefix_subtract_left_vbcoefficientdiagonaltermrightentry. ff_h_pfp_prefix_subtract_left_vbcoefficientdiagonaltermrightentry + S (pfc_right_prefix_subtract_left_vbcoefficientdiagonalterm) = S ((S (pfc_complement_prefix_subtract_left_vbcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_prefix_subtract_left_vbcoefficientdiagonaltermrightentry. bb = ff_q_pfp_prefix_subtract_left_vbcoefficientdiagonaltermrightentry * S ((S (pfc_complement_prefix_subtract_left_vbcoefficientdiagonalterm)) * bc) + (pfc_right_prefix_subtract_left_vbcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_prefix_subtract_left_vbcoefficientdiagonaltermrightoutside. pfc_gap_prefix_subtract_left_vbcoefficientdiagonaltermrightoutside+(L)=(pfc_complement_prefix_subtract_left_vbcoefficientdiagonalterm)) /\ (((pfc_right_prefix_subtract_left_vbcoefficientdiagonalterm)=0))))) /\ (((pfc_value_prefix_subtract_left_vbcoefficientdiagonal)=pfc_left_prefix_subtract_left_vbcoefficientdiagonalterm*pfc_right_prefix_subtract_left_vbcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_subtract_left_vbcoefficientsum fs_v_pfc_prefix_subtract_left_vbcoefficientsum. ((((exists fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_start. fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_start. fs_u_pfc_prefix_subtract_left_vbcoefficientsum = fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_terminal. fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_terminal + S (pfc_natural_sum_prefix_subtract_left_vbcoefficient) = S ((S (S (pfc_index_prefix_subtract_left_vb))) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_terminal. fs_u_pfc_prefix_subtract_left_vbcoefficientsum = fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_terminal * S ((S (S (pfc_index_prefix_subtract_left_vb))) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum) + (pfc_natural_sum_prefix_subtract_left_vbcoefficient))) /\ forall fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps. (exists fs_lt_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_bound. fs_lt_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_bound + S fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps = S (pfc_index_prefix_subtract_left_vb)) -> exists fs_a_pfc_prefix_subtract_left_vbcoefficientsum_body_steps fs_r_pfc_prefix_subtract_left_vbcoefficientsum_body_steps fs_s_pfc_prefix_subtract_left_vbcoefficientsum_body_steps. ((((exists fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_summand. fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_summand + S (fs_a_pfc_prefix_subtract_left_vbcoefficientsum_body_steps) = S ((S (fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps)) * pfc_terms_scale_prefix_subtract_left_vbcoefficient)) /\ exists fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_summand. pfc_terms_code_prefix_subtract_left_vbcoefficient = fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps)) * pfc_terms_scale_prefix_subtract_left_vbcoefficient) + (fs_a_pfc_prefix_subtract_left_vbcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_partial. fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_partial + S (fs_r_pfc_prefix_subtract_left_vbcoefficientsum_body_steps) = S ((S (fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_partial. fs_u_pfc_prefix_subtract_left_vbcoefficientsum = fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum) + (fs_r_pfc_prefix_subtract_left_vbcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_successor. fs_h_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_successor + S (fs_s_pfc_prefix_subtract_left_vbcoefficientsum_body_steps) = S ((S (S fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_successor. fs_u_pfc_prefix_subtract_left_vbcoefficientsum = fs_q_pfc_prefix_subtract_left_vbcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_prefix_subtract_left_vbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_vbcoefficientsum) + (fs_s_pfc_prefix_subtract_left_vbcoefficientsum_body_steps))) /\ fs_s_pfc_prefix_subtract_left_vbcoefficientsum_body_steps = fs_r_pfc_prefix_subtract_left_vbcoefficientsum_body_steps + fs_a_pfc_prefix_subtract_left_vbcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_prefix_subtract_left_vbcoefficientresiduebound. pfa_gap_prefix_subtract_left_vbcoefficientresiduebound + S (pfc_value_prefix_subtract_left_vb) = (p)) /\ ((exists pfa_offset_left_prefix_subtract_left_vbcoefficientresiduecongruence pfa_offset_right_prefix_subtract_left_vbcoefficientresiduecongruence. (pfc_natural_sum_prefix_subtract_left_vbcoefficient) + (p) * pfa_offset_left_prefix_subtract_left_vbcoefficientresiduecongruence = (pfc_value_prefix_subtract_left_vb) + (p) * pfa_offset_right_prefix_subtract_left_vbcoefficientresiduecongruence)))))))))))) -> (forall pfc_index_prefix_subtract_left_wb. (exists pfa_gap_prefix_subtract_left_wbbound. pfa_gap_prefix_subtract_left_wbbound + S (pfc_index_prefix_subtract_left_wb) = (N)) -> exists pfc_value_prefix_subtract_left_wb. ((((exists ff_h_pfp_prefix_subtract_left_wbentry. ff_h_pfp_prefix_subtract_left_wbentry + S (pfc_value_prefix_subtract_left_wb) = S ((S (pfc_index_prefix_subtract_left_wb)) * wc)) /\ exists ff_q_pfp_prefix_subtract_left_wbentry. wb = ff_q_pfp_prefix_subtract_left_wbentry * S ((S (pfc_index_prefix_subtract_left_wb)) * wc) + (pfc_value_prefix_subtract_left_wb))) /\ ((exists pfc_terms_code_prefix_subtract_left_wbcoefficient pfc_terms_scale_prefix_subtract_left_wbcoefficient pfc_natural_sum_prefix_subtract_left_wbcoefficient. ((forall pfc_index_prefix_subtract_left_wbcoefficientdiagonal. (exists pfa_gap_prefix_subtract_left_wbcoefficientdiagonalbound. pfa_gap_prefix_subtract_left_wbcoefficientdiagonalbound + S (pfc_index_prefix_subtract_left_wbcoefficientdiagonal) = (S (pfc_index_prefix_subtract_left_wb))) -> exists pfc_value_prefix_subtract_left_wbcoefficientdiagonal. ((((exists ff_h_pfp_prefix_subtract_left_wbcoefficientdiagonalentry. ff_h_pfp_prefix_subtract_left_wbcoefficientdiagonalentry + S (pfc_value_prefix_subtract_left_wbcoefficientdiagonal) = S ((S (pfc_index_prefix_subtract_left_wbcoefficientdiagonal)) * pfc_terms_scale_prefix_subtract_left_wbcoefficient)) /\ exists ff_q_pfp_prefix_subtract_left_wbcoefficientdiagonalentry. pfc_terms_code_prefix_subtract_left_wbcoefficient = ff_q_pfp_prefix_subtract_left_wbcoefficientdiagonalentry * S ((S (pfc_index_prefix_subtract_left_wbcoefficientdiagonal)) * pfc_terms_scale_prefix_subtract_left_wbcoefficient) + (pfc_value_prefix_subtract_left_wbcoefficientdiagonal))) /\ ((exists pfc_complement_prefix_subtract_left_wbcoefficientdiagonalterm pfc_left_prefix_subtract_left_wbcoefficientdiagonalterm pfc_right_prefix_subtract_left_wbcoefficientdiagonalterm. (((pfc_index_prefix_subtract_left_wbcoefficientdiagonal)+pfc_complement_prefix_subtract_left_wbcoefficientdiagonalterm=(pfc_index_prefix_subtract_left_wb)) /\ ((((((exists pfa_gap_prefix_subtract_left_wbcoefficientdiagonaltermleftinside. pfa_gap_prefix_subtract_left_wbcoefficientdiagonaltermleftinside + S (pfc_index_prefix_subtract_left_wbcoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_prefix_subtract_left_wbcoefficientdiagonaltermleftentry. ff_h_pfp_prefix_subtract_left_wbcoefficientdiagonaltermleftentry + S (pfc_left_prefix_subtract_left_wbcoefficientdiagonalterm) = S ((S (pfc_index_prefix_subtract_left_wbcoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_prefix_subtract_left_wbcoefficientdiagonaltermleftentry. db = ff_q_pfp_prefix_subtract_left_wbcoefficientdiagonaltermleftentry * S ((S (pfc_index_prefix_subtract_left_wbcoefficientdiagonal)) * dc) + (pfc_left_prefix_subtract_left_wbcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_prefix_subtract_left_wbcoefficientdiagonaltermleftoutside. pfc_gap_prefix_subtract_left_wbcoefficientdiagonaltermleftoutside+(M)=(pfc_index_prefix_subtract_left_wbcoefficientdiagonal)) /\ (((pfc_left_prefix_subtract_left_wbcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_prefix_subtract_left_wbcoefficientdiagonaltermrightinside. pfa_gap_prefix_subtract_left_wbcoefficientdiagonaltermrightinside + S (pfc_complement_prefix_subtract_left_wbcoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_prefix_subtract_left_wbcoefficientdiagonaltermrightentry. ff_h_pfp_prefix_subtract_left_wbcoefficientdiagonaltermrightentry + S (pfc_right_prefix_subtract_left_wbcoefficientdiagonalterm) = S ((S (pfc_complement_prefix_subtract_left_wbcoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_prefix_subtract_left_wbcoefficientdiagonaltermrightentry. cb = ff_q_pfp_prefix_subtract_left_wbcoefficientdiagonaltermrightentry * S ((S (pfc_complement_prefix_subtract_left_wbcoefficientdiagonalterm)) * cc) + (pfc_right_prefix_subtract_left_wbcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_prefix_subtract_left_wbcoefficientdiagonaltermrightoutside. pfc_gap_prefix_subtract_left_wbcoefficientdiagonaltermrightoutside+(L)=(pfc_complement_prefix_subtract_left_wbcoefficientdiagonalterm)) /\ (((pfc_right_prefix_subtract_left_wbcoefficientdiagonalterm)=0))))) /\ (((pfc_value_prefix_subtract_left_wbcoefficientdiagonal)=pfc_left_prefix_subtract_left_wbcoefficientdiagonalterm*pfc_right_prefix_subtract_left_wbcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_prefix_subtract_left_wbcoefficientsum fs_v_pfc_prefix_subtract_left_wbcoefficientsum. ((((exists fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_start. fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_start. fs_u_pfc_prefix_subtract_left_wbcoefficientsum = fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_terminal. fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_terminal + S (pfc_natural_sum_prefix_subtract_left_wbcoefficient) = S ((S (S (pfc_index_prefix_subtract_left_wb))) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_terminal. fs_u_pfc_prefix_subtract_left_wbcoefficientsum = fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_terminal * S ((S (S (pfc_index_prefix_subtract_left_wb))) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum) + (pfc_natural_sum_prefix_subtract_left_wbcoefficient))) /\ forall fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps. (exists fs_lt_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_bound. fs_lt_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_bound + S fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps = S (pfc_index_prefix_subtract_left_wb)) -> exists fs_a_pfc_prefix_subtract_left_wbcoefficientsum_body_steps fs_r_pfc_prefix_subtract_left_wbcoefficientsum_body_steps fs_s_pfc_prefix_subtract_left_wbcoefficientsum_body_steps. ((((exists fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_summand. fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_summand + S (fs_a_pfc_prefix_subtract_left_wbcoefficientsum_body_steps) = S ((S (fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps)) * pfc_terms_scale_prefix_subtract_left_wbcoefficient)) /\ exists fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_summand. pfc_terms_code_prefix_subtract_left_wbcoefficient = fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps)) * pfc_terms_scale_prefix_subtract_left_wbcoefficient) + (fs_a_pfc_prefix_subtract_left_wbcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_partial. fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_partial + S (fs_r_pfc_prefix_subtract_left_wbcoefficientsum_body_steps) = S ((S (fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_partial. fs_u_pfc_prefix_subtract_left_wbcoefficientsum = fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum) + (fs_r_pfc_prefix_subtract_left_wbcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_successor. fs_h_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_successor + S (fs_s_pfc_prefix_subtract_left_wbcoefficientsum_body_steps) = S ((S (S fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum)) /\ exists fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_successor. fs_u_pfc_prefix_subtract_left_wbcoefficientsum = fs_q_pfc_prefix_subtract_left_wbcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_prefix_subtract_left_wbcoefficientsum_body_steps)) * fs_v_pfc_prefix_subtract_left_wbcoefficientsum) + (fs_s_pfc_prefix_subtract_left_wbcoefficientsum_body_steps))) /\ fs_s_pfc_prefix_subtract_left_wbcoefficientsum_body_steps = fs_r_pfc_prefix_subtract_left_wbcoefficientsum_body_steps + fs_a_pfc_prefix_subtract_left_wbcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_prefix_subtract_left_wbcoefficientresiduebound. pfa_gap_prefix_subtract_left_wbcoefficientresiduebound + S (pfc_value_prefix_subtract_left_wb) = (p)) /\ ((exists pfa_offset_left_prefix_subtract_left_wbcoefficientresiduecongruence pfa_offset_right_prefix_subtract_left_wbcoefficientresiduecongruence. (pfc_natural_sum_prefix_subtract_left_wbcoefficient) + (p) * pfa_offset_left_prefix_subtract_left_wbcoefficientresiduecongruence = (pfc_value_prefix_subtract_left_wb) + (p) * pfa_offset_right_prefix_subtract_left_wbcoefficientresiduecongruence)))))))))))) -> (forall pfs_index_prefix_subtract_left_result. (exists pfa_gap_prefix_subtract_left_resultindex. pfa_gap_prefix_subtract_left_resultindex + S (pfs_index_prefix_subtract_left_result) = (N)) -> exists pfs_left_prefix_subtract_left_result pfs_right_prefix_subtract_left_result pfs_result_prefix_subtract_left_result. ((((exists ff_h_pfp_prefix_subtract_left_resultleft. ff_h_pfp_prefix_subtract_left_resultleft + S (pfs_left_prefix_subtract_left_result) = S ((S (pfs_index_prefix_subtract_left_result)) * uc)) /\ exists ff_q_pfp_prefix_subtract_left_resultleft. ub = ff_q_pfp_prefix_subtract_left_resultleft * S ((S (pfs_index_prefix_subtract_left_result)) * uc) + (pfs_left_prefix_subtract_left_result))) /\ (((((exists ff_h_pfp_prefix_subtract_left_resultright. ff_h_pfp_prefix_subtract_left_resultright + S (pfs_right_prefix_subtract_left_result) = S ((S (pfs_index_prefix_subtract_left_result)) * vc)) /\ exists ff_q_pfp_prefix_subtract_left_resultright. vb = ff_q_pfp_prefix_subtract_left_resultright * S ((S (pfs_index_prefix_subtract_left_result)) * vc) + (pfs_right_prefix_subtract_left_result))) /\ (((((exists ff_h_pfp_prefix_subtract_left_resultresult. ff_h_pfp_prefix_subtract_left_resultresult + S (pfs_result_prefix_subtract_left_result) = S ((S (pfs_index_prefix_subtract_left_result)) * wc)) /\ exists ff_q_pfp_prefix_subtract_left_resultresult. wb = ff_q_pfp_prefix_subtract_left_resultresult * S ((S (pfs_index_prefix_subtract_left_result)) * wc) + (pfs_result_prefix_subtract_left_result))) /\ ((((exists pfa_gap_prefix_subtract_left_resultoperationleft. pfa_gap_prefix_subtract_left_resultoperationleft + S (pfs_right_prefix_subtract_left_result) = (p)) /\ (((exists pfa_gap_prefix_subtract_left_resultoperationright. pfa_gap_prefix_subtract_left_resultoperationright + S (pfs_result_prefix_subtract_left_result) = (p)) /\ ((((exists pfa_gap_prefix_subtract_left_resultoperationresultbound. pfa_gap_prefix_subtract_left_resultoperationresultbound + S (pfs_left_prefix_subtract_left_result) = (p)) /\ ((exists pfa_offset_left_prefix_subtract_left_resultoperationresultcongruence pfa_offset_right_prefix_subtract_left_resultoperationresultcongruence. ((pfs_right_prefix_subtract_left_result) + (pfs_result_prefix_subtract_left_result)) + (p) * pfa_offset_left_prefix_subtract_left_resultoperationresultcongruence = (pfs_left_prefix_subtract_left_result) + (p) * pfa_offset_right_prefix_subtract_left_resultoperationresultcongruence))))))))))))))))