prime_field_polynomial_normal_right_associates_equivalent

Exact expanded first-order arithmetic statement

forall p gb gc G hb hc H. (~((p) = 1) /\ forall pfa_factor_left_normal_prime pfa_factor_right_normal_prime. (p) = pfa_factor_left_normal_prime * pfa_factor_right_normal_prime -> pfa_factor_left_normal_prime = 1 \/ pfa_factor_right_normal_prime = 1) -> ((G)=0 \/ (((~((G) = 0)) /\ (((forall fom_index_pfp_normal_G_moniccoefficients. (exists fom_gap_pfp_normal_G_moniccoefficients_index_bound. fom_gap_pfp_normal_G_moniccoefficients_index_bound + S (fom_index_pfp_normal_G_moniccoefficients) = G) -> exists fom_value_pfp_normal_G_moniccoefficients. ((((exists fom_beta_height_pfp_normal_G_moniccoefficients_entry. fom_beta_height_pfp_normal_G_moniccoefficients_entry + S (fom_value_pfp_normal_G_moniccoefficients) = S ((S (fom_index_pfp_normal_G_moniccoefficients)) * gc)) /\ exists fom_beta_quotient_pfp_normal_G_moniccoefficients_entry. gb = fom_beta_quotient_pfp_normal_G_moniccoefficients_entry * S ((S (fom_index_pfp_normal_G_moniccoefficients)) * gc) + (fom_value_pfp_normal_G_moniccoefficients))) /\ (exists fom_gap_pfp_normal_G_moniccoefficients_value_bound. fom_gap_pfp_normal_G_moniccoefficients_value_bound + S (fom_value_pfp_normal_G_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normal_G_monicleading. ff_h_pfp_normal_G_monicleading + S (1) = S ((S (0)) * gc)) /\ exists ff_q_pfp_normal_G_monicleading. gb = ff_q_pfp_normal_G_monicleading * S ((S (0)) * gc) + (1))))))))) -> ((H)=0 \/ (((~((H) = 0)) /\ (((forall fom_index_pfp_normal_H_moniccoefficients. (exists fom_gap_pfp_normal_H_moniccoefficients_index_bound. fom_gap_pfp_normal_H_moniccoefficients_index_bound + S (fom_index_pfp_normal_H_moniccoefficients) = H) -> exists fom_value_pfp_normal_H_moniccoefficients. ((((exists fom_beta_height_pfp_normal_H_moniccoefficients_entry. fom_beta_height_pfp_normal_H_moniccoefficients_entry + S (fom_value_pfp_normal_H_moniccoefficients) = S ((S (fom_index_pfp_normal_H_moniccoefficients)) * hc)) /\ exists fom_beta_quotient_pfp_normal_H_moniccoefficients_entry. hb = fom_beta_quotient_pfp_normal_H_moniccoefficients_entry * S ((S (fom_index_pfp_normal_H_moniccoefficients)) * hc) + (fom_value_pfp_normal_H_moniccoefficients))) /\ (exists fom_gap_pfp_normal_H_moniccoefficients_value_bound. fom_gap_pfp_normal_H_moniccoefficients_value_bound + S (fom_value_pfp_normal_H_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normal_H_monicleading. ff_h_pfp_normal_H_monicleading + S (1) = S ((S (0)) * hc)) /\ exists ff_q_pfp_normal_H_monicleading. hb = ff_q_pfp_normal_H_monicleading * S ((S (0)) * hc) + (1))))))))) -> (((forall fom_index_pfp_normal_GH_canonical. (exists fom_gap_pfp_normal_GH_canonical_index_bound. fom_gap_pfp_normal_GH_canonical_index_bound + S (fom_index_pfp_normal_GH_canonical) = H) -> exists fom_value_pfp_normal_GH_canonical. ((((exists fom_beta_height_pfp_normal_GH_canonical_entry. fom_beta_height_pfp_normal_GH_canonical_entry + S (fom_value_pfp_normal_GH_canonical) = S ((S (fom_index_pfp_normal_GH_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_normal_GH_canonical_entry. hb = fom_beta_quotient_pfp_normal_GH_canonical_entry * S ((S (fom_index_pfp_normal_GH_canonical)) * hc) + (fom_value_pfp_normal_GH_canonical))) /\ (exists fom_gap_pfp_normal_GH_canonical_value_bound. fom_gap_pfp_normal_GH_canonical_value_bound + S (fom_value_pfp_normal_GH_canonical) = p))) /\ ((exists pfgu_qb_normal_GH pfgu_qc_normal_GH pfgu_Q_normal_GH pfgu_pb_normal_GH pfgu_pc_normal_GH pfgu_P_normal_GH. ((((forall fom_index_pfp_normal_GH_productleft. (exists fom_gap_pfp_normal_GH_productleft_index_bound. fom_gap_pfp_normal_GH_productleft_index_bound + S (fom_index_pfp_normal_GH_productleft) = pfgu_Q_normal_GH) -> exists fom_value_pfp_normal_GH_productleft. ((((exists fom_beta_height_pfp_normal_GH_productleft_entry. fom_beta_height_pfp_normal_GH_productleft_entry + S (fom_value_pfp_normal_GH_productleft) = S ((S (fom_index_pfp_normal_GH_productleft)) * pfgu_qc_normal_GH)) /\ exists fom_beta_quotient_pfp_normal_GH_productleft_entry. pfgu_qb_normal_GH = fom_beta_quotient_pfp_normal_GH_productleft_entry * S ((S (fom_index_pfp_normal_GH_productleft)) * pfgu_qc_normal_GH) + (fom_value_pfp_normal_GH_productleft))) /\ (exists fom_gap_pfp_normal_GH_productleft_value_bound. fom_gap_pfp_normal_GH_productleft_value_bound + S (fom_value_pfp_normal_GH_productleft) = p))) /\ (((forall fom_index_pfp_normal_GH_productright. (exists fom_gap_pfp_normal_GH_productright_index_bound. fom_gap_pfp_normal_GH_productright_index_bound + S (fom_index_pfp_normal_GH_productright) = G) -> exists fom_value_pfp_normal_GH_productright. ((((exists fom_beta_height_pfp_normal_GH_productright_entry. fom_beta_height_pfp_normal_GH_productright_entry + S (fom_value_pfp_normal_GH_productright) = S ((S (fom_index_pfp_normal_GH_productright)) * gc)) /\ exists fom_beta_quotient_pfp_normal_GH_productright_entry. gb = fom_beta_quotient_pfp_normal_GH_productright_entry * S ((S (fom_index_pfp_normal_GH_productright)) * gc) + (fom_value_pfp_normal_GH_productright))) /\ (exists fom_gap_pfp_normal_GH_productright_value_bound. fom_gap_pfp_normal_GH_productright_value_bound + S (fom_value_pfp_normal_GH_productright) = p))) /\ (((((((pfgu_Q_normal_GH)=0 \/ (G)=0) /\ (((pfgu_P_normal_GH)=0)))) \/ (((~((pfgu_Q_normal_GH)=0)) /\ (((~((G)=0)) /\ (((pfgu_Q_normal_GH)+(G)=S (pfgu_P_normal_GH)))))))) /\ ((forall pfc_index_normal_GH_productcoefficients. (exists pfa_gap_normal_GH_productcoefficientsbound. pfa_gap_normal_GH_productcoefficientsbound + S (pfc_index_normal_GH_productcoefficients) = (pfgu_P_normal_GH)) -> exists pfc_value_normal_GH_productcoefficients. ((((exists ff_h_pfp_normal_GH_productcoefficientsentry. ff_h_pfp_normal_GH_productcoefficientsentry + S (pfc_value_normal_GH_productcoefficients) = S ((S (pfc_index_normal_GH_productcoefficients)) * pfgu_pc_normal_GH)) /\ exists ff_q_pfp_normal_GH_productcoefficientsentry. pfgu_pb_normal_GH = ff_q_pfp_normal_GH_productcoefficientsentry * S ((S (pfc_index_normal_GH_productcoefficients)) * pfgu_pc_normal_GH) + (pfc_value_normal_GH_productcoefficients))) /\ ((exists pfc_terms_code_normal_GH_productcoefficientscoefficient pfc_terms_scale_normal_GH_productcoefficientscoefficient pfc_natural_sum_normal_GH_productcoefficientscoefficient. ((forall pfc_index_normal_GH_productcoefficientscoefficientdiagonal. (exists pfa_gap_normal_GH_productcoefficientscoefficientdiagonalbound. pfa_gap_normal_GH_productcoefficientscoefficientdiagonalbound + S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal) = (S (pfc_index_normal_GH_productcoefficients))) -> exists pfc_value_normal_GH_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonalentry + S (pfc_value_normal_GH_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient)) /\ exists ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normal_GH_productcoefficientscoefficient = ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient) + (pfc_value_normal_GH_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm. (((pfc_index_normal_GH_productcoefficientscoefficientdiagonal)+pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm=(pfc_index_normal_GH_productcoefficients)) /\ ((((((exists pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal) = (pfgu_Q_normal_GH)) /\ ((((exists ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_GH)) /\ exists ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_normal_GH = ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_GH) + (pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_normal_GH)=(pfc_index_normal_GH_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_normal_GH_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normal_GH_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_normal_GH_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normal_GH_productcoefficientscoefficientdiagonal)=pfc_left_normal_GH_productcoefficientscoefficientdiagonalterm*pfc_right_normal_GH_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normal_GH_productcoefficientscoefficientsum fs_v_pfc_normal_GH_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_start. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_start. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normal_GH_productcoefficientscoefficient) = S ((S (S (pfc_index_normal_GH_productcoefficients))) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normal_GH_productcoefficients))) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (pfc_natural_sum_normal_GH_productcoefficientscoefficient))) /\ forall fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps = S (pfc_index_normal_GH_productcoefficients)) -> exists fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normal_GH_productcoefficientscoefficient = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_GH_productcoefficientscoefficient) + (fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normal_GH_productcoefficientscoefficientsum = fs_q_pfc_normal_GH_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_GH_productcoefficientscoefficientsum) + (fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normal_GH_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normal_GH_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normal_GH_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normal_GH_productcoefficientscoefficientresiduebound. pfa_gap_normal_GH_productcoefficientscoefficientresiduebound + S (pfc_value_normal_GH_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normal_GH_productcoefficientscoefficientresiduecongruence pfa_offset_right_normal_GH_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normal_GH_productcoefficientscoefficient) + (p) * pfa_offset_left_normal_GH_productcoefficientscoefficientresiduecongruence = (pfc_value_normal_GH_productcoefficients) + (p) * pfa_offset_right_normal_GH_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normal_GH_target pfrep_left_normal_GH_target pfrep_right_normal_GH_target. ((exists pfrep_position_normal_GH_targetfirst. ((pfrep_position_normal_GH_targetfirst+S (pfrep_power_normal_GH_target)=(pfgu_P_normal_GH)) /\ ((((exists ff_h_pfp_normal_GH_targetfirstentry. ff_h_pfp_normal_GH_targetfirstentry + S (pfrep_left_normal_GH_target) = S ((S (pfrep_position_normal_GH_targetfirst)) * pfgu_pc_normal_GH)) /\ exists ff_q_pfp_normal_GH_targetfirstentry. pfgu_pb_normal_GH = ff_q_pfp_normal_GH_targetfirstentry * S ((S (pfrep_position_normal_GH_targetfirst)) * pfgu_pc_normal_GH) + (pfrep_left_normal_GH_target)))))) \/ (((exists pfrep_gap_normal_GH_targetfirstoutside. pfrep_gap_normal_GH_targetfirstoutside+(pfgu_P_normal_GH)=(pfrep_power_normal_GH_target)) /\ (((pfrep_left_normal_GH_target)=0))))) -> ((exists pfrep_position_normal_GH_targetsecond. ((pfrep_position_normal_GH_targetsecond+S (pfrep_power_normal_GH_target)=(H)) /\ ((((exists ff_h_pfp_normal_GH_targetsecondentry. ff_h_pfp_normal_GH_targetsecondentry + S (pfrep_right_normal_GH_target) = S ((S (pfrep_position_normal_GH_targetsecond)) * hc)) /\ exists ff_q_pfp_normal_GH_targetsecondentry. hb = ff_q_pfp_normal_GH_targetsecondentry * S ((S (pfrep_position_normal_GH_targetsecond)) * hc) + (pfrep_right_normal_GH_target)))))) \/ (((exists pfrep_gap_normal_GH_targetsecondoutside. pfrep_gap_normal_GH_targetsecondoutside+(H)=(pfrep_power_normal_GH_target)) /\ (((pfrep_right_normal_GH_target)=0))))) -> pfrep_left_normal_GH_target=pfrep_right_normal_GH_target))))))) -> (((forall fom_index_pfp_normal_HG_canonical. (exists fom_gap_pfp_normal_HG_canonical_index_bound. fom_gap_pfp_normal_HG_canonical_index_bound + S (fom_index_pfp_normal_HG_canonical) = G) -> exists fom_value_pfp_normal_HG_canonical. ((((exists fom_beta_height_pfp_normal_HG_canonical_entry. fom_beta_height_pfp_normal_HG_canonical_entry + S (fom_value_pfp_normal_HG_canonical) = S ((S (fom_index_pfp_normal_HG_canonical)) * gc)) /\ exists fom_beta_quotient_pfp_normal_HG_canonical_entry. gb = fom_beta_quotient_pfp_normal_HG_canonical_entry * S ((S (fom_index_pfp_normal_HG_canonical)) * gc) + (fom_value_pfp_normal_HG_canonical))) /\ (exists fom_gap_pfp_normal_HG_canonical_value_bound. fom_gap_pfp_normal_HG_canonical_value_bound + S (fom_value_pfp_normal_HG_canonical) = p))) /\ ((exists pfgu_qb_normal_HG pfgu_qc_normal_HG pfgu_Q_normal_HG pfgu_pb_normal_HG pfgu_pc_normal_HG pfgu_P_normal_HG. ((((forall fom_index_pfp_normal_HG_productleft. (exists fom_gap_pfp_normal_HG_productleft_index_bound. fom_gap_pfp_normal_HG_productleft_index_bound + S (fom_index_pfp_normal_HG_productleft) = pfgu_Q_normal_HG) -> exists fom_value_pfp_normal_HG_productleft. ((((exists fom_beta_height_pfp_normal_HG_productleft_entry. fom_beta_height_pfp_normal_HG_productleft_entry + S (fom_value_pfp_normal_HG_productleft) = S ((S (fom_index_pfp_normal_HG_productleft)) * pfgu_qc_normal_HG)) /\ exists fom_beta_quotient_pfp_normal_HG_productleft_entry. pfgu_qb_normal_HG = fom_beta_quotient_pfp_normal_HG_productleft_entry * S ((S (fom_index_pfp_normal_HG_productleft)) * pfgu_qc_normal_HG) + (fom_value_pfp_normal_HG_productleft))) /\ (exists fom_gap_pfp_normal_HG_productleft_value_bound. fom_gap_pfp_normal_HG_productleft_value_bound + S (fom_value_pfp_normal_HG_productleft) = p))) /\ (((forall fom_index_pfp_normal_HG_productright. (exists fom_gap_pfp_normal_HG_productright_index_bound. fom_gap_pfp_normal_HG_productright_index_bound + S (fom_index_pfp_normal_HG_productright) = H) -> exists fom_value_pfp_normal_HG_productright. ((((exists fom_beta_height_pfp_normal_HG_productright_entry. fom_beta_height_pfp_normal_HG_productright_entry + S (fom_value_pfp_normal_HG_productright) = S ((S (fom_index_pfp_normal_HG_productright)) * hc)) /\ exists fom_beta_quotient_pfp_normal_HG_productright_entry. hb = fom_beta_quotient_pfp_normal_HG_productright_entry * S ((S (fom_index_pfp_normal_HG_productright)) * hc) + (fom_value_pfp_normal_HG_productright))) /\ (exists fom_gap_pfp_normal_HG_productright_value_bound. fom_gap_pfp_normal_HG_productright_value_bound + S (fom_value_pfp_normal_HG_productright) = p))) /\ (((((((pfgu_Q_normal_HG)=0 \/ (H)=0) /\ (((pfgu_P_normal_HG)=0)))) \/ (((~((pfgu_Q_normal_HG)=0)) /\ (((~((H)=0)) /\ (((pfgu_Q_normal_HG)+(H)=S (pfgu_P_normal_HG)))))))) /\ ((forall pfc_index_normal_HG_productcoefficients. (exists pfa_gap_normal_HG_productcoefficientsbound. pfa_gap_normal_HG_productcoefficientsbound + S (pfc_index_normal_HG_productcoefficients) = (pfgu_P_normal_HG)) -> exists pfc_value_normal_HG_productcoefficients. ((((exists ff_h_pfp_normal_HG_productcoefficientsentry. ff_h_pfp_normal_HG_productcoefficientsentry + S (pfc_value_normal_HG_productcoefficients) = S ((S (pfc_index_normal_HG_productcoefficients)) * pfgu_pc_normal_HG)) /\ exists ff_q_pfp_normal_HG_productcoefficientsentry. pfgu_pb_normal_HG = ff_q_pfp_normal_HG_productcoefficientsentry * S ((S (pfc_index_normal_HG_productcoefficients)) * pfgu_pc_normal_HG) + (pfc_value_normal_HG_productcoefficients))) /\ ((exists pfc_terms_code_normal_HG_productcoefficientscoefficient pfc_terms_scale_normal_HG_productcoefficientscoefficient pfc_natural_sum_normal_HG_productcoefficientscoefficient. ((forall pfc_index_normal_HG_productcoefficientscoefficientdiagonal. (exists pfa_gap_normal_HG_productcoefficientscoefficientdiagonalbound. pfa_gap_normal_HG_productcoefficientscoefficientdiagonalbound + S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal) = (S (pfc_index_normal_HG_productcoefficients))) -> exists pfc_value_normal_HG_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonalentry + S (pfc_value_normal_HG_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient)) /\ exists ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normal_HG_productcoefficientscoefficient = ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient) + (pfc_value_normal_HG_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm. (((pfc_index_normal_HG_productcoefficientscoefficientdiagonal)+pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm=(pfc_index_normal_HG_productcoefficients)) /\ ((((((exists pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal) = (pfgu_Q_normal_HG)) /\ ((((exists ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_HG)) /\ exists ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_normal_HG = ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) * pfgu_qc_normal_HG) + (pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_normal_HG)=(pfc_index_normal_HG_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_normal_HG_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normal_HG_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_normal_HG_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normal_HG_productcoefficientscoefficientdiagonal)=pfc_left_normal_HG_productcoefficientscoefficientdiagonalterm*pfc_right_normal_HG_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normal_HG_productcoefficientscoefficientsum fs_v_pfc_normal_HG_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_start. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_start. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normal_HG_productcoefficientscoefficient) = S ((S (S (pfc_index_normal_HG_productcoefficients))) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normal_HG_productcoefficients))) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (pfc_natural_sum_normal_HG_productcoefficientscoefficient))) /\ forall fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps = S (pfc_index_normal_HG_productcoefficients)) -> exists fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normal_HG_productcoefficientscoefficient = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normal_HG_productcoefficientscoefficient) + (fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normal_HG_productcoefficientscoefficientsum = fs_q_pfc_normal_HG_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normal_HG_productcoefficientscoefficientsum) + (fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normal_HG_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normal_HG_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normal_HG_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normal_HG_productcoefficientscoefficientresiduebound. pfa_gap_normal_HG_productcoefficientscoefficientresiduebound + S (pfc_value_normal_HG_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normal_HG_productcoefficientscoefficientresiduecongruence pfa_offset_right_normal_HG_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normal_HG_productcoefficientscoefficient) + (p) * pfa_offset_left_normal_HG_productcoefficientscoefficientresiduecongruence = (pfc_value_normal_HG_productcoefficients) + (p) * pfa_offset_right_normal_HG_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normal_HG_target pfrep_left_normal_HG_target pfrep_right_normal_HG_target. ((exists pfrep_position_normal_HG_targetfirst. ((pfrep_position_normal_HG_targetfirst+S (pfrep_power_normal_HG_target)=(pfgu_P_normal_HG)) /\ ((((exists ff_h_pfp_normal_HG_targetfirstentry. ff_h_pfp_normal_HG_targetfirstentry + S (pfrep_left_normal_HG_target) = S ((S (pfrep_position_normal_HG_targetfirst)) * pfgu_pc_normal_HG)) /\ exists ff_q_pfp_normal_HG_targetfirstentry. pfgu_pb_normal_HG = ff_q_pfp_normal_HG_targetfirstentry * S ((S (pfrep_position_normal_HG_targetfirst)) * pfgu_pc_normal_HG) + (pfrep_left_normal_HG_target)))))) \/ (((exists pfrep_gap_normal_HG_targetfirstoutside. pfrep_gap_normal_HG_targetfirstoutside+(pfgu_P_normal_HG)=(pfrep_power_normal_HG_target)) /\ (((pfrep_left_normal_HG_target)=0))))) -> ((exists pfrep_position_normal_HG_targetsecond. ((pfrep_position_normal_HG_targetsecond+S (pfrep_power_normal_HG_target)=(G)) /\ ((((exists ff_h_pfp_normal_HG_targetsecondentry. ff_h_pfp_normal_HG_targetsecondentry + S (pfrep_right_normal_HG_target) = S ((S (pfrep_position_normal_HG_targetsecond)) * gc)) /\ exists ff_q_pfp_normal_HG_targetsecondentry. gb = ff_q_pfp_normal_HG_targetsecondentry * S ((S (pfrep_position_normal_HG_targetsecond)) * gc) + (pfrep_right_normal_HG_target)))))) \/ (((exists pfrep_gap_normal_HG_targetsecondoutside. pfrep_gap_normal_HG_targetsecondoutside+(G)=(pfrep_power_normal_HG_target)) /\ (((pfrep_right_normal_HG_target)=0))))) -> pfrep_left_normal_HG_target=pfrep_right_normal_HG_target))))))) -> (forall pfrep_power_normal_result pfrep_left_normal_result pfrep_right_normal_result. ((exists pfrep_position_normal_resultfirst. ((pfrep_position_normal_resultfirst+S (pfrep_power_normal_result)=(G)) /\ ((((exists ff_h_pfp_normal_resultfirstentry. ff_h_pfp_normal_resultfirstentry + S (pfrep_left_normal_result) = S ((S (pfrep_position_normal_resultfirst)) * gc)) /\ exists ff_q_pfp_normal_resultfirstentry. gb = ff_q_pfp_normal_resultfirstentry * S ((S (pfrep_position_normal_resultfirst)) * gc) + (pfrep_left_normal_result)))))) \/ (((exists pfrep_gap_normal_resultfirstoutside. pfrep_gap_normal_resultfirstoutside+(G)=(pfrep_power_normal_result)) /\ (((pfrep_left_normal_result)=0))))) -> ((exists pfrep_position_normal_resultsecond. ((pfrep_position_normal_resultsecond+S (pfrep_power_normal_result)=(H)) /\ ((((exists ff_h_pfp_normal_resultsecondentry. ff_h_pfp_normal_resultsecondentry + S (pfrep_right_normal_result) = S ((S (pfrep_position_normal_resultsecond)) * hc)) /\ exists ff_q_pfp_normal_resultsecondentry. hb = ff_q_pfp_normal_resultsecondentry * S ((S (pfrep_position_normal_resultsecond)) * hc) + (pfrep_right_normal_result)))))) \/ (((exists pfrep_gap_normal_resultsecondoutside. pfrep_gap_normal_resultsecondoutside+(H)=(pfrep_power_normal_result)) /\ (((pfrep_right_normal_result)=0))))) -> pfrep_left_normal_result=pfrep_right_normal_result)