prime_field_polynomial_convolution_left_add

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 pfp_index_proper_left_add_source. (exists pfa_gap_proper_left_add_sourceindex. pfa_gap_proper_left_add_sourceindex + S (pfp_index_proper_left_add_source) = (L)) -> exists pfp_left_proper_left_add_source pfp_right_proper_left_add_source pfp_value_proper_left_add_source. ((((exists ff_h_pfp_proper_left_add_sourceleft. ff_h_pfp_proper_left_add_sourceleft + S (pfp_left_proper_left_add_source) = S ((S (pfp_index_proper_left_add_source)) * ac)) /\ exists ff_q_pfp_proper_left_add_sourceleft. ab = ff_q_pfp_proper_left_add_sourceleft * S ((S (pfp_index_proper_left_add_source)) * ac) + (pfp_left_proper_left_add_source))) /\ (((((exists ff_h_pfp_proper_left_add_sourceright. ff_h_pfp_proper_left_add_sourceright + S (pfp_right_proper_left_add_source) = S ((S (pfp_index_proper_left_add_source)) * bc)) /\ exists ff_q_pfp_proper_left_add_sourceright. bb = ff_q_pfp_proper_left_add_sourceright * S ((S (pfp_index_proper_left_add_source)) * bc) + (pfp_right_proper_left_add_source))) /\ (((((exists ff_h_pfp_proper_left_add_sourcetarget. ff_h_pfp_proper_left_add_sourcetarget + S (pfp_value_proper_left_add_source) = S ((S (pfp_index_proper_left_add_source)) * cc)) /\ exists ff_q_pfp_proper_left_add_sourcetarget. cb = ff_q_pfp_proper_left_add_sourcetarget * S ((S (pfp_index_proper_left_add_source)) * cc) + (pfp_value_proper_left_add_source))) /\ ((((exists pfa_gap_proper_left_add_sourceoperationleft. pfa_gap_proper_left_add_sourceoperationleft + S (pfp_left_proper_left_add_source) = (p)) /\ (((exists pfa_gap_proper_left_add_sourceoperationright. pfa_gap_proper_left_add_sourceoperationright + S (pfp_right_proper_left_add_source) = (p)) /\ ((((exists pfa_gap_proper_left_add_sourceoperationresultbound. pfa_gap_proper_left_add_sourceoperationresultbound + S (pfp_value_proper_left_add_source) = (p)) /\ ((exists pfa_offset_left_proper_left_add_sourceoperationresultcongruence pfa_offset_right_proper_left_add_sourceoperationresultcongruence. ((pfp_left_proper_left_add_source) + (pfp_right_proper_left_add_source)) + (p) * pfa_offset_left_proper_left_add_sourceoperationresultcongruence = (pfp_value_proper_left_add_source) + (p) * pfa_offset_right_proper_left_add_sourceoperationresultcongruence)))))))))))))))) -> (((forall fom_index_pfp_proper_left_add_ubleft. (exists fom_gap_pfp_proper_left_add_ubleft_index_bound. fom_gap_pfp_proper_left_add_ubleft_index_bound + S (fom_index_pfp_proper_left_add_ubleft) = M) -> exists fom_value_pfp_proper_left_add_ubleft. ((((exists fom_beta_height_pfp_proper_left_add_ubleft_entry. fom_beta_height_pfp_proper_left_add_ubleft_entry + S (fom_value_pfp_proper_left_add_ubleft) = S ((S (fom_index_pfp_proper_left_add_ubleft)) * dc)) /\ exists fom_beta_quotient_pfp_proper_left_add_ubleft_entry. db = fom_beta_quotient_pfp_proper_left_add_ubleft_entry * S ((S (fom_index_pfp_proper_left_add_ubleft)) * dc) + (fom_value_pfp_proper_left_add_ubleft))) /\ (exists fom_gap_pfp_proper_left_add_ubleft_value_bound. fom_gap_pfp_proper_left_add_ubleft_value_bound + S (fom_value_pfp_proper_left_add_ubleft) = p))) /\ (((forall fom_index_pfp_proper_left_add_ubright. (exists fom_gap_pfp_proper_left_add_ubright_index_bound. fom_gap_pfp_proper_left_add_ubright_index_bound + S (fom_index_pfp_proper_left_add_ubright) = L) -> exists fom_value_pfp_proper_left_add_ubright. ((((exists fom_beta_height_pfp_proper_left_add_ubright_entry. fom_beta_height_pfp_proper_left_add_ubright_entry + S (fom_value_pfp_proper_left_add_ubright) = S ((S (fom_index_pfp_proper_left_add_ubright)) * ac)) /\ exists fom_beta_quotient_pfp_proper_left_add_ubright_entry. ab = fom_beta_quotient_pfp_proper_left_add_ubright_entry * S ((S (fom_index_pfp_proper_left_add_ubright)) * ac) + (fom_value_pfp_proper_left_add_ubright))) /\ (exists fom_gap_pfp_proper_left_add_ubright_value_bound. fom_gap_pfp_proper_left_add_ubright_value_bound + S (fom_value_pfp_proper_left_add_ubright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_proper_left_add_ubcoefficients. (exists pfa_gap_proper_left_add_ubcoefficientsbound. pfa_gap_proper_left_add_ubcoefficientsbound + S (pfc_index_proper_left_add_ubcoefficients) = (N)) -> exists pfc_value_proper_left_add_ubcoefficients. ((((exists ff_h_pfp_proper_left_add_ubcoefficientsentry. ff_h_pfp_proper_left_add_ubcoefficientsentry + S (pfc_value_proper_left_add_ubcoefficients) = S ((S (pfc_index_proper_left_add_ubcoefficients)) * uc)) /\ exists ff_q_pfp_proper_left_add_ubcoefficientsentry. ub = ff_q_pfp_proper_left_add_ubcoefficientsentry * S ((S (pfc_index_proper_left_add_ubcoefficients)) * uc) + (pfc_value_proper_left_add_ubcoefficients))) /\ ((exists pfc_terms_code_proper_left_add_ubcoefficientscoefficient pfc_terms_scale_proper_left_add_ubcoefficientscoefficient pfc_natural_sum_proper_left_add_ubcoefficientscoefficient. ((forall pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal. (exists pfa_gap_proper_left_add_ubcoefficientscoefficientdiagonalbound. pfa_gap_proper_left_add_ubcoefficientscoefficientdiagonalbound + S (pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal) = (S (pfc_index_proper_left_add_ubcoefficients))) -> exists pfc_value_proper_left_add_ubcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_proper_left_add_ubcoefficientscoefficientdiagonalentry. ff_h_pfp_proper_left_add_ubcoefficientscoefficientdiagonalentry + S (pfc_value_proper_left_add_ubcoefficientscoefficientdiagonal) = S ((S (pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_add_ubcoefficientscoefficient)) /\ exists ff_q_pfp_proper_left_add_ubcoefficientscoefficientdiagonalentry. pfc_terms_code_proper_left_add_ubcoefficientscoefficient = ff_q_pfp_proper_left_add_ubcoefficientscoefficientdiagonalentry * S ((S (pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_add_ubcoefficientscoefficient) + (pfc_value_proper_left_add_ubcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_proper_left_add_ubcoefficientscoefficientdiagonalterm pfc_left_proper_left_add_ubcoefficientscoefficientdiagonalterm pfc_right_proper_left_add_ubcoefficientscoefficientdiagonalterm. (((pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal)+pfc_complement_proper_left_add_ubcoefficientscoefficientdiagonalterm=(pfc_index_proper_left_add_ubcoefficients)) /\ ((((((exists pfa_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermleftinside. pfa_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_proper_left_add_ubcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal)) * dc) + (pfc_left_proper_left_add_ubcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_proper_left_add_ubcoefficientscoefficientdiagonal)) /\ (((pfc_left_proper_left_add_ubcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermrightinside. pfa_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_proper_left_add_ubcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_proper_left_add_ubcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_proper_left_add_ubcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_proper_left_add_ubcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_proper_left_add_ubcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_proper_left_add_ubcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_proper_left_add_ubcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_proper_left_add_ubcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_proper_left_add_ubcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_proper_left_add_ubcoefficientscoefficientdiagonal)=pfc_left_proper_left_add_ubcoefficientscoefficientdiagonalterm*pfc_right_proper_left_add_ubcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_proper_left_add_ubcoefficientscoefficientsum fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum. ((((exists fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_start. fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_start. fs_u_pfc_proper_left_add_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_terminal. fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_proper_left_add_ubcoefficientscoefficient) = S ((S (S (pfc_index_proper_left_add_ubcoefficients))) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_terminal. fs_u_pfc_proper_left_add_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_proper_left_add_ubcoefficients))) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum) + (pfc_natural_sum_proper_left_add_ubcoefficientscoefficient))) /\ forall fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps = S (pfc_index_proper_left_add_ubcoefficients)) -> exists fs_a_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps fs_r_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps fs_s_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_add_ubcoefficientscoefficient)) /\ exists fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_proper_left_add_ubcoefficientscoefficient = fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_add_ubcoefficientscoefficient) + (fs_a_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_proper_left_add_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum) + (fs_r_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_proper_left_add_ubcoefficientscoefficientsum = fs_q_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_ubcoefficientscoefficientsum) + (fs_s_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps = fs_r_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps + fs_a_pfc_proper_left_add_ubcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_proper_left_add_ubcoefficientscoefficientresiduebound. pfa_gap_proper_left_add_ubcoefficientscoefficientresiduebound + S (pfc_value_proper_left_add_ubcoefficients) = (p)) /\ ((exists pfa_offset_left_proper_left_add_ubcoefficientscoefficientresiduecongruence pfa_offset_right_proper_left_add_ubcoefficientscoefficientresiduecongruence. (pfc_natural_sum_proper_left_add_ubcoefficientscoefficient) + (p) * pfa_offset_left_proper_left_add_ubcoefficientscoefficientresiduecongruence = (pfc_value_proper_left_add_ubcoefficients) + (p) * pfa_offset_right_proper_left_add_ubcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_proper_left_add_vbleft. (exists fom_gap_pfp_proper_left_add_vbleft_index_bound. fom_gap_pfp_proper_left_add_vbleft_index_bound + S (fom_index_pfp_proper_left_add_vbleft) = M) -> exists fom_value_pfp_proper_left_add_vbleft. ((((exists fom_beta_height_pfp_proper_left_add_vbleft_entry. fom_beta_height_pfp_proper_left_add_vbleft_entry + S (fom_value_pfp_proper_left_add_vbleft) = S ((S (fom_index_pfp_proper_left_add_vbleft)) * dc)) /\ exists fom_beta_quotient_pfp_proper_left_add_vbleft_entry. db = fom_beta_quotient_pfp_proper_left_add_vbleft_entry * S ((S (fom_index_pfp_proper_left_add_vbleft)) * dc) + (fom_value_pfp_proper_left_add_vbleft))) /\ (exists fom_gap_pfp_proper_left_add_vbleft_value_bound. fom_gap_pfp_proper_left_add_vbleft_value_bound + S (fom_value_pfp_proper_left_add_vbleft) = p))) /\ (((forall fom_index_pfp_proper_left_add_vbright. (exists fom_gap_pfp_proper_left_add_vbright_index_bound. fom_gap_pfp_proper_left_add_vbright_index_bound + S (fom_index_pfp_proper_left_add_vbright) = L) -> exists fom_value_pfp_proper_left_add_vbright. ((((exists fom_beta_height_pfp_proper_left_add_vbright_entry. fom_beta_height_pfp_proper_left_add_vbright_entry + S (fom_value_pfp_proper_left_add_vbright) = S ((S (fom_index_pfp_proper_left_add_vbright)) * bc)) /\ exists fom_beta_quotient_pfp_proper_left_add_vbright_entry. bb = fom_beta_quotient_pfp_proper_left_add_vbright_entry * S ((S (fom_index_pfp_proper_left_add_vbright)) * bc) + (fom_value_pfp_proper_left_add_vbright))) /\ (exists fom_gap_pfp_proper_left_add_vbright_value_bound. fom_gap_pfp_proper_left_add_vbright_value_bound + S (fom_value_pfp_proper_left_add_vbright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_proper_left_add_vbcoefficients. (exists pfa_gap_proper_left_add_vbcoefficientsbound. pfa_gap_proper_left_add_vbcoefficientsbound + S (pfc_index_proper_left_add_vbcoefficients) = (N)) -> exists pfc_value_proper_left_add_vbcoefficients. ((((exists ff_h_pfp_proper_left_add_vbcoefficientsentry. ff_h_pfp_proper_left_add_vbcoefficientsentry + S (pfc_value_proper_left_add_vbcoefficients) = S ((S (pfc_index_proper_left_add_vbcoefficients)) * vc)) /\ exists ff_q_pfp_proper_left_add_vbcoefficientsentry. vb = ff_q_pfp_proper_left_add_vbcoefficientsentry * S ((S (pfc_index_proper_left_add_vbcoefficients)) * vc) + (pfc_value_proper_left_add_vbcoefficients))) /\ ((exists pfc_terms_code_proper_left_add_vbcoefficientscoefficient pfc_terms_scale_proper_left_add_vbcoefficientscoefficient pfc_natural_sum_proper_left_add_vbcoefficientscoefficient. ((forall pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal. (exists pfa_gap_proper_left_add_vbcoefficientscoefficientdiagonalbound. pfa_gap_proper_left_add_vbcoefficientscoefficientdiagonalbound + S (pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal) = (S (pfc_index_proper_left_add_vbcoefficients))) -> exists pfc_value_proper_left_add_vbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_proper_left_add_vbcoefficientscoefficientdiagonalentry. ff_h_pfp_proper_left_add_vbcoefficientscoefficientdiagonalentry + S (pfc_value_proper_left_add_vbcoefficientscoefficientdiagonal) = S ((S (pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_add_vbcoefficientscoefficient)) /\ exists ff_q_pfp_proper_left_add_vbcoefficientscoefficientdiagonalentry. pfc_terms_code_proper_left_add_vbcoefficientscoefficient = ff_q_pfp_proper_left_add_vbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_add_vbcoefficientscoefficient) + (pfc_value_proper_left_add_vbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_proper_left_add_vbcoefficientscoefficientdiagonalterm pfc_left_proper_left_add_vbcoefficientscoefficientdiagonalterm pfc_right_proper_left_add_vbcoefficientscoefficientdiagonalterm. (((pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal)+pfc_complement_proper_left_add_vbcoefficientscoefficientdiagonalterm=(pfc_index_proper_left_add_vbcoefficients)) /\ ((((((exists pfa_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_proper_left_add_vbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_proper_left_add_vbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_proper_left_add_vbcoefficientscoefficientdiagonal)) /\ (((pfc_left_proper_left_add_vbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_proper_left_add_vbcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_proper_left_add_vbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_proper_left_add_vbcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_proper_left_add_vbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_proper_left_add_vbcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_proper_left_add_vbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_proper_left_add_vbcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_proper_left_add_vbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_proper_left_add_vbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_proper_left_add_vbcoefficientscoefficientdiagonal)=pfc_left_proper_left_add_vbcoefficientscoefficientdiagonalterm*pfc_right_proper_left_add_vbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_proper_left_add_vbcoefficientscoefficientsum fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum. ((((exists fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_start. fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_start. fs_u_pfc_proper_left_add_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_terminal. fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_proper_left_add_vbcoefficientscoefficient) = S ((S (S (pfc_index_proper_left_add_vbcoefficients))) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_terminal. fs_u_pfc_proper_left_add_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_proper_left_add_vbcoefficients))) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum) + (pfc_natural_sum_proper_left_add_vbcoefficientscoefficient))) /\ forall fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps = S (pfc_index_proper_left_add_vbcoefficients)) -> exists fs_a_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps fs_r_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps fs_s_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_add_vbcoefficientscoefficient)) /\ exists fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_proper_left_add_vbcoefficientscoefficient = fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_add_vbcoefficientscoefficient) + (fs_a_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_proper_left_add_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum) + (fs_r_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_proper_left_add_vbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_vbcoefficientscoefficientsum) + (fs_s_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps = fs_r_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps + fs_a_pfc_proper_left_add_vbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_proper_left_add_vbcoefficientscoefficientresiduebound. pfa_gap_proper_left_add_vbcoefficientscoefficientresiduebound + S (pfc_value_proper_left_add_vbcoefficients) = (p)) /\ ((exists pfa_offset_left_proper_left_add_vbcoefficientscoefficientresiduecongruence pfa_offset_right_proper_left_add_vbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_proper_left_add_vbcoefficientscoefficient) + (p) * pfa_offset_left_proper_left_add_vbcoefficientscoefficientresiduecongruence = (pfc_value_proper_left_add_vbcoefficients) + (p) * pfa_offset_right_proper_left_add_vbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_proper_left_add_wbleft. (exists fom_gap_pfp_proper_left_add_wbleft_index_bound. fom_gap_pfp_proper_left_add_wbleft_index_bound + S (fom_index_pfp_proper_left_add_wbleft) = M) -> exists fom_value_pfp_proper_left_add_wbleft. ((((exists fom_beta_height_pfp_proper_left_add_wbleft_entry. fom_beta_height_pfp_proper_left_add_wbleft_entry + S (fom_value_pfp_proper_left_add_wbleft) = S ((S (fom_index_pfp_proper_left_add_wbleft)) * dc)) /\ exists fom_beta_quotient_pfp_proper_left_add_wbleft_entry. db = fom_beta_quotient_pfp_proper_left_add_wbleft_entry * S ((S (fom_index_pfp_proper_left_add_wbleft)) * dc) + (fom_value_pfp_proper_left_add_wbleft))) /\ (exists fom_gap_pfp_proper_left_add_wbleft_value_bound. fom_gap_pfp_proper_left_add_wbleft_value_bound + S (fom_value_pfp_proper_left_add_wbleft) = p))) /\ (((forall fom_index_pfp_proper_left_add_wbright. (exists fom_gap_pfp_proper_left_add_wbright_index_bound. fom_gap_pfp_proper_left_add_wbright_index_bound + S (fom_index_pfp_proper_left_add_wbright) = L) -> exists fom_value_pfp_proper_left_add_wbright. ((((exists fom_beta_height_pfp_proper_left_add_wbright_entry. fom_beta_height_pfp_proper_left_add_wbright_entry + S (fom_value_pfp_proper_left_add_wbright) = S ((S (fom_index_pfp_proper_left_add_wbright)) * cc)) /\ exists fom_beta_quotient_pfp_proper_left_add_wbright_entry. cb = fom_beta_quotient_pfp_proper_left_add_wbright_entry * S ((S (fom_index_pfp_proper_left_add_wbright)) * cc) + (fom_value_pfp_proper_left_add_wbright))) /\ (exists fom_gap_pfp_proper_left_add_wbright_value_bound. fom_gap_pfp_proper_left_add_wbright_value_bound + S (fom_value_pfp_proper_left_add_wbright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_proper_left_add_wbcoefficients. (exists pfa_gap_proper_left_add_wbcoefficientsbound. pfa_gap_proper_left_add_wbcoefficientsbound + S (pfc_index_proper_left_add_wbcoefficients) = (N)) -> exists pfc_value_proper_left_add_wbcoefficients. ((((exists ff_h_pfp_proper_left_add_wbcoefficientsentry. ff_h_pfp_proper_left_add_wbcoefficientsentry + S (pfc_value_proper_left_add_wbcoefficients) = S ((S (pfc_index_proper_left_add_wbcoefficients)) * wc)) /\ exists ff_q_pfp_proper_left_add_wbcoefficientsentry. wb = ff_q_pfp_proper_left_add_wbcoefficientsentry * S ((S (pfc_index_proper_left_add_wbcoefficients)) * wc) + (pfc_value_proper_left_add_wbcoefficients))) /\ ((exists pfc_terms_code_proper_left_add_wbcoefficientscoefficient pfc_terms_scale_proper_left_add_wbcoefficientscoefficient pfc_natural_sum_proper_left_add_wbcoefficientscoefficient. ((forall pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal. (exists pfa_gap_proper_left_add_wbcoefficientscoefficientdiagonalbound. pfa_gap_proper_left_add_wbcoefficientscoefficientdiagonalbound + S (pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal) = (S (pfc_index_proper_left_add_wbcoefficients))) -> exists pfc_value_proper_left_add_wbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_proper_left_add_wbcoefficientscoefficientdiagonalentry. ff_h_pfp_proper_left_add_wbcoefficientscoefficientdiagonalentry + S (pfc_value_proper_left_add_wbcoefficientscoefficientdiagonal) = S ((S (pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_add_wbcoefficientscoefficient)) /\ exists ff_q_pfp_proper_left_add_wbcoefficientscoefficientdiagonalentry. pfc_terms_code_proper_left_add_wbcoefficientscoefficient = ff_q_pfp_proper_left_add_wbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal)) * pfc_terms_scale_proper_left_add_wbcoefficientscoefficient) + (pfc_value_proper_left_add_wbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_proper_left_add_wbcoefficientscoefficientdiagonalterm pfc_left_proper_left_add_wbcoefficientscoefficientdiagonalterm pfc_right_proper_left_add_wbcoefficientscoefficientdiagonalterm. (((pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal)+pfc_complement_proper_left_add_wbcoefficientscoefficientdiagonalterm=(pfc_index_proper_left_add_wbcoefficients)) /\ ((((((exists pfa_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_proper_left_add_wbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_proper_left_add_wbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_proper_left_add_wbcoefficientscoefficientdiagonal)) /\ (((pfc_left_proper_left_add_wbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_proper_left_add_wbcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_proper_left_add_wbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_proper_left_add_wbcoefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_proper_left_add_wbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_proper_left_add_wbcoefficientscoefficientdiagonalterm)) * cc) + (pfc_right_proper_left_add_wbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_proper_left_add_wbcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_proper_left_add_wbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_proper_left_add_wbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_proper_left_add_wbcoefficientscoefficientdiagonal)=pfc_left_proper_left_add_wbcoefficientscoefficientdiagonalterm*pfc_right_proper_left_add_wbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_proper_left_add_wbcoefficientscoefficientsum fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum. ((((exists fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_start. fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_start. fs_u_pfc_proper_left_add_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_terminal. fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_proper_left_add_wbcoefficientscoefficient) = S ((S (S (pfc_index_proper_left_add_wbcoefficients))) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_terminal. fs_u_pfc_proper_left_add_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_proper_left_add_wbcoefficients))) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum) + (pfc_natural_sum_proper_left_add_wbcoefficientscoefficient))) /\ forall fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps = S (pfc_index_proper_left_add_wbcoefficients)) -> exists fs_a_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps fs_r_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps fs_s_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_add_wbcoefficientscoefficient)) /\ exists fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_proper_left_add_wbcoefficientscoefficient = fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_proper_left_add_wbcoefficientscoefficient) + (fs_a_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_proper_left_add_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum) + (fs_r_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_proper_left_add_wbcoefficientscoefficientsum = fs_q_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_proper_left_add_wbcoefficientscoefficientsum) + (fs_s_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps = fs_r_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps + fs_a_pfc_proper_left_add_wbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_proper_left_add_wbcoefficientscoefficientresiduebound. pfa_gap_proper_left_add_wbcoefficientscoefficientresiduebound + S (pfc_value_proper_left_add_wbcoefficients) = (p)) /\ ((exists pfa_offset_left_proper_left_add_wbcoefficientscoefficientresiduecongruence pfa_offset_right_proper_left_add_wbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_proper_left_add_wbcoefficientscoefficient) + (p) * pfa_offset_left_proper_left_add_wbcoefficientscoefficientresiduecongruence = (pfc_value_proper_left_add_wbcoefficients) + (p) * pfa_offset_right_proper_left_add_wbcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfp_index_proper_left_add_result. (exists pfa_gap_proper_left_add_resultindex. pfa_gap_proper_left_add_resultindex + S (pfp_index_proper_left_add_result) = (N)) -> exists pfp_left_proper_left_add_result pfp_right_proper_left_add_result pfp_value_proper_left_add_result. ((((exists ff_h_pfp_proper_left_add_resultleft. ff_h_pfp_proper_left_add_resultleft + S (pfp_left_proper_left_add_result) = S ((S (pfp_index_proper_left_add_result)) * uc)) /\ exists ff_q_pfp_proper_left_add_resultleft. ub = ff_q_pfp_proper_left_add_resultleft * S ((S (pfp_index_proper_left_add_result)) * uc) + (pfp_left_proper_left_add_result))) /\ (((((exists ff_h_pfp_proper_left_add_resultright. ff_h_pfp_proper_left_add_resultright + S (pfp_right_proper_left_add_result) = S ((S (pfp_index_proper_left_add_result)) * vc)) /\ exists ff_q_pfp_proper_left_add_resultright. vb = ff_q_pfp_proper_left_add_resultright * S ((S (pfp_index_proper_left_add_result)) * vc) + (pfp_right_proper_left_add_result))) /\ (((((exists ff_h_pfp_proper_left_add_resulttarget. ff_h_pfp_proper_left_add_resulttarget + S (pfp_value_proper_left_add_result) = S ((S (pfp_index_proper_left_add_result)) * wc)) /\ exists ff_q_pfp_proper_left_add_resulttarget. wb = ff_q_pfp_proper_left_add_resulttarget * S ((S (pfp_index_proper_left_add_result)) * wc) + (pfp_value_proper_left_add_result))) /\ ((((exists pfa_gap_proper_left_add_resultoperationleft. pfa_gap_proper_left_add_resultoperationleft + S (pfp_left_proper_left_add_result) = (p)) /\ (((exists pfa_gap_proper_left_add_resultoperationright. pfa_gap_proper_left_add_resultoperationright + S (pfp_right_proper_left_add_result) = (p)) /\ ((((exists pfa_gap_proper_left_add_resultoperationresultbound. pfa_gap_proper_left_add_resultoperationresultbound + S (pfp_value_proper_left_add_result) = (p)) /\ ((exists pfa_offset_left_proper_left_add_resultoperationresultcongruence pfa_offset_right_proper_left_add_resultoperationresultcongruence. ((pfp_left_proper_left_add_result) + (pfp_right_proper_left_add_result)) + (p) * pfa_offset_left_proper_left_add_resultoperationresultcongruence = (pfp_value_proper_left_add_result) + (p) * pfa_offset_right_proper_left_add_resultoperationresultcongruence))))))))))))))))