prime_field_polynomial_left_distributive_products_exists

Exact expanded first-order arithmetic statement

forall p ab ac bb bc cb cc L db dc M. (~(p=0)) -> (forall fom_index_pfp_products_left_fixed_input. (exists fom_gap_pfp_products_left_fixed_input_index_bound. fom_gap_pfp_products_left_fixed_input_index_bound + S (fom_index_pfp_products_left_fixed_input) = M) -> exists fom_value_pfp_products_left_fixed_input. ((((exists fom_beta_height_pfp_products_left_fixed_input_entry. fom_beta_height_pfp_products_left_fixed_input_entry + S (fom_value_pfp_products_left_fixed_input) = S ((S (fom_index_pfp_products_left_fixed_input)) * dc)) /\ exists fom_beta_quotient_pfp_products_left_fixed_input_entry. db = fom_beta_quotient_pfp_products_left_fixed_input_entry * S ((S (fom_index_pfp_products_left_fixed_input)) * dc) + (fom_value_pfp_products_left_fixed_input))) /\ (exists fom_gap_pfp_products_left_fixed_input_value_bound. fom_gap_pfp_products_left_fixed_input_value_bound + S (fom_value_pfp_products_left_fixed_input) = p))) -> (forall pfp_index_products_left_input_addition. (exists pfa_gap_products_left_input_additionindex. pfa_gap_products_left_input_additionindex + S (pfp_index_products_left_input_addition) = (L)) -> exists pfp_left_products_left_input_addition pfp_right_products_left_input_addition pfp_value_products_left_input_addition. ((((exists ff_h_pfp_products_left_input_additionleft. ff_h_pfp_products_left_input_additionleft + S (pfp_left_products_left_input_addition) = S ((S (pfp_index_products_left_input_addition)) * ac)) /\ exists ff_q_pfp_products_left_input_additionleft. ab = ff_q_pfp_products_left_input_additionleft * S ((S (pfp_index_products_left_input_addition)) * ac) + (pfp_left_products_left_input_addition))) /\ (((((exists ff_h_pfp_products_left_input_additionright. ff_h_pfp_products_left_input_additionright + S (pfp_right_products_left_input_addition) = S ((S (pfp_index_products_left_input_addition)) * bc)) /\ exists ff_q_pfp_products_left_input_additionright. bb = ff_q_pfp_products_left_input_additionright * S ((S (pfp_index_products_left_input_addition)) * bc) + (pfp_right_products_left_input_addition))) /\ (((((exists ff_h_pfp_products_left_input_additiontarget. ff_h_pfp_products_left_input_additiontarget + S (pfp_value_products_left_input_addition) = S ((S (pfp_index_products_left_input_addition)) * cc)) /\ exists ff_q_pfp_products_left_input_additiontarget. cb = ff_q_pfp_products_left_input_additiontarget * S ((S (pfp_index_products_left_input_addition)) * cc) + (pfp_value_products_left_input_addition))) /\ ((((exists pfa_gap_products_left_input_additionoperationleft. pfa_gap_products_left_input_additionoperationleft + S (pfp_left_products_left_input_addition) = (p)) /\ (((exists pfa_gap_products_left_input_additionoperationright. pfa_gap_products_left_input_additionoperationright + S (pfp_right_products_left_input_addition) = (p)) /\ ((((exists pfa_gap_products_left_input_additionoperationresultbound. pfa_gap_products_left_input_additionoperationresultbound + S (pfp_value_products_left_input_addition) = (p)) /\ ((exists pfa_offset_left_products_left_input_additionoperationresultcongruence pfa_offset_right_products_left_input_additionoperationresultcongruence. ((pfp_left_products_left_input_addition) + (pfp_right_products_left_input_addition)) + (p) * pfa_offset_left_products_left_input_additionoperationresultcongruence = (pfp_value_products_left_input_addition) + (p) * pfa_offset_right_products_left_input_additionoperationresultcongruence)))))))))))))))) -> (exists N ub uc vb vc wb wc. ((((forall fom_index_pfp_products_left_result_ubleft. (exists fom_gap_pfp_products_left_result_ubleft_index_bound. fom_gap_pfp_products_left_result_ubleft_index_bound + S (fom_index_pfp_products_left_result_ubleft) = M) -> exists fom_value_pfp_products_left_result_ubleft. ((((exists fom_beta_height_pfp_products_left_result_ubleft_entry. fom_beta_height_pfp_products_left_result_ubleft_entry + S (fom_value_pfp_products_left_result_ubleft) = S ((S (fom_index_pfp_products_left_result_ubleft)) * dc)) /\ exists fom_beta_quotient_pfp_products_left_result_ubleft_entry. db = fom_beta_quotient_pfp_products_left_result_ubleft_entry * S ((S (fom_index_pfp_products_left_result_ubleft)) * dc) + (fom_value_pfp_products_left_result_ubleft))) /\ (exists fom_gap_pfp_products_left_result_ubleft_value_bound. fom_gap_pfp_products_left_result_ubleft_value_bound + S (fom_value_pfp_products_left_result_ubleft) = p))) /\ (((forall fom_index_pfp_products_left_result_ubright. (exists fom_gap_pfp_products_left_result_ubright_index_bound. fom_gap_pfp_products_left_result_ubright_index_bound + S (fom_index_pfp_products_left_result_ubright) = L) -> exists fom_value_pfp_products_left_result_ubright. ((((exists fom_beta_height_pfp_products_left_result_ubright_entry. fom_beta_height_pfp_products_left_result_ubright_entry + S (fom_value_pfp_products_left_result_ubright) = S ((S (fom_index_pfp_products_left_result_ubright)) * ac)) /\ exists fom_beta_quotient_pfp_products_left_result_ubright_entry. ab = fom_beta_quotient_pfp_products_left_result_ubright_entry * S ((S (fom_index_pfp_products_left_result_ubright)) * ac) + (fom_value_pfp_products_left_result_ubright))) /\ (exists fom_gap_pfp_products_left_result_ubright_value_bound. fom_gap_pfp_products_left_result_ubright_value_bound + S (fom_value_pfp_products_left_result_ubright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_products_left_result_ubcoefficients. (exists pfa_gap_products_left_result_ubcoefficientsbound. pfa_gap_products_left_result_ubcoefficientsbound + S (pfc_index_products_left_result_ubcoefficients) = (N)) -> exists pfc_value_products_left_result_ubcoefficients. ((((exists ff_h_pfp_products_left_result_ubcoefficientsentry. ff_h_pfp_products_left_result_ubcoefficientsentry + S (pfc_value_products_left_result_ubcoefficients) = S ((S (pfc_index_products_left_result_ubcoefficients)) * uc)) /\ exists ff_q_pfp_products_left_result_ubcoefficientsentry. ub = ff_q_pfp_products_left_result_ubcoefficientsentry * S ((S (pfc_index_products_left_result_ubcoefficients)) * uc) + (pfc_value_products_left_result_ubcoefficients))) /\ ((exists pfc_terms_code_products_left_result_ubcoefficientscoefficient pfc_terms_scale_products_left_result_ubcoefficientscoefficient pfc_natural_sum_products_left_result_ubcoefficientscoefficient. ((forall pfc_index_products_left_result_ubcoefficientscoefficientdiagonal. (exists pfa_gap_products_left_result_ubcoefficientscoefficientdiagonalbound. pfa_gap_products_left_result_ubcoefficientscoefficientdiagonalbound + S (pfc_index_products_left_result_ubcoefficientscoefficientdiagonal) = (S (pfc_index_products_left_result_ubcoefficients))) -> exists pfc_value_products_left_result_ubcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_products_left_result_ubcoefficientscoefficientdiagonalentry. ff_h_pfp_products_left_result_ubcoefficientscoefficientdiagonalentry + S (pfc_value_products_left_result_ubcoefficientscoefficientdiagonal) = S ((S (pfc_index_products_left_result_ubcoefficientscoefficientdiagonal)) * pfc_terms_scale_products_left_result_ubcoefficientscoefficient)) /\ exists ff_q_pfp_products_left_result_ubcoefficientscoefficientdiagonalentry. pfc_terms_code_products_left_result_ubcoefficientscoefficient = ff_q_pfp_products_left_result_ubcoefficientscoefficientdiagonalentry * S ((S (pfc_index_products_left_result_ubcoefficientscoefficientdiagonal)) * pfc_terms_scale_products_left_result_ubcoefficientscoefficient) + (pfc_value_products_left_result_ubcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_products_left_result_ubcoefficientscoefficientdiagonalterm pfc_left_products_left_result_ubcoefficientscoefficientdiagonalterm pfc_right_products_left_result_ubcoefficientscoefficientdiagonalterm. (((pfc_index_products_left_result_ubcoefficientscoefficientdiagonal)+pfc_complement_products_left_result_ubcoefficientscoefficientdiagonalterm=(pfc_index_products_left_result_ubcoefficients)) /\ ((((((exists pfa_gap_products_left_result_ubcoefficientscoefficientdiagonaltermleftinside. pfa_gap_products_left_result_ubcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_products_left_result_ubcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_products_left_result_ubcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_products_left_result_ubcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_products_left_result_ubcoefficientscoefficientdiagonal)) * dc) + (pfc_left_products_left_result_ubcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_products_left_result_ubcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_products_left_result_ubcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_products_left_result_ubcoefficientscoefficientdiagonal)) /\ (((pfc_left_products_left_result_ubcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_products_left_result_ubcoefficientscoefficientdiagonaltermrightinside. pfa_gap_products_left_result_ubcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_products_left_result_ubcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_products_left_result_ubcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_products_left_result_ubcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_products_left_result_ubcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_products_left_result_ubcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_products_left_result_ubcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_products_left_result_ubcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_products_left_result_ubcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_products_left_result_ubcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_products_left_result_ubcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_products_left_result_ubcoefficientscoefficientdiagonal)=pfc_left_products_left_result_ubcoefficientscoefficientdiagonalterm*pfc_right_products_left_result_ubcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_products_left_result_ubcoefficientscoefficientsum fs_v_pfc_products_left_result_ubcoefficientscoefficientsum. ((((exists fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_start. fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_start. fs_u_pfc_products_left_result_ubcoefficientscoefficientsum = fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_terminal. fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_products_left_result_ubcoefficientscoefficient) = S ((S (S (pfc_index_products_left_result_ubcoefficients))) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_terminal. fs_u_pfc_products_left_result_ubcoefficientscoefficientsum = fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_products_left_result_ubcoefficients))) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum) + (pfc_natural_sum_products_left_result_ubcoefficientscoefficient))) /\ forall fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps = S (pfc_index_products_left_result_ubcoefficients)) -> exists fs_a_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps fs_r_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps fs_s_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_products_left_result_ubcoefficientscoefficient)) /\ exists fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_products_left_result_ubcoefficientscoefficient = fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_products_left_result_ubcoefficientscoefficient) + (fs_a_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_products_left_result_ubcoefficientscoefficientsum = fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum) + (fs_r_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_products_left_result_ubcoefficientscoefficientsum = fs_q_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_ubcoefficientscoefficientsum) + (fs_s_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps = fs_r_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps + fs_a_pfc_products_left_result_ubcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_products_left_result_ubcoefficientscoefficientresiduebound. pfa_gap_products_left_result_ubcoefficientscoefficientresiduebound + S (pfc_value_products_left_result_ubcoefficients) = (p)) /\ ((exists pfa_offset_left_products_left_result_ubcoefficientscoefficientresiduecongruence pfa_offset_right_products_left_result_ubcoefficientscoefficientresiduecongruence. (pfc_natural_sum_products_left_result_ubcoefficientscoefficient) + (p) * pfa_offset_left_products_left_result_ubcoefficientscoefficientresiduecongruence = (pfc_value_products_left_result_ubcoefficients) + (p) * pfa_offset_right_products_left_result_ubcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_products_left_result_vbleft. (exists fom_gap_pfp_products_left_result_vbleft_index_bound. fom_gap_pfp_products_left_result_vbleft_index_bound + S (fom_index_pfp_products_left_result_vbleft) = M) -> exists fom_value_pfp_products_left_result_vbleft. ((((exists fom_beta_height_pfp_products_left_result_vbleft_entry. fom_beta_height_pfp_products_left_result_vbleft_entry + S (fom_value_pfp_products_left_result_vbleft) = S ((S (fom_index_pfp_products_left_result_vbleft)) * dc)) /\ exists fom_beta_quotient_pfp_products_left_result_vbleft_entry. db = fom_beta_quotient_pfp_products_left_result_vbleft_entry * S ((S (fom_index_pfp_products_left_result_vbleft)) * dc) + (fom_value_pfp_products_left_result_vbleft))) /\ (exists fom_gap_pfp_products_left_result_vbleft_value_bound. fom_gap_pfp_products_left_result_vbleft_value_bound + S (fom_value_pfp_products_left_result_vbleft) = p))) /\ (((forall fom_index_pfp_products_left_result_vbright. (exists fom_gap_pfp_products_left_result_vbright_index_bound. fom_gap_pfp_products_left_result_vbright_index_bound + S (fom_index_pfp_products_left_result_vbright) = L) -> exists fom_value_pfp_products_left_result_vbright. ((((exists fom_beta_height_pfp_products_left_result_vbright_entry. fom_beta_height_pfp_products_left_result_vbright_entry + S (fom_value_pfp_products_left_result_vbright) = S ((S (fom_index_pfp_products_left_result_vbright)) * bc)) /\ exists fom_beta_quotient_pfp_products_left_result_vbright_entry. bb = fom_beta_quotient_pfp_products_left_result_vbright_entry * S ((S (fom_index_pfp_products_left_result_vbright)) * bc) + (fom_value_pfp_products_left_result_vbright))) /\ (exists fom_gap_pfp_products_left_result_vbright_value_bound. fom_gap_pfp_products_left_result_vbright_value_bound + S (fom_value_pfp_products_left_result_vbright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_products_left_result_vbcoefficients. (exists pfa_gap_products_left_result_vbcoefficientsbound. pfa_gap_products_left_result_vbcoefficientsbound + S (pfc_index_products_left_result_vbcoefficients) = (N)) -> exists pfc_value_products_left_result_vbcoefficients. ((((exists ff_h_pfp_products_left_result_vbcoefficientsentry. ff_h_pfp_products_left_result_vbcoefficientsentry + S (pfc_value_products_left_result_vbcoefficients) = S ((S (pfc_index_products_left_result_vbcoefficients)) * vc)) /\ exists ff_q_pfp_products_left_result_vbcoefficientsentry. vb = ff_q_pfp_products_left_result_vbcoefficientsentry * S ((S (pfc_index_products_left_result_vbcoefficients)) * vc) + (pfc_value_products_left_result_vbcoefficients))) /\ ((exists pfc_terms_code_products_left_result_vbcoefficientscoefficient pfc_terms_scale_products_left_result_vbcoefficientscoefficient pfc_natural_sum_products_left_result_vbcoefficientscoefficient. ((forall pfc_index_products_left_result_vbcoefficientscoefficientdiagonal. (exists pfa_gap_products_left_result_vbcoefficientscoefficientdiagonalbound. pfa_gap_products_left_result_vbcoefficientscoefficientdiagonalbound + S (pfc_index_products_left_result_vbcoefficientscoefficientdiagonal) = (S (pfc_index_products_left_result_vbcoefficients))) -> exists pfc_value_products_left_result_vbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_products_left_result_vbcoefficientscoefficientdiagonalentry. ff_h_pfp_products_left_result_vbcoefficientscoefficientdiagonalentry + S (pfc_value_products_left_result_vbcoefficientscoefficientdiagonal) = S ((S (pfc_index_products_left_result_vbcoefficientscoefficientdiagonal)) * pfc_terms_scale_products_left_result_vbcoefficientscoefficient)) /\ exists ff_q_pfp_products_left_result_vbcoefficientscoefficientdiagonalentry. pfc_terms_code_products_left_result_vbcoefficientscoefficient = ff_q_pfp_products_left_result_vbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_products_left_result_vbcoefficientscoefficientdiagonal)) * pfc_terms_scale_products_left_result_vbcoefficientscoefficient) + (pfc_value_products_left_result_vbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_products_left_result_vbcoefficientscoefficientdiagonalterm pfc_left_products_left_result_vbcoefficientscoefficientdiagonalterm pfc_right_products_left_result_vbcoefficientscoefficientdiagonalterm. (((pfc_index_products_left_result_vbcoefficientscoefficientdiagonal)+pfc_complement_products_left_result_vbcoefficientscoefficientdiagonalterm=(pfc_index_products_left_result_vbcoefficients)) /\ ((((((exists pfa_gap_products_left_result_vbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_products_left_result_vbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_products_left_result_vbcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_products_left_result_vbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_products_left_result_vbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_products_left_result_vbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_products_left_result_vbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_products_left_result_vbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_products_left_result_vbcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_products_left_result_vbcoefficientscoefficientdiagonal)) /\ (((pfc_left_products_left_result_vbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_products_left_result_vbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_products_left_result_vbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_products_left_result_vbcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_products_left_result_vbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_products_left_result_vbcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_products_left_result_vbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_products_left_result_vbcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_products_left_result_vbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_products_left_result_vbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_products_left_result_vbcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_products_left_result_vbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_products_left_result_vbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_products_left_result_vbcoefficientscoefficientdiagonal)=pfc_left_products_left_result_vbcoefficientscoefficientdiagonalterm*pfc_right_products_left_result_vbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_products_left_result_vbcoefficientscoefficientsum fs_v_pfc_products_left_result_vbcoefficientscoefficientsum. ((((exists fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_start. fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_start. fs_u_pfc_products_left_result_vbcoefficientscoefficientsum = fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_terminal. fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_products_left_result_vbcoefficientscoefficient) = S ((S (S (pfc_index_products_left_result_vbcoefficients))) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_terminal. fs_u_pfc_products_left_result_vbcoefficientscoefficientsum = fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_products_left_result_vbcoefficients))) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum) + (pfc_natural_sum_products_left_result_vbcoefficientscoefficient))) /\ forall fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps = S (pfc_index_products_left_result_vbcoefficients)) -> exists fs_a_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps fs_r_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps fs_s_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_products_left_result_vbcoefficientscoefficient)) /\ exists fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_products_left_result_vbcoefficientscoefficient = fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_products_left_result_vbcoefficientscoefficient) + (fs_a_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_products_left_result_vbcoefficientscoefficientsum = fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum) + (fs_r_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_products_left_result_vbcoefficientscoefficientsum = fs_q_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_vbcoefficientscoefficientsum) + (fs_s_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps = fs_r_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps + fs_a_pfc_products_left_result_vbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_products_left_result_vbcoefficientscoefficientresiduebound. pfa_gap_products_left_result_vbcoefficientscoefficientresiduebound + S (pfc_value_products_left_result_vbcoefficients) = (p)) /\ ((exists pfa_offset_left_products_left_result_vbcoefficientscoefficientresiduecongruence pfa_offset_right_products_left_result_vbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_products_left_result_vbcoefficientscoefficient) + (p) * pfa_offset_left_products_left_result_vbcoefficientscoefficientresiduecongruence = (pfc_value_products_left_result_vbcoefficients) + (p) * pfa_offset_right_products_left_result_vbcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_products_left_result_wbleft. (exists fom_gap_pfp_products_left_result_wbleft_index_bound. fom_gap_pfp_products_left_result_wbleft_index_bound + S (fom_index_pfp_products_left_result_wbleft) = M) -> exists fom_value_pfp_products_left_result_wbleft. ((((exists fom_beta_height_pfp_products_left_result_wbleft_entry. fom_beta_height_pfp_products_left_result_wbleft_entry + S (fom_value_pfp_products_left_result_wbleft) = S ((S (fom_index_pfp_products_left_result_wbleft)) * dc)) /\ exists fom_beta_quotient_pfp_products_left_result_wbleft_entry. db = fom_beta_quotient_pfp_products_left_result_wbleft_entry * S ((S (fom_index_pfp_products_left_result_wbleft)) * dc) + (fom_value_pfp_products_left_result_wbleft))) /\ (exists fom_gap_pfp_products_left_result_wbleft_value_bound. fom_gap_pfp_products_left_result_wbleft_value_bound + S (fom_value_pfp_products_left_result_wbleft) = p))) /\ (((forall fom_index_pfp_products_left_result_wbright. (exists fom_gap_pfp_products_left_result_wbright_index_bound. fom_gap_pfp_products_left_result_wbright_index_bound + S (fom_index_pfp_products_left_result_wbright) = L) -> exists fom_value_pfp_products_left_result_wbright. ((((exists fom_beta_height_pfp_products_left_result_wbright_entry. fom_beta_height_pfp_products_left_result_wbright_entry + S (fom_value_pfp_products_left_result_wbright) = S ((S (fom_index_pfp_products_left_result_wbright)) * cc)) /\ exists fom_beta_quotient_pfp_products_left_result_wbright_entry. cb = fom_beta_quotient_pfp_products_left_result_wbright_entry * S ((S (fom_index_pfp_products_left_result_wbright)) * cc) + (fom_value_pfp_products_left_result_wbright))) /\ (exists fom_gap_pfp_products_left_result_wbright_value_bound. fom_gap_pfp_products_left_result_wbright_value_bound + S (fom_value_pfp_products_left_result_wbright) = p))) /\ (((((((M)=0 \/ (L)=0) /\ (((N)=0)))) \/ (((~((M)=0)) /\ (((~((L)=0)) /\ (((M)+(L)=S (N)))))))) /\ ((forall pfc_index_products_left_result_wbcoefficients. (exists pfa_gap_products_left_result_wbcoefficientsbound. pfa_gap_products_left_result_wbcoefficientsbound + S (pfc_index_products_left_result_wbcoefficients) = (N)) -> exists pfc_value_products_left_result_wbcoefficients. ((((exists ff_h_pfp_products_left_result_wbcoefficientsentry. ff_h_pfp_products_left_result_wbcoefficientsentry + S (pfc_value_products_left_result_wbcoefficients) = S ((S (pfc_index_products_left_result_wbcoefficients)) * wc)) /\ exists ff_q_pfp_products_left_result_wbcoefficientsentry. wb = ff_q_pfp_products_left_result_wbcoefficientsentry * S ((S (pfc_index_products_left_result_wbcoefficients)) * wc) + (pfc_value_products_left_result_wbcoefficients))) /\ ((exists pfc_terms_code_products_left_result_wbcoefficientscoefficient pfc_terms_scale_products_left_result_wbcoefficientscoefficient pfc_natural_sum_products_left_result_wbcoefficientscoefficient. ((forall pfc_index_products_left_result_wbcoefficientscoefficientdiagonal. (exists pfa_gap_products_left_result_wbcoefficientscoefficientdiagonalbound. pfa_gap_products_left_result_wbcoefficientscoefficientdiagonalbound + S (pfc_index_products_left_result_wbcoefficientscoefficientdiagonal) = (S (pfc_index_products_left_result_wbcoefficients))) -> exists pfc_value_products_left_result_wbcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_products_left_result_wbcoefficientscoefficientdiagonalentry. ff_h_pfp_products_left_result_wbcoefficientscoefficientdiagonalentry + S (pfc_value_products_left_result_wbcoefficientscoefficientdiagonal) = S ((S (pfc_index_products_left_result_wbcoefficientscoefficientdiagonal)) * pfc_terms_scale_products_left_result_wbcoefficientscoefficient)) /\ exists ff_q_pfp_products_left_result_wbcoefficientscoefficientdiagonalentry. pfc_terms_code_products_left_result_wbcoefficientscoefficient = ff_q_pfp_products_left_result_wbcoefficientscoefficientdiagonalentry * S ((S (pfc_index_products_left_result_wbcoefficientscoefficientdiagonal)) * pfc_terms_scale_products_left_result_wbcoefficientscoefficient) + (pfc_value_products_left_result_wbcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_products_left_result_wbcoefficientscoefficientdiagonalterm pfc_left_products_left_result_wbcoefficientscoefficientdiagonalterm pfc_right_products_left_result_wbcoefficientscoefficientdiagonalterm. (((pfc_index_products_left_result_wbcoefficientscoefficientdiagonal)+pfc_complement_products_left_result_wbcoefficientscoefficientdiagonalterm=(pfc_index_products_left_result_wbcoefficients)) /\ ((((((exists pfa_gap_products_left_result_wbcoefficientscoefficientdiagonaltermleftinside. pfa_gap_products_left_result_wbcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_products_left_result_wbcoefficientscoefficientdiagonal) = (M)) /\ ((((exists ff_h_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_products_left_result_wbcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_products_left_result_wbcoefficientscoefficientdiagonal)) * dc)) /\ exists ff_q_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermleftentry. db = ff_q_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_products_left_result_wbcoefficientscoefficientdiagonal)) * dc) + (pfc_left_products_left_result_wbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_products_left_result_wbcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_products_left_result_wbcoefficientscoefficientdiagonaltermleftoutside+(M)=(pfc_index_products_left_result_wbcoefficientscoefficientdiagonal)) /\ (((pfc_left_products_left_result_wbcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_products_left_result_wbcoefficientscoefficientdiagonaltermrightinside. pfa_gap_products_left_result_wbcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_products_left_result_wbcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_products_left_result_wbcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_products_left_result_wbcoefficientscoefficientdiagonalterm)) * cc)) /\ exists ff_q_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermrightentry. cb = ff_q_pfp_products_left_result_wbcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_products_left_result_wbcoefficientscoefficientdiagonalterm)) * cc) + (pfc_right_products_left_result_wbcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_products_left_result_wbcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_products_left_result_wbcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_products_left_result_wbcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_products_left_result_wbcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_products_left_result_wbcoefficientscoefficientdiagonal)=pfc_left_products_left_result_wbcoefficientscoefficientdiagonalterm*pfc_right_products_left_result_wbcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_products_left_result_wbcoefficientscoefficientsum fs_v_pfc_products_left_result_wbcoefficientscoefficientsum. ((((exists fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_start. fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_start. fs_u_pfc_products_left_result_wbcoefficientscoefficientsum = fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_terminal. fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_products_left_result_wbcoefficientscoefficient) = S ((S (S (pfc_index_products_left_result_wbcoefficients))) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_terminal. fs_u_pfc_products_left_result_wbcoefficientscoefficientsum = fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_products_left_result_wbcoefficients))) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum) + (pfc_natural_sum_products_left_result_wbcoefficientscoefficient))) /\ forall fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps = S (pfc_index_products_left_result_wbcoefficients)) -> exists fs_a_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps fs_r_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps fs_s_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_products_left_result_wbcoefficientscoefficient)) /\ exists fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_products_left_result_wbcoefficientscoefficient = fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_products_left_result_wbcoefficientscoefficient) + (fs_a_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_products_left_result_wbcoefficientscoefficientsum = fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum) + (fs_r_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum)) /\ exists fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_products_left_result_wbcoefficientscoefficientsum = fs_q_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps)) * fs_v_pfc_products_left_result_wbcoefficientscoefficientsum) + (fs_s_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps = fs_r_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps + fs_a_pfc_products_left_result_wbcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_products_left_result_wbcoefficientscoefficientresiduebound. pfa_gap_products_left_result_wbcoefficientscoefficientresiduebound + S (pfc_value_products_left_result_wbcoefficients) = (p)) /\ ((exists pfa_offset_left_products_left_result_wbcoefficientscoefficientresiduecongruence pfa_offset_right_products_left_result_wbcoefficientscoefficientresiduecongruence. (pfc_natural_sum_products_left_result_wbcoefficientscoefficient) + (p) * pfa_offset_left_products_left_result_wbcoefficientscoefficientresiduecongruence = (pfc_value_products_left_result_wbcoefficients) + (p) * pfa_offset_right_products_left_result_wbcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfp_index_products_left_addition. (exists pfa_gap_products_left_additionindex. pfa_gap_products_left_additionindex + S (pfp_index_products_left_addition) = (N)) -> exists pfp_left_products_left_addition pfp_right_products_left_addition pfp_value_products_left_addition. ((((exists ff_h_pfp_products_left_additionleft. ff_h_pfp_products_left_additionleft + S (pfp_left_products_left_addition) = S ((S (pfp_index_products_left_addition)) * uc)) /\ exists ff_q_pfp_products_left_additionleft. ub = ff_q_pfp_products_left_additionleft * S ((S (pfp_index_products_left_addition)) * uc) + (pfp_left_products_left_addition))) /\ (((((exists ff_h_pfp_products_left_additionright. ff_h_pfp_products_left_additionright + S (pfp_right_products_left_addition) = S ((S (pfp_index_products_left_addition)) * vc)) /\ exists ff_q_pfp_products_left_additionright. vb = ff_q_pfp_products_left_additionright * S ((S (pfp_index_products_left_addition)) * vc) + (pfp_right_products_left_addition))) /\ (((((exists ff_h_pfp_products_left_additiontarget. ff_h_pfp_products_left_additiontarget + S (pfp_value_products_left_addition) = S ((S (pfp_index_products_left_addition)) * wc)) /\ exists ff_q_pfp_products_left_additiontarget. wb = ff_q_pfp_products_left_additiontarget * S ((S (pfp_index_products_left_addition)) * wc) + (pfp_value_products_left_addition))) /\ ((((exists pfa_gap_products_left_additionoperationleft. pfa_gap_products_left_additionoperationleft + S (pfp_left_products_left_addition) = (p)) /\ (((exists pfa_gap_products_left_additionoperationright. pfa_gap_products_left_additionoperationright + S (pfp_right_products_left_addition) = (p)) /\ ((((exists pfa_gap_products_left_additionoperationresultbound. pfa_gap_products_left_additionoperationresultbound + S (pfp_value_products_left_addition) = (p)) /\ ((exists pfa_offset_left_products_left_additionoperationresultcongruence pfa_offset_right_products_left_additionoperationresultcongruence. ((pfp_left_products_left_addition) + (pfp_right_products_left_addition)) + (p) * pfa_offset_left_products_left_additionoperationresultcongruence = (pfp_value_products_left_addition) + (p) * pfa_offset_right_products_left_additionoperationresultcongruence)))))))))))))))))))))))