prime_field_polynomial_normalized_gcd_equivalent_unique

Exact expanded first-order arithmetic statement

forall p gb gc G hb hc H ab ac L bb bc M. (~((p) = 1) /\ forall pfa_factor_left_gcd_unique_prime pfa_factor_right_gcd_unique_prime. (p) = pfa_factor_left_gcd_unique_prime * pfa_factor_right_gcd_unique_prime -> pfa_factor_left_gcd_unique_prime = 1 \/ pfa_factor_right_gcd_unique_prime = 1) -> ((((G)=0 \/ (((~((G) = 0)) /\ (((forall fom_index_pfp_gcd_unique_G_normal_moniccoefficients. (exists fom_gap_pfp_gcd_unique_G_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_unique_G_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_unique_G_normal_moniccoefficients) = G) -> exists fom_value_pfp_gcd_unique_G_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_unique_G_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_unique_G_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_unique_G_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_unique_G_normal_moniccoefficients)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_normal_moniccoefficients_entry. gb = fom_beta_quotient_pfp_gcd_unique_G_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_unique_G_normal_moniccoefficients)) * gc) + (fom_value_pfp_gcd_unique_G_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_unique_G_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_unique_G_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_unique_G_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_unique_G_normal_monicleading. ff_h_pfp_gcd_unique_G_normal_monicleading + S (1) = S ((S (0)) * gc)) /\ exists ff_q_pfp_gcd_unique_G_normal_monicleading. gb = ff_q_pfp_gcd_unique_G_normal_monicleading * S ((S (0)) * gc) + (1))))))))) /\ ((((((((forall fom_index_pfp_gcd_unique_G_gcd_common_left_canonical. (exists fom_gap_pfp_gcd_unique_G_gcd_common_left_canonical_index_bound. fom_gap_pfp_gcd_unique_G_gcd_common_left_canonical_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_common_left_canonical) = L) -> exists fom_value_pfp_gcd_unique_G_gcd_common_left_canonical. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_common_left_canonical_entry. fom_beta_height_pfp_gcd_unique_G_gcd_common_left_canonical_entry + S (fom_value_pfp_gcd_unique_G_gcd_common_left_canonical) = S ((S (fom_index_pfp_gcd_unique_G_gcd_common_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_common_left_canonical_entry. ab = fom_beta_quotient_pfp_gcd_unique_G_gcd_common_left_canonical_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_common_left_canonical)) * ac) + (fom_value_pfp_gcd_unique_G_gcd_common_left_canonical))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_common_left_canonical_value_bound. fom_gap_pfp_gcd_unique_G_gcd_common_left_canonical_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_common_left_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_G_gcd_common_left pfgu_qc_gcd_unique_G_gcd_common_left pfgu_Q_gcd_unique_G_gcd_common_left pfgu_pb_gcd_unique_G_gcd_common_left pfgu_pc_gcd_unique_G_gcd_common_left pfgu_P_gcd_unique_G_gcd_common_left. ((((forall fom_index_pfp_gcd_unique_G_gcd_common_left_productleft. (exists fom_gap_pfp_gcd_unique_G_gcd_common_left_productleft_index_bound. fom_gap_pfp_gcd_unique_G_gcd_common_left_productleft_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_common_left_productleft) = pfgu_Q_gcd_unique_G_gcd_common_left) -> exists fom_value_pfp_gcd_unique_G_gcd_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_common_left_productleft_entry. fom_beta_height_pfp_gcd_unique_G_gcd_common_left_productleft_entry + S (fom_value_pfp_gcd_unique_G_gcd_common_left_productleft) = S ((S (fom_index_pfp_gcd_unique_G_gcd_common_left_productleft)) * pfgu_qc_gcd_unique_G_gcd_common_left)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_common_left_productleft_entry. pfgu_qb_gcd_unique_G_gcd_common_left = fom_beta_quotient_pfp_gcd_unique_G_gcd_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_common_left_productleft)) * pfgu_qc_gcd_unique_G_gcd_common_left) + (fom_value_pfp_gcd_unique_G_gcd_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_common_left_productleft_value_bound. fom_gap_pfp_gcd_unique_G_gcd_common_left_productleft_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_G_gcd_common_left_productright. (exists fom_gap_pfp_gcd_unique_G_gcd_common_left_productright_index_bound. fom_gap_pfp_gcd_unique_G_gcd_common_left_productright_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_common_left_productright) = G) -> exists fom_value_pfp_gcd_unique_G_gcd_common_left_productright. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_common_left_productright_entry. fom_beta_height_pfp_gcd_unique_G_gcd_common_left_productright_entry + S (fom_value_pfp_gcd_unique_G_gcd_common_left_productright) = S ((S (fom_index_pfp_gcd_unique_G_gcd_common_left_productright)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_common_left_productright_entry. gb = fom_beta_quotient_pfp_gcd_unique_G_gcd_common_left_productright_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_common_left_productright)) * gc) + (fom_value_pfp_gcd_unique_G_gcd_common_left_productright))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_common_left_productright_value_bound. fom_gap_pfp_gcd_unique_G_gcd_common_left_productright_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_common_left_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_G_gcd_common_left)=0 \/ (G)=0) /\ (((pfgu_P_gcd_unique_G_gcd_common_left)=0)))) \/ (((~((pfgu_Q_gcd_unique_G_gcd_common_left)=0)) /\ (((~((G)=0)) /\ (((pfgu_Q_gcd_unique_G_gcd_common_left)+(G)=S (pfgu_P_gcd_unique_G_gcd_common_left)))))))) /\ ((forall pfc_index_gcd_unique_G_gcd_common_left_productcoefficients. (exists pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientsbound. pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientsbound + S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficients) = (pfgu_P_gcd_unique_G_gcd_common_left)) -> exists pfc_value_gcd_unique_G_gcd_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientsentry. ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientsentry + S (pfc_value_gcd_unique_G_gcd_common_left_productcoefficients) = S ((S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_common_left)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientsentry. pfgu_pb_gcd_unique_G_gcd_common_left = ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_common_left) + (pfc_value_gcd_unique_G_gcd_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_G_gcd_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_unique_G_gcd_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_unique_G_gcd_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficients))) -> exists pfc_value_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_G_gcd_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_common_left_productcoefficientscoefficient) + (pfc_value_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_G_gcd_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_G_gcd_common_left)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_common_left)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_G_gcd_common_left = ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_common_left) + (pfc_left_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_G_gcd_common_left)=(pfc_index_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_G_gcd_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_G_gcd_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_G_gcd_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_G_gcd_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_G_gcd_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_G_gcd_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_G_gcd_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_G_gcd_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_G_gcd_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_G_gcd_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_G_gcd_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_G_gcd_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_G_gcd_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_unique_G_gcd_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_G_gcd_common_left_target pfrep_left_gcd_unique_G_gcd_common_left_target pfrep_right_gcd_unique_G_gcd_common_left_target. ((exists pfrep_position_gcd_unique_G_gcd_common_left_targetfirst. ((pfrep_position_gcd_unique_G_gcd_common_left_targetfirst+S (pfrep_power_gcd_unique_G_gcd_common_left_target)=(pfgu_P_gcd_unique_G_gcd_common_left)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_left_targetfirstentry. ff_h_pfp_gcd_unique_G_gcd_common_left_targetfirstentry + S (pfrep_left_gcd_unique_G_gcd_common_left_target) = S ((S (pfrep_position_gcd_unique_G_gcd_common_left_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_common_left)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_left_targetfirstentry. pfgu_pb_gcd_unique_G_gcd_common_left = ff_q_pfp_gcd_unique_G_gcd_common_left_targetfirstentry * S ((S (pfrep_position_gcd_unique_G_gcd_common_left_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_common_left) + (pfrep_left_gcd_unique_G_gcd_common_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_common_left_targetfirstoutside. pfrep_gap_gcd_unique_G_gcd_common_left_targetfirstoutside+(pfgu_P_gcd_unique_G_gcd_common_left)=(pfrep_power_gcd_unique_G_gcd_common_left_target)) /\ (((pfrep_left_gcd_unique_G_gcd_common_left_target)=0))))) -> ((exists pfrep_position_gcd_unique_G_gcd_common_left_targetsecond. ((pfrep_position_gcd_unique_G_gcd_common_left_targetsecond+S (pfrep_power_gcd_unique_G_gcd_common_left_target)=(L)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_left_targetsecondentry. ff_h_pfp_gcd_unique_G_gcd_common_left_targetsecondentry + S (pfrep_right_gcd_unique_G_gcd_common_left_target) = S ((S (pfrep_position_gcd_unique_G_gcd_common_left_targetsecond)) * ac)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_left_targetsecondentry. ab = ff_q_pfp_gcd_unique_G_gcd_common_left_targetsecondentry * S ((S (pfrep_position_gcd_unique_G_gcd_common_left_targetsecond)) * ac) + (pfrep_right_gcd_unique_G_gcd_common_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_common_left_targetsecondoutside. pfrep_gap_gcd_unique_G_gcd_common_left_targetsecondoutside+(L)=(pfrep_power_gcd_unique_G_gcd_common_left_target)) /\ (((pfrep_right_gcd_unique_G_gcd_common_left_target)=0))))) -> pfrep_left_gcd_unique_G_gcd_common_left_target=pfrep_right_gcd_unique_G_gcd_common_left_target))))))) /\ ((((forall fom_index_pfp_gcd_unique_G_gcd_common_right_canonical. (exists fom_gap_pfp_gcd_unique_G_gcd_common_right_canonical_index_bound. fom_gap_pfp_gcd_unique_G_gcd_common_right_canonical_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_common_right_canonical) = M) -> exists fom_value_pfp_gcd_unique_G_gcd_common_right_canonical. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_common_right_canonical_entry. fom_beta_height_pfp_gcd_unique_G_gcd_common_right_canonical_entry + S (fom_value_pfp_gcd_unique_G_gcd_common_right_canonical) = S ((S (fom_index_pfp_gcd_unique_G_gcd_common_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_common_right_canonical_entry. bb = fom_beta_quotient_pfp_gcd_unique_G_gcd_common_right_canonical_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_common_right_canonical)) * bc) + (fom_value_pfp_gcd_unique_G_gcd_common_right_canonical))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_common_right_canonical_value_bound. fom_gap_pfp_gcd_unique_G_gcd_common_right_canonical_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_common_right_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_G_gcd_common_right pfgu_qc_gcd_unique_G_gcd_common_right pfgu_Q_gcd_unique_G_gcd_common_right pfgu_pb_gcd_unique_G_gcd_common_right pfgu_pc_gcd_unique_G_gcd_common_right pfgu_P_gcd_unique_G_gcd_common_right. ((((forall fom_index_pfp_gcd_unique_G_gcd_common_right_productleft. (exists fom_gap_pfp_gcd_unique_G_gcd_common_right_productleft_index_bound. fom_gap_pfp_gcd_unique_G_gcd_common_right_productleft_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_common_right_productleft) = pfgu_Q_gcd_unique_G_gcd_common_right) -> exists fom_value_pfp_gcd_unique_G_gcd_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_common_right_productleft_entry. fom_beta_height_pfp_gcd_unique_G_gcd_common_right_productleft_entry + S (fom_value_pfp_gcd_unique_G_gcd_common_right_productleft) = S ((S (fom_index_pfp_gcd_unique_G_gcd_common_right_productleft)) * pfgu_qc_gcd_unique_G_gcd_common_right)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_common_right_productleft_entry. pfgu_qb_gcd_unique_G_gcd_common_right = fom_beta_quotient_pfp_gcd_unique_G_gcd_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_common_right_productleft)) * pfgu_qc_gcd_unique_G_gcd_common_right) + (fom_value_pfp_gcd_unique_G_gcd_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_common_right_productleft_value_bound. fom_gap_pfp_gcd_unique_G_gcd_common_right_productleft_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_G_gcd_common_right_productright. (exists fom_gap_pfp_gcd_unique_G_gcd_common_right_productright_index_bound. fom_gap_pfp_gcd_unique_G_gcd_common_right_productright_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_common_right_productright) = G) -> exists fom_value_pfp_gcd_unique_G_gcd_common_right_productright. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_common_right_productright_entry. fom_beta_height_pfp_gcd_unique_G_gcd_common_right_productright_entry + S (fom_value_pfp_gcd_unique_G_gcd_common_right_productright) = S ((S (fom_index_pfp_gcd_unique_G_gcd_common_right_productright)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_common_right_productright_entry. gb = fom_beta_quotient_pfp_gcd_unique_G_gcd_common_right_productright_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_common_right_productright)) * gc) + (fom_value_pfp_gcd_unique_G_gcd_common_right_productright))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_common_right_productright_value_bound. fom_gap_pfp_gcd_unique_G_gcd_common_right_productright_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_common_right_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_G_gcd_common_right)=0 \/ (G)=0) /\ (((pfgu_P_gcd_unique_G_gcd_common_right)=0)))) \/ (((~((pfgu_Q_gcd_unique_G_gcd_common_right)=0)) /\ (((~((G)=0)) /\ (((pfgu_Q_gcd_unique_G_gcd_common_right)+(G)=S (pfgu_P_gcd_unique_G_gcd_common_right)))))))) /\ ((forall pfc_index_gcd_unique_G_gcd_common_right_productcoefficients. (exists pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientsbound. pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientsbound + S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficients) = (pfgu_P_gcd_unique_G_gcd_common_right)) -> exists pfc_value_gcd_unique_G_gcd_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientsentry. ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientsentry + S (pfc_value_gcd_unique_G_gcd_common_right_productcoefficients) = S ((S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_common_right)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientsentry. pfgu_pb_gcd_unique_G_gcd_common_right = ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_common_right) + (pfc_value_gcd_unique_G_gcd_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_G_gcd_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_unique_G_gcd_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_unique_G_gcd_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficients))) -> exists pfc_value_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_G_gcd_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_common_right_productcoefficientscoefficient) + (pfc_value_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_G_gcd_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_G_gcd_common_right)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_common_right)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_G_gcd_common_right = ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_common_right) + (pfc_left_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_G_gcd_common_right)=(pfc_index_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_G_gcd_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_G_gcd_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_G_gcd_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_G_gcd_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_G_gcd_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_G_gcd_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_G_gcd_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_G_gcd_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_G_gcd_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_G_gcd_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_G_gcd_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_G_gcd_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_G_gcd_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_unique_G_gcd_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_G_gcd_common_right_target pfrep_left_gcd_unique_G_gcd_common_right_target pfrep_right_gcd_unique_G_gcd_common_right_target. ((exists pfrep_position_gcd_unique_G_gcd_common_right_targetfirst. ((pfrep_position_gcd_unique_G_gcd_common_right_targetfirst+S (pfrep_power_gcd_unique_G_gcd_common_right_target)=(pfgu_P_gcd_unique_G_gcd_common_right)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_right_targetfirstentry. ff_h_pfp_gcd_unique_G_gcd_common_right_targetfirstentry + S (pfrep_left_gcd_unique_G_gcd_common_right_target) = S ((S (pfrep_position_gcd_unique_G_gcd_common_right_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_common_right)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_right_targetfirstentry. pfgu_pb_gcd_unique_G_gcd_common_right = ff_q_pfp_gcd_unique_G_gcd_common_right_targetfirstentry * S ((S (pfrep_position_gcd_unique_G_gcd_common_right_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_common_right) + (pfrep_left_gcd_unique_G_gcd_common_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_common_right_targetfirstoutside. pfrep_gap_gcd_unique_G_gcd_common_right_targetfirstoutside+(pfgu_P_gcd_unique_G_gcd_common_right)=(pfrep_power_gcd_unique_G_gcd_common_right_target)) /\ (((pfrep_left_gcd_unique_G_gcd_common_right_target)=0))))) -> ((exists pfrep_position_gcd_unique_G_gcd_common_right_targetsecond. ((pfrep_position_gcd_unique_G_gcd_common_right_targetsecond+S (pfrep_power_gcd_unique_G_gcd_common_right_target)=(M)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_common_right_targetsecondentry. ff_h_pfp_gcd_unique_G_gcd_common_right_targetsecondentry + S (pfrep_right_gcd_unique_G_gcd_common_right_target) = S ((S (pfrep_position_gcd_unique_G_gcd_common_right_targetsecond)) * bc)) /\ exists ff_q_pfp_gcd_unique_G_gcd_common_right_targetsecondentry. bb = ff_q_pfp_gcd_unique_G_gcd_common_right_targetsecondentry * S ((S (pfrep_position_gcd_unique_G_gcd_common_right_targetsecond)) * bc) + (pfrep_right_gcd_unique_G_gcd_common_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_common_right_targetsecondoutside. pfrep_gap_gcd_unique_G_gcd_common_right_targetsecondoutside+(M)=(pfrep_power_gcd_unique_G_gcd_common_right_target)) /\ (((pfrep_right_gcd_unique_G_gcd_common_right_target)=0))))) -> pfrep_left_gcd_unique_G_gcd_common_right_target=pfrep_right_gcd_unique_G_gcd_common_right_target)))))))))) /\ ((forall pfgu_db_gcd_unique_G_gcd pfgu_dc_gcd_unique_G_gcd pfgu_D_gcd_unique_G_gcd. (((((forall fom_index_pfp_gcd_unique_G_gcd_divisor_left_canonical. (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_left_canonical_index_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_left_canonical_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_canonical) = L) -> exists fom_value_pfp_gcd_unique_G_gcd_divisor_left_canonical. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_divisor_left_canonical_entry. fom_beta_height_pfp_gcd_unique_G_gcd_divisor_left_canonical_entry + S (fom_value_pfp_gcd_unique_G_gcd_divisor_left_canonical) = S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_left_canonical_entry. ab = fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_left_canonical_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_canonical)) * ac) + (fom_value_pfp_gcd_unique_G_gcd_divisor_left_canonical))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_left_canonical_value_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_left_canonical_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_divisor_left_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_G_gcd_divisor_left pfgu_qc_gcd_unique_G_gcd_divisor_left pfgu_Q_gcd_unique_G_gcd_divisor_left pfgu_pb_gcd_unique_G_gcd_divisor_left pfgu_pc_gcd_unique_G_gcd_divisor_left pfgu_P_gcd_unique_G_gcd_divisor_left. ((((forall fom_index_pfp_gcd_unique_G_gcd_divisor_left_productleft. (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productleft_index_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productleft_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_productleft) = pfgu_Q_gcd_unique_G_gcd_divisor_left) -> exists fom_value_pfp_gcd_unique_G_gcd_divisor_left_productleft. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_divisor_left_productleft_entry. fom_beta_height_pfp_gcd_unique_G_gcd_divisor_left_productleft_entry + S (fom_value_pfp_gcd_unique_G_gcd_divisor_left_productleft) = S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_productleft)) * pfgu_qc_gcd_unique_G_gcd_divisor_left)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_left_productleft_entry. pfgu_qb_gcd_unique_G_gcd_divisor_left = fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_left_productleft_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_productleft)) * pfgu_qc_gcd_unique_G_gcd_divisor_left) + (fom_value_pfp_gcd_unique_G_gcd_divisor_left_productleft))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productleft_value_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productleft_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_divisor_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_G_gcd_divisor_left_productright. (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productright_index_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productright_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_productright) = pfgu_D_gcd_unique_G_gcd) -> exists fom_value_pfp_gcd_unique_G_gcd_divisor_left_productright. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_divisor_left_productright_entry. fom_beta_height_pfp_gcd_unique_G_gcd_divisor_left_productright_entry + S (fom_value_pfp_gcd_unique_G_gcd_divisor_left_productright) = S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_productright)) * pfgu_dc_gcd_unique_G_gcd)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_left_productright_entry. pfgu_db_gcd_unique_G_gcd = fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_left_productright_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_left_productright)) * pfgu_dc_gcd_unique_G_gcd) + (fom_value_pfp_gcd_unique_G_gcd_divisor_left_productright))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productright_value_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_left_productright_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_divisor_left_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_G_gcd_divisor_left)=0 \/ (pfgu_D_gcd_unique_G_gcd)=0) /\ (((pfgu_P_gcd_unique_G_gcd_divisor_left)=0)))) \/ (((~((pfgu_Q_gcd_unique_G_gcd_divisor_left)=0)) /\ (((~((pfgu_D_gcd_unique_G_gcd)=0)) /\ (((pfgu_Q_gcd_unique_G_gcd_divisor_left)+(pfgu_D_gcd_unique_G_gcd)=S (pfgu_P_gcd_unique_G_gcd_divisor_left)))))))) /\ ((forall pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients. (exists pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientsbound. pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientsbound + S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients) = (pfgu_P_gcd_unique_G_gcd_divisor_left)) -> exists pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficients. ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientsentry. ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientsentry + S (pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficients) = S ((S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_divisor_left)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientsentry. pfgu_pb_gcd_unique_G_gcd_divisor_left = ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientsentry * S ((S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_divisor_left) + (pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient pfc_terms_scale_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient pfc_natural_sum_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients))) -> exists pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient = ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient) + (pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_G_gcd_divisor_left)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_divisor_left)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_G_gcd_divisor_left = ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_divisor_left) + (pfc_left_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_G_gcd_divisor_left)=(pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = (pfgu_D_gcd_unique_G_gcd)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_G_gcd)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. pfgu_db_gcd_unique_G_gcd = ff_q_pfp_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_G_gcd) + (pfc_right_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgu_D_gcd_unique_G_gcd)=(pfc_complement_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_G_gcd_divisor_left_productcoefficients)) -> exists fs_a_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient = fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_G_gcd_divisor_left_productcoefficients) + (p) * pfa_offset_right_gcd_unique_G_gcd_divisor_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_G_gcd_divisor_left_target pfrep_left_gcd_unique_G_gcd_divisor_left_target pfrep_right_gcd_unique_G_gcd_divisor_left_target. ((exists pfrep_position_gcd_unique_G_gcd_divisor_left_targetfirst. ((pfrep_position_gcd_unique_G_gcd_divisor_left_targetfirst+S (pfrep_power_gcd_unique_G_gcd_divisor_left_target)=(pfgu_P_gcd_unique_G_gcd_divisor_left)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_left_targetfirstentry. ff_h_pfp_gcd_unique_G_gcd_divisor_left_targetfirstentry + S (pfrep_left_gcd_unique_G_gcd_divisor_left_target) = S ((S (pfrep_position_gcd_unique_G_gcd_divisor_left_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_divisor_left)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_left_targetfirstentry. pfgu_pb_gcd_unique_G_gcd_divisor_left = ff_q_pfp_gcd_unique_G_gcd_divisor_left_targetfirstentry * S ((S (pfrep_position_gcd_unique_G_gcd_divisor_left_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_divisor_left) + (pfrep_left_gcd_unique_G_gcd_divisor_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_divisor_left_targetfirstoutside. pfrep_gap_gcd_unique_G_gcd_divisor_left_targetfirstoutside+(pfgu_P_gcd_unique_G_gcd_divisor_left)=(pfrep_power_gcd_unique_G_gcd_divisor_left_target)) /\ (((pfrep_left_gcd_unique_G_gcd_divisor_left_target)=0))))) -> ((exists pfrep_position_gcd_unique_G_gcd_divisor_left_targetsecond. ((pfrep_position_gcd_unique_G_gcd_divisor_left_targetsecond+S (pfrep_power_gcd_unique_G_gcd_divisor_left_target)=(L)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_left_targetsecondentry. ff_h_pfp_gcd_unique_G_gcd_divisor_left_targetsecondentry + S (pfrep_right_gcd_unique_G_gcd_divisor_left_target) = S ((S (pfrep_position_gcd_unique_G_gcd_divisor_left_targetsecond)) * ac)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_left_targetsecondentry. ab = ff_q_pfp_gcd_unique_G_gcd_divisor_left_targetsecondentry * S ((S (pfrep_position_gcd_unique_G_gcd_divisor_left_targetsecond)) * ac) + (pfrep_right_gcd_unique_G_gcd_divisor_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_divisor_left_targetsecondoutside. pfrep_gap_gcd_unique_G_gcd_divisor_left_targetsecondoutside+(L)=(pfrep_power_gcd_unique_G_gcd_divisor_left_target)) /\ (((pfrep_right_gcd_unique_G_gcd_divisor_left_target)=0))))) -> pfrep_left_gcd_unique_G_gcd_divisor_left_target=pfrep_right_gcd_unique_G_gcd_divisor_left_target))))))) /\ ((((forall fom_index_pfp_gcd_unique_G_gcd_divisor_right_canonical. (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_right_canonical_index_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_right_canonical_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_canonical) = M) -> exists fom_value_pfp_gcd_unique_G_gcd_divisor_right_canonical. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_divisor_right_canonical_entry. fom_beta_height_pfp_gcd_unique_G_gcd_divisor_right_canonical_entry + S (fom_value_pfp_gcd_unique_G_gcd_divisor_right_canonical) = S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_right_canonical_entry. bb = fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_right_canonical_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_canonical)) * bc) + (fom_value_pfp_gcd_unique_G_gcd_divisor_right_canonical))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_right_canonical_value_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_right_canonical_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_divisor_right_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_G_gcd_divisor_right pfgu_qc_gcd_unique_G_gcd_divisor_right pfgu_Q_gcd_unique_G_gcd_divisor_right pfgu_pb_gcd_unique_G_gcd_divisor_right pfgu_pc_gcd_unique_G_gcd_divisor_right pfgu_P_gcd_unique_G_gcd_divisor_right. ((((forall fom_index_pfp_gcd_unique_G_gcd_divisor_right_productleft. (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productleft_index_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productleft_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_productleft) = pfgu_Q_gcd_unique_G_gcd_divisor_right) -> exists fom_value_pfp_gcd_unique_G_gcd_divisor_right_productleft. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_divisor_right_productleft_entry. fom_beta_height_pfp_gcd_unique_G_gcd_divisor_right_productleft_entry + S (fom_value_pfp_gcd_unique_G_gcd_divisor_right_productleft) = S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_productleft)) * pfgu_qc_gcd_unique_G_gcd_divisor_right)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_right_productleft_entry. pfgu_qb_gcd_unique_G_gcd_divisor_right = fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_right_productleft_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_productleft)) * pfgu_qc_gcd_unique_G_gcd_divisor_right) + (fom_value_pfp_gcd_unique_G_gcd_divisor_right_productleft))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productleft_value_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productleft_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_divisor_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_G_gcd_divisor_right_productright. (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productright_index_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productright_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_productright) = pfgu_D_gcd_unique_G_gcd) -> exists fom_value_pfp_gcd_unique_G_gcd_divisor_right_productright. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_divisor_right_productright_entry. fom_beta_height_pfp_gcd_unique_G_gcd_divisor_right_productright_entry + S (fom_value_pfp_gcd_unique_G_gcd_divisor_right_productright) = S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_productright)) * pfgu_dc_gcd_unique_G_gcd)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_right_productright_entry. pfgu_db_gcd_unique_G_gcd = fom_beta_quotient_pfp_gcd_unique_G_gcd_divisor_right_productright_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_divisor_right_productright)) * pfgu_dc_gcd_unique_G_gcd) + (fom_value_pfp_gcd_unique_G_gcd_divisor_right_productright))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productright_value_bound. fom_gap_pfp_gcd_unique_G_gcd_divisor_right_productright_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_divisor_right_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_G_gcd_divisor_right)=0 \/ (pfgu_D_gcd_unique_G_gcd)=0) /\ (((pfgu_P_gcd_unique_G_gcd_divisor_right)=0)))) \/ (((~((pfgu_Q_gcd_unique_G_gcd_divisor_right)=0)) /\ (((~((pfgu_D_gcd_unique_G_gcd)=0)) /\ (((pfgu_Q_gcd_unique_G_gcd_divisor_right)+(pfgu_D_gcd_unique_G_gcd)=S (pfgu_P_gcd_unique_G_gcd_divisor_right)))))))) /\ ((forall pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients. (exists pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientsbound. pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientsbound + S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients) = (pfgu_P_gcd_unique_G_gcd_divisor_right)) -> exists pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficients. ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientsentry. ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientsentry + S (pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficients) = S ((S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_divisor_right)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientsentry. pfgu_pb_gcd_unique_G_gcd_divisor_right = ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientsentry * S ((S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_divisor_right) + (pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient pfc_terms_scale_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient pfc_natural_sum_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients))) -> exists pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient = ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient) + (pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_G_gcd_divisor_right)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_divisor_right)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_G_gcd_divisor_right = ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_divisor_right) + (pfc_left_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_G_gcd_divisor_right)=(pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = (pfgu_D_gcd_unique_G_gcd)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_G_gcd)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. pfgu_db_gcd_unique_G_gcd = ff_q_pfp_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_G_gcd) + (pfc_right_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgu_D_gcd_unique_G_gcd)=(pfc_complement_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_G_gcd_divisor_right_productcoefficients)) -> exists fs_a_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient = fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_G_gcd_divisor_right_productcoefficients) + (p) * pfa_offset_right_gcd_unique_G_gcd_divisor_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_G_gcd_divisor_right_target pfrep_left_gcd_unique_G_gcd_divisor_right_target pfrep_right_gcd_unique_G_gcd_divisor_right_target. ((exists pfrep_position_gcd_unique_G_gcd_divisor_right_targetfirst. ((pfrep_position_gcd_unique_G_gcd_divisor_right_targetfirst+S (pfrep_power_gcd_unique_G_gcd_divisor_right_target)=(pfgu_P_gcd_unique_G_gcd_divisor_right)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_right_targetfirstentry. ff_h_pfp_gcd_unique_G_gcd_divisor_right_targetfirstentry + S (pfrep_left_gcd_unique_G_gcd_divisor_right_target) = S ((S (pfrep_position_gcd_unique_G_gcd_divisor_right_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_divisor_right)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_right_targetfirstentry. pfgu_pb_gcd_unique_G_gcd_divisor_right = ff_q_pfp_gcd_unique_G_gcd_divisor_right_targetfirstentry * S ((S (pfrep_position_gcd_unique_G_gcd_divisor_right_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_divisor_right) + (pfrep_left_gcd_unique_G_gcd_divisor_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_divisor_right_targetfirstoutside. pfrep_gap_gcd_unique_G_gcd_divisor_right_targetfirstoutside+(pfgu_P_gcd_unique_G_gcd_divisor_right)=(pfrep_power_gcd_unique_G_gcd_divisor_right_target)) /\ (((pfrep_left_gcd_unique_G_gcd_divisor_right_target)=0))))) -> ((exists pfrep_position_gcd_unique_G_gcd_divisor_right_targetsecond. ((pfrep_position_gcd_unique_G_gcd_divisor_right_targetsecond+S (pfrep_power_gcd_unique_G_gcd_divisor_right_target)=(M)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_divisor_right_targetsecondentry. ff_h_pfp_gcd_unique_G_gcd_divisor_right_targetsecondentry + S (pfrep_right_gcd_unique_G_gcd_divisor_right_target) = S ((S (pfrep_position_gcd_unique_G_gcd_divisor_right_targetsecond)) * bc)) /\ exists ff_q_pfp_gcd_unique_G_gcd_divisor_right_targetsecondentry. bb = ff_q_pfp_gcd_unique_G_gcd_divisor_right_targetsecondentry * S ((S (pfrep_position_gcd_unique_G_gcd_divisor_right_targetsecond)) * bc) + (pfrep_right_gcd_unique_G_gcd_divisor_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_divisor_right_targetsecondoutside. pfrep_gap_gcd_unique_G_gcd_divisor_right_targetsecondoutside+(M)=(pfrep_power_gcd_unique_G_gcd_divisor_right_target)) /\ (((pfrep_right_gcd_unique_G_gcd_divisor_right_target)=0))))) -> pfrep_left_gcd_unique_G_gcd_divisor_right_target=pfrep_right_gcd_unique_G_gcd_divisor_right_target)))))))))) -> (((forall fom_index_pfp_gcd_unique_G_gcd_greatest_canonical. (exists fom_gap_pfp_gcd_unique_G_gcd_greatest_canonical_index_bound. fom_gap_pfp_gcd_unique_G_gcd_greatest_canonical_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_greatest_canonical) = G) -> exists fom_value_pfp_gcd_unique_G_gcd_greatest_canonical. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_greatest_canonical_entry. fom_beta_height_pfp_gcd_unique_G_gcd_greatest_canonical_entry + S (fom_value_pfp_gcd_unique_G_gcd_greatest_canonical) = S ((S (fom_index_pfp_gcd_unique_G_gcd_greatest_canonical)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_greatest_canonical_entry. gb = fom_beta_quotient_pfp_gcd_unique_G_gcd_greatest_canonical_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_greatest_canonical)) * gc) + (fom_value_pfp_gcd_unique_G_gcd_greatest_canonical))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_greatest_canonical_value_bound. fom_gap_pfp_gcd_unique_G_gcd_greatest_canonical_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_greatest_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_G_gcd_greatest pfgu_qc_gcd_unique_G_gcd_greatest pfgu_Q_gcd_unique_G_gcd_greatest pfgu_pb_gcd_unique_G_gcd_greatest pfgu_pc_gcd_unique_G_gcd_greatest pfgu_P_gcd_unique_G_gcd_greatest. ((((forall fom_index_pfp_gcd_unique_G_gcd_greatest_productleft. (exists fom_gap_pfp_gcd_unique_G_gcd_greatest_productleft_index_bound. fom_gap_pfp_gcd_unique_G_gcd_greatest_productleft_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_greatest_productleft) = pfgu_Q_gcd_unique_G_gcd_greatest) -> exists fom_value_pfp_gcd_unique_G_gcd_greatest_productleft. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_greatest_productleft_entry. fom_beta_height_pfp_gcd_unique_G_gcd_greatest_productleft_entry + S (fom_value_pfp_gcd_unique_G_gcd_greatest_productleft) = S ((S (fom_index_pfp_gcd_unique_G_gcd_greatest_productleft)) * pfgu_qc_gcd_unique_G_gcd_greatest)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_greatest_productleft_entry. pfgu_qb_gcd_unique_G_gcd_greatest = fom_beta_quotient_pfp_gcd_unique_G_gcd_greatest_productleft_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_greatest_productleft)) * pfgu_qc_gcd_unique_G_gcd_greatest) + (fom_value_pfp_gcd_unique_G_gcd_greatest_productleft))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_greatest_productleft_value_bound. fom_gap_pfp_gcd_unique_G_gcd_greatest_productleft_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_greatest_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_G_gcd_greatest_productright. (exists fom_gap_pfp_gcd_unique_G_gcd_greatest_productright_index_bound. fom_gap_pfp_gcd_unique_G_gcd_greatest_productright_index_bound + S (fom_index_pfp_gcd_unique_G_gcd_greatest_productright) = pfgu_D_gcd_unique_G_gcd) -> exists fom_value_pfp_gcd_unique_G_gcd_greatest_productright. ((((exists fom_beta_height_pfp_gcd_unique_G_gcd_greatest_productright_entry. fom_beta_height_pfp_gcd_unique_G_gcd_greatest_productright_entry + S (fom_value_pfp_gcd_unique_G_gcd_greatest_productright) = S ((S (fom_index_pfp_gcd_unique_G_gcd_greatest_productright)) * pfgu_dc_gcd_unique_G_gcd)) /\ exists fom_beta_quotient_pfp_gcd_unique_G_gcd_greatest_productright_entry. pfgu_db_gcd_unique_G_gcd = fom_beta_quotient_pfp_gcd_unique_G_gcd_greatest_productright_entry * S ((S (fom_index_pfp_gcd_unique_G_gcd_greatest_productright)) * pfgu_dc_gcd_unique_G_gcd) + (fom_value_pfp_gcd_unique_G_gcd_greatest_productright))) /\ (exists fom_gap_pfp_gcd_unique_G_gcd_greatest_productright_value_bound. fom_gap_pfp_gcd_unique_G_gcd_greatest_productright_value_bound + S (fom_value_pfp_gcd_unique_G_gcd_greatest_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_G_gcd_greatest)=0 \/ (pfgu_D_gcd_unique_G_gcd)=0) /\ (((pfgu_P_gcd_unique_G_gcd_greatest)=0)))) \/ (((~((pfgu_Q_gcd_unique_G_gcd_greatest)=0)) /\ (((~((pfgu_D_gcd_unique_G_gcd)=0)) /\ (((pfgu_Q_gcd_unique_G_gcd_greatest)+(pfgu_D_gcd_unique_G_gcd)=S (pfgu_P_gcd_unique_G_gcd_greatest)))))))) /\ ((forall pfc_index_gcd_unique_G_gcd_greatest_productcoefficients. (exists pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientsbound. pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientsbound + S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficients) = (pfgu_P_gcd_unique_G_gcd_greatest)) -> exists pfc_value_gcd_unique_G_gcd_greatest_productcoefficients. ((((exists ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientsentry. ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientsentry + S (pfc_value_gcd_unique_G_gcd_greatest_productcoefficients) = S ((S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_greatest)) /\ exists ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientsentry. pfgu_pb_gcd_unique_G_gcd_greatest = ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientsentry * S ((S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficients)) * pfgu_pc_gcd_unique_G_gcd_greatest) + (pfc_value_gcd_unique_G_gcd_greatest_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_G_gcd_greatest_productcoefficientscoefficient pfc_terms_scale_gcd_unique_G_gcd_greatest_productcoefficientscoefficient pfc_natural_sum_gcd_unique_G_gcd_greatest_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficients))) -> exists pfc_value_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_greatest_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_G_gcd_greatest_productcoefficientscoefficient = ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_G_gcd_greatest_productcoefficientscoefficient) + (pfc_value_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_G_gcd_greatest_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_G_gcd_greatest)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_greatest)) /\ exists ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_G_gcd_greatest = ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_G_gcd_greatest) + (pfc_left_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_G_gcd_greatest)=(pfc_index_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm) = (pfgu_D_gcd_unique_G_gcd)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_G_gcd)) /\ exists ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry. pfgu_db_gcd_unique_G_gcd = ff_q_pfp_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_G_gcd) + (pfc_right_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonaltermrightoutside+(pfgu_D_gcd_unique_G_gcd)=(pfc_complement_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_G_gcd_greatest_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_G_gcd_greatest_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficients))) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_G_gcd_greatest_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_G_gcd_greatest_productcoefficients)) -> exists fs_a_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_greatest_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_G_gcd_greatest_productcoefficientscoefficient = fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_G_gcd_greatest_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_G_gcd_greatest_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_G_gcd_greatest_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_G_gcd_greatest_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_G_gcd_greatest_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_G_gcd_greatest_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_G_gcd_greatest_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_G_gcd_greatest_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_G_gcd_greatest_productcoefficients) + (p) * pfa_offset_right_gcd_unique_G_gcd_greatest_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_G_gcd_greatest_target pfrep_left_gcd_unique_G_gcd_greatest_target pfrep_right_gcd_unique_G_gcd_greatest_target. ((exists pfrep_position_gcd_unique_G_gcd_greatest_targetfirst. ((pfrep_position_gcd_unique_G_gcd_greatest_targetfirst+S (pfrep_power_gcd_unique_G_gcd_greatest_target)=(pfgu_P_gcd_unique_G_gcd_greatest)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_greatest_targetfirstentry. ff_h_pfp_gcd_unique_G_gcd_greatest_targetfirstentry + S (pfrep_left_gcd_unique_G_gcd_greatest_target) = S ((S (pfrep_position_gcd_unique_G_gcd_greatest_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_greatest)) /\ exists ff_q_pfp_gcd_unique_G_gcd_greatest_targetfirstentry. pfgu_pb_gcd_unique_G_gcd_greatest = ff_q_pfp_gcd_unique_G_gcd_greatest_targetfirstentry * S ((S (pfrep_position_gcd_unique_G_gcd_greatest_targetfirst)) * pfgu_pc_gcd_unique_G_gcd_greatest) + (pfrep_left_gcd_unique_G_gcd_greatest_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_greatest_targetfirstoutside. pfrep_gap_gcd_unique_G_gcd_greatest_targetfirstoutside+(pfgu_P_gcd_unique_G_gcd_greatest)=(pfrep_power_gcd_unique_G_gcd_greatest_target)) /\ (((pfrep_left_gcd_unique_G_gcd_greatest_target)=0))))) -> ((exists pfrep_position_gcd_unique_G_gcd_greatest_targetsecond. ((pfrep_position_gcd_unique_G_gcd_greatest_targetsecond+S (pfrep_power_gcd_unique_G_gcd_greatest_target)=(G)) /\ ((((exists ff_h_pfp_gcd_unique_G_gcd_greatest_targetsecondentry. ff_h_pfp_gcd_unique_G_gcd_greatest_targetsecondentry + S (pfrep_right_gcd_unique_G_gcd_greatest_target) = S ((S (pfrep_position_gcd_unique_G_gcd_greatest_targetsecond)) * gc)) /\ exists ff_q_pfp_gcd_unique_G_gcd_greatest_targetsecondentry. gb = ff_q_pfp_gcd_unique_G_gcd_greatest_targetsecondentry * S ((S (pfrep_position_gcd_unique_G_gcd_greatest_targetsecond)) * gc) + (pfrep_right_gcd_unique_G_gcd_greatest_target)))))) \/ (((exists pfrep_gap_gcd_unique_G_gcd_greatest_targetsecondoutside. pfrep_gap_gcd_unique_G_gcd_greatest_targetsecondoutside+(G)=(pfrep_power_gcd_unique_G_gcd_greatest_target)) /\ (((pfrep_right_gcd_unique_G_gcd_greatest_target)=0))))) -> pfrep_left_gcd_unique_G_gcd_greatest_target=pfrep_right_gcd_unique_G_gcd_greatest_target)))))))))))))) -> ((((H)=0 \/ (((~((H) = 0)) /\ (((forall fom_index_pfp_gcd_unique_H_normal_moniccoefficients. (exists fom_gap_pfp_gcd_unique_H_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_unique_H_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_unique_H_normal_moniccoefficients) = H) -> exists fom_value_pfp_gcd_unique_H_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_unique_H_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_unique_H_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_unique_H_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_unique_H_normal_moniccoefficients)) * hc)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_normal_moniccoefficients_entry. hb = fom_beta_quotient_pfp_gcd_unique_H_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_unique_H_normal_moniccoefficients)) * hc) + (fom_value_pfp_gcd_unique_H_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_unique_H_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_unique_H_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_unique_H_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_unique_H_normal_monicleading. ff_h_pfp_gcd_unique_H_normal_monicleading + S (1) = S ((S (0)) * hc)) /\ exists ff_q_pfp_gcd_unique_H_normal_monicleading. hb = ff_q_pfp_gcd_unique_H_normal_monicleading * S ((S (0)) * hc) + (1))))))))) /\ ((((((((forall fom_index_pfp_gcd_unique_H_gcd_common_left_canonical. (exists fom_gap_pfp_gcd_unique_H_gcd_common_left_canonical_index_bound. fom_gap_pfp_gcd_unique_H_gcd_common_left_canonical_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_common_left_canonical) = L) -> exists fom_value_pfp_gcd_unique_H_gcd_common_left_canonical. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_common_left_canonical_entry. fom_beta_height_pfp_gcd_unique_H_gcd_common_left_canonical_entry + S (fom_value_pfp_gcd_unique_H_gcd_common_left_canonical) = S ((S (fom_index_pfp_gcd_unique_H_gcd_common_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_common_left_canonical_entry. ab = fom_beta_quotient_pfp_gcd_unique_H_gcd_common_left_canonical_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_common_left_canonical)) * ac) + (fom_value_pfp_gcd_unique_H_gcd_common_left_canonical))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_common_left_canonical_value_bound. fom_gap_pfp_gcd_unique_H_gcd_common_left_canonical_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_common_left_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_H_gcd_common_left pfgu_qc_gcd_unique_H_gcd_common_left pfgu_Q_gcd_unique_H_gcd_common_left pfgu_pb_gcd_unique_H_gcd_common_left pfgu_pc_gcd_unique_H_gcd_common_left pfgu_P_gcd_unique_H_gcd_common_left. ((((forall fom_index_pfp_gcd_unique_H_gcd_common_left_productleft. (exists fom_gap_pfp_gcd_unique_H_gcd_common_left_productleft_index_bound. fom_gap_pfp_gcd_unique_H_gcd_common_left_productleft_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_common_left_productleft) = pfgu_Q_gcd_unique_H_gcd_common_left) -> exists fom_value_pfp_gcd_unique_H_gcd_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_common_left_productleft_entry. fom_beta_height_pfp_gcd_unique_H_gcd_common_left_productleft_entry + S (fom_value_pfp_gcd_unique_H_gcd_common_left_productleft) = S ((S (fom_index_pfp_gcd_unique_H_gcd_common_left_productleft)) * pfgu_qc_gcd_unique_H_gcd_common_left)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_common_left_productleft_entry. pfgu_qb_gcd_unique_H_gcd_common_left = fom_beta_quotient_pfp_gcd_unique_H_gcd_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_common_left_productleft)) * pfgu_qc_gcd_unique_H_gcd_common_left) + (fom_value_pfp_gcd_unique_H_gcd_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_common_left_productleft_value_bound. fom_gap_pfp_gcd_unique_H_gcd_common_left_productleft_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_H_gcd_common_left_productright. (exists fom_gap_pfp_gcd_unique_H_gcd_common_left_productright_index_bound. fom_gap_pfp_gcd_unique_H_gcd_common_left_productright_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_common_left_productright) = H) -> exists fom_value_pfp_gcd_unique_H_gcd_common_left_productright. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_common_left_productright_entry. fom_beta_height_pfp_gcd_unique_H_gcd_common_left_productright_entry + S (fom_value_pfp_gcd_unique_H_gcd_common_left_productright) = S ((S (fom_index_pfp_gcd_unique_H_gcd_common_left_productright)) * hc)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_common_left_productright_entry. hb = fom_beta_quotient_pfp_gcd_unique_H_gcd_common_left_productright_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_common_left_productright)) * hc) + (fom_value_pfp_gcd_unique_H_gcd_common_left_productright))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_common_left_productright_value_bound. fom_gap_pfp_gcd_unique_H_gcd_common_left_productright_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_common_left_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_H_gcd_common_left)=0 \/ (H)=0) /\ (((pfgu_P_gcd_unique_H_gcd_common_left)=0)))) \/ (((~((pfgu_Q_gcd_unique_H_gcd_common_left)=0)) /\ (((~((H)=0)) /\ (((pfgu_Q_gcd_unique_H_gcd_common_left)+(H)=S (pfgu_P_gcd_unique_H_gcd_common_left)))))))) /\ ((forall pfc_index_gcd_unique_H_gcd_common_left_productcoefficients. (exists pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientsbound. pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientsbound + S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficients) = (pfgu_P_gcd_unique_H_gcd_common_left)) -> exists pfc_value_gcd_unique_H_gcd_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientsentry. ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientsentry + S (pfc_value_gcd_unique_H_gcd_common_left_productcoefficients) = S ((S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_common_left)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientsentry. pfgu_pb_gcd_unique_H_gcd_common_left = ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_common_left) + (pfc_value_gcd_unique_H_gcd_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_H_gcd_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_unique_H_gcd_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_unique_H_gcd_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficients))) -> exists pfc_value_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_H_gcd_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_common_left_productcoefficientscoefficient) + (pfc_value_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_H_gcd_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_H_gcd_common_left)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_common_left)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_H_gcd_common_left = ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_common_left) + (pfc_left_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_H_gcd_common_left)=(pfc_index_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_H_gcd_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_H_gcd_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_H_gcd_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_H_gcd_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_H_gcd_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_H_gcd_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_H_gcd_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_H_gcd_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_H_gcd_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_H_gcd_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_H_gcd_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_H_gcd_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_H_gcd_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_unique_H_gcd_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_H_gcd_common_left_target pfrep_left_gcd_unique_H_gcd_common_left_target pfrep_right_gcd_unique_H_gcd_common_left_target. ((exists pfrep_position_gcd_unique_H_gcd_common_left_targetfirst. ((pfrep_position_gcd_unique_H_gcd_common_left_targetfirst+S (pfrep_power_gcd_unique_H_gcd_common_left_target)=(pfgu_P_gcd_unique_H_gcd_common_left)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_left_targetfirstentry. ff_h_pfp_gcd_unique_H_gcd_common_left_targetfirstentry + S (pfrep_left_gcd_unique_H_gcd_common_left_target) = S ((S (pfrep_position_gcd_unique_H_gcd_common_left_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_common_left)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_left_targetfirstentry. pfgu_pb_gcd_unique_H_gcd_common_left = ff_q_pfp_gcd_unique_H_gcd_common_left_targetfirstentry * S ((S (pfrep_position_gcd_unique_H_gcd_common_left_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_common_left) + (pfrep_left_gcd_unique_H_gcd_common_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_common_left_targetfirstoutside. pfrep_gap_gcd_unique_H_gcd_common_left_targetfirstoutside+(pfgu_P_gcd_unique_H_gcd_common_left)=(pfrep_power_gcd_unique_H_gcd_common_left_target)) /\ (((pfrep_left_gcd_unique_H_gcd_common_left_target)=0))))) -> ((exists pfrep_position_gcd_unique_H_gcd_common_left_targetsecond. ((pfrep_position_gcd_unique_H_gcd_common_left_targetsecond+S (pfrep_power_gcd_unique_H_gcd_common_left_target)=(L)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_left_targetsecondentry. ff_h_pfp_gcd_unique_H_gcd_common_left_targetsecondentry + S (pfrep_right_gcd_unique_H_gcd_common_left_target) = S ((S (pfrep_position_gcd_unique_H_gcd_common_left_targetsecond)) * ac)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_left_targetsecondentry. ab = ff_q_pfp_gcd_unique_H_gcd_common_left_targetsecondentry * S ((S (pfrep_position_gcd_unique_H_gcd_common_left_targetsecond)) * ac) + (pfrep_right_gcd_unique_H_gcd_common_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_common_left_targetsecondoutside. pfrep_gap_gcd_unique_H_gcd_common_left_targetsecondoutside+(L)=(pfrep_power_gcd_unique_H_gcd_common_left_target)) /\ (((pfrep_right_gcd_unique_H_gcd_common_left_target)=0))))) -> pfrep_left_gcd_unique_H_gcd_common_left_target=pfrep_right_gcd_unique_H_gcd_common_left_target))))))) /\ ((((forall fom_index_pfp_gcd_unique_H_gcd_common_right_canonical. (exists fom_gap_pfp_gcd_unique_H_gcd_common_right_canonical_index_bound. fom_gap_pfp_gcd_unique_H_gcd_common_right_canonical_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_common_right_canonical) = M) -> exists fom_value_pfp_gcd_unique_H_gcd_common_right_canonical. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_common_right_canonical_entry. fom_beta_height_pfp_gcd_unique_H_gcd_common_right_canonical_entry + S (fom_value_pfp_gcd_unique_H_gcd_common_right_canonical) = S ((S (fom_index_pfp_gcd_unique_H_gcd_common_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_common_right_canonical_entry. bb = fom_beta_quotient_pfp_gcd_unique_H_gcd_common_right_canonical_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_common_right_canonical)) * bc) + (fom_value_pfp_gcd_unique_H_gcd_common_right_canonical))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_common_right_canonical_value_bound. fom_gap_pfp_gcd_unique_H_gcd_common_right_canonical_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_common_right_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_H_gcd_common_right pfgu_qc_gcd_unique_H_gcd_common_right pfgu_Q_gcd_unique_H_gcd_common_right pfgu_pb_gcd_unique_H_gcd_common_right pfgu_pc_gcd_unique_H_gcd_common_right pfgu_P_gcd_unique_H_gcd_common_right. ((((forall fom_index_pfp_gcd_unique_H_gcd_common_right_productleft. (exists fom_gap_pfp_gcd_unique_H_gcd_common_right_productleft_index_bound. fom_gap_pfp_gcd_unique_H_gcd_common_right_productleft_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_common_right_productleft) = pfgu_Q_gcd_unique_H_gcd_common_right) -> exists fom_value_pfp_gcd_unique_H_gcd_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_common_right_productleft_entry. fom_beta_height_pfp_gcd_unique_H_gcd_common_right_productleft_entry + S (fom_value_pfp_gcd_unique_H_gcd_common_right_productleft) = S ((S (fom_index_pfp_gcd_unique_H_gcd_common_right_productleft)) * pfgu_qc_gcd_unique_H_gcd_common_right)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_common_right_productleft_entry. pfgu_qb_gcd_unique_H_gcd_common_right = fom_beta_quotient_pfp_gcd_unique_H_gcd_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_common_right_productleft)) * pfgu_qc_gcd_unique_H_gcd_common_right) + (fom_value_pfp_gcd_unique_H_gcd_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_common_right_productleft_value_bound. fom_gap_pfp_gcd_unique_H_gcd_common_right_productleft_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_H_gcd_common_right_productright. (exists fom_gap_pfp_gcd_unique_H_gcd_common_right_productright_index_bound. fom_gap_pfp_gcd_unique_H_gcd_common_right_productright_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_common_right_productright) = H) -> exists fom_value_pfp_gcd_unique_H_gcd_common_right_productright. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_common_right_productright_entry. fom_beta_height_pfp_gcd_unique_H_gcd_common_right_productright_entry + S (fom_value_pfp_gcd_unique_H_gcd_common_right_productright) = S ((S (fom_index_pfp_gcd_unique_H_gcd_common_right_productright)) * hc)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_common_right_productright_entry. hb = fom_beta_quotient_pfp_gcd_unique_H_gcd_common_right_productright_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_common_right_productright)) * hc) + (fom_value_pfp_gcd_unique_H_gcd_common_right_productright))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_common_right_productright_value_bound. fom_gap_pfp_gcd_unique_H_gcd_common_right_productright_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_common_right_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_H_gcd_common_right)=0 \/ (H)=0) /\ (((pfgu_P_gcd_unique_H_gcd_common_right)=0)))) \/ (((~((pfgu_Q_gcd_unique_H_gcd_common_right)=0)) /\ (((~((H)=0)) /\ (((pfgu_Q_gcd_unique_H_gcd_common_right)+(H)=S (pfgu_P_gcd_unique_H_gcd_common_right)))))))) /\ ((forall pfc_index_gcd_unique_H_gcd_common_right_productcoefficients. (exists pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientsbound. pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientsbound + S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficients) = (pfgu_P_gcd_unique_H_gcd_common_right)) -> exists pfc_value_gcd_unique_H_gcd_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientsentry. ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientsentry + S (pfc_value_gcd_unique_H_gcd_common_right_productcoefficients) = S ((S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_common_right)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientsentry. pfgu_pb_gcd_unique_H_gcd_common_right = ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_common_right) + (pfc_value_gcd_unique_H_gcd_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_H_gcd_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_unique_H_gcd_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_unique_H_gcd_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficients))) -> exists pfc_value_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_H_gcd_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_common_right_productcoefficientscoefficient) + (pfc_value_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_H_gcd_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_H_gcd_common_right)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_common_right)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_H_gcd_common_right = ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_common_right) + (pfc_left_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_H_gcd_common_right)=(pfc_index_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm) = (H)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm)) * hc)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry. hb = ff_q_pfp_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm)) * hc) + (pfc_right_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(H)=(pfc_complement_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_H_gcd_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_H_gcd_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_H_gcd_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_H_gcd_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_H_gcd_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_H_gcd_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_H_gcd_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_H_gcd_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_H_gcd_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_H_gcd_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_H_gcd_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_H_gcd_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_H_gcd_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_unique_H_gcd_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_H_gcd_common_right_target pfrep_left_gcd_unique_H_gcd_common_right_target pfrep_right_gcd_unique_H_gcd_common_right_target. ((exists pfrep_position_gcd_unique_H_gcd_common_right_targetfirst. ((pfrep_position_gcd_unique_H_gcd_common_right_targetfirst+S (pfrep_power_gcd_unique_H_gcd_common_right_target)=(pfgu_P_gcd_unique_H_gcd_common_right)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_right_targetfirstentry. ff_h_pfp_gcd_unique_H_gcd_common_right_targetfirstentry + S (pfrep_left_gcd_unique_H_gcd_common_right_target) = S ((S (pfrep_position_gcd_unique_H_gcd_common_right_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_common_right)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_right_targetfirstentry. pfgu_pb_gcd_unique_H_gcd_common_right = ff_q_pfp_gcd_unique_H_gcd_common_right_targetfirstentry * S ((S (pfrep_position_gcd_unique_H_gcd_common_right_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_common_right) + (pfrep_left_gcd_unique_H_gcd_common_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_common_right_targetfirstoutside. pfrep_gap_gcd_unique_H_gcd_common_right_targetfirstoutside+(pfgu_P_gcd_unique_H_gcd_common_right)=(pfrep_power_gcd_unique_H_gcd_common_right_target)) /\ (((pfrep_left_gcd_unique_H_gcd_common_right_target)=0))))) -> ((exists pfrep_position_gcd_unique_H_gcd_common_right_targetsecond. ((pfrep_position_gcd_unique_H_gcd_common_right_targetsecond+S (pfrep_power_gcd_unique_H_gcd_common_right_target)=(M)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_common_right_targetsecondentry. ff_h_pfp_gcd_unique_H_gcd_common_right_targetsecondentry + S (pfrep_right_gcd_unique_H_gcd_common_right_target) = S ((S (pfrep_position_gcd_unique_H_gcd_common_right_targetsecond)) * bc)) /\ exists ff_q_pfp_gcd_unique_H_gcd_common_right_targetsecondentry. bb = ff_q_pfp_gcd_unique_H_gcd_common_right_targetsecondentry * S ((S (pfrep_position_gcd_unique_H_gcd_common_right_targetsecond)) * bc) + (pfrep_right_gcd_unique_H_gcd_common_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_common_right_targetsecondoutside. pfrep_gap_gcd_unique_H_gcd_common_right_targetsecondoutside+(M)=(pfrep_power_gcd_unique_H_gcd_common_right_target)) /\ (((pfrep_right_gcd_unique_H_gcd_common_right_target)=0))))) -> pfrep_left_gcd_unique_H_gcd_common_right_target=pfrep_right_gcd_unique_H_gcd_common_right_target)))))))))) /\ ((forall pfgu_db_gcd_unique_H_gcd pfgu_dc_gcd_unique_H_gcd pfgu_D_gcd_unique_H_gcd. (((((forall fom_index_pfp_gcd_unique_H_gcd_divisor_left_canonical. (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_left_canonical_index_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_left_canonical_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_canonical) = L) -> exists fom_value_pfp_gcd_unique_H_gcd_divisor_left_canonical. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_divisor_left_canonical_entry. fom_beta_height_pfp_gcd_unique_H_gcd_divisor_left_canonical_entry + S (fom_value_pfp_gcd_unique_H_gcd_divisor_left_canonical) = S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_left_canonical_entry. ab = fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_left_canonical_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_canonical)) * ac) + (fom_value_pfp_gcd_unique_H_gcd_divisor_left_canonical))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_left_canonical_value_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_left_canonical_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_divisor_left_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_H_gcd_divisor_left pfgu_qc_gcd_unique_H_gcd_divisor_left pfgu_Q_gcd_unique_H_gcd_divisor_left pfgu_pb_gcd_unique_H_gcd_divisor_left pfgu_pc_gcd_unique_H_gcd_divisor_left pfgu_P_gcd_unique_H_gcd_divisor_left. ((((forall fom_index_pfp_gcd_unique_H_gcd_divisor_left_productleft. (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productleft_index_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productleft_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_productleft) = pfgu_Q_gcd_unique_H_gcd_divisor_left) -> exists fom_value_pfp_gcd_unique_H_gcd_divisor_left_productleft. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_divisor_left_productleft_entry. fom_beta_height_pfp_gcd_unique_H_gcd_divisor_left_productleft_entry + S (fom_value_pfp_gcd_unique_H_gcd_divisor_left_productleft) = S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_productleft)) * pfgu_qc_gcd_unique_H_gcd_divisor_left)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_left_productleft_entry. pfgu_qb_gcd_unique_H_gcd_divisor_left = fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_left_productleft_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_productleft)) * pfgu_qc_gcd_unique_H_gcd_divisor_left) + (fom_value_pfp_gcd_unique_H_gcd_divisor_left_productleft))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productleft_value_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productleft_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_divisor_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_H_gcd_divisor_left_productright. (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productright_index_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productright_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_productright) = pfgu_D_gcd_unique_H_gcd) -> exists fom_value_pfp_gcd_unique_H_gcd_divisor_left_productright. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_divisor_left_productright_entry. fom_beta_height_pfp_gcd_unique_H_gcd_divisor_left_productright_entry + S (fom_value_pfp_gcd_unique_H_gcd_divisor_left_productright) = S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_productright)) * pfgu_dc_gcd_unique_H_gcd)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_left_productright_entry. pfgu_db_gcd_unique_H_gcd = fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_left_productright_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_left_productright)) * pfgu_dc_gcd_unique_H_gcd) + (fom_value_pfp_gcd_unique_H_gcd_divisor_left_productright))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productright_value_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_left_productright_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_divisor_left_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_H_gcd_divisor_left)=0 \/ (pfgu_D_gcd_unique_H_gcd)=0) /\ (((pfgu_P_gcd_unique_H_gcd_divisor_left)=0)))) \/ (((~((pfgu_Q_gcd_unique_H_gcd_divisor_left)=0)) /\ (((~((pfgu_D_gcd_unique_H_gcd)=0)) /\ (((pfgu_Q_gcd_unique_H_gcd_divisor_left)+(pfgu_D_gcd_unique_H_gcd)=S (pfgu_P_gcd_unique_H_gcd_divisor_left)))))))) /\ ((forall pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients. (exists pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientsbound. pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientsbound + S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients) = (pfgu_P_gcd_unique_H_gcd_divisor_left)) -> exists pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficients. ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientsentry. ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientsentry + S (pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficients) = S ((S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_divisor_left)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientsentry. pfgu_pb_gcd_unique_H_gcd_divisor_left = ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientsentry * S ((S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_divisor_left) + (pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient pfc_terms_scale_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient pfc_natural_sum_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients))) -> exists pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient = ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient) + (pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_H_gcd_divisor_left)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_divisor_left)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_H_gcd_divisor_left = ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_divisor_left) + (pfc_left_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_H_gcd_divisor_left)=(pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = (pfgu_D_gcd_unique_H_gcd)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_H_gcd)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. pfgu_db_gcd_unique_H_gcd = ff_q_pfp_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_H_gcd) + (pfc_right_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgu_D_gcd_unique_H_gcd)=(pfc_complement_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_H_gcd_divisor_left_productcoefficients)) -> exists fs_a_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient = fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_H_gcd_divisor_left_productcoefficients) + (p) * pfa_offset_right_gcd_unique_H_gcd_divisor_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_H_gcd_divisor_left_target pfrep_left_gcd_unique_H_gcd_divisor_left_target pfrep_right_gcd_unique_H_gcd_divisor_left_target. ((exists pfrep_position_gcd_unique_H_gcd_divisor_left_targetfirst. ((pfrep_position_gcd_unique_H_gcd_divisor_left_targetfirst+S (pfrep_power_gcd_unique_H_gcd_divisor_left_target)=(pfgu_P_gcd_unique_H_gcd_divisor_left)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_left_targetfirstentry. ff_h_pfp_gcd_unique_H_gcd_divisor_left_targetfirstentry + S (pfrep_left_gcd_unique_H_gcd_divisor_left_target) = S ((S (pfrep_position_gcd_unique_H_gcd_divisor_left_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_divisor_left)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_left_targetfirstentry. pfgu_pb_gcd_unique_H_gcd_divisor_left = ff_q_pfp_gcd_unique_H_gcd_divisor_left_targetfirstentry * S ((S (pfrep_position_gcd_unique_H_gcd_divisor_left_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_divisor_left) + (pfrep_left_gcd_unique_H_gcd_divisor_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_divisor_left_targetfirstoutside. pfrep_gap_gcd_unique_H_gcd_divisor_left_targetfirstoutside+(pfgu_P_gcd_unique_H_gcd_divisor_left)=(pfrep_power_gcd_unique_H_gcd_divisor_left_target)) /\ (((pfrep_left_gcd_unique_H_gcd_divisor_left_target)=0))))) -> ((exists pfrep_position_gcd_unique_H_gcd_divisor_left_targetsecond. ((pfrep_position_gcd_unique_H_gcd_divisor_left_targetsecond+S (pfrep_power_gcd_unique_H_gcd_divisor_left_target)=(L)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_left_targetsecondentry. ff_h_pfp_gcd_unique_H_gcd_divisor_left_targetsecondentry + S (pfrep_right_gcd_unique_H_gcd_divisor_left_target) = S ((S (pfrep_position_gcd_unique_H_gcd_divisor_left_targetsecond)) * ac)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_left_targetsecondentry. ab = ff_q_pfp_gcd_unique_H_gcd_divisor_left_targetsecondentry * S ((S (pfrep_position_gcd_unique_H_gcd_divisor_left_targetsecond)) * ac) + (pfrep_right_gcd_unique_H_gcd_divisor_left_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_divisor_left_targetsecondoutside. pfrep_gap_gcd_unique_H_gcd_divisor_left_targetsecondoutside+(L)=(pfrep_power_gcd_unique_H_gcd_divisor_left_target)) /\ (((pfrep_right_gcd_unique_H_gcd_divisor_left_target)=0))))) -> pfrep_left_gcd_unique_H_gcd_divisor_left_target=pfrep_right_gcd_unique_H_gcd_divisor_left_target))))))) /\ ((((forall fom_index_pfp_gcd_unique_H_gcd_divisor_right_canonical. (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_right_canonical_index_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_right_canonical_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_canonical) = M) -> exists fom_value_pfp_gcd_unique_H_gcd_divisor_right_canonical. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_divisor_right_canonical_entry. fom_beta_height_pfp_gcd_unique_H_gcd_divisor_right_canonical_entry + S (fom_value_pfp_gcd_unique_H_gcd_divisor_right_canonical) = S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_canonical)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_right_canonical_entry. bb = fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_right_canonical_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_canonical)) * bc) + (fom_value_pfp_gcd_unique_H_gcd_divisor_right_canonical))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_right_canonical_value_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_right_canonical_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_divisor_right_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_H_gcd_divisor_right pfgu_qc_gcd_unique_H_gcd_divisor_right pfgu_Q_gcd_unique_H_gcd_divisor_right pfgu_pb_gcd_unique_H_gcd_divisor_right pfgu_pc_gcd_unique_H_gcd_divisor_right pfgu_P_gcd_unique_H_gcd_divisor_right. ((((forall fom_index_pfp_gcd_unique_H_gcd_divisor_right_productleft. (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productleft_index_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productleft_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_productleft) = pfgu_Q_gcd_unique_H_gcd_divisor_right) -> exists fom_value_pfp_gcd_unique_H_gcd_divisor_right_productleft. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_divisor_right_productleft_entry. fom_beta_height_pfp_gcd_unique_H_gcd_divisor_right_productleft_entry + S (fom_value_pfp_gcd_unique_H_gcd_divisor_right_productleft) = S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_productleft)) * pfgu_qc_gcd_unique_H_gcd_divisor_right)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_right_productleft_entry. pfgu_qb_gcd_unique_H_gcd_divisor_right = fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_right_productleft_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_productleft)) * pfgu_qc_gcd_unique_H_gcd_divisor_right) + (fom_value_pfp_gcd_unique_H_gcd_divisor_right_productleft))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productleft_value_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productleft_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_divisor_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_H_gcd_divisor_right_productright. (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productright_index_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productright_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_productright) = pfgu_D_gcd_unique_H_gcd) -> exists fom_value_pfp_gcd_unique_H_gcd_divisor_right_productright. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_divisor_right_productright_entry. fom_beta_height_pfp_gcd_unique_H_gcd_divisor_right_productright_entry + S (fom_value_pfp_gcd_unique_H_gcd_divisor_right_productright) = S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_productright)) * pfgu_dc_gcd_unique_H_gcd)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_right_productright_entry. pfgu_db_gcd_unique_H_gcd = fom_beta_quotient_pfp_gcd_unique_H_gcd_divisor_right_productright_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_divisor_right_productright)) * pfgu_dc_gcd_unique_H_gcd) + (fom_value_pfp_gcd_unique_H_gcd_divisor_right_productright))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productright_value_bound. fom_gap_pfp_gcd_unique_H_gcd_divisor_right_productright_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_divisor_right_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_H_gcd_divisor_right)=0 \/ (pfgu_D_gcd_unique_H_gcd)=0) /\ (((pfgu_P_gcd_unique_H_gcd_divisor_right)=0)))) \/ (((~((pfgu_Q_gcd_unique_H_gcd_divisor_right)=0)) /\ (((~((pfgu_D_gcd_unique_H_gcd)=0)) /\ (((pfgu_Q_gcd_unique_H_gcd_divisor_right)+(pfgu_D_gcd_unique_H_gcd)=S (pfgu_P_gcd_unique_H_gcd_divisor_right)))))))) /\ ((forall pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients. (exists pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientsbound. pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientsbound + S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients) = (pfgu_P_gcd_unique_H_gcd_divisor_right)) -> exists pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficients. ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientsentry. ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientsentry + S (pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficients) = S ((S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_divisor_right)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientsentry. pfgu_pb_gcd_unique_H_gcd_divisor_right = ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientsentry * S ((S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_divisor_right) + (pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient pfc_terms_scale_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient pfc_natural_sum_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients))) -> exists pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient = ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient) + (pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_H_gcd_divisor_right)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_divisor_right)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_H_gcd_divisor_right = ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_divisor_right) + (pfc_left_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_H_gcd_divisor_right)=(pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = (pfgu_D_gcd_unique_H_gcd)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_H_gcd)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. pfgu_db_gcd_unique_H_gcd = ff_q_pfp_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_H_gcd) + (pfc_right_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgu_D_gcd_unique_H_gcd)=(pfc_complement_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_H_gcd_divisor_right_productcoefficients)) -> exists fs_a_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient = fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_H_gcd_divisor_right_productcoefficients) + (p) * pfa_offset_right_gcd_unique_H_gcd_divisor_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_H_gcd_divisor_right_target pfrep_left_gcd_unique_H_gcd_divisor_right_target pfrep_right_gcd_unique_H_gcd_divisor_right_target. ((exists pfrep_position_gcd_unique_H_gcd_divisor_right_targetfirst. ((pfrep_position_gcd_unique_H_gcd_divisor_right_targetfirst+S (pfrep_power_gcd_unique_H_gcd_divisor_right_target)=(pfgu_P_gcd_unique_H_gcd_divisor_right)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_right_targetfirstentry. ff_h_pfp_gcd_unique_H_gcd_divisor_right_targetfirstentry + S (pfrep_left_gcd_unique_H_gcd_divisor_right_target) = S ((S (pfrep_position_gcd_unique_H_gcd_divisor_right_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_divisor_right)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_right_targetfirstentry. pfgu_pb_gcd_unique_H_gcd_divisor_right = ff_q_pfp_gcd_unique_H_gcd_divisor_right_targetfirstentry * S ((S (pfrep_position_gcd_unique_H_gcd_divisor_right_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_divisor_right) + (pfrep_left_gcd_unique_H_gcd_divisor_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_divisor_right_targetfirstoutside. pfrep_gap_gcd_unique_H_gcd_divisor_right_targetfirstoutside+(pfgu_P_gcd_unique_H_gcd_divisor_right)=(pfrep_power_gcd_unique_H_gcd_divisor_right_target)) /\ (((pfrep_left_gcd_unique_H_gcd_divisor_right_target)=0))))) -> ((exists pfrep_position_gcd_unique_H_gcd_divisor_right_targetsecond. ((pfrep_position_gcd_unique_H_gcd_divisor_right_targetsecond+S (pfrep_power_gcd_unique_H_gcd_divisor_right_target)=(M)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_divisor_right_targetsecondentry. ff_h_pfp_gcd_unique_H_gcd_divisor_right_targetsecondentry + S (pfrep_right_gcd_unique_H_gcd_divisor_right_target) = S ((S (pfrep_position_gcd_unique_H_gcd_divisor_right_targetsecond)) * bc)) /\ exists ff_q_pfp_gcd_unique_H_gcd_divisor_right_targetsecondentry. bb = ff_q_pfp_gcd_unique_H_gcd_divisor_right_targetsecondentry * S ((S (pfrep_position_gcd_unique_H_gcd_divisor_right_targetsecond)) * bc) + (pfrep_right_gcd_unique_H_gcd_divisor_right_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_divisor_right_targetsecondoutside. pfrep_gap_gcd_unique_H_gcd_divisor_right_targetsecondoutside+(M)=(pfrep_power_gcd_unique_H_gcd_divisor_right_target)) /\ (((pfrep_right_gcd_unique_H_gcd_divisor_right_target)=0))))) -> pfrep_left_gcd_unique_H_gcd_divisor_right_target=pfrep_right_gcd_unique_H_gcd_divisor_right_target)))))))))) -> (((forall fom_index_pfp_gcd_unique_H_gcd_greatest_canonical. (exists fom_gap_pfp_gcd_unique_H_gcd_greatest_canonical_index_bound. fom_gap_pfp_gcd_unique_H_gcd_greatest_canonical_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_greatest_canonical) = H) -> exists fom_value_pfp_gcd_unique_H_gcd_greatest_canonical. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_greatest_canonical_entry. fom_beta_height_pfp_gcd_unique_H_gcd_greatest_canonical_entry + S (fom_value_pfp_gcd_unique_H_gcd_greatest_canonical) = S ((S (fom_index_pfp_gcd_unique_H_gcd_greatest_canonical)) * hc)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_greatest_canonical_entry. hb = fom_beta_quotient_pfp_gcd_unique_H_gcd_greatest_canonical_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_greatest_canonical)) * hc) + (fom_value_pfp_gcd_unique_H_gcd_greatest_canonical))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_greatest_canonical_value_bound. fom_gap_pfp_gcd_unique_H_gcd_greatest_canonical_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_greatest_canonical) = p))) /\ ((exists pfgu_qb_gcd_unique_H_gcd_greatest pfgu_qc_gcd_unique_H_gcd_greatest pfgu_Q_gcd_unique_H_gcd_greatest pfgu_pb_gcd_unique_H_gcd_greatest pfgu_pc_gcd_unique_H_gcd_greatest pfgu_P_gcd_unique_H_gcd_greatest. ((((forall fom_index_pfp_gcd_unique_H_gcd_greatest_productleft. (exists fom_gap_pfp_gcd_unique_H_gcd_greatest_productleft_index_bound. fom_gap_pfp_gcd_unique_H_gcd_greatest_productleft_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_greatest_productleft) = pfgu_Q_gcd_unique_H_gcd_greatest) -> exists fom_value_pfp_gcd_unique_H_gcd_greatest_productleft. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_greatest_productleft_entry. fom_beta_height_pfp_gcd_unique_H_gcd_greatest_productleft_entry + S (fom_value_pfp_gcd_unique_H_gcd_greatest_productleft) = S ((S (fom_index_pfp_gcd_unique_H_gcd_greatest_productleft)) * pfgu_qc_gcd_unique_H_gcd_greatest)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_greatest_productleft_entry. pfgu_qb_gcd_unique_H_gcd_greatest = fom_beta_quotient_pfp_gcd_unique_H_gcd_greatest_productleft_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_greatest_productleft)) * pfgu_qc_gcd_unique_H_gcd_greatest) + (fom_value_pfp_gcd_unique_H_gcd_greatest_productleft))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_greatest_productleft_value_bound. fom_gap_pfp_gcd_unique_H_gcd_greatest_productleft_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_greatest_productleft) = p))) /\ (((forall fom_index_pfp_gcd_unique_H_gcd_greatest_productright. (exists fom_gap_pfp_gcd_unique_H_gcd_greatest_productright_index_bound. fom_gap_pfp_gcd_unique_H_gcd_greatest_productright_index_bound + S (fom_index_pfp_gcd_unique_H_gcd_greatest_productright) = pfgu_D_gcd_unique_H_gcd) -> exists fom_value_pfp_gcd_unique_H_gcd_greatest_productright. ((((exists fom_beta_height_pfp_gcd_unique_H_gcd_greatest_productright_entry. fom_beta_height_pfp_gcd_unique_H_gcd_greatest_productright_entry + S (fom_value_pfp_gcd_unique_H_gcd_greatest_productright) = S ((S (fom_index_pfp_gcd_unique_H_gcd_greatest_productright)) * pfgu_dc_gcd_unique_H_gcd)) /\ exists fom_beta_quotient_pfp_gcd_unique_H_gcd_greatest_productright_entry. pfgu_db_gcd_unique_H_gcd = fom_beta_quotient_pfp_gcd_unique_H_gcd_greatest_productright_entry * S ((S (fom_index_pfp_gcd_unique_H_gcd_greatest_productright)) * pfgu_dc_gcd_unique_H_gcd) + (fom_value_pfp_gcd_unique_H_gcd_greatest_productright))) /\ (exists fom_gap_pfp_gcd_unique_H_gcd_greatest_productright_value_bound. fom_gap_pfp_gcd_unique_H_gcd_greatest_productright_value_bound + S (fom_value_pfp_gcd_unique_H_gcd_greatest_productright) = p))) /\ (((((((pfgu_Q_gcd_unique_H_gcd_greatest)=0 \/ (pfgu_D_gcd_unique_H_gcd)=0) /\ (((pfgu_P_gcd_unique_H_gcd_greatest)=0)))) \/ (((~((pfgu_Q_gcd_unique_H_gcd_greatest)=0)) /\ (((~((pfgu_D_gcd_unique_H_gcd)=0)) /\ (((pfgu_Q_gcd_unique_H_gcd_greatest)+(pfgu_D_gcd_unique_H_gcd)=S (pfgu_P_gcd_unique_H_gcd_greatest)))))))) /\ ((forall pfc_index_gcd_unique_H_gcd_greatest_productcoefficients. (exists pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientsbound. pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientsbound + S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficients) = (pfgu_P_gcd_unique_H_gcd_greatest)) -> exists pfc_value_gcd_unique_H_gcd_greatest_productcoefficients. ((((exists ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientsentry. ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientsentry + S (pfc_value_gcd_unique_H_gcd_greatest_productcoefficients) = S ((S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_greatest)) /\ exists ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientsentry. pfgu_pb_gcd_unique_H_gcd_greatest = ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientsentry * S ((S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficients)) * pfgu_pc_gcd_unique_H_gcd_greatest) + (pfc_value_gcd_unique_H_gcd_greatest_productcoefficients))) /\ ((exists pfc_terms_code_gcd_unique_H_gcd_greatest_productcoefficientscoefficient pfc_terms_scale_gcd_unique_H_gcd_greatest_productcoefficientscoefficient pfc_natural_sum_gcd_unique_H_gcd_greatest_productcoefficientscoefficient. ((forall pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficients))) -> exists pfc_value_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_greatest_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_unique_H_gcd_greatest_productcoefficientscoefficient = ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_unique_H_gcd_greatest_productcoefficientscoefficient) + (pfc_value_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm pfc_left_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm pfc_right_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_unique_H_gcd_greatest_productcoefficients)) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal) = (pfgu_Q_gcd_unique_H_gcd_greatest)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_greatest)) /\ exists ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_gcd_unique_H_gcd_greatest = ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfgu_qc_gcd_unique_H_gcd_greatest) + (pfc_left_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_gcd_unique_H_gcd_greatest)=(pfc_index_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm) = (pfgu_D_gcd_unique_H_gcd)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_H_gcd)) /\ exists ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry. pfgu_db_gcd_unique_H_gcd = ff_q_pfp_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm)) * pfgu_dc_gcd_unique_H_gcd) + (pfc_right_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonaltermrightoutside+(pfgu_D_gcd_unique_H_gcd)=(pfc_complement_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonal)=pfc_left_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_unique_H_gcd_greatest_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_unique_H_gcd_greatest_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficients))) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_unique_H_gcd_greatest_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_unique_H_gcd_greatest_productcoefficients)) -> exists fs_a_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_greatest_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_unique_H_gcd_greatest_productcoefficientscoefficient = fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_unique_H_gcd_greatest_productcoefficientscoefficient) + (fs_a_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_unique_H_gcd_greatest_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientresiduebound. pfa_gap_gcd_unique_H_gcd_greatest_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_unique_H_gcd_greatest_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_unique_H_gcd_greatest_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_unique_H_gcd_greatest_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_unique_H_gcd_greatest_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_unique_H_gcd_greatest_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_unique_H_gcd_greatest_productcoefficients) + (p) * pfa_offset_right_gcd_unique_H_gcd_greatest_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_unique_H_gcd_greatest_target pfrep_left_gcd_unique_H_gcd_greatest_target pfrep_right_gcd_unique_H_gcd_greatest_target. ((exists pfrep_position_gcd_unique_H_gcd_greatest_targetfirst. ((pfrep_position_gcd_unique_H_gcd_greatest_targetfirst+S (pfrep_power_gcd_unique_H_gcd_greatest_target)=(pfgu_P_gcd_unique_H_gcd_greatest)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_greatest_targetfirstentry. ff_h_pfp_gcd_unique_H_gcd_greatest_targetfirstentry + S (pfrep_left_gcd_unique_H_gcd_greatest_target) = S ((S (pfrep_position_gcd_unique_H_gcd_greatest_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_greatest)) /\ exists ff_q_pfp_gcd_unique_H_gcd_greatest_targetfirstentry. pfgu_pb_gcd_unique_H_gcd_greatest = ff_q_pfp_gcd_unique_H_gcd_greatest_targetfirstentry * S ((S (pfrep_position_gcd_unique_H_gcd_greatest_targetfirst)) * pfgu_pc_gcd_unique_H_gcd_greatest) + (pfrep_left_gcd_unique_H_gcd_greatest_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_greatest_targetfirstoutside. pfrep_gap_gcd_unique_H_gcd_greatest_targetfirstoutside+(pfgu_P_gcd_unique_H_gcd_greatest)=(pfrep_power_gcd_unique_H_gcd_greatest_target)) /\ (((pfrep_left_gcd_unique_H_gcd_greatest_target)=0))))) -> ((exists pfrep_position_gcd_unique_H_gcd_greatest_targetsecond. ((pfrep_position_gcd_unique_H_gcd_greatest_targetsecond+S (pfrep_power_gcd_unique_H_gcd_greatest_target)=(H)) /\ ((((exists ff_h_pfp_gcd_unique_H_gcd_greatest_targetsecondentry. ff_h_pfp_gcd_unique_H_gcd_greatest_targetsecondentry + S (pfrep_right_gcd_unique_H_gcd_greatest_target) = S ((S (pfrep_position_gcd_unique_H_gcd_greatest_targetsecond)) * hc)) /\ exists ff_q_pfp_gcd_unique_H_gcd_greatest_targetsecondentry. hb = ff_q_pfp_gcd_unique_H_gcd_greatest_targetsecondentry * S ((S (pfrep_position_gcd_unique_H_gcd_greatest_targetsecond)) * hc) + (pfrep_right_gcd_unique_H_gcd_greatest_target)))))) \/ (((exists pfrep_gap_gcd_unique_H_gcd_greatest_targetsecondoutside. pfrep_gap_gcd_unique_H_gcd_greatest_targetsecondoutside+(H)=(pfrep_power_gcd_unique_H_gcd_greatest_target)) /\ (((pfrep_right_gcd_unique_H_gcd_greatest_target)=0))))) -> pfrep_left_gcd_unique_H_gcd_greatest_target=pfrep_right_gcd_unique_H_gcd_greatest_target)))))))))))))) -> (forall pfrep_power_gcd_unique_result pfrep_left_gcd_unique_result pfrep_right_gcd_unique_result. ((exists pfrep_position_gcd_unique_resultfirst. ((pfrep_position_gcd_unique_resultfirst+S (pfrep_power_gcd_unique_result)=(G)) /\ ((((exists ff_h_pfp_gcd_unique_resultfirstentry. ff_h_pfp_gcd_unique_resultfirstentry + S (pfrep_left_gcd_unique_result) = S ((S (pfrep_position_gcd_unique_resultfirst)) * gc)) /\ exists ff_q_pfp_gcd_unique_resultfirstentry. gb = ff_q_pfp_gcd_unique_resultfirstentry * S ((S (pfrep_position_gcd_unique_resultfirst)) * gc) + (pfrep_left_gcd_unique_result)))))) \/ (((exists pfrep_gap_gcd_unique_resultfirstoutside. pfrep_gap_gcd_unique_resultfirstoutside+(G)=(pfrep_power_gcd_unique_result)) /\ (((pfrep_left_gcd_unique_result)=0))))) -> ((exists pfrep_position_gcd_unique_resultsecond. ((pfrep_position_gcd_unique_resultsecond+S (pfrep_power_gcd_unique_result)=(H)) /\ ((((exists ff_h_pfp_gcd_unique_resultsecondentry. ff_h_pfp_gcd_unique_resultsecondentry + S (pfrep_right_gcd_unique_result) = S ((S (pfrep_position_gcd_unique_resultsecond)) * hc)) /\ exists ff_q_pfp_gcd_unique_resultsecondentry. hb = ff_q_pfp_gcd_unique_resultsecondentry * S ((S (pfrep_position_gcd_unique_resultsecond)) * hc) + (pfrep_right_gcd_unique_result)))))) \/ (((exists pfrep_gap_gcd_unique_resultsecondoutside. pfrep_gap_gcd_unique_resultsecondoutside+(H)=(pfrep_power_gcd_unique_result)) /\ (((pfrep_right_gcd_unique_result)=0))))) -> pfrep_left_gcd_unique_result=pfrep_right_gcd_unique_result)