prime_field_polynomial_monic_right_associates_equivalent

Exact expanded first-order arithmetic statement

forall p gb gc G hb hc H. (~((p) = 1) /\ forall pfa_factor_left_associates_prime pfa_factor_right_associates_prime. (p) = pfa_factor_left_associates_prime * pfa_factor_right_associates_prime -> pfa_factor_left_associates_prime = 1 \/ pfa_factor_right_associates_prime = 1) -> (((~((G) = 0)) /\ (((forall fom_index_pfp_associates_Gcoefficients. (exists fom_gap_pfp_associates_Gcoefficients_index_bound. fom_gap_pfp_associates_Gcoefficients_index_bound + S (fom_index_pfp_associates_Gcoefficients) = G) -> exists fom_value_pfp_associates_Gcoefficients. ((((exists fom_beta_height_pfp_associates_Gcoefficients_entry. fom_beta_height_pfp_associates_Gcoefficients_entry + S (fom_value_pfp_associates_Gcoefficients) = S ((S (fom_index_pfp_associates_Gcoefficients)) * gc)) /\ exists fom_beta_quotient_pfp_associates_Gcoefficients_entry. gb = fom_beta_quotient_pfp_associates_Gcoefficients_entry * S ((S (fom_index_pfp_associates_Gcoefficients)) * gc) + (fom_value_pfp_associates_Gcoefficients))) /\ (exists fom_gap_pfp_associates_Gcoefficients_value_bound. fom_gap_pfp_associates_Gcoefficients_value_bound + S (fom_value_pfp_associates_Gcoefficients) = p))) /\ ((((exists ff_h_pfp_associates_Gleading. ff_h_pfp_associates_Gleading + S (1) = S ((S (0)) * gc)) /\ exists ff_q_pfp_associates_Gleading. gb = ff_q_pfp_associates_Gleading * S ((S (0)) * gc) + (1)))))))) -> (((~((H) = 0)) /\ (((forall fom_index_pfp_associates_Hcoefficients. (exists fom_gap_pfp_associates_Hcoefficients_index_bound. fom_gap_pfp_associates_Hcoefficients_index_bound + S (fom_index_pfp_associates_Hcoefficients) = H) -> exists fom_value_pfp_associates_Hcoefficients. ((((exists fom_beta_height_pfp_associates_Hcoefficients_entry. fom_beta_height_pfp_associates_Hcoefficients_entry + S (fom_value_pfp_associates_Hcoefficients) = S ((S (fom_index_pfp_associates_Hcoefficients)) * hc)) /\ exists fom_beta_quotient_pfp_associates_Hcoefficients_entry. hb = fom_beta_quotient_pfp_associates_Hcoefficients_entry * S ((S (fom_index_pfp_associates_Hcoefficients)) * hc) + (fom_value_pfp_associates_Hcoefficients))) /\ (exists fom_gap_pfp_associates_Hcoefficients_value_bound. fom_gap_pfp_associates_Hcoefficients_value_bound + S (fom_value_pfp_associates_Hcoefficients) = p))) /\ ((((exists ff_h_pfp_associates_Hleading. ff_h_pfp_associates_Hleading + S (1) = S ((S (0)) * hc)) /\ exists ff_q_pfp_associates_Hleading. hb = ff_q_pfp_associates_Hleading * S ((S (0)) * hc) + (1)))))))) -> (((forall fom_index_pfp_associates_GH_canonical. (exists fom_gap_pfp_associates_GH_canonical_index_bound. fom_gap_pfp_associates_GH_canonical_index_bound + S (fom_index_pfp_associates_GH_canonical) = H) -> exists fom_value_pfp_associates_GH_canonical. ((((exists fom_beta_height_pfp_associates_GH_canonical_entry. fom_beta_height_pfp_associates_GH_canonical_entry + S (fom_value_pfp_associates_GH_canonical) = S ((S (fom_index_pfp_associates_GH_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_associates_GH_canonical_entry. hb = fom_beta_quotient_pfp_associates_GH_canonical_entry * S ((S (fom_index_pfp_associates_GH_canonical)) * hc) + (fom_value_pfp_associates_GH_canonical))) /\ (exists fom_gap_pfp_associates_GH_canonical_value_bound. fom_gap_pfp_associates_GH_canonical_value_bound + S (fom_value_pfp_associates_GH_canonical) = p))) /\ ((exists pfgu_qb_associates_GH pfgu_qc_associates_GH pfgu_Q_associates_GH pfgu_pb_associates_GH pfgu_pc_associates_GH pfgu_P_associates_GH. ((((forall fom_index_pfp_associates_GH_productleft. (exists fom_gap_pfp_associates_GH_productleft_index_bound. fom_gap_pfp_associates_GH_productleft_index_bound + S (fom_index_pfp_associates_GH_productleft) = pfgu_Q_associates_GH) -> exists fom_value_pfp_associates_GH_productleft. ((((exists fom_beta_height_pfp_associates_GH_productleft_entry. fom_beta_height_pfp_associates_GH_productleft_entry + S (fom_value_pfp_associates_GH_productleft) = S ((S (fom_index_pfp_associates_GH_productleft)) * pfgu_qc_associates_GH)) /\ exists fom_beta_quotient_pfp_associates_GH_productleft_entry. pfgu_qb_associates_GH = fom_beta_quotient_pfp_associates_GH_productleft_entry * S ((S (fom_index_pfp_associates_GH_productleft)) * pfgu_qc_associates_GH) + (fom_value_pfp_associates_GH_productleft))) /\ (exists fom_gap_pfp_associates_GH_productleft_value_bound. fom_gap_pfp_associates_GH_productleft_value_bound + S (fom_value_pfp_associates_GH_productleft) = p))) /\ (((forall fom_index_pfp_associates_GH_productright. (exists fom_gap_pfp_associates_GH_productright_index_bound. fom_gap_pfp_associates_GH_productright_index_bound + S (fom_index_pfp_associates_GH_productright) = G) -> exists fom_value_pfp_associates_GH_productright. ((((exists fom_beta_height_pfp_associates_GH_productright_entry. fom_beta_height_pfp_associates_GH_productright_entry + S (fom_value_pfp_associates_GH_productright) = S ((S (fom_index_pfp_associates_GH_productright)) * gc)) /\ exists fom_beta_quotient_pfp_associates_GH_productright_entry. gb = fom_beta_quotient_pfp_associates_GH_productright_entry * S ((S (fom_index_pfp_associates_GH_productright)) * gc) + (fom_value_pfp_associates_GH_productright))) /\ (exists fom_gap_pfp_associates_GH_productright_value_bound. fom_gap_pfp_associates_GH_productright_value_bound + S (fom_value_pfp_associates_GH_productright) = p))) /\ (((((((pfgu_Q_associates_GH)=0 \/ (G)=0) /\ (((pfgu_P_associates_GH)=0)))) \/ (((~((pfgu_Q_associates_GH)=0)) /\ (((~((G)=0)) /\ (((pfgu_Q_associates_GH)+(G)=S (pfgu_P_associates_GH)))))))) /\ ((forall pfc_index_associates_GH_productcoefficients. (exists pfa_gap_associates_GH_productcoefficientsbound. pfa_gap_associates_GH_productcoefficientsbound + S (pfc_index_associates_GH_productcoefficients) = (pfgu_P_associates_GH)) -> exists pfc_value_associates_GH_productcoefficients. ((((exists ff_h_pfp_associates_GH_productcoefficientsentry. ff_h_pfp_associates_GH_productcoefficientsentry + S (pfc_value_associates_GH_productcoefficients) = S ((S (pfc_index_associates_GH_productcoefficients)) * pfgu_pc_associates_GH)) /\ exists ff_q_pfp_associates_GH_productcoefficientsentry. pfgu_pb_associates_GH = ff_q_pfp_associates_GH_productcoefficientsentry * S ((S (pfc_index_associates_GH_productcoefficients)) * pfgu_pc_associates_GH) + (pfc_value_associates_GH_productcoefficients))) /\ ((exists pfc_terms_code_associates_GH_productcoefficientscoefficient pfc_terms_scale_associates_GH_productcoefficientscoefficient pfc_natural_sum_associates_GH_productcoefficientscoefficient. ((forall pfc_index_associates_GH_productcoefficientscoefficientdiagonal. (exists pfa_gap_associates_GH_productcoefficientscoefficientdiagonalbound. pfa_gap_associates_GH_productcoefficientscoefficientdiagonalbound + S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal) = (S (pfc_index_associates_GH_productcoefficients))) -> exists pfc_value_associates_GH_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonalentry. ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonalentry + S (pfc_value_associates_GH_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient)) /\ exists ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonalentry. pfc_terms_code_associates_GH_productcoefficientscoefficient = ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient) + (pfc_value_associates_GH_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm. (((pfc_index_associates_GH_productcoefficientscoefficientdiagonal)+pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm=(pfc_index_associates_GH_productcoefficients)) /\ ((((((exists pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal) = (pfgu_Q_associates_GH)) /\ ((((exists ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_GH)) /\ exists ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_associates_GH = ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_GH) + (pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_associates_GH)=(pfc_index_associates_GH_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_associates_GH_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associates_GH_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_associates_GH_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associates_GH_productcoefficientscoefficientdiagonal)=pfc_left_associates_GH_productcoefficientscoefficientdiagonalterm*pfc_right_associates_GH_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associates_GH_productcoefficientscoefficientsum fs_v_pfc_associates_GH_productcoefficientscoefficientsum. ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_start. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_start. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associates_GH_productcoefficientscoefficient) = S ((S (S (pfc_index_associates_GH_productcoefficients))) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associates_GH_productcoefficients))) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (pfc_natural_sum_associates_GH_productcoefficientscoefficient))) /\ forall fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps = S (pfc_index_associates_GH_productcoefficients)) -> exists fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associates_GH_productcoefficientscoefficient = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_GH_productcoefficientscoefficient) + (fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associates_GH_productcoefficientscoefficientsum = fs_q_pfc_associates_GH_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_GH_productcoefficientscoefficientsum) + (fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associates_GH_productcoefficientscoefficientsum_body_steps = fs_r_pfc_associates_GH_productcoefficientscoefficientsum_body_steps + fs_a_pfc_associates_GH_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associates_GH_productcoefficientscoefficientresiduebound. pfa_gap_associates_GH_productcoefficientscoefficientresiduebound + S (pfc_value_associates_GH_productcoefficients) = (p)) /\ ((exists pfa_offset_left_associates_GH_productcoefficientscoefficientresiduecongruence pfa_offset_right_associates_GH_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associates_GH_productcoefficientscoefficient) + (p) * pfa_offset_left_associates_GH_productcoefficientscoefficientresiduecongruence = (pfc_value_associates_GH_productcoefficients) + (p) * pfa_offset_right_associates_GH_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_associates_GH_target pfrep_left_associates_GH_target pfrep_right_associates_GH_target. ((exists pfrep_position_associates_GH_targetfirst. ((pfrep_position_associates_GH_targetfirst+S (pfrep_power_associates_GH_target)=(pfgu_P_associates_GH)) /\ ((((exists ff_h_pfp_associates_GH_targetfirstentry. ff_h_pfp_associates_GH_targetfirstentry + S (pfrep_left_associates_GH_target) = S ((S (pfrep_position_associates_GH_targetfirst)) * pfgu_pc_associates_GH)) /\ exists ff_q_pfp_associates_GH_targetfirstentry. pfgu_pb_associates_GH = ff_q_pfp_associates_GH_targetfirstentry * S ((S (pfrep_position_associates_GH_targetfirst)) * pfgu_pc_associates_GH) + (pfrep_left_associates_GH_target)))))) \/ (((exists pfrep_gap_associates_GH_targetfirstoutside. pfrep_gap_associates_GH_targetfirstoutside+(pfgu_P_associates_GH)=(pfrep_power_associates_GH_target)) /\ (((pfrep_left_associates_GH_target)=0))))) -> ((exists pfrep_position_associates_GH_targetsecond. ((pfrep_position_associates_GH_targetsecond+S (pfrep_power_associates_GH_target)=(H)) /\ ((((exists ff_h_pfp_associates_GH_targetsecondentry. ff_h_pfp_associates_GH_targetsecondentry + S (pfrep_right_associates_GH_target) = S ((S (pfrep_position_associates_GH_targetsecond)) * hc)) /\ exists ff_q_pfp_associates_GH_targetsecondentry. hb = ff_q_pfp_associates_GH_targetsecondentry * S ((S (pfrep_position_associates_GH_targetsecond)) * hc) + (pfrep_right_associates_GH_target)))))) \/ (((exists pfrep_gap_associates_GH_targetsecondoutside. pfrep_gap_associates_GH_targetsecondoutside+(H)=(pfrep_power_associates_GH_target)) /\ (((pfrep_right_associates_GH_target)=0))))) -> pfrep_left_associates_GH_target=pfrep_right_associates_GH_target))))))) -> (((forall fom_index_pfp_associates_HG_canonical. (exists fom_gap_pfp_associates_HG_canonical_index_bound. fom_gap_pfp_associates_HG_canonical_index_bound + S (fom_index_pfp_associates_HG_canonical) = G) -> exists fom_value_pfp_associates_HG_canonical. ((((exists fom_beta_height_pfp_associates_HG_canonical_entry. fom_beta_height_pfp_associates_HG_canonical_entry + S (fom_value_pfp_associates_HG_canonical) = S ((S (fom_index_pfp_associates_HG_canonical)) * gc)) /\ exists fom_beta_quotient_pfp_associates_HG_canonical_entry. gb = fom_beta_quotient_pfp_associates_HG_canonical_entry * S ((S (fom_index_pfp_associates_HG_canonical)) * gc) + (fom_value_pfp_associates_HG_canonical))) /\ (exists fom_gap_pfp_associates_HG_canonical_value_bound. fom_gap_pfp_associates_HG_canonical_value_bound + S (fom_value_pfp_associates_HG_canonical) = p))) /\ ((exists pfgu_qb_associates_HG pfgu_qc_associates_HG pfgu_Q_associates_HG pfgu_pb_associates_HG pfgu_pc_associates_HG pfgu_P_associates_HG. ((((forall fom_index_pfp_associates_HG_productleft. (exists fom_gap_pfp_associates_HG_productleft_index_bound. fom_gap_pfp_associates_HG_productleft_index_bound + S (fom_index_pfp_associates_HG_productleft) = pfgu_Q_associates_HG) -> exists fom_value_pfp_associates_HG_productleft. ((((exists fom_beta_height_pfp_associates_HG_productleft_entry. fom_beta_height_pfp_associates_HG_productleft_entry + S (fom_value_pfp_associates_HG_productleft) = S ((S (fom_index_pfp_associates_HG_productleft)) * pfgu_qc_associates_HG)) /\ exists fom_beta_quotient_pfp_associates_HG_productleft_entry. pfgu_qb_associates_HG = fom_beta_quotient_pfp_associates_HG_productleft_entry * S ((S (fom_index_pfp_associates_HG_productleft)) * pfgu_qc_associates_HG) + (fom_value_pfp_associates_HG_productleft))) /\ (exists fom_gap_pfp_associates_HG_productleft_value_bound. fom_gap_pfp_associates_HG_productleft_value_bound + S (fom_value_pfp_associates_HG_productleft) = p))) /\ (((forall fom_index_pfp_associates_HG_productright. (exists fom_gap_pfp_associates_HG_productright_index_bound. fom_gap_pfp_associates_HG_productright_index_bound + S (fom_index_pfp_associates_HG_productright) = H) -> exists fom_value_pfp_associates_HG_productright. ((((exists fom_beta_height_pfp_associates_HG_productright_entry. fom_beta_height_pfp_associates_HG_productright_entry + S (fom_value_pfp_associates_HG_productright) = S ((S (fom_index_pfp_associates_HG_productright)) * hc)) /\ exists fom_beta_quotient_pfp_associates_HG_productright_entry. hb = fom_beta_quotient_pfp_associates_HG_productright_entry * S ((S (fom_index_pfp_associates_HG_productright)) * hc) + (fom_value_pfp_associates_HG_productright))) /\ (exists fom_gap_pfp_associates_HG_productright_value_bound. fom_gap_pfp_associates_HG_productright_value_bound + S (fom_value_pfp_associates_HG_productright) = p))) /\ (((((((pfgu_Q_associates_HG)=0 \/ (H)=0) /\ (((pfgu_P_associates_HG)=0)))) \/ (((~((pfgu_Q_associates_HG)=0)) /\ (((~((H)=0)) /\ (((pfgu_Q_associates_HG)+(H)=S (pfgu_P_associates_HG)))))))) /\ ((forall pfc_index_associates_HG_productcoefficients. (exists pfa_gap_associates_HG_productcoefficientsbound. pfa_gap_associates_HG_productcoefficientsbound + S (pfc_index_associates_HG_productcoefficients) = (pfgu_P_associates_HG)) -> exists pfc_value_associates_HG_productcoefficients. ((((exists ff_h_pfp_associates_HG_productcoefficientsentry. ff_h_pfp_associates_HG_productcoefficientsentry + S (pfc_value_associates_HG_productcoefficients) = S ((S (pfc_index_associates_HG_productcoefficients)) * pfgu_pc_associates_HG)) /\ exists ff_q_pfp_associates_HG_productcoefficientsentry. pfgu_pb_associates_HG = ff_q_pfp_associates_HG_productcoefficientsentry * S ((S (pfc_index_associates_HG_productcoefficients)) * pfgu_pc_associates_HG) + (pfc_value_associates_HG_productcoefficients))) /\ ((exists pfc_terms_code_associates_HG_productcoefficientscoefficient pfc_terms_scale_associates_HG_productcoefficientscoefficient pfc_natural_sum_associates_HG_productcoefficientscoefficient. ((forall pfc_index_associates_HG_productcoefficientscoefficientdiagonal. (exists pfa_gap_associates_HG_productcoefficientscoefficientdiagonalbound. pfa_gap_associates_HG_productcoefficientscoefficientdiagonalbound + S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal) = (S (pfc_index_associates_HG_productcoefficients))) -> exists pfc_value_associates_HG_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonalentry. ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonalentry + S (pfc_value_associates_HG_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient)) /\ exists ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonalentry. pfc_terms_code_associates_HG_productcoefficientscoefficient = ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient) + (pfc_value_associates_HG_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm. (((pfc_index_associates_HG_productcoefficientscoefficientdiagonal)+pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm=(pfc_index_associates_HG_productcoefficients)) /\ ((((((exists pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal) = (pfgu_Q_associates_HG)) /\ ((((exists ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_HG)) /\ exists ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_associates_HG = ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_associates_HG) + (pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_associates_HG)=(pfc_index_associates_HG_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_associates_HG_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_associates_HG_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_associates_HG_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_associates_HG_productcoefficientscoefficientdiagonal)=pfc_left_associates_HG_productcoefficientscoefficientdiagonalterm*pfc_right_associates_HG_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_associates_HG_productcoefficientscoefficientsum fs_v_pfc_associates_HG_productcoefficientscoefficientsum. ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_start. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_start. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_associates_HG_productcoefficientscoefficient) = S ((S (S (pfc_index_associates_HG_productcoefficients))) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_associates_HG_productcoefficients))) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (pfc_natural_sum_associates_HG_productcoefficientscoefficient))) /\ forall fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps = S (pfc_index_associates_HG_productcoefficients)) -> exists fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_associates_HG_productcoefficientscoefficient = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_associates_HG_productcoefficientscoefficient) + (fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_associates_HG_productcoefficientscoefficientsum = fs_q_pfc_associates_HG_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_associates_HG_productcoefficientscoefficientsum) + (fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_associates_HG_productcoefficientscoefficientsum_body_steps = fs_r_pfc_associates_HG_productcoefficientscoefficientsum_body_steps + fs_a_pfc_associates_HG_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_associates_HG_productcoefficientscoefficientresiduebound. pfa_gap_associates_HG_productcoefficientscoefficientresiduebound + S (pfc_value_associates_HG_productcoefficients) = (p)) /\ ((exists pfa_offset_left_associates_HG_productcoefficientscoefficientresiduecongruence pfa_offset_right_associates_HG_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_associates_HG_productcoefficientscoefficient) + (p) * pfa_offset_left_associates_HG_productcoefficientscoefficientresiduecongruence = (pfc_value_associates_HG_productcoefficients) + (p) * pfa_offset_right_associates_HG_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_associates_HG_target pfrep_left_associates_HG_target pfrep_right_associates_HG_target. ((exists pfrep_position_associates_HG_targetfirst. ((pfrep_position_associates_HG_targetfirst+S (pfrep_power_associates_HG_target)=(pfgu_P_associates_HG)) /\ ((((exists ff_h_pfp_associates_HG_targetfirstentry. ff_h_pfp_associates_HG_targetfirstentry + S (pfrep_left_associates_HG_target) = S ((S (pfrep_position_associates_HG_targetfirst)) * pfgu_pc_associates_HG)) /\ exists ff_q_pfp_associates_HG_targetfirstentry. pfgu_pb_associates_HG = ff_q_pfp_associates_HG_targetfirstentry * S ((S (pfrep_position_associates_HG_targetfirst)) * pfgu_pc_associates_HG) + (pfrep_left_associates_HG_target)))))) \/ (((exists pfrep_gap_associates_HG_targetfirstoutside. pfrep_gap_associates_HG_targetfirstoutside+(pfgu_P_associates_HG)=(pfrep_power_associates_HG_target)) /\ (((pfrep_left_associates_HG_target)=0))))) -> ((exists pfrep_position_associates_HG_targetsecond. ((pfrep_position_associates_HG_targetsecond+S (pfrep_power_associates_HG_target)=(G)) /\ ((((exists ff_h_pfp_associates_HG_targetsecondentry. ff_h_pfp_associates_HG_targetsecondentry + S (pfrep_right_associates_HG_target) = S ((S (pfrep_position_associates_HG_targetsecond)) * gc)) /\ exists ff_q_pfp_associates_HG_targetsecondentry. gb = ff_q_pfp_associates_HG_targetsecondentry * S ((S (pfrep_position_associates_HG_targetsecond)) * gc) + (pfrep_right_associates_HG_target)))))) \/ (((exists pfrep_gap_associates_HG_targetsecondoutside. pfrep_gap_associates_HG_targetsecondoutside+(G)=(pfrep_power_associates_HG_target)) /\ (((pfrep_right_associates_HG_target)=0))))) -> pfrep_left_associates_HG_target=pfrep_right_associates_HG_target))))))) -> (forall pfrep_power_associates_result pfrep_left_associates_result pfrep_right_associates_result. ((exists pfrep_position_associates_resultfirst. ((pfrep_position_associates_resultfirst+S (pfrep_power_associates_result)=(G)) /\ ((((exists ff_h_pfp_associates_resultfirstentry. ff_h_pfp_associates_resultfirstentry + S (pfrep_left_associates_result) = S ((S (pfrep_position_associates_resultfirst)) * gc)) /\ exists ff_q_pfp_associates_resultfirstentry. gb = ff_q_pfp_associates_resultfirstentry * S ((S (pfrep_position_associates_resultfirst)) * gc) + (pfrep_left_associates_result)))))) \/ (((exists pfrep_gap_associates_resultfirstoutside. pfrep_gap_associates_resultfirstoutside+(G)=(pfrep_power_associates_result)) /\ (((pfrep_left_associates_result)=0))))) -> ((exists pfrep_position_associates_resultsecond. ((pfrep_position_associates_resultsecond+S (pfrep_power_associates_result)=(H)) /\ ((((exists ff_h_pfp_associates_resultsecondentry. ff_h_pfp_associates_resultsecondentry + S (pfrep_right_associates_result) = S ((S (pfrep_position_associates_resultsecond)) * hc)) /\ exists ff_q_pfp_associates_resultsecondentry. hb = ff_q_pfp_associates_resultsecondentry * S ((S (pfrep_position_associates_resultsecond)) * hc) + (pfrep_right_associates_result)))))) \/ (((exists pfrep_gap_associates_resultsecondoutside. pfrep_gap_associates_resultsecondoutside+(H)=(pfrep_power_associates_result)) /\ (((pfrep_right_associates_result)=0))))) -> pfrep_left_associates_result=pfrep_right_associates_result)