Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
Exact theorem in conservative defined notation
∀ p. ∀ gb. ∀ gc. ∀ G. ∀ hb. ∀ hc. ∀ H. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. Prime(p) → FpPolynomialNormalizedGcd(p,gb,gc,G,ab,ac,L,bb,bc,M) → FpPolynomialNormalizedGcd(p,hb,hc,H,ab,ac,L,bb,bc,M) → PolynomialEquivalent(gb,gc,G,hb,hc,H)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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)Complete tactic proof in conservative notation
All 41 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
41 script commands · 6 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–16
03Separate the logical casesL17–20
04Use earlier factsL21–30
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
specialize prime_field_polynomial_normal_right_associates_equivalent (p) - L22
specialize prime_field_polynomial_normal_right_associates_equivalent (gb) - L23
specialize prime_field_polynomial_normal_right_associates_equivalent (gc) - L24
specialize prime_field_polynomial_normal_right_associates_equivalent (G) - L25
specialize prime_field_polynomial_normal_right_associates_equivalent (hb) - L26
specialize prime_field_polynomial_normal_right_associates_equivalent (hc) - L27
specialize prime_field_polynomial_normal_right_associates_equivalent (H) - L28
apply prime_field_polynomial_normal_right_associates_equivalent - L29
exact hp - L30
exact hg_left
05Use earlier factsL31–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
06Use earlier factsL41–41
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
exact hh_right_left
Original defined command ledger · 41 lines
- 0001
intro p - 0002
intro gb - 0003
intro gc - 0004
intro G - 0005
intro hb - 0006
intro hc - 0007
intro H - 0008
intro ab - 0009
intro ac - 0010
intro L - 0011
intro bb - 0012
intro bc - 0013
intro M - 0014
intro hp - 0015
intro hg - 0016
intro hh - 0017
cases hg - 0018
cases hg_right - 0019
cases hh - 0020
cases hh_right - 0021
specialize prime_field_polynomial_normal_right_associates_equivalent (p) - 0022
specialize prime_field_polynomial_normal_right_associates_equivalent (gb) - 0023
specialize prime_field_polynomial_normal_right_associates_equivalent (gc) - 0024
specialize prime_field_polynomial_normal_right_associates_equivalent (G) - 0025
specialize prime_field_polynomial_normal_right_associates_equivalent (hb) - 0026
specialize prime_field_polynomial_normal_right_associates_equivalent (hc) - 0027
specialize prime_field_polynomial_normal_right_associates_equivalent (H) - 0028
apply prime_field_polynomial_normal_right_associates_equivalent - 0029
exact hp - 0030
exact hg_left - 0031
exact hh_left - 0032
specialize hh_right_right (gb) - 0033
specialize hh_right_right (gc) - 0034
specialize hh_right_right (G) - 0035
apply hh_right_right - 0036
exact hg_right_left - 0037
specialize hg_right_right (hb) - 0038
specialize hg_right_right (hc) - 0039
specialize hg_right_right (H) - 0040
apply hg_right_right - 0041
exact hh_right_left