prime_field_polynomial_convolution_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_proper_left_subtract_source. (exists pfa_gap_proper_left_subtract_sourceindex. pfa_gap_proper_left_subtract_sourceindex + S (pfs_index_proper_left_subtract_source) = (L)) -> exists pfs_left_proper_left_subtract_source pfs_right_proper_left_subtract_source pfs_result_proper_left_subtract_source. ((((exists ff_h_pfp_proper_left_subtract_sourceleft. ff_h_pfp_proper_left_subtract_sourceleft + S (pfs_left_proper_left_subtract_source) = S ((S (pfs_index_proper_left_subtract_source)) * ac)) /\ exists ff_q_pfp_proper_left_subtract_sourceleft. ab = ff_q_pfp_proper_left_subtract_sourceleft * S ((S (pfs_index_proper_left_subtract_source)) * ac) + (pfs_left_proper_left_subtract_source))) /\ (((((exists ff_h_pfp_proper_left_subtract_sourceright. ff_h_pfp_proper_left_subtract_sourceright + S (pfs_right_proper_left_subtract_source) = S ((S (pfs_index_proper_left_subtract_source)) * bc)) /\ exists ff_q_pfp_proper_left_subtract_sourceright. bb = ff_q_pfp_proper_left_subtract_sourceright * S ((S (pfs_index_proper_left_subtract_source)) * bc) + (pfs_right_proper_left_subtract_source))) /\ (((((exists ff_h_pfp_proper_left_subtract_sourceresult. ff_h_pfp_proper_left_subtract_sourceresult + S (pfs_result_proper_left_subtract_source) = S ((S (pfs_index_proper_left_subtract_source)) * cc)) /\ exists ff_q_pfp_proper_left_subtract_sourceresult. cb = ff_q_pfp_proper_left_subtract_sourceresult * S ((S (pfs_index_proper_left_subtract_source)) * cc) + (pfs_result_proper_left_subtract_source))) /\ ((((exists pfa_gap_proper_left_subtract_sourceoperationleft. pfa_gap_proper_left_subtract_sourceoperationleft + S (pfs_right_proper_left_subtract_source) = (p)) /\ (((exists pfa_gap_proper_left_subtract_sourceoperationright. pfa_gap_proper_left_subtract_sourceoperationright + S (pfs_result_proper_left_subtract_source) = (p)) /\ ((((exists pfa_gap_proper_left_subtract_sourceoperationresultbound. pfa_gap_proper_left_subtract_sourceoperationresultbound + S (pfs_left_proper_left_subtract_source) = (p)) /\ ((exists pfa_offset_left_proper_left_subtract_sourceoperationresultcongruence pfa_offset_right_proper_left_subtract_sourceoperationresultcongruence. ((pfs_right_proper_left_subtract_source) + (pfs_result_proper_left_subtract_source)) + (p) * pfa_offset_left_proper_left_subtract_sourceoperationresultcongruence = (pfs_left_proper_left_subtract_source) + (p) * pfa_offset_right_proper_left_subtract_sourceoperationresultcongruence)))))))))))))))) -> (((forall fom_index_pfp_proper_left_subtract_ubleft. (exists fom_gap_pfp_proper_left_subtract_ubleft_index_bound. fom_gap_pfp_proper_left_subtract_ubleft_index_bound + S (fom_index_pfp_proper_left_subtract_ubleft) = M) -> exists fom_value_pfp_proper_left_subtract_ubleft. ((((exists fom_beta_height_pfp_proper_left_subtract_ubleft_entry. fom_beta_height_pfp_proper_left_subtract_ubleft_entry + S (fom_value_pfp_proper_left_subtract_ubleft) = S ((S (fom_index_pfp_proper_left_subtract_ubleft)) * dc)) /\ exists fom_beta_quotient_pfp_proper_left_subtract_ubleft_entry. db = fom_beta_quotient_pfp_proper_left_subtract_ubleft_entry * S ((S (fom_index_pfp_proper_left_subtract_ubleft)) * dc) + (fom_value_pfp_proper_left_subtract_ubleft))) /\ (exists fom_gap_pfp_proper_left_subtract_ubleft_value_bound. fom_gap_pfp_proper_left_subtract_ubleft_value_bound + S (fom_value_pfp_proper_left_subtract_ubleft) = p))) /\ (((forall fom_index_pfp_proper_left_subtract_ubright. (exists fom_gap_pfp_proper_left_subtract_ubright_index_bound. fom_gap_pfp_proper_left_subtract_ubright_index_bound + S (fom_index_pfp_proper_left_subtract_ubright) = L) -> exists fom_value_pfp_proper_left_subtract_ubright. ((((exists fom_beta_height_pfp_proper_left_subtract_ubright_entry. fom_beta_height_pfp_proper_left_subtract_ubright_entry + S (fom_value_pfp_proper_left_subtract_ubright) = S ((S (fom_index_pfp_proper_left_subtract_ubright)) * ac)) /\ exists fom_beta_quotient_pfp_proper_left_subtract_ubright_entry. ab = fom_beta_quotient_pfp_proper_left_subtract_ubright_entry * S ((S (fom_index_pfp_proper_left_subtract_ubright)) * ac) + (fom_value_pfp_proper_left_subtract_ubright))) /\ (exists fom_gap_pfp_proper_left_subtract_ubright_value_bound. fom_gap_pfp_proper_left_subtract_ubright_value_bound + S (fom_value_pfp_proper_left_subtract_ubright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_proper_left_subtract_ubcoefficients. (exists pfa_gap_proper_left_subtract_ubcoefficientsbound. pfa_gap_proper_left_subtract_ubcoefficientsbound + S (pfc_index_proper_left_subtract_ubcoefficients) = (N)) -> exists pfc_value_proper_left_subtract_ubcoefficients. ((((exists ff_h_pfp_proper_left_subtract_ubcoefficientsentry. ff_h_pfp_proper_left_subtract_ubcoefficientsentry + S (pfc_value_proper_left_subtract_ubcoefficients) = S ((S (pfc_index_proper_left_subtract_ubcoefficients)) * uc)) /\ exists ff_q_pfp_proper_left_subtract_ubcoefficientsentry. ub = ff_q_pfp_proper_left_subtract_ubcoefficientsentry * S ((S (pfc_index_proper_left_subtract_ubcoefficients)) * uc) + (pfc_value_proper_left_subtract_ubcoefficients))) /\ ((exists pfc_terms_code_proper_left_subtract_ubcoefficientscoefficient pfc_terms_scale_proper_left_subtract_ubcoefficientscoefficient pfc_natural_sum_proper_left_subtract_ubcoefficientscoefficient. ((forall pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal. (exists pfa_gap_proper_left_subtract_ubcoefficientscoefficientdiagonalbound. pfa_gap_proper_left_subtract_ubcoefficientscoefficientdiagonalbound + S (pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal) = (S (pfc_index_proper_left_subtract_ubcoefficients))) -> exists pfc_value_proper_left_subtract_ubcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonalentry. ff_h_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonalentry + S (pfc_value_proper_left_subtract_ubcoefficientscoefficientdiagonal) = S ((S (pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_subtract_ubcoefficientscoefficient)) /\ exists ff_q_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonalentry. pfc_terms_code_proper_left_subtract_ubcoefficientscoefficient = ff_q_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonalentry * S ((S (pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_subtract_ubcoefficientscoefficient) + (pfc_value_proper_left_subtract_ubcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_proper_left_subtract_ubcoefficientscoefficientdiagonalterm pfc_left_proper_left_subtract_ubcoefficientscoefficientdiagonalterm pfc_right_proper_left_subtract_ubcoefficientscoefficientdiagonalterm. (((pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal)+pfc_complement_proper_left_subtract_ubcoefficientscoefficientdiagonalterm=(pfc_index_proper_left_subtract_ubcoefficients)) /\ ((((((exists pfa_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftinside. pfa_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_proper_left_subtract_ubcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal)) * dc) + (pfc_left_proper_left_subtract_ubcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_proper_left_subtract_ubcoefficientscoefficientdiagonal)) /\ (((pfc_left_proper_left_subtract_ubcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightinside. pfa_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_proper_left_subtract_ubcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_proper_left_subtract_ubcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_proper_left_subtract_ubcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_proper_left_subtract_ubcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_proper_left_subtract_ubcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_proper_left_subtract_ubcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_proper_left_subtract_ubcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_proper_left_subtract_ubcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_proper_left_subtract_ubcoefficientscoefficientdiagonal)=pfc_left_proper_left_subtract_ubcoefficientscoefficientdiagonalterm*pfc_right_proper_left_subtract_ubcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_proper_left_subtract_ubcoefficientscoefficientsum fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum. ((((exists fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_start. fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_start. fs_u_pfc_proper_left_subtract_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_terminal. fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_proper_left_subtract_ubcoefficientscoefficient) = S ((S (S (pfc_index_proper_left_subtract_ubcoefficients))) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_terminal. fs_u_pfc_proper_left_subtract_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_proper_left_subtract_ubcoefficients))) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum) + (pfc_natural_sum_proper_left_subtract_ubcoefficientscoefficient))) /\ forall fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps = S (pfc_index_proper_left_subtract_ubcoefficients)) -> exists fs_a_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps fs_r_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps fs_s_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_subtract_ubcoefficientscoefficient)) /\ exists fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_proper_left_subtract_ubcoefficientscoefficient = fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_subtract_ubcoefficientscoefficient) + (fs_a_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_proper_left_subtract_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum) + (fs_r_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_proper_left_subtract_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_ubcoefficientscoefficientsum) + (fs_s_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps = fs_r_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps + fs_a_pfc_proper_left_subtract_ubcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_proper_left_subtract_ubcoefficientscoefficientresiduebound. pfa_gap_proper_left_subtract_ubcoefficientscoefficientresiduebound + S (pfc_value_proper_left_subtract_ubcoefficients) = (p)) /\ ((exists pfa_offset_left_proper_left_subtract_ubcoefficientscoefficientresiduecongruence pfa_offset_right_proper_left_subtract_ubcoefficientscoefficientresiduecongruence. (pfc_natural_sum_proper_left_subtract_ubcoefficientscoefficient) + (p) * pfa_offset_left_proper_left_subtract_ubcoefficientscoefficientresiduecongruence = (pfc_value_proper_left_subtract_ubcoefficients) + (p) * pfa_offset_right_proper_left_subtract_ubcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_proper_left_subtract_vbleft. (exists fom_gap_pfp_proper_left_subtract_vbleft_index_bound. fom_gap_pfp_proper_left_subtract_vbleft_index_bound + S (fom_index_pfp_proper_left_subtract_vbleft) = M) -> exists fom_value_pfp_proper_left_subtract_vbleft. ((((exists fom_beta_height_pfp_proper_left_subtract_vbleft_entry. fom_beta_height_pfp_proper_left_subtract_vbleft_entry + S (fom_value_pfp_proper_left_subtract_vbleft) = S ((S (fom_index_pfp_proper_left_subtract_vbleft)) * dc)) /\ exists fom_beta_quotient_pfp_proper_left_subtract_vbleft_entry. db = fom_beta_quotient_pfp_proper_left_subtract_vbleft_entry * S ((S (fom_index_pfp_proper_left_subtract_vbleft)) * dc) + (fom_value_pfp_proper_left_subtract_vbleft))) /\ (exists fom_gap_pfp_proper_left_subtract_vbleft_value_bound. fom_gap_pfp_proper_left_subtract_vbleft_value_bound + S (fom_value_pfp_proper_left_subtract_vbleft) = p))) /\ (((forall fom_index_pfp_proper_left_subtract_vbright. (exists fom_gap_pfp_proper_left_subtract_vbright_index_bound. fom_gap_pfp_proper_left_subtract_vbright_index_bound + S (fom_index_pfp_proper_left_subtract_vbright) = L) -> exists fom_value_pfp_proper_left_subtract_vbright. ((((exists fom_beta_height_pfp_proper_left_subtract_vbright_entry. fom_beta_height_pfp_proper_left_subtract_vbright_entry + S (fom_value_pfp_proper_left_subtract_vbright) = S ((S (fom_index_pfp_proper_left_subtract_vbright)) * bc)) /\ exists fom_beta_quotient_pfp_proper_left_subtract_vbright_entry. bb = fom_beta_quotient_pfp_proper_left_subtract_vbright_entry * S ((S (fom_index_pfp_proper_left_subtract_vbright)) * bc) + (fom_value_pfp_proper_left_subtract_vbright))) /\ (exists fom_gap_pfp_proper_left_subtract_vbright_value_bound. fom_gap_pfp_proper_left_subtract_vbright_value_bound + S (fom_value_pfp_proper_left_subtract_vbright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_proper_left_subtract_vbcoefficients. (exists pfa_gap_proper_left_subtract_vbcoefficientsbound. pfa_gap_proper_left_subtract_vbcoefficientsbound + S (pfc_index_proper_left_subtract_vbcoefficients) = (N)) -> exists pfc_value_proper_left_subtract_vbcoefficients. ((((exists ff_h_pfp_proper_left_subtract_vbcoefficientsentry. ff_h_pfp_proper_left_subtract_vbcoefficientsentry + S (pfc_value_proper_left_subtract_vbcoefficients) = S ((S (pfc_index_proper_left_subtract_vbcoefficients)) * vc)) /\ exists ff_q_pfp_proper_left_subtract_vbcoefficientsentry. vb = ff_q_pfp_proper_left_subtract_vbcoefficientsentry * S ((S (pfc_index_proper_left_subtract_vbcoefficients)) * vc) + (pfc_value_proper_left_subtract_vbcoefficients))) /\ ((exists pfc_terms_code_proper_left_subtract_vbcoefficientscoefficient pfc_terms_scale_proper_left_subtract_vbcoefficientscoefficient pfc_natural_sum_proper_left_subtract_vbcoefficientscoefficient. ((forall pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal. (exists pfa_gap_proper_left_subtract_vbcoefficientscoefficientdiagonalbound. pfa_gap_proper_left_subtract_vbcoefficientscoefficientdiagonalbound + S (pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal) = (S (pfc_index_proper_left_subtract_vbcoefficients))) -> exists pfc_value_proper_left_subtract_vbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonalentry. ff_h_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonalentry + S (pfc_value_proper_left_subtract_vbcoefficientscoefficientdiagonal) = S ((S (pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_subtract_vbcoefficientscoefficient)) /\ exists ff_q_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonalentry. pfc_terms_code_proper_left_subtract_vbcoefficientscoefficient = ff_q_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_subtract_vbcoefficientscoefficient) + (pfc_value_proper_left_subtract_vbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_proper_left_subtract_vbcoefficientscoefficientdiagonalterm pfc_left_proper_left_subtract_vbcoefficientscoefficientdiagonalterm pfc_right_proper_left_subtract_vbcoefficientscoefficientdiagonalterm. (((pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal)+pfc_complement_proper_left_subtract_vbcoefficientscoefficientdiagonalterm=(pfc_index_proper_left_subtract_vbcoefficients)) /\ ((((((exists pfa_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_proper_left_subtract_vbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_proper_left_subtract_vbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_proper_left_subtract_vbcoefficientscoefficientdiagonal)) /\ (((pfc_left_proper_left_subtract_vbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_proper_left_subtract_vbcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_proper_left_subtract_vbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_proper_left_subtract_vbcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_proper_left_subtract_vbcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_proper_left_subtract_vbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_proper_left_subtract_vbcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_proper_left_subtract_vbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_proper_left_subtract_vbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_proper_left_subtract_vbcoefficientscoefficientdiagonal)=pfc_left_proper_left_subtract_vbcoefficientscoefficientdiagonalterm*pfc_right_proper_left_subtract_vbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_proper_left_subtract_vbcoefficientscoefficientsum fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum. ((((exists fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_start. fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_start. fs_u_pfc_proper_left_subtract_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_terminal. fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_proper_left_subtract_vbcoefficientscoefficient) = S ((S (S (pfc_index_proper_left_subtract_vbcoefficients))) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_terminal. fs_u_pfc_proper_left_subtract_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_proper_left_subtract_vbcoefficients))) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum) + (pfc_natural_sum_proper_left_subtract_vbcoefficientscoefficient))) /\ forall fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps = S (pfc_index_proper_left_subtract_vbcoefficients)) -> exists fs_a_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps fs_r_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps fs_s_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_subtract_vbcoefficientscoefficient)) /\ exists fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_proper_left_subtract_vbcoefficientscoefficient = fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_subtract_vbcoefficientscoefficient) + (fs_a_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_proper_left_subtract_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum) + (fs_r_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_proper_left_subtract_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_vbcoefficientscoefficientsum) + (fs_s_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps = fs_r_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps + fs_a_pfc_proper_left_subtract_vbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_proper_left_subtract_vbcoefficientscoefficientresiduebound. pfa_gap_proper_left_subtract_vbcoefficientscoefficientresiduebound + S (pfc_value_proper_left_subtract_vbcoefficients) = (p)) /\ ((exists pfa_offset_left_proper_left_subtract_vbcoefficientscoefficientresiduecongruence pfa_offset_right_proper_left_subtract_vbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_proper_left_subtract_vbcoefficientscoefficient) + (p) * pfa_offset_left_proper_left_subtract_vbcoefficientscoefficientresiduecongruence = (pfc_value_proper_left_subtract_vbcoefficients) + (p) * pfa_offset_right_proper_left_subtract_vbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_proper_left_subtract_wbleft. (exists fom_gap_pfp_proper_left_subtract_wbleft_index_bound. fom_gap_pfp_proper_left_subtract_wbleft_index_bound + S (fom_index_pfp_proper_left_subtract_wbleft) = M) -> exists fom_value_pfp_proper_left_subtract_wbleft. ((((exists fom_beta_height_pfp_proper_left_subtract_wbleft_entry. fom_beta_height_pfp_proper_left_subtract_wbleft_entry + S (fom_value_pfp_proper_left_subtract_wbleft) = S ((S (fom_index_pfp_proper_left_subtract_wbleft)) * dc)) /\ exists fom_beta_quotient_pfp_proper_left_subtract_wbleft_entry. db = fom_beta_quotient_pfp_proper_left_subtract_wbleft_entry * S ((S (fom_index_pfp_proper_left_subtract_wbleft)) * dc) + (fom_value_pfp_proper_left_subtract_wbleft))) /\ (exists fom_gap_pfp_proper_left_subtract_wbleft_value_bound. fom_gap_pfp_proper_left_subtract_wbleft_value_bound + S (fom_value_pfp_proper_left_subtract_wbleft) = p))) /\ (((forall fom_index_pfp_proper_left_subtract_wbright. (exists fom_gap_pfp_proper_left_subtract_wbright_index_bound. fom_gap_pfp_proper_left_subtract_wbright_index_bound + S (fom_index_pfp_proper_left_subtract_wbright) = L) -> exists fom_value_pfp_proper_left_subtract_wbright. ((((exists fom_beta_height_pfp_proper_left_subtract_wbright_entry. fom_beta_height_pfp_proper_left_subtract_wbright_entry + S (fom_value_pfp_proper_left_subtract_wbright) = S ((S (fom_index_pfp_proper_left_subtract_wbright)) * cc)) /\ exists fom_beta_quotient_pfp_proper_left_subtract_wbright_entry. cb = fom_beta_quotient_pfp_proper_left_subtract_wbright_entry * S ((S (fom_index_pfp_proper_left_subtract_wbright)) * cc) + (fom_value_pfp_proper_left_subtract_wbright))) /\ (exists fom_gap_pfp_proper_left_subtract_wbright_value_bound. fom_gap_pfp_proper_left_subtract_wbright_value_bound + S (fom_value_pfp_proper_left_subtract_wbright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_proper_left_subtract_wbcoefficients. (exists pfa_gap_proper_left_subtract_wbcoefficientsbound. pfa_gap_proper_left_subtract_wbcoefficientsbound + S (pfc_index_proper_left_subtract_wbcoefficients) = (N)) -> exists pfc_value_proper_left_subtract_wbcoefficients. ((((exists ff_h_pfp_proper_left_subtract_wbcoefficientsentry. ff_h_pfp_proper_left_subtract_wbcoefficientsentry + S (pfc_value_proper_left_subtract_wbcoefficients) = S ((S (pfc_index_proper_left_subtract_wbcoefficients)) * wc)) /\ exists ff_q_pfp_proper_left_subtract_wbcoefficientsentry. wb = ff_q_pfp_proper_left_subtract_wbcoefficientsentry * S ((S (pfc_index_proper_left_subtract_wbcoefficients)) * wc) + (pfc_value_proper_left_subtract_wbcoefficients))) /\ ((exists pfc_terms_code_proper_left_subtract_wbcoefficientscoefficient pfc_terms_scale_proper_left_subtract_wbcoefficientscoefficient pfc_natural_sum_proper_left_subtract_wbcoefficientscoefficient. ((forall pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal. (exists pfa_gap_proper_left_subtract_wbcoefficientscoefficientdiagonalbound. pfa_gap_proper_left_subtract_wbcoefficientscoefficientdiagonalbound + S (pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal) = (S (pfc_index_proper_left_subtract_wbcoefficients))) -> exists pfc_value_proper_left_subtract_wbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonalentry. ff_h_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonalentry + S (pfc_value_proper_left_subtract_wbcoefficientscoefficientdiagonal) = S ((S (pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_subtract_wbcoefficientscoefficient)) /\ exists ff_q_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonalentry. pfc_terms_code_proper_left_subtract_wbcoefficientscoefficient = ff_q_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_subtract_wbcoefficientscoefficient) + (pfc_value_proper_left_subtract_wbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_proper_left_subtract_wbcoefficientscoefficientdiagonalterm pfc_left_proper_left_subtract_wbcoefficientscoefficientdiagonalterm pfc_right_proper_left_subtract_wbcoefficientscoefficientdiagonalterm. (((pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal)+pfc_complement_proper_left_subtract_wbcoefficientscoefficientdiagonalterm=(pfc_index_proper_left_subtract_wbcoefficients)) /\ ((((((exists pfa_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_proper_left_subtract_wbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_proper_left_subtract_wbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_proper_left_subtract_wbcoefficientscoefficientdiagonal)) /\ (((pfc_left_proper_left_subtract_wbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_proper_left_subtract_wbcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_proper_left_subtract_wbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_proper_left_subtract_wbcoefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_proper_left_subtract_wbcoefficientscoefficientdiagonalterm)) * cc) + (pfc_right_proper_left_subtract_wbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_proper_left_subtract_wbcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_proper_left_subtract_wbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_proper_left_subtract_wbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_proper_left_subtract_wbcoefficientscoefficientdiagonal)=pfc_left_proper_left_subtract_wbcoefficientscoefficientdiagonalterm*pfc_right_proper_left_subtract_wbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_proper_left_subtract_wbcoefficientscoefficientsum fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum. ((((exists fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_start. fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_start. fs_u_pfc_proper_left_subtract_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_terminal. fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_proper_left_subtract_wbcoefficientscoefficient) = S ((S (S (pfc_index_proper_left_subtract_wbcoefficients))) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_terminal. fs_u_pfc_proper_left_subtract_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_proper_left_subtract_wbcoefficients))) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum) + (pfc_natural_sum_proper_left_subtract_wbcoefficientscoefficient))) /\ forall fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps = S (pfc_index_proper_left_subtract_wbcoefficients)) -> exists fs_a_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps fs_r_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps fs_s_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_subtract_wbcoefficientscoefficient)) /\ exists fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_proper_left_subtract_wbcoefficientscoefficient = fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_subtract_wbcoefficientscoefficient) + (fs_a_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_proper_left_subtract_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum) + (fs_r_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_proper_left_subtract_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_subtract_wbcoefficientscoefficientsum) + (fs_s_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps = fs_r_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps + fs_a_pfc_proper_left_subtract_wbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_proper_left_subtract_wbcoefficientscoefficientresiduebound. pfa_gap_proper_left_subtract_wbcoefficientscoefficientresiduebound + S (pfc_value_proper_left_subtract_wbcoefficients) = (p)) /\ ((exists pfa_offset_left_proper_left_subtract_wbcoefficientscoefficientresiduecongruence pfa_offset_right_proper_left_subtract_wbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_proper_left_subtract_wbcoefficientscoefficient) + (p) * pfa_offset_left_proper_left_subtract_wbcoefficientscoefficientresiduecongruence = (pfc_value_proper_left_subtract_wbcoefficients) + (p) * pfa_offset_right_proper_left_subtract_wbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfs_index_proper_left_subtract_result. (exists pfa_gap_proper_left_subtract_resultindex. pfa_gap_proper_left_subtract_resultindex + S (pfs_index_proper_left_subtract_result) = (N)) -> exists pfs_left_proper_left_subtract_result pfs_right_proper_left_subtract_result pfs_result_proper_left_subtract_result. ((((exists ff_h_pfp_proper_left_subtract_resultleft. ff_h_pfp_proper_left_subtract_resultleft + S (pfs_left_proper_left_subtract_result) = S ((S (pfs_index_proper_left_subtract_result)) * uc)) /\ exists ff_q_pfp_proper_left_subtract_resultleft. ub = ff_q_pfp_proper_left_subtract_resultleft * S ((S (pfs_index_proper_left_subtract_result)) * uc) + (pfs_left_proper_left_subtract_result))) /\ (((((exists ff_h_pfp_proper_left_subtract_resultright. ff_h_pfp_proper_left_subtract_resultright + S (pfs_right_proper_left_subtract_result) = S ((S (pfs_index_proper_left_subtract_result)) * vc)) /\ exists ff_q_pfp_proper_left_subtract_resultright. vb = ff_q_pfp_proper_left_subtract_resultright * S ((S (pfs_index_proper_left_subtract_result)) * vc) + (pfs_right_proper_left_subtract_result))) /\ (((((exists ff_h_pfp_proper_left_subtract_resultresult. ff_h_pfp_proper_left_subtract_resultresult + S (pfs_result_proper_left_subtract_result) = S ((S (pfs_index_proper_left_subtract_result)) * wc)) /\ exists ff_q_pfp_proper_left_subtract_resultresult. wb = ff_q_pfp_proper_left_subtract_resultresult * S ((S (pfs_index_proper_left_subtract_result)) * wc) + (pfs_result_proper_left_subtract_result))) /\ ((((exists pfa_gap_proper_left_subtract_resultoperationleft. pfa_gap_proper_left_subtract_resultoperationleft + S (pfs_right_proper_left_subtract_result) = (p)) /\ (((exists pfa_gap_proper_left_subtract_resultoperationright. pfa_gap_proper_left_subtract_resultoperationright + S (pfs_result_proper_left_subtract_result) = (p)) /\ ((((exists pfa_gap_proper_left_subtract_resultoperationresultbound. pfa_gap_proper_left_subtract_resultoperationresultbound + S (pfs_left_proper_left_subtract_result) = (p)) /\ ((exists pfa_offset_left_proper_left_subtract_resultoperationresultcongruence pfa_offset_right_proper_left_subtract_resultoperationresultcongruence. ((pfs_right_proper_left_subtract_result) + (pfs_result_proper_left_subtract_result)) + (p) * pfa_offset_left_proper_left_subtract_resultoperationresultcongruence = (pfs_left_proper_left_subtract_result) + (p) * pfa_offset_right_proper_left_subtract_resultoperationresultcongruence))))))))))))))))