prime_field_polynomial_right_divides_left_product

Exact expanded first-order arithmetic statement

forall p db dc J bb bc M qb qc H pb pc I. (~((p) = 1) /\ forall pfa_factor_left_left_product_prime pfa_factor_right_left_product_prime. (p) = pfa_factor_left_left_product_prime * pfa_factor_right_left_product_prime -> pfa_factor_left_left_product_prime = 1 \/ pfa_factor_right_left_product_prime = 1) -> (((forall fom_index_pfp_left_product_divisor_canonical. (exists fom_gap_pfp_left_product_divisor_canonical_index_bound. fom_gap_pfp_left_product_divisor_canonical_index_bound + S (fom_index_pfp_left_product_divisor_canonical) = M) -> exists fom_value_pfp_left_product_divisor_canonical. ((((exists fom_beta_height_pfp_left_product_divisor_canonical_entry. fom_beta_height_pfp_left_product_divisor_canonical_entry + S (fom_value_pfp_left_product_divisor_canonical) = S ((S (fom_index_pfp_left_product_divisor_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_left_product_divisor_canonical_entry. bb = fom_beta_quotient_pfp_left_product_divisor_canonical_entry * S ((S (fom_index_pfp_left_product_divisor_canonical)) * bc) + (fom_value_pfp_left_product_divisor_canonical))) /\ (exists fom_gap_pfp_left_product_divisor_canonical_value_bound. fom_gap_pfp_left_product_divisor_canonical_value_bound + S (fom_value_pfp_left_product_divisor_canonical) = p))) /\ ((exists pfrd_qb_left_product_divisor pfrd_qc_left_product_divisor pfrd_qlen_left_product_divisor pfrd_pb_left_product_divisor pfrd_pc_left_product_divisor pfrd_plen_left_product_divisor. ((((forall fom_index_pfp_left_product_divisor_productleft. (exists fom_gap_pfp_left_product_divisor_productleft_index_bound. fom_gap_pfp_left_product_divisor_productleft_index_bound + S (fom_index_pfp_left_product_divisor_productleft) = pfrd_qlen_left_product_divisor) -> exists fom_value_pfp_left_product_divisor_productleft. ((((exists fom_beta_height_pfp_left_product_divisor_productleft_entry. fom_beta_height_pfp_left_product_divisor_productleft_entry + S (fom_value_pfp_left_product_divisor_productleft) = S ((S (fom_index_pfp_left_product_divisor_productleft)) * pfrd_qc_left_product_divisor)) /\ exists fom_beta_quotient_pfp_left_product_divisor_productleft_entry. pfrd_qb_left_product_divisor = fom_beta_quotient_pfp_left_product_divisor_productleft_entry * S ((S (fom_index_pfp_left_product_divisor_productleft)) * pfrd_qc_left_product_divisor) + (fom_value_pfp_left_product_divisor_productleft))) /\ (exists fom_gap_pfp_left_product_divisor_productleft_value_bound. fom_gap_pfp_left_product_divisor_productleft_value_bound + S (fom_value_pfp_left_product_divisor_productleft) = p))) /\ (((forall fom_index_pfp_left_product_divisor_productright. (exists fom_gap_pfp_left_product_divisor_productright_index_bound. fom_gap_pfp_left_product_divisor_productright_index_bound + S (fom_index_pfp_left_product_divisor_productright) = J) -> exists fom_value_pfp_left_product_divisor_productright. ((((exists fom_beta_height_pfp_left_product_divisor_productright_entry. fom_beta_height_pfp_left_product_divisor_productright_entry + S (fom_value_pfp_left_product_divisor_productright) = S ((S (fom_index_pfp_left_product_divisor_productright)) * dc)) /\ exists fom_beta_quotient_pfp_left_product_divisor_productright_entry. db = fom_beta_quotient_pfp_left_product_divisor_productright_entry * S ((S (fom_index_pfp_left_product_divisor_productright)) * dc) + (fom_value_pfp_left_product_divisor_productright))) /\ (exists fom_gap_pfp_left_product_divisor_productright_value_bound. fom_gap_pfp_left_product_divisor_productright_value_bound + S (fom_value_pfp_left_product_divisor_productright) = p))) /\ (((((((pfrd_qlen_left_product_divisor)=0 \/ (J)=0) /\ (((pfrd_plen_left_product_divisor)=0)))) \/ (((~((pfrd_qlen_left_product_divisor)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_left_product_divisor)+(J)=S (pfrd_plen_left_product_divisor)))))))) /\ ((forall pfc_index_left_product_divisor_productcoefficients. (exists pfa_gap_left_product_divisor_productcoefficientsbound. pfa_gap_left_product_divisor_productcoefficientsbound + S (pfc_index_left_product_divisor_productcoefficients) = (pfrd_plen_left_product_divisor)) -> exists pfc_value_left_product_divisor_productcoefficients. ((((exists ff_h_pfp_left_product_divisor_productcoefficientsentry. ff_h_pfp_left_product_divisor_productcoefficientsentry + S (pfc_value_left_product_divisor_productcoefficients) = S ((S (pfc_index_left_product_divisor_productcoefficients)) * pfrd_pc_left_product_divisor)) /\ exists ff_q_pfp_left_product_divisor_productcoefficientsentry. pfrd_pb_left_product_divisor = ff_q_pfp_left_product_divisor_productcoefficientsentry * S ((S (pfc_index_left_product_divisor_productcoefficients)) * pfrd_pc_left_product_divisor) + (pfc_value_left_product_divisor_productcoefficients))) /\ ((exists pfc_terms_code_left_product_divisor_productcoefficientscoefficient pfc_terms_scale_left_product_divisor_productcoefficientscoefficient pfc_natural_sum_left_product_divisor_productcoefficientscoefficient. ((forall pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal. (exists pfa_gap_left_product_divisor_productcoefficientscoefficientdiagonalbound. pfa_gap_left_product_divisor_productcoefficientscoefficientdiagonalbound + S (pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal) = (S (pfc_index_left_product_divisor_productcoefficients))) -> exists pfc_value_left_product_divisor_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_left_product_divisor_productcoefficientscoefficientdiagonalentry. ff_h_pfp_left_product_divisor_productcoefficientscoefficientdiagonalentry + S (pfc_value_left_product_divisor_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_product_divisor_productcoefficientscoefficient)) /\ exists ff_q_pfp_left_product_divisor_productcoefficientscoefficientdiagonalentry. pfc_terms_code_left_product_divisor_productcoefficientscoefficient = ff_q_pfp_left_product_divisor_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_product_divisor_productcoefficientscoefficient) + (pfc_value_left_product_divisor_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_left_product_divisor_productcoefficientscoefficientdiagonalterm pfc_left_left_product_divisor_productcoefficientscoefficientdiagonalterm pfc_right_left_product_divisor_productcoefficientscoefficientdiagonalterm. (((pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal)+pfc_complement_left_product_divisor_productcoefficientscoefficientdiagonalterm=(pfc_index_left_product_divisor_productcoefficients)) /\ ((((((exists pfa_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal) = (pfrd_qlen_left_product_divisor)) /\ ((((exists ff_h_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_left_product_divisor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal)) * pfrd_qc_left_product_divisor)) /\ exists ff_q_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_left_product_divisor = ff_q_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal)) * pfrd_qc_left_product_divisor) + (pfc_left_left_product_divisor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_left_product_divisor)=(pfc_index_left_product_divisor_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_left_product_divisor_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_left_product_divisor_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_left_product_divisor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_left_product_divisor_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_left_product_divisor_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_left_product_divisor_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_left_product_divisor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_left_product_divisor_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_left_product_divisor_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_left_product_divisor_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_left_product_divisor_productcoefficientscoefficientdiagonal)=pfc_left_left_product_divisor_productcoefficientscoefficientdiagonalterm*pfc_right_left_product_divisor_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_left_product_divisor_productcoefficientscoefficientsum fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum. ((((exists fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_start. fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_start. fs_u_pfc_left_product_divisor_productcoefficientscoefficientsum = fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_left_product_divisor_productcoefficientscoefficient) = S ((S (S (pfc_index_left_product_divisor_productcoefficients))) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_left_product_divisor_productcoefficientscoefficientsum = fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_left_product_divisor_productcoefficients))) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum) + (pfc_natural_sum_left_product_divisor_productcoefficientscoefficient))) /\ forall fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps = S (pfc_index_left_product_divisor_productcoefficients)) -> exists fs_a_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps fs_r_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps fs_s_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_product_divisor_productcoefficientscoefficient)) /\ exists fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_left_product_divisor_productcoefficientscoefficient = fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_product_divisor_productcoefficientscoefficient) + (fs_a_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_left_product_divisor_productcoefficientscoefficientsum = fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum) + (fs_r_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_left_product_divisor_productcoefficientscoefficientsum = fs_q_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_divisor_productcoefficientscoefficientsum) + (fs_s_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps = fs_r_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps + fs_a_pfc_left_product_divisor_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_left_product_divisor_productcoefficientscoefficientresiduebound. pfa_gap_left_product_divisor_productcoefficientscoefficientresiduebound + S (pfc_value_left_product_divisor_productcoefficients) = (p)) /\ ((exists pfa_offset_left_left_product_divisor_productcoefficientscoefficientresiduecongruence pfa_offset_right_left_product_divisor_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_left_product_divisor_productcoefficientscoefficient) + (p) * pfa_offset_left_left_product_divisor_productcoefficientscoefficientresiduecongruence = (pfc_value_left_product_divisor_productcoefficients) + (p) * pfa_offset_right_left_product_divisor_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_left_product_divisor_target pfrep_left_left_product_divisor_target pfrep_right_left_product_divisor_target. ((exists pfrep_position_left_product_divisor_targetfirst. ((pfrep_position_left_product_divisor_targetfirst+S (pfrep_power_left_product_divisor_target)=(pfrd_plen_left_product_divisor)) /\ ((((exists ff_h_pfp_left_product_divisor_targetfirstentry. ff_h_pfp_left_product_divisor_targetfirstentry + S (pfrep_left_left_product_divisor_target) = S ((S (pfrep_position_left_product_divisor_targetfirst)) * pfrd_pc_left_product_divisor)) /\ exists ff_q_pfp_left_product_divisor_targetfirstentry. pfrd_pb_left_product_divisor = ff_q_pfp_left_product_divisor_targetfirstentry * S ((S (pfrep_position_left_product_divisor_targetfirst)) * pfrd_pc_left_product_divisor) + (pfrep_left_left_product_divisor_target)))))) \/ (((exists pfrep_gap_left_product_divisor_targetfirstoutside. pfrep_gap_left_product_divisor_targetfirstoutside+(pfrd_plen_left_product_divisor)=(pfrep_power_left_product_divisor_target)) /\ (((pfrep_left_left_product_divisor_target)=0))))) -> ((exists pfrep_position_left_product_divisor_targetsecond. ((pfrep_position_left_product_divisor_targetsecond+S (pfrep_power_left_product_divisor_target)=(M)) /\ ((((exists ff_h_pfp_left_product_divisor_targetsecondentry. ff_h_pfp_left_product_divisor_targetsecondentry + S (pfrep_right_left_product_divisor_target) = S ((S (pfrep_position_left_product_divisor_targetsecond)) * bc)) /\ exists ff_q_pfp_left_product_divisor_targetsecondentry. bb = ff_q_pfp_left_product_divisor_targetsecondentry * S ((S (pfrep_position_left_product_divisor_targetsecond)) * bc) + (pfrep_right_left_product_divisor_target)))))) \/ (((exists pfrep_gap_left_product_divisor_targetsecondoutside. pfrep_gap_left_product_divisor_targetsecondoutside+(M)=(pfrep_power_left_product_divisor_target)) /\ (((pfrep_right_left_product_divisor_target)=0))))) -> pfrep_left_left_product_divisor_target=pfrep_right_left_product_divisor_target))))))) -> (((forall fom_index_pfp_left_product_actualleft. (exists fom_gap_pfp_left_product_actualleft_index_bound. fom_gap_pfp_left_product_actualleft_index_bound + S (fom_index_pfp_left_product_actualleft) = H) -> exists fom_value_pfp_left_product_actualleft. ((((exists fom_beta_height_pfp_left_product_actualleft_entry. fom_beta_height_pfp_left_product_actualleft_entry + S (fom_value_pfp_left_product_actualleft) = S ((S (fom_index_pfp_left_product_actualleft)) * qc)) /\ exists fom_beta_quotient_pfp_left_product_actualleft_entry. qb = fom_beta_quotient_pfp_left_product_actualleft_entry * S ((S (fom_index_pfp_left_product_actualleft)) * qc) + (fom_value_pfp_left_product_actualleft))) /\ (exists fom_gap_pfp_left_product_actualleft_value_bound. fom_gap_pfp_left_product_actualleft_value_bound + S (fom_value_pfp_left_product_actualleft) = p))) /\ (((forall fom_index_pfp_left_product_actualright. (exists fom_gap_pfp_left_product_actualright_index_bound. fom_gap_pfp_left_product_actualright_index_bound + S (fom_index_pfp_left_product_actualright) = M) -> exists fom_value_pfp_left_product_actualright. ((((exists fom_beta_height_pfp_left_product_actualright_entry. fom_beta_height_pfp_left_product_actualright_entry + S (fom_value_pfp_left_product_actualright) = S ((S (fom_index_pfp_left_product_actualright)) * bc)) /\ exists fom_beta_quotient_pfp_left_product_actualright_entry. bb = fom_beta_quotient_pfp_left_product_actualright_entry * S ((S (fom_index_pfp_left_product_actualright)) * bc) + (fom_value_pfp_left_product_actualright))) /\ (exists fom_gap_pfp_left_product_actualright_value_bound. fom_gap_pfp_left_product_actualright_value_bound + S (fom_value_pfp_left_product_actualright) = p))) /\ (((((((H)=0 \/ (M)=0) /\ (((I)=0)))) \/ (((~((H)=0)) /\ (((~((M)=0)) /\ (((H)+(M)=S (I)))))))) /\ ((forall pfc_index_left_product_actualcoefficients. (exists pfa_gap_left_product_actualcoefficientsbound. pfa_gap_left_product_actualcoefficientsbound + S (pfc_index_left_product_actualcoefficients) = (I)) -> exists pfc_value_left_product_actualcoefficients. ((((exists ff_h_pfp_left_product_actualcoefficientsentry. ff_h_pfp_left_product_actualcoefficientsentry + S (pfc_value_left_product_actualcoefficients) = S ((S (pfc_index_left_product_actualcoefficients)) * pc)) /\ exists ff_q_pfp_left_product_actualcoefficientsentry. pb = ff_q_pfp_left_product_actualcoefficientsentry * S ((S (pfc_index_left_product_actualcoefficients)) * pc) + (pfc_value_left_product_actualcoefficients))) /\ ((exists pfc_terms_code_left_product_actualcoefficientscoefficient pfc_terms_scale_left_product_actualcoefficientscoefficient pfc_natural_sum_left_product_actualcoefficientscoefficient. ((forall pfc_index_left_product_actualcoefficientscoefficientdiagonal. (exists pfa_gap_left_product_actualcoefficientscoefficientdiagonalbound. pfa_gap_left_product_actualcoefficientscoefficientdiagonalbound + S (pfc_index_left_product_actualcoefficientscoefficientdiagonal) = (S (pfc_index_left_product_actualcoefficients))) -> exists pfc_value_left_product_actualcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_left_product_actualcoefficientscoefficientdiagonalentry. ff_h_pfp_left_product_actualcoefficientscoefficientdiagonalentry + S (pfc_value_left_product_actualcoefficientscoefficientdiagonal) = S ((S (pfc_index_left_product_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_product_actualcoefficientscoefficient)) /\ exists ff_q_pfp_left_product_actualcoefficientscoefficientdiagonalentry. pfc_terms_code_left_product_actualcoefficientscoefficient = ff_q_pfp_left_product_actualcoefficientscoefficientdiagonalentry * S ((S (pfc_index_left_product_actualcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_product_actualcoefficientscoefficient) + (pfc_value_left_product_actualcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_left_product_actualcoefficientscoefficientdiagonalterm pfc_left_left_product_actualcoefficientscoefficientdiagonalterm pfc_right_left_product_actualcoefficientscoefficientdiagonalterm. (((pfc_index_left_product_actualcoefficientscoefficientdiagonal)+pfc_complement_left_product_actualcoefficientscoefficientdiagonalterm=(pfc_index_left_product_actualcoefficients)) /\ ((((((exists pfa_gap_left_product_actualcoefficientscoefficientdiagonaltermleftinside. pfa_gap_left_product_actualcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_left_product_actualcoefficientscoefficientdiagonal) = (H)) /\ ((((exists ff_h_pfp_left_product_actualcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_left_product_actualcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_left_product_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_left_product_actualcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_left_product_actualcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_left_product_actualcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_left_product_actualcoefficientscoefficientdiagonal)) * qc) + (pfc_left_left_product_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_product_actualcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_left_product_actualcoefficientscoefficientdiagonaltermleftoutside+(H)=(pfc_index_left_product_actualcoefficientscoefficientdiagonal)) /\ (((pfc_left_left_product_actualcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_left_product_actualcoefficientscoefficientdiagonaltermrightinside. pfa_gap_left_product_actualcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_left_product_actualcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_left_product_actualcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_left_product_actualcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_left_product_actualcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_left_product_actualcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_left_product_actualcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_left_product_actualcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_left_product_actualcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_left_product_actualcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_product_actualcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_left_product_actualcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_left_product_actualcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_left_product_actualcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_left_product_actualcoefficientscoefficientdiagonal)=pfc_left_left_product_actualcoefficientscoefficientdiagonalterm*pfc_right_left_product_actualcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_left_product_actualcoefficientscoefficientsum fs_v_pfc_left_product_actualcoefficientscoefficientsum. ((((exists fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_start. fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_start. fs_u_pfc_left_product_actualcoefficientscoefficientsum = fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_left_product_actualcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_terminal. fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_left_product_actualcoefficientscoefficient) = S ((S (S (pfc_index_left_product_actualcoefficients))) * fs_v_pfc_left_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_terminal. fs_u_pfc_left_product_actualcoefficientscoefficientsum = fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_left_product_actualcoefficients))) * fs_v_pfc_left_product_actualcoefficientscoefficientsum) + (pfc_natural_sum_left_product_actualcoefficientscoefficient))) /\ forall fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_left_product_actualcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_left_product_actualcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps = S (pfc_index_left_product_actualcoefficients)) -> exists fs_a_pfc_left_product_actualcoefficientscoefficientsum_body_steps fs_r_pfc_left_product_actualcoefficientscoefficientsum_body_steps fs_s_pfc_left_product_actualcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_left_product_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_product_actualcoefficientscoefficient)) /\ exists fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_left_product_actualcoefficientscoefficient = fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_product_actualcoefficientscoefficient) + (fs_a_pfc_left_product_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_left_product_actualcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_left_product_actualcoefficientscoefficientsum = fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_actualcoefficientscoefficientsum) + (fs_r_pfc_left_product_actualcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_left_product_actualcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_left_product_actualcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_actualcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_left_product_actualcoefficientscoefficientsum = fs_q_pfc_left_product_actualcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_left_product_actualcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_actualcoefficientscoefficientsum) + (fs_s_pfc_left_product_actualcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_left_product_actualcoefficientscoefficientsum_body_steps = fs_r_pfc_left_product_actualcoefficientscoefficientsum_body_steps + fs_a_pfc_left_product_actualcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_left_product_actualcoefficientscoefficientresiduebound. pfa_gap_left_product_actualcoefficientscoefficientresiduebound + S (pfc_value_left_product_actualcoefficients) = (p)) /\ ((exists pfa_offset_left_left_product_actualcoefficientscoefficientresiduecongruence pfa_offset_right_left_product_actualcoefficientscoefficientresiduecongruence. (pfc_natural_sum_left_product_actualcoefficientscoefficient) + (p) * pfa_offset_left_left_product_actualcoefficientscoefficientresiduecongruence = (pfc_value_left_product_actualcoefficients) + (p) * pfa_offset_right_left_product_actualcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_left_product_result_canonical. (exists fom_gap_pfp_left_product_result_canonical_index_bound. fom_gap_pfp_left_product_result_canonical_index_bound + S (fom_index_pfp_left_product_result_canonical) = I) -> exists fom_value_pfp_left_product_result_canonical. ((((exists fom_beta_height_pfp_left_product_result_canonical_entry. fom_beta_height_pfp_left_product_result_canonical_entry + S (fom_value_pfp_left_product_result_canonical) = S ((S (fom_index_pfp_left_product_result_canonical)) * pc)) /\ exists fom_beta_quotient_pfp_left_product_result_canonical_entry. pb = fom_beta_quotient_pfp_left_product_result_canonical_entry * S ((S (fom_index_pfp_left_product_result_canonical)) * pc) + (fom_value_pfp_left_product_result_canonical))) /\ (exists fom_gap_pfp_left_product_result_canonical_value_bound. fom_gap_pfp_left_product_result_canonical_value_bound + S (fom_value_pfp_left_product_result_canonical) = p))) /\ ((exists pfrd_qb_left_product_result pfrd_qc_left_product_result pfrd_qlen_left_product_result pfrd_pb_left_product_result pfrd_pc_left_product_result pfrd_plen_left_product_result. ((((forall fom_index_pfp_left_product_result_productleft. (exists fom_gap_pfp_left_product_result_productleft_index_bound. fom_gap_pfp_left_product_result_productleft_index_bound + S (fom_index_pfp_left_product_result_productleft) = pfrd_qlen_left_product_result) -> exists fom_value_pfp_left_product_result_productleft. ((((exists fom_beta_height_pfp_left_product_result_productleft_entry. fom_beta_height_pfp_left_product_result_productleft_entry + S (fom_value_pfp_left_product_result_productleft) = S ((S (fom_index_pfp_left_product_result_productleft)) * pfrd_qc_left_product_result)) /\ exists fom_beta_quotient_pfp_left_product_result_productleft_entry. pfrd_qb_left_product_result = fom_beta_quotient_pfp_left_product_result_productleft_entry * S ((S (fom_index_pfp_left_product_result_productleft)) * pfrd_qc_left_product_result) + (fom_value_pfp_left_product_result_productleft))) /\ (exists fom_gap_pfp_left_product_result_productleft_value_bound. fom_gap_pfp_left_product_result_productleft_value_bound + S (fom_value_pfp_left_product_result_productleft) = p))) /\ (((forall fom_index_pfp_left_product_result_productright. (exists fom_gap_pfp_left_product_result_productright_index_bound. fom_gap_pfp_left_product_result_productright_index_bound + S (fom_index_pfp_left_product_result_productright) = J) -> exists fom_value_pfp_left_product_result_productright. ((((exists fom_beta_height_pfp_left_product_result_productright_entry. fom_beta_height_pfp_left_product_result_productright_entry + S (fom_value_pfp_left_product_result_productright) = S ((S (fom_index_pfp_left_product_result_productright)) * dc)) /\ exists fom_beta_quotient_pfp_left_product_result_productright_entry. db = fom_beta_quotient_pfp_left_product_result_productright_entry * S ((S (fom_index_pfp_left_product_result_productright)) * dc) + (fom_value_pfp_left_product_result_productright))) /\ (exists fom_gap_pfp_left_product_result_productright_value_bound. fom_gap_pfp_left_product_result_productright_value_bound + S (fom_value_pfp_left_product_result_productright) = p))) /\ (((((((pfrd_qlen_left_product_result)=0 \/ (J)=0) /\ (((pfrd_plen_left_product_result)=0)))) \/ (((~((pfrd_qlen_left_product_result)=0)) /\ (((~((J)=0)) /\ (((pfrd_qlen_left_product_result)+(J)=S (pfrd_plen_left_product_result)))))))) /\ ((forall pfc_index_left_product_result_productcoefficients. (exists pfa_gap_left_product_result_productcoefficientsbound. pfa_gap_left_product_result_productcoefficientsbound + S (pfc_index_left_product_result_productcoefficients) = (pfrd_plen_left_product_result)) -> exists pfc_value_left_product_result_productcoefficients. ((((exists ff_h_pfp_left_product_result_productcoefficientsentry. ff_h_pfp_left_product_result_productcoefficientsentry + S (pfc_value_left_product_result_productcoefficients) = S ((S (pfc_index_left_product_result_productcoefficients)) * pfrd_pc_left_product_result)) /\ exists ff_q_pfp_left_product_result_productcoefficientsentry. pfrd_pb_left_product_result = ff_q_pfp_left_product_result_productcoefficientsentry * S ((S (pfc_index_left_product_result_productcoefficients)) * pfrd_pc_left_product_result) + (pfc_value_left_product_result_productcoefficients))) /\ ((exists pfc_terms_code_left_product_result_productcoefficientscoefficient pfc_terms_scale_left_product_result_productcoefficientscoefficient pfc_natural_sum_left_product_result_productcoefficientscoefficient. ((forall pfc_index_left_product_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_left_product_result_productcoefficientscoefficientdiagonalbound. pfa_gap_left_product_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_left_product_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_left_product_result_productcoefficients))) -> exists pfc_value_left_product_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_left_product_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_left_product_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_left_product_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_left_product_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_product_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_left_product_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_left_product_result_productcoefficientscoefficient = ff_q_pfp_left_product_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_left_product_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_left_product_result_productcoefficientscoefficient) + (pfc_value_left_product_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_left_product_result_productcoefficientscoefficientdiagonalterm pfc_left_left_product_result_productcoefficientscoefficientdiagonalterm pfc_right_left_product_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_left_product_result_productcoefficientscoefficientdiagonal)+pfc_complement_left_product_result_productcoefficientscoefficientdiagonalterm=(pfc_index_left_product_result_productcoefficients)) /\ ((((((exists pfa_gap_left_product_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_left_product_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_left_product_result_productcoefficientscoefficientdiagonal) = (pfrd_qlen_left_product_result)) /\ ((((exists ff_h_pfp_left_product_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_left_product_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_left_product_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_left_product_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_left_product_result)) /\ exists ff_q_pfp_left_product_result_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_left_product_result = ff_q_pfp_left_product_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_left_product_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_left_product_result) + (pfc_left_left_product_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_product_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_left_product_result_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_left_product_result)=(pfc_index_left_product_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_left_product_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_left_product_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_left_product_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_left_product_result_productcoefficientscoefficientdiagonalterm) = (J)) /\ ((((exists ff_h_pfp_left_product_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_left_product_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_left_product_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_left_product_result_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_left_product_result_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_left_product_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_left_product_result_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_left_product_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_left_product_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_left_product_result_productcoefficientscoefficientdiagonaltermrightoutside+(J)=(pfc_complement_left_product_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_left_product_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_left_product_result_productcoefficientscoefficientdiagonal)=pfc_left_left_product_result_productcoefficientscoefficientdiagonalterm*pfc_right_left_product_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_left_product_result_productcoefficientscoefficientsum fs_v_pfc_left_product_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_left_product_result_productcoefficientscoefficientsum = fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_left_product_result_productcoefficientscoefficient) = S ((S (S (pfc_index_left_product_result_productcoefficients))) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_left_product_result_productcoefficientscoefficientsum = fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_left_product_result_productcoefficients))) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum) + (pfc_natural_sum_left_product_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_left_product_result_productcoefficients)) -> exists fs_a_pfc_left_product_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_left_product_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_left_product_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_left_product_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_product_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_left_product_result_productcoefficientscoefficient = fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_left_product_result_productcoefficientscoefficient) + (fs_a_pfc_left_product_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_left_product_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_left_product_result_productcoefficientscoefficientsum = fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum) + (fs_r_pfc_left_product_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_left_product_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_left_product_result_productcoefficientscoefficientsum = fs_q_pfc_left_product_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_left_product_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_left_product_result_productcoefficientscoefficientsum) + (fs_s_pfc_left_product_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_left_product_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_left_product_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_left_product_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_left_product_result_productcoefficientscoefficientresiduebound. pfa_gap_left_product_result_productcoefficientscoefficientresiduebound + S (pfc_value_left_product_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_left_product_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_left_product_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_left_product_result_productcoefficientscoefficient) + (p) * pfa_offset_left_left_product_result_productcoefficientscoefficientresiduecongruence = (pfc_value_left_product_result_productcoefficients) + (p) * pfa_offset_right_left_product_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_left_product_result_target pfrep_left_left_product_result_target pfrep_right_left_product_result_target. ((exists pfrep_position_left_product_result_targetfirst. ((pfrep_position_left_product_result_targetfirst+S (pfrep_power_left_product_result_target)=(pfrd_plen_left_product_result)) /\ ((((exists ff_h_pfp_left_product_result_targetfirstentry. ff_h_pfp_left_product_result_targetfirstentry + S (pfrep_left_left_product_result_target) = S ((S (pfrep_position_left_product_result_targetfirst)) * pfrd_pc_left_product_result)) /\ exists ff_q_pfp_left_product_result_targetfirstentry. pfrd_pb_left_product_result = ff_q_pfp_left_product_result_targetfirstentry * S ((S (pfrep_position_left_product_result_targetfirst)) * pfrd_pc_left_product_result) + (pfrep_left_left_product_result_target)))))) \/ (((exists pfrep_gap_left_product_result_targetfirstoutside. pfrep_gap_left_product_result_targetfirstoutside+(pfrd_plen_left_product_result)=(pfrep_power_left_product_result_target)) /\ (((pfrep_left_left_product_result_target)=0))))) -> ((exists pfrep_position_left_product_result_targetsecond. ((pfrep_position_left_product_result_targetsecond+S (pfrep_power_left_product_result_target)=(I)) /\ ((((exists ff_h_pfp_left_product_result_targetsecondentry. ff_h_pfp_left_product_result_targetsecondentry + S (pfrep_right_left_product_result_target) = S ((S (pfrep_position_left_product_result_targetsecond)) * pc)) /\ exists ff_q_pfp_left_product_result_targetsecondentry. pb = ff_q_pfp_left_product_result_targetsecondentry * S ((S (pfrep_position_left_product_result_targetsecond)) * pc) + (pfrep_right_left_product_result_target)))))) \/ (((exists pfrep_gap_left_product_result_targetsecondoutside. pfrep_gap_left_product_result_targetsecondoutside+(I)=(pfrep_power_left_product_result_target)) /\ (((pfrep_right_left_product_result_target)=0))))) -> pfrep_left_left_product_result_target=pfrep_right_left_product_result_target)))))))