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. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. Prime(p) → BetaPrefixInto(ab,ac,L,p) → BetaPrefixInto(bb,bc,M,p) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. FpPolynomialNormalizedGcd(p,x,y,z,ab,ac,L,bb,bc,M) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,M,x,y,z,n,m,k,i,j,u)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall p ab ac L bb bc M. (~((p) = 1) /\ forall pfa_factor_left_normalized_exists_prime pfa_factor_right_normalized_exists_prime. (p) = pfa_factor_left_normalized_exists_prime * pfa_factor_right_normalized_exists_prime -> pfa_factor_left_normalized_exists_prime = 1 \/ pfa_factor_right_normalized_exists_prime = 1) -> (forall fom_index_pfp_normalized_exists_A. (exists fom_gap_pfp_normalized_exists_A_index_bound. fom_gap_pfp_normalized_exists_A_index_bound + S (fom_index_pfp_normalized_exists_A) = L) -> exists fom_value_pfp_normalized_exists_A. ((((exists fom_beta_height_pfp_normalized_exists_A_entry. fom_beta_height_pfp_normalized_exists_A_entry + S (fom_value_pfp_normalized_exists_A) = S ((S (fom_index_pfp_normalized_exists_A)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_exists_A_entry. ab = fom_beta_quotient_pfp_normalized_exists_A_entry * S ((S (fom_index_pfp_normalized_exists_A)) * ac) + (fom_value_pfp_normalized_exists_A))) /\ (exists fom_gap_pfp_normalized_exists_A_value_bound. fom_gap_pfp_normalized_exists_A_value_bound + S (fom_value_pfp_normalized_exists_A) = p))) -> (forall fom_index_pfp_normalized_exists_B. (exists fom_gap_pfp_normalized_exists_B_index_bound. fom_gap_pfp_normalized_exists_B_index_bound + S (fom_index_pfp_normalized_exists_B) = M) -> exists fom_value_pfp_normalized_exists_B. ((((exists fom_beta_height_pfp_normalized_exists_B_entry. fom_beta_height_pfp_normalized_exists_B_entry + S (fom_value_pfp_normalized_exists_B) = S ((S (fom_index_pfp_normalized_exists_B)) * bc)) /\ exists fom_beta_quotient_pfp_normalized_exists_B_entry. bb = fom_beta_quotient_pfp_normalized_exists_B_entry * S ((S (fom_index_pfp_normalized_exists_B)) * bc) + (fom_value_pfp_normalized_exists_B))) /\ (exists fom_gap_pfp_normalized_exists_B_value_bound. fom_gap_pfp_normalized_exists_B_value_bound + S (fom_value_pfp_normalized_exists_B) = p))) -> (exists gb gc G ub uc U vb vc V. (((((G)=0 \/ (((~((G) = 0)) /\ (((forall fom_index_pfp_normalized_exists_gcd_normal_moniccoefficients. (exists fom_gap_pfp_normalized_exists_gcd_normal_moniccoefficients_index_bound. fom_gap_pfp_normalized_exists_gcd_normal_moniccoefficients_index_bound + S (fom_index_pfp_normalized_exists_gcd_normal_moniccoefficients) = G) -> exists fom_value_pfp_normalized_exists_gcd_normal_moniccoefficients. ((((exists fom_beta_height_pfp_normalized_exists_gcd_normal_moniccoefficients_entry. fom_beta_height_pfp_normalized_exists_gcd_normal_moniccoefficients_entry + S (fom_value_pfp_normalized_exists_gcd_normal_moniccoefficients) = S ((S (fom_index_pfp_normalized_exists_gcd_normal_moniccoefficients)) * gc)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_normal_moniccoefficients_entry. gb = fom_beta_quotient_pfp_normalized_exists_gcd_normal_moniccoefficients_entry * S ((S (fom_index_pfp_normalized_exists_gcd_normal_moniccoefficients)) * gc) + (fom_value_pfp_normalized_exists_gcd_normal_moniccoefficients))) /\ (exists fom_gap_pfp_normalized_exists_gcd_normal_moniccoefficients_value_bound. fom_gap_pfp_normalized_exists_gcd_normal_moniccoefficients_value_bound + S (fom_value_pfp_normalized_exists_gcd_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normalized_exists_gcd_normal_monicleading. ff_h_pfp_normalized_exists_gcd_normal_monicleading + S (1) = S ((S (0)) * gc)) /\ exists ff_q_pfp_normalized_exists_gcd_normal_monicleading. gb = ff_q_pfp_normalized_exists_gcd_normal_monicleading * S ((S (0)) * gc) + (1))))))))) /\ ((((((((forall fom_index_pfp_normalized_exists_gcd_gcd_common_left_bounded. (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_left_bounded_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_left_bounded_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_bounded) = L) -> exists fom_value_pfp_normalized_exists_gcd_gcd_common_left_bounded. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_common_left_bounded_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_common_left_bounded_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_common_left_bounded) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_left_bounded_entry. ab = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_left_bounded_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_bounded)) * ac) + (fom_value_pfp_normalized_exists_gcd_gcd_common_left_bounded))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_left_bounded_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_left_bounded_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_common_left_bounded) = p))) /\ ((exists pfgd_qb_normalized_exists_gcd_gcd_common_left pfgd_qc_normalized_exists_gcd_gcd_common_left pfgd_Q_normalized_exists_gcd_gcd_common_left pfgd_pb_normalized_exists_gcd_gcd_common_left pfgd_pc_normalized_exists_gcd_gcd_common_left pfgd_P_normalized_exists_gcd_gcd_common_left. ((((forall fom_index_pfp_normalized_exists_gcd_gcd_common_left_productleft. (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productleft_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productleft_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_productleft) = pfgd_Q_normalized_exists_gcd_gcd_common_left) -> exists fom_value_pfp_normalized_exists_gcd_gcd_common_left_productleft. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_common_left_productleft_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_common_left_productleft_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_common_left_productleft) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_common_left)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_left_productleft_entry. pfgd_qb_normalized_exists_gcd_gcd_common_left = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_left_productleft_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_common_left) + (fom_value_pfp_normalized_exists_gcd_gcd_common_left_productleft))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productleft_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productleft_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_common_left_productleft) = p))) /\ (((forall fom_index_pfp_normalized_exists_gcd_gcd_common_left_productright. (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productright_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productright_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_productright) = G) -> exists fom_value_pfp_normalized_exists_gcd_gcd_common_left_productright. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_common_left_productright_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_common_left_productright_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_common_left_productright) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_productright)) * gc)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_left_productright_entry. gb = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_left_productright_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_left_productright)) * gc) + (fom_value_pfp_normalized_exists_gcd_gcd_common_left_productright))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productright_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_left_productright_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_common_left_productright) = p))) /\ (((((((pfgd_Q_normalized_exists_gcd_gcd_common_left)=0 \/ (G)=0) /\ (((pfgd_P_normalized_exists_gcd_gcd_common_left)=0)))) \/ (((~((pfgd_Q_normalized_exists_gcd_gcd_common_left)=0)) /\ (((~((G)=0)) /\ (((pfgd_Q_normalized_exists_gcd_gcd_common_left)+(G)=S (pfgd_P_normalized_exists_gcd_gcd_common_left)))))))) /\ ((forall pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients. (exists pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientsbound. pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientsbound + S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients) = (pfgd_P_normalized_exists_gcd_gcd_common_left)) -> exists pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficients. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientsentry. ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientsentry + S (pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficients) = S ((S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_common_left)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientsentry. pfgd_pb_normalized_exists_gcd_gcd_common_left = ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientsentry * S ((S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_common_left) + (pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficients))) /\ ((exists pfc_terms_code_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient pfc_terms_scale_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient pfc_natural_sum_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient. ((forall pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients))) -> exists pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient = ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient) + (pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm pfc_left_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm pfc_right_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients)) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_normalized_exists_gcd_gcd_common_left)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_common_left)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_normalized_exists_gcd_gcd_common_left = ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_common_left) + (pfc_left_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_normalized_exists_gcd_gcd_common_left)=(pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonal)=pfc_left_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_exists_gcd_gcd_common_left_productcoefficients)) -> exists fs_a_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient = fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient) + (fs_a_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientresiduebound. pfa_gap_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_exists_gcd_gcd_common_left_productcoefficients) + (p) * pfa_offset_right_normalized_exists_gcd_gcd_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_exists_gcd_gcd_common_left_equivalent pfrep_left_normalized_exists_gcd_gcd_common_left_equivalent pfrep_right_normalized_exists_gcd_gcd_common_left_equivalent. ((exists pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentfirst. ((pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentfirst+S (pfrep_power_normalized_exists_gcd_gcd_common_left_equivalent)=(pfgd_P_normalized_exists_gcd_gcd_common_left)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_left_equivalentfirstentry. ff_h_pfp_normalized_exists_gcd_gcd_common_left_equivalentfirstentry + S (pfrep_left_normalized_exists_gcd_gcd_common_left_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_common_left)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_left_equivalentfirstentry. pfgd_pb_normalized_exists_gcd_gcd_common_left = ff_q_pfp_normalized_exists_gcd_gcd_common_left_equivalentfirstentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_common_left) + (pfrep_left_normalized_exists_gcd_gcd_common_left_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_common_left_equivalentfirstoutside. pfrep_gap_normalized_exists_gcd_gcd_common_left_equivalentfirstoutside+(pfgd_P_normalized_exists_gcd_gcd_common_left)=(pfrep_power_normalized_exists_gcd_gcd_common_left_equivalent)) /\ (((pfrep_left_normalized_exists_gcd_gcd_common_left_equivalent)=0))))) -> ((exists pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentsecond. ((pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentsecond+S (pfrep_power_normalized_exists_gcd_gcd_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_left_equivalentsecondentry. ff_h_pfp_normalized_exists_gcd_gcd_common_left_equivalentsecondentry + S (pfrep_right_normalized_exists_gcd_gcd_common_left_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_left_equivalentsecondentry. ab = ff_q_pfp_normalized_exists_gcd_gcd_common_left_equivalentsecondentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_common_left_equivalentsecond)) * ac) + (pfrep_right_normalized_exists_gcd_gcd_common_left_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_common_left_equivalentsecondoutside. pfrep_gap_normalized_exists_gcd_gcd_common_left_equivalentsecondoutside+(L)=(pfrep_power_normalized_exists_gcd_gcd_common_left_equivalent)) /\ (((pfrep_right_normalized_exists_gcd_gcd_common_left_equivalent)=0))))) -> pfrep_left_normalized_exists_gcd_gcd_common_left_equivalent=pfrep_right_normalized_exists_gcd_gcd_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_normalized_exists_gcd_gcd_common_right_bounded. (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_right_bounded_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_right_bounded_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_bounded) = M) -> exists fom_value_pfp_normalized_exists_gcd_gcd_common_right_bounded. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_common_right_bounded_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_common_right_bounded_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_common_right_bounded) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_right_bounded_entry. bb = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_right_bounded_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_bounded)) * bc) + (fom_value_pfp_normalized_exists_gcd_gcd_common_right_bounded))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_right_bounded_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_right_bounded_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_common_right_bounded) = p))) /\ ((exists pfgd_qb_normalized_exists_gcd_gcd_common_right pfgd_qc_normalized_exists_gcd_gcd_common_right pfgd_Q_normalized_exists_gcd_gcd_common_right pfgd_pb_normalized_exists_gcd_gcd_common_right pfgd_pc_normalized_exists_gcd_gcd_common_right pfgd_P_normalized_exists_gcd_gcd_common_right. ((((forall fom_index_pfp_normalized_exists_gcd_gcd_common_right_productleft. (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productleft_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productleft_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_productleft) = pfgd_Q_normalized_exists_gcd_gcd_common_right) -> exists fom_value_pfp_normalized_exists_gcd_gcd_common_right_productleft. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_common_right_productleft_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_common_right_productleft_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_common_right_productleft) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_common_right)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_right_productleft_entry. pfgd_qb_normalized_exists_gcd_gcd_common_right = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_right_productleft_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_common_right) + (fom_value_pfp_normalized_exists_gcd_gcd_common_right_productleft))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productleft_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productleft_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_common_right_productleft) = p))) /\ (((forall fom_index_pfp_normalized_exists_gcd_gcd_common_right_productright. (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productright_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productright_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_productright) = G) -> exists fom_value_pfp_normalized_exists_gcd_gcd_common_right_productright. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_common_right_productright_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_common_right_productright_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_common_right_productright) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_productright)) * gc)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_right_productright_entry. gb = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_common_right_productright_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_common_right_productright)) * gc) + (fom_value_pfp_normalized_exists_gcd_gcd_common_right_productright))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productright_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_common_right_productright_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_common_right_productright) = p))) /\ (((((((pfgd_Q_normalized_exists_gcd_gcd_common_right)=0 \/ (G)=0) /\ (((pfgd_P_normalized_exists_gcd_gcd_common_right)=0)))) \/ (((~((pfgd_Q_normalized_exists_gcd_gcd_common_right)=0)) /\ (((~((G)=0)) /\ (((pfgd_Q_normalized_exists_gcd_gcd_common_right)+(G)=S (pfgd_P_normalized_exists_gcd_gcd_common_right)))))))) /\ ((forall pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients. (exists pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientsbound. pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientsbound + S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients) = (pfgd_P_normalized_exists_gcd_gcd_common_right)) -> exists pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficients. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientsentry. ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientsentry + S (pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficients) = S ((S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_common_right)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientsentry. pfgd_pb_normalized_exists_gcd_gcd_common_right = ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientsentry * S ((S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_common_right) + (pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficients))) /\ ((exists pfc_terms_code_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient pfc_terms_scale_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient pfc_natural_sum_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient. ((forall pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients))) -> exists pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient = ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient) + (pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm pfc_left_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm pfc_right_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients)) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_normalized_exists_gcd_gcd_common_right)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_common_right)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_normalized_exists_gcd_gcd_common_right = ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_common_right) + (pfc_left_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_normalized_exists_gcd_gcd_common_right)=(pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonal)=pfc_left_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_exists_gcd_gcd_common_right_productcoefficients)) -> exists fs_a_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient = fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient) + (fs_a_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientresiduebound. pfa_gap_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_exists_gcd_gcd_common_right_productcoefficients) + (p) * pfa_offset_right_normalized_exists_gcd_gcd_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_exists_gcd_gcd_common_right_equivalent pfrep_left_normalized_exists_gcd_gcd_common_right_equivalent pfrep_right_normalized_exists_gcd_gcd_common_right_equivalent. ((exists pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentfirst. ((pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentfirst+S (pfrep_power_normalized_exists_gcd_gcd_common_right_equivalent)=(pfgd_P_normalized_exists_gcd_gcd_common_right)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_right_equivalentfirstentry. ff_h_pfp_normalized_exists_gcd_gcd_common_right_equivalentfirstentry + S (pfrep_left_normalized_exists_gcd_gcd_common_right_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_common_right)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_right_equivalentfirstentry. pfgd_pb_normalized_exists_gcd_gcd_common_right = ff_q_pfp_normalized_exists_gcd_gcd_common_right_equivalentfirstentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_common_right) + (pfrep_left_normalized_exists_gcd_gcd_common_right_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_common_right_equivalentfirstoutside. pfrep_gap_normalized_exists_gcd_gcd_common_right_equivalentfirstoutside+(pfgd_P_normalized_exists_gcd_gcd_common_right)=(pfrep_power_normalized_exists_gcd_gcd_common_right_equivalent)) /\ (((pfrep_left_normalized_exists_gcd_gcd_common_right_equivalent)=0))))) -> ((exists pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentsecond. ((pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentsecond+S (pfrep_power_normalized_exists_gcd_gcd_common_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_common_right_equivalentsecondentry. ff_h_pfp_normalized_exists_gcd_gcd_common_right_equivalentsecondentry + S (pfrep_right_normalized_exists_gcd_gcd_common_right_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_common_right_equivalentsecondentry. bb = ff_q_pfp_normalized_exists_gcd_gcd_common_right_equivalentsecondentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_common_right_equivalentsecond)) * bc) + (pfrep_right_normalized_exists_gcd_gcd_common_right_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_common_right_equivalentsecondoutside. pfrep_gap_normalized_exists_gcd_gcd_common_right_equivalentsecondoutside+(M)=(pfrep_power_normalized_exists_gcd_gcd_common_right_equivalent)) /\ (((pfrep_right_normalized_exists_gcd_gcd_common_right_equivalent)=0))))) -> pfrep_left_normalized_exists_gcd_gcd_common_right_equivalent=pfrep_right_normalized_exists_gcd_gcd_common_right_equivalent)))))))))) /\ ((forall pfgg_db_normalized_exists_gcd_gcd pfgg_dc_normalized_exists_gcd_gcd pfgg_D_normalized_exists_gcd_gcd. (((((forall fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_bounded. (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_bounded) = L) -> exists fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_bounded. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_bounded) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_entry. ab = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_bounded)) * ac) + (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_bounded))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_bounded_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_bounded) = p))) /\ ((exists pfgd_qb_normalized_exists_gcd_gcd_divisor_left pfgd_qc_normalized_exists_gcd_gcd_divisor_left pfgd_Q_normalized_exists_gcd_gcd_divisor_left pfgd_pb_normalized_exists_gcd_gcd_divisor_left pfgd_pc_normalized_exists_gcd_gcd_divisor_left pfgd_P_normalized_exists_gcd_gcd_divisor_left. ((((forall fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productleft. (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productleft) = pfgd_Q_normalized_exists_gcd_gcd_divisor_left) -> exists fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productleft. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productleft) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_left)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_entry. pfgd_qb_normalized_exists_gcd_gcd_divisor_left = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_left) + (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productleft))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productleft_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productleft) = p))) /\ (((forall fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productright. (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productright_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productright_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productright) = pfgg_D_normalized_exists_gcd_gcd) -> exists fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productright. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_left_productright_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_left_productright_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productright) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productright)) * pfgg_dc_normalized_exists_gcd_gcd)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_left_productright_entry. pfgg_db_normalized_exists_gcd_gcd = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_left_productright_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_left_productright)) * pfgg_dc_normalized_exists_gcd_gcd) + (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productright))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productright_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_left_productright_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_left_productright) = p))) /\ (((((((pfgd_Q_normalized_exists_gcd_gcd_divisor_left)=0 \/ (pfgg_D_normalized_exists_gcd_gcd)=0) /\ (((pfgd_P_normalized_exists_gcd_gcd_divisor_left)=0)))) \/ (((~((pfgd_Q_normalized_exists_gcd_gcd_divisor_left)=0)) /\ (((~((pfgg_D_normalized_exists_gcd_gcd)=0)) /\ (((pfgd_Q_normalized_exists_gcd_gcd_divisor_left)+(pfgg_D_normalized_exists_gcd_gcd)=S (pfgd_P_normalized_exists_gcd_gcd_divisor_left)))))))) /\ ((forall pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients. (exists pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientsbound. pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientsbound + S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients) = (pfgd_P_normalized_exists_gcd_gcd_divisor_left)) -> exists pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficients. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientsentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientsentry + S (pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficients) = S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_left)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientsentry. pfgd_pb_normalized_exists_gcd_gcd_divisor_left = ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientsentry * S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_left) + (pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficients))) /\ ((exists pfc_terms_code_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient pfc_terms_scale_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient pfc_natural_sum_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient. ((forall pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients))) -> exists pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient = ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient) + (pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm pfc_left_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm pfc_right_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients)) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_normalized_exists_gcd_gcd_divisor_left)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_left)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_normalized_exists_gcd_gcd_divisor_left = ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_left) + (pfc_left_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_normalized_exists_gcd_gcd_divisor_left)=(pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = (pfgg_D_normalized_exists_gcd_gcd)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_normalized_exists_gcd_gcd)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. pfgg_db_normalized_exists_gcd_gcd = ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_normalized_exists_gcd_gcd) + (pfc_right_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgg_D_normalized_exists_gcd_gcd)=(pfc_complement_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonal)=pfc_left_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_exists_gcd_gcd_divisor_left_productcoefficients)) -> exists fs_a_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient = fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient) + (fs_a_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientresiduebound. pfa_gap_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_exists_gcd_gcd_divisor_left_productcoefficients) + (p) * pfa_offset_right_normalized_exists_gcd_gcd_divisor_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_exists_gcd_gcd_divisor_left_equivalent pfrep_left_normalized_exists_gcd_gcd_divisor_left_equivalent pfrep_right_normalized_exists_gcd_gcd_divisor_left_equivalent. ((exists pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentfirst. ((pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentfirst+S (pfrep_power_normalized_exists_gcd_gcd_divisor_left_equivalent)=(pfgd_P_normalized_exists_gcd_gcd_divisor_left)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentfirstentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentfirstentry + S (pfrep_left_normalized_exists_gcd_gcd_divisor_left_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_left)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentfirstentry. pfgd_pb_normalized_exists_gcd_gcd_divisor_left = ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentfirstentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_left) + (pfrep_left_normalized_exists_gcd_gcd_divisor_left_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_divisor_left_equivalentfirstoutside. pfrep_gap_normalized_exists_gcd_gcd_divisor_left_equivalentfirstoutside+(pfgd_P_normalized_exists_gcd_gcd_divisor_left)=(pfrep_power_normalized_exists_gcd_gcd_divisor_left_equivalent)) /\ (((pfrep_left_normalized_exists_gcd_gcd_divisor_left_equivalent)=0))))) -> ((exists pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentsecond. ((pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentsecond+S (pfrep_power_normalized_exists_gcd_gcd_divisor_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentsecondentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentsecondentry + S (pfrep_right_normalized_exists_gcd_gcd_divisor_left_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentsecondentry. ab = ff_q_pfp_normalized_exists_gcd_gcd_divisor_left_equivalentsecondentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_left_equivalentsecond)) * ac) + (pfrep_right_normalized_exists_gcd_gcd_divisor_left_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_divisor_left_equivalentsecondoutside. pfrep_gap_normalized_exists_gcd_gcd_divisor_left_equivalentsecondoutside+(L)=(pfrep_power_normalized_exists_gcd_gcd_divisor_left_equivalent)) /\ (((pfrep_right_normalized_exists_gcd_gcd_divisor_left_equivalent)=0))))) -> pfrep_left_normalized_exists_gcd_gcd_divisor_left_equivalent=pfrep_right_normalized_exists_gcd_gcd_divisor_left_equivalent))))))) /\ ((((forall fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_bounded. (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_bounded) = M) -> exists fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_bounded. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_bounded) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_entry. bb = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_bounded)) * bc) + (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_bounded))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_bounded_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_bounded) = p))) /\ ((exists pfgd_qb_normalized_exists_gcd_gcd_divisor_right pfgd_qc_normalized_exists_gcd_gcd_divisor_right pfgd_Q_normalized_exists_gcd_gcd_divisor_right pfgd_pb_normalized_exists_gcd_gcd_divisor_right pfgd_pc_normalized_exists_gcd_gcd_divisor_right pfgd_P_normalized_exists_gcd_gcd_divisor_right. ((((forall fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productleft. (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productleft) = pfgd_Q_normalized_exists_gcd_gcd_divisor_right) -> exists fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productleft. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productleft) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_right)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_entry. pfgd_qb_normalized_exists_gcd_gcd_divisor_right = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_right) + (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productleft))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productleft_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productleft) = p))) /\ (((forall fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productright. (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productright_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productright_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productright) = pfgg_D_normalized_exists_gcd_gcd) -> exists fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productright. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_right_productright_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_divisor_right_productright_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productright) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productright)) * pfgg_dc_normalized_exists_gcd_gcd)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_right_productright_entry. pfgg_db_normalized_exists_gcd_gcd = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_divisor_right_productright_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_divisor_right_productright)) * pfgg_dc_normalized_exists_gcd_gcd) + (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productright))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productright_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_divisor_right_productright_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_divisor_right_productright) = p))) /\ (((((((pfgd_Q_normalized_exists_gcd_gcd_divisor_right)=0 \/ (pfgg_D_normalized_exists_gcd_gcd)=0) /\ (((pfgd_P_normalized_exists_gcd_gcd_divisor_right)=0)))) \/ (((~((pfgd_Q_normalized_exists_gcd_gcd_divisor_right)=0)) /\ (((~((pfgg_D_normalized_exists_gcd_gcd)=0)) /\ (((pfgd_Q_normalized_exists_gcd_gcd_divisor_right)+(pfgg_D_normalized_exists_gcd_gcd)=S (pfgd_P_normalized_exists_gcd_gcd_divisor_right)))))))) /\ ((forall pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients. (exists pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientsbound. pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientsbound + S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients) = (pfgd_P_normalized_exists_gcd_gcd_divisor_right)) -> exists pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficients. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientsentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientsentry + S (pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficients) = S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_right)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientsentry. pfgd_pb_normalized_exists_gcd_gcd_divisor_right = ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientsentry * S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_right) + (pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficients))) /\ ((exists pfc_terms_code_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient pfc_terms_scale_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient pfc_natural_sum_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient. ((forall pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients))) -> exists pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient = ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient) + (pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm pfc_left_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm pfc_right_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients)) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_normalized_exists_gcd_gcd_divisor_right)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_right)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_normalized_exists_gcd_gcd_divisor_right = ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_divisor_right) + (pfc_left_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_normalized_exists_gcd_gcd_divisor_right)=(pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = (pfgg_D_normalized_exists_gcd_gcd)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_normalized_exists_gcd_gcd)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. pfgg_db_normalized_exists_gcd_gcd = ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_normalized_exists_gcd_gcd) + (pfc_right_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgg_D_normalized_exists_gcd_gcd)=(pfc_complement_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonal)=pfc_left_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_exists_gcd_gcd_divisor_right_productcoefficients)) -> exists fs_a_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient = fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient) + (fs_a_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientresiduebound. pfa_gap_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_exists_gcd_gcd_divisor_right_productcoefficients) + (p) * pfa_offset_right_normalized_exists_gcd_gcd_divisor_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_exists_gcd_gcd_divisor_right_equivalent pfrep_left_normalized_exists_gcd_gcd_divisor_right_equivalent pfrep_right_normalized_exists_gcd_gcd_divisor_right_equivalent. ((exists pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentfirst. ((pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentfirst+S (pfrep_power_normalized_exists_gcd_gcd_divisor_right_equivalent)=(pfgd_P_normalized_exists_gcd_gcd_divisor_right)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentfirstentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentfirstentry + S (pfrep_left_normalized_exists_gcd_gcd_divisor_right_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_right)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentfirstentry. pfgd_pb_normalized_exists_gcd_gcd_divisor_right = ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentfirstentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_divisor_right) + (pfrep_left_normalized_exists_gcd_gcd_divisor_right_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_divisor_right_equivalentfirstoutside. pfrep_gap_normalized_exists_gcd_gcd_divisor_right_equivalentfirstoutside+(pfgd_P_normalized_exists_gcd_gcd_divisor_right)=(pfrep_power_normalized_exists_gcd_gcd_divisor_right_equivalent)) /\ (((pfrep_left_normalized_exists_gcd_gcd_divisor_right_equivalent)=0))))) -> ((exists pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentsecond. ((pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentsecond+S (pfrep_power_normalized_exists_gcd_gcd_divisor_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentsecondentry. ff_h_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentsecondentry + S (pfrep_right_normalized_exists_gcd_gcd_divisor_right_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentsecondentry. bb = ff_q_pfp_normalized_exists_gcd_gcd_divisor_right_equivalentsecondentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_divisor_right_equivalentsecond)) * bc) + (pfrep_right_normalized_exists_gcd_gcd_divisor_right_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_divisor_right_equivalentsecondoutside. pfrep_gap_normalized_exists_gcd_gcd_divisor_right_equivalentsecondoutside+(M)=(pfrep_power_normalized_exists_gcd_gcd_divisor_right_equivalent)) /\ (((pfrep_right_normalized_exists_gcd_gcd_divisor_right_equivalent)=0))))) -> pfrep_left_normalized_exists_gcd_gcd_divisor_right_equivalent=pfrep_right_normalized_exists_gcd_gcd_divisor_right_equivalent)))))))))) -> (((forall fom_index_pfp_normalized_exists_gcd_gcd_greatest_bounded. (exists fom_gap_pfp_normalized_exists_gcd_gcd_greatest_bounded_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_greatest_bounded_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_bounded) = G) -> exists fom_value_pfp_normalized_exists_gcd_gcd_greatest_bounded. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_greatest_bounded_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_greatest_bounded_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_greatest_bounded) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_greatest_bounded_entry. gb = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_greatest_bounded_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_bounded)) * gc) + (fom_value_pfp_normalized_exists_gcd_gcd_greatest_bounded))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_greatest_bounded_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_greatest_bounded_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_greatest_bounded) = p))) /\ ((exists pfgd_qb_normalized_exists_gcd_gcd_greatest pfgd_qc_normalized_exists_gcd_gcd_greatest pfgd_Q_normalized_exists_gcd_gcd_greatest pfgd_pb_normalized_exists_gcd_gcd_greatest pfgd_pc_normalized_exists_gcd_gcd_greatest pfgd_P_normalized_exists_gcd_gcd_greatest. ((((forall fom_index_pfp_normalized_exists_gcd_gcd_greatest_productleft. (exists fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productleft_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productleft_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_productleft) = pfgd_Q_normalized_exists_gcd_gcd_greatest) -> exists fom_value_pfp_normalized_exists_gcd_gcd_greatest_productleft. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_greatest_productleft_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_greatest_productleft_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_greatest_productleft) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_greatest)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_greatest_productleft_entry. pfgd_qb_normalized_exists_gcd_gcd_greatest = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_greatest_productleft_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_productleft)) * pfgd_qc_normalized_exists_gcd_gcd_greatest) + (fom_value_pfp_normalized_exists_gcd_gcd_greatest_productleft))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productleft_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productleft_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_greatest_productleft) = p))) /\ (((forall fom_index_pfp_normalized_exists_gcd_gcd_greatest_productright. (exists fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productright_index_bound. fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productright_index_bound + S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_productright) = pfgg_D_normalized_exists_gcd_gcd) -> exists fom_value_pfp_normalized_exists_gcd_gcd_greatest_productright. ((((exists fom_beta_height_pfp_normalized_exists_gcd_gcd_greatest_productright_entry. fom_beta_height_pfp_normalized_exists_gcd_gcd_greatest_productright_entry + S (fom_value_pfp_normalized_exists_gcd_gcd_greatest_productright) = S ((S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_productright)) * pfgg_dc_normalized_exists_gcd_gcd)) /\ exists fom_beta_quotient_pfp_normalized_exists_gcd_gcd_greatest_productright_entry. pfgg_db_normalized_exists_gcd_gcd = fom_beta_quotient_pfp_normalized_exists_gcd_gcd_greatest_productright_entry * S ((S (fom_index_pfp_normalized_exists_gcd_gcd_greatest_productright)) * pfgg_dc_normalized_exists_gcd_gcd) + (fom_value_pfp_normalized_exists_gcd_gcd_greatest_productright))) /\ (exists fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productright_value_bound. fom_gap_pfp_normalized_exists_gcd_gcd_greatest_productright_value_bound + S (fom_value_pfp_normalized_exists_gcd_gcd_greatest_productright) = p))) /\ (((((((pfgd_Q_normalized_exists_gcd_gcd_greatest)=0 \/ (pfgg_D_normalized_exists_gcd_gcd)=0) /\ (((pfgd_P_normalized_exists_gcd_gcd_greatest)=0)))) \/ (((~((pfgd_Q_normalized_exists_gcd_gcd_greatest)=0)) /\ (((~((pfgg_D_normalized_exists_gcd_gcd)=0)) /\ (((pfgd_Q_normalized_exists_gcd_gcd_greatest)+(pfgg_D_normalized_exists_gcd_gcd)=S (pfgd_P_normalized_exists_gcd_gcd_greatest)))))))) /\ ((forall pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients. (exists pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientsbound. pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientsbound + S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients) = (pfgd_P_normalized_exists_gcd_gcd_greatest)) -> exists pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficients. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientsentry. ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientsentry + S (pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficients) = S ((S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_greatest)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientsentry. pfgd_pb_normalized_exists_gcd_gcd_greatest = ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientsentry * S ((S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients)) * pfgd_pc_normalized_exists_gcd_gcd_greatest) + (pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficients))) /\ ((exists pfc_terms_code_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient pfc_terms_scale_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient pfc_natural_sum_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient. ((forall pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalbound. pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients))) -> exists pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient = ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient) + (pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm pfc_left_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm pfc_right_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal)+pfc_complement_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm=(pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients)) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal) = (pfgd_Q_normalized_exists_gcd_gcd_greatest)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_greatest)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_normalized_exists_gcd_gcd_greatest = ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal)) * pfgd_qc_normalized_exists_gcd_gcd_greatest) + (pfc_left_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_normalized_exists_gcd_gcd_greatest)=(pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm) = (pfgg_D_normalized_exists_gcd_gcd)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_normalized_exists_gcd_gcd)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry. pfgg_db_normalized_exists_gcd_gcd = ff_q_pfp_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_normalized_exists_gcd_gcd) + (pfc_right_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonaltermrightoutside+(pfgg_D_normalized_exists_gcd_gcd)=(pfc_complement_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonal)=pfc_left_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm*pfc_right_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient) = S ((S (S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients))) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum) + (pfc_natural_sum_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_exists_gcd_gcd_greatest_productcoefficients)) -> exists fs_a_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient = fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient) + (fs_a_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum) + (fs_r_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum = fs_q_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum) + (fs_s_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientresiduebound. pfa_gap_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientresiduebound + S (pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficient) + (p) * pfa_offset_left_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientresiduecongruence = (pfc_value_normalized_exists_gcd_gcd_greatest_productcoefficients) + (p) * pfa_offset_right_normalized_exists_gcd_gcd_greatest_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_normalized_exists_gcd_gcd_greatest_equivalent pfrep_left_normalized_exists_gcd_gcd_greatest_equivalent pfrep_right_normalized_exists_gcd_gcd_greatest_equivalent. ((exists pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentfirst. ((pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentfirst+S (pfrep_power_normalized_exists_gcd_gcd_greatest_equivalent)=(pfgd_P_normalized_exists_gcd_gcd_greatest)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_greatest_equivalentfirstentry. ff_h_pfp_normalized_exists_gcd_gcd_greatest_equivalentfirstentry + S (pfrep_left_normalized_exists_gcd_gcd_greatest_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_greatest)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_greatest_equivalentfirstentry. pfgd_pb_normalized_exists_gcd_gcd_greatest = ff_q_pfp_normalized_exists_gcd_gcd_greatest_equivalentfirstentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentfirst)) * pfgd_pc_normalized_exists_gcd_gcd_greatest) + (pfrep_left_normalized_exists_gcd_gcd_greatest_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_greatest_equivalentfirstoutside. pfrep_gap_normalized_exists_gcd_gcd_greatest_equivalentfirstoutside+(pfgd_P_normalized_exists_gcd_gcd_greatest)=(pfrep_power_normalized_exists_gcd_gcd_greatest_equivalent)) /\ (((pfrep_left_normalized_exists_gcd_gcd_greatest_equivalent)=0))))) -> ((exists pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentsecond. ((pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentsecond+S (pfrep_power_normalized_exists_gcd_gcd_greatest_equivalent)=(G)) /\ ((((exists ff_h_pfp_normalized_exists_gcd_gcd_greatest_equivalentsecondentry. ff_h_pfp_normalized_exists_gcd_gcd_greatest_equivalentsecondentry + S (pfrep_right_normalized_exists_gcd_gcd_greatest_equivalent) = S ((S (pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentsecond)) * gc)) /\ exists ff_q_pfp_normalized_exists_gcd_gcd_greatest_equivalentsecondentry. gb = ff_q_pfp_normalized_exists_gcd_gcd_greatest_equivalentsecondentry * S ((S (pfrep_position_normalized_exists_gcd_gcd_greatest_equivalentsecond)) * gc) + (pfrep_right_normalized_exists_gcd_gcd_greatest_equivalent)))))) \/ (((exists pfrep_gap_normalized_exists_gcd_gcd_greatest_equivalentsecondoutside. pfrep_gap_normalized_exists_gcd_gcd_greatest_equivalentsecondoutside+(G)=(pfrep_power_normalized_exists_gcd_gcd_greatest_equivalent)) /\ (((pfrep_right_normalized_exists_gcd_gcd_greatest_equivalent)=0))))) -> pfrep_left_normalized_exists_gcd_gcd_greatest_equivalent=pfrep_right_normalized_exists_gcd_gcd_greatest_equivalent)))))))))))))) /\ ((exists pfgb_pb_normalized_exists_bezout pfgb_pc_normalized_exists_bezout pfgb_P_normalized_exists_bezout pfgb_qb_normalized_exists_bezout pfgb_qc_normalized_exists_bezout pfgb_Q_normalized_exists_bezout. ((((forall fom_index_pfp_normalized_exists_bezout_leftleft. (exists fom_gap_pfp_normalized_exists_bezout_leftleft_index_bound. fom_gap_pfp_normalized_exists_bezout_leftleft_index_bound + S (fom_index_pfp_normalized_exists_bezout_leftleft) = U) -> exists fom_value_pfp_normalized_exists_bezout_leftleft. ((((exists fom_beta_height_pfp_normalized_exists_bezout_leftleft_entry. fom_beta_height_pfp_normalized_exists_bezout_leftleft_entry + S (fom_value_pfp_normalized_exists_bezout_leftleft) = S ((S (fom_index_pfp_normalized_exists_bezout_leftleft)) * uc)) /\ exists fom_beta_quotient_pfp_normalized_exists_bezout_leftleft_entry. ub = fom_beta_quotient_pfp_normalized_exists_bezout_leftleft_entry * S ((S (fom_index_pfp_normalized_exists_bezout_leftleft)) * uc) + (fom_value_pfp_normalized_exists_bezout_leftleft))) /\ (exists fom_gap_pfp_normalized_exists_bezout_leftleft_value_bound. fom_gap_pfp_normalized_exists_bezout_leftleft_value_bound + S (fom_value_pfp_normalized_exists_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_normalized_exists_bezout_leftright. (exists fom_gap_pfp_normalized_exists_bezout_leftright_index_bound. fom_gap_pfp_normalized_exists_bezout_leftright_index_bound + S (fom_index_pfp_normalized_exists_bezout_leftright) = L) -> exists fom_value_pfp_normalized_exists_bezout_leftright. ((((exists fom_beta_height_pfp_normalized_exists_bezout_leftright_entry. fom_beta_height_pfp_normalized_exists_bezout_leftright_entry + S (fom_value_pfp_normalized_exists_bezout_leftright) = S ((S (fom_index_pfp_normalized_exists_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_normalized_exists_bezout_leftright_entry. ab = fom_beta_quotient_pfp_normalized_exists_bezout_leftright_entry * S ((S (fom_index_pfp_normalized_exists_bezout_leftright)) * ac) + (fom_value_pfp_normalized_exists_bezout_leftright))) /\ (exists fom_gap_pfp_normalized_exists_bezout_leftright_value_bound. fom_gap_pfp_normalized_exists_bezout_leftright_value_bound + S (fom_value_pfp_normalized_exists_bezout_leftright) = p))) /\ (((((((U)=0 \/ (L)=0) /\ (((pfgb_P_normalized_exists_bezout)=0)))) \/ (((~((U)=0)) /\ (((~((L)=0)) /\ (((U)+(L)=S (pfgb_P_normalized_exists_bezout)))))))) /\ ((forall pfc_index_normalized_exists_bezout_leftcoefficients. (exists pfa_gap_normalized_exists_bezout_leftcoefficientsbound. pfa_gap_normalized_exists_bezout_leftcoefficientsbound + S (pfc_index_normalized_exists_bezout_leftcoefficients) = (pfgb_P_normalized_exists_bezout)) -> exists pfc_value_normalized_exists_bezout_leftcoefficients. ((((exists ff_h_pfp_normalized_exists_bezout_leftcoefficientsentry. ff_h_pfp_normalized_exists_bezout_leftcoefficientsentry + S (pfc_value_normalized_exists_bezout_leftcoefficients) = S ((S (pfc_index_normalized_exists_bezout_leftcoefficients)) * pfgb_pc_normalized_exists_bezout)) /\ exists ff_q_pfp_normalized_exists_bezout_leftcoefficientsentry. pfgb_pb_normalized_exists_bezout = ff_q_pfp_normalized_exists_bezout_leftcoefficientsentry * S ((S (pfc_index_normalized_exists_bezout_leftcoefficients)) * pfgb_pc_normalized_exists_bezout) + (pfc_value_normalized_exists_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_normalized_exists_bezout_leftcoefficientscoefficient pfc_terms_scale_normalized_exists_bezout_leftcoefficientscoefficient pfc_natural_sum_normalized_exists_bezout_leftcoefficientscoefficient. ((forall pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_exists_bezout_leftcoefficients))) -> exists pfc_value_normalized_exists_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_exists_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_exists_bezout_leftcoefficientscoefficient = ff_q_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_bezout_leftcoefficientscoefficient) + (pfc_value_normalized_exists_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_normalized_exists_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal) = (U)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal)) * uc) + (pfc_left_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(U)=(pfc_index_normalized_exists_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_exists_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_exists_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_normalized_exists_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_exists_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_normalized_exists_bezout_leftcoefficients))) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_exists_bezout_leftcoefficients))) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_normalized_exists_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_exists_bezout_leftcoefficients)) -> exists fs_a_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_exists_bezout_leftcoefficientscoefficient = fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_bezout_leftcoefficientscoefficient) + (fs_a_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_exists_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_normalized_exists_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_normalized_exists_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_exists_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_exists_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_exists_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_normalized_exists_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_normalized_exists_bezout_leftcoefficients) + (p) * pfa_offset_right_normalized_exists_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_normalized_exists_bezout_rightleft. (exists fom_gap_pfp_normalized_exists_bezout_rightleft_index_bound. fom_gap_pfp_normalized_exists_bezout_rightleft_index_bound + S (fom_index_pfp_normalized_exists_bezout_rightleft) = V) -> exists fom_value_pfp_normalized_exists_bezout_rightleft. ((((exists fom_beta_height_pfp_normalized_exists_bezout_rightleft_entry. fom_beta_height_pfp_normalized_exists_bezout_rightleft_entry + S (fom_value_pfp_normalized_exists_bezout_rightleft) = S ((S (fom_index_pfp_normalized_exists_bezout_rightleft)) * vc)) /\ exists fom_beta_quotient_pfp_normalized_exists_bezout_rightleft_entry. vb = fom_beta_quotient_pfp_normalized_exists_bezout_rightleft_entry * S ((S (fom_index_pfp_normalized_exists_bezout_rightleft)) * vc) + (fom_value_pfp_normalized_exists_bezout_rightleft))) /\ (exists fom_gap_pfp_normalized_exists_bezout_rightleft_value_bound. fom_gap_pfp_normalized_exists_bezout_rightleft_value_bound + S (fom_value_pfp_normalized_exists_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_normalized_exists_bezout_rightright. (exists fom_gap_pfp_normalized_exists_bezout_rightright_index_bound. fom_gap_pfp_normalized_exists_bezout_rightright_index_bound + S (fom_index_pfp_normalized_exists_bezout_rightright) = M) -> exists fom_value_pfp_normalized_exists_bezout_rightright. ((((exists fom_beta_height_pfp_normalized_exists_bezout_rightright_entry. fom_beta_height_pfp_normalized_exists_bezout_rightright_entry + S (fom_value_pfp_normalized_exists_bezout_rightright) = S ((S (fom_index_pfp_normalized_exists_bezout_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_normalized_exists_bezout_rightright_entry. bb = fom_beta_quotient_pfp_normalized_exists_bezout_rightright_entry * S ((S (fom_index_pfp_normalized_exists_bezout_rightright)) * bc) + (fom_value_pfp_normalized_exists_bezout_rightright))) /\ (exists fom_gap_pfp_normalized_exists_bezout_rightright_value_bound. fom_gap_pfp_normalized_exists_bezout_rightright_value_bound + S (fom_value_pfp_normalized_exists_bezout_rightright) = p))) /\ (((((((V)=0 \/ (M)=0) /\ (((pfgb_Q_normalized_exists_bezout)=0)))) \/ (((~((V)=0)) /\ (((~((M)=0)) /\ (((V)+(M)=S (pfgb_Q_normalized_exists_bezout)))))))) /\ ((forall pfc_index_normalized_exists_bezout_rightcoefficients. (exists pfa_gap_normalized_exists_bezout_rightcoefficientsbound. pfa_gap_normalized_exists_bezout_rightcoefficientsbound + S (pfc_index_normalized_exists_bezout_rightcoefficients) = (pfgb_Q_normalized_exists_bezout)) -> exists pfc_value_normalized_exists_bezout_rightcoefficients. ((((exists ff_h_pfp_normalized_exists_bezout_rightcoefficientsentry. ff_h_pfp_normalized_exists_bezout_rightcoefficientsentry + S (pfc_value_normalized_exists_bezout_rightcoefficients) = S ((S (pfc_index_normalized_exists_bezout_rightcoefficients)) * pfgb_qc_normalized_exists_bezout)) /\ exists ff_q_pfp_normalized_exists_bezout_rightcoefficientsentry. pfgb_qb_normalized_exists_bezout = ff_q_pfp_normalized_exists_bezout_rightcoefficientsentry * S ((S (pfc_index_normalized_exists_bezout_rightcoefficients)) * pfgb_qc_normalized_exists_bezout) + (pfc_value_normalized_exists_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_normalized_exists_bezout_rightcoefficientscoefficient pfc_terms_scale_normalized_exists_bezout_rightcoefficientscoefficient pfc_natural_sum_normalized_exists_bezout_rightcoefficientscoefficient. ((forall pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_normalized_exists_bezout_rightcoefficients))) -> exists pfc_value_normalized_exists_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_normalized_exists_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_normalized_exists_bezout_rightcoefficientscoefficient = ff_q_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_normalized_exists_bezout_rightcoefficientscoefficient) + (pfc_value_normalized_exists_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_normalized_exists_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal) = (V)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal)) * vc) + (pfc_left_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(V)=(pfc_index_normalized_exists_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_normalized_exists_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_normalized_exists_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_normalized_exists_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_normalized_exists_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_normalized_exists_bezout_rightcoefficients))) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_normalized_exists_bezout_rightcoefficients))) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_normalized_exists_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_normalized_exists_bezout_rightcoefficients)) -> exists fs_a_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_normalized_exists_bezout_rightcoefficientscoefficient = fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_normalized_exists_bezout_rightcoefficientscoefficient) + (fs_a_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum = fs_q_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_normalized_exists_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_normalized_exists_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_normalized_exists_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_normalized_exists_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_normalized_exists_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_normalized_exists_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_normalized_exists_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_normalized_exists_bezout_rightcoefficients) + (p) * pfa_offset_right_normalized_exists_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_normalized_exists_bezout_sum_left_bounded. (exists fom_gap_pfp_normalized_exists_bezout_sum_left_bounded_index_bound. fom_gap_pfp_normalized_exists_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_normalized_exists_bezout_sum_left_bounded) = pfgb_P_normalized_exists_bezout) -> exists fom_value_pfp_normalized_exists_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_normalized_exists_bezout_sum_left_bounded_entry. fom_beta_height_pfp_normalized_exists_bezout_sum_left_bounded_entry + S (fom_value_pfp_normalized_exists_bezout_sum_left_bounded) = S ((S (fom_index_pfp_normalized_exists_bezout_sum_left_bounded)) * pfgb_pc_normalized_exists_bezout)) /\ exists fom_beta_quotient_pfp_normalized_exists_bezout_sum_left_bounded_entry. pfgb_pb_normalized_exists_bezout = fom_beta_quotient_pfp_normalized_exists_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_normalized_exists_bezout_sum_left_bounded)) * pfgb_pc_normalized_exists_bezout) + (fom_value_pfp_normalized_exists_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_normalized_exists_bezout_sum_left_bounded_value_bound. fom_gap_pfp_normalized_exists_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_normalized_exists_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_normalized_exists_bezout_sum_right_bounded. (exists fom_gap_pfp_normalized_exists_bezout_sum_right_bounded_index_bound. fom_gap_pfp_normalized_exists_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_normalized_exists_bezout_sum_right_bounded) = pfgb_Q_normalized_exists_bezout) -> exists fom_value_pfp_normalized_exists_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_normalized_exists_bezout_sum_right_bounded_entry. fom_beta_height_pfp_normalized_exists_bezout_sum_right_bounded_entry + S (fom_value_pfp_normalized_exists_bezout_sum_right_bounded) = S ((S (fom_index_pfp_normalized_exists_bezout_sum_right_bounded)) * pfgb_qc_normalized_exists_bezout)) /\ exists fom_beta_quotient_pfp_normalized_exists_bezout_sum_right_bounded_entry. pfgb_qb_normalized_exists_bezout = fom_beta_quotient_pfp_normalized_exists_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_normalized_exists_bezout_sum_right_bounded)) * pfgb_qc_normalized_exists_bezout) + (fom_value_pfp_normalized_exists_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_normalized_exists_bezout_sum_right_bounded_value_bound. fom_gap_pfp_normalized_exists_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_normalized_exists_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_normalized_exists_bezout_sum_result_bounded. (exists fom_gap_pfp_normalized_exists_bezout_sum_result_bounded_index_bound. fom_gap_pfp_normalized_exists_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_normalized_exists_bezout_sum_result_bounded) = G) -> exists fom_value_pfp_normalized_exists_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_normalized_exists_bezout_sum_result_bounded_entry. fom_beta_height_pfp_normalized_exists_bezout_sum_result_bounded_entry + S (fom_value_pfp_normalized_exists_bezout_sum_result_bounded) = S ((S (fom_index_pfp_normalized_exists_bezout_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_normalized_exists_bezout_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_normalized_exists_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_normalized_exists_bezout_sum_result_bounded)) * gc) + (fom_value_pfp_normalized_exists_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_normalized_exists_bezout_sum_result_bounded_value_bound. fom_gap_pfp_normalized_exists_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_normalized_exists_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_normalized_exists_bezout_sum pfga_uc_normalized_exists_bezout_sum pfga_vb_normalized_exists_bezout_sum pfga_vc_normalized_exists_bezout_sum pfga_tb_normalized_exists_bezout_sum pfga_tc_normalized_exists_bezout_sum pfga_K_normalized_exists_bezout_sum. ((((forall pfrep_power_normalized_exists_bezout_sum_left pfrep_left_normalized_exists_bezout_sum_left pfrep_right_normalized_exists_bezout_sum_left. ((exists pfrep_position_normalized_exists_bezout_sum_leftfirst. ((pfrep_position_normalized_exists_bezout_sum_leftfirst+S (pfrep_power_normalized_exists_bezout_sum_left)=(pfgb_P_normalized_exists_bezout)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_sum_leftfirstentry. ff_h_pfp_normalized_exists_bezout_sum_leftfirstentry + S (pfrep_left_normalized_exists_bezout_sum_left) = S ((S (pfrep_position_normalized_exists_bezout_sum_leftfirst)) * pfgb_pc_normalized_exists_bezout)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_leftfirstentry. pfgb_pb_normalized_exists_bezout = ff_q_pfp_normalized_exists_bezout_sum_leftfirstentry * S ((S (pfrep_position_normalized_exists_bezout_sum_leftfirst)) * pfgb_pc_normalized_exists_bezout) + (pfrep_left_normalized_exists_bezout_sum_left)))))) \/ (((exists pfrep_gap_normalized_exists_bezout_sum_leftfirstoutside. pfrep_gap_normalized_exists_bezout_sum_leftfirstoutside+(pfgb_P_normalized_exists_bezout)=(pfrep_power_normalized_exists_bezout_sum_left)) /\ (((pfrep_left_normalized_exists_bezout_sum_left)=0))))) -> ((exists pfrep_position_normalized_exists_bezout_sum_leftsecond. ((pfrep_position_normalized_exists_bezout_sum_leftsecond+S (pfrep_power_normalized_exists_bezout_sum_left)=(pfga_K_normalized_exists_bezout_sum)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_sum_leftsecondentry. ff_h_pfp_normalized_exists_bezout_sum_leftsecondentry + S (pfrep_right_normalized_exists_bezout_sum_left) = S ((S (pfrep_position_normalized_exists_bezout_sum_leftsecond)) * pfga_uc_normalized_exists_bezout_sum)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_leftsecondentry. pfga_ub_normalized_exists_bezout_sum = ff_q_pfp_normalized_exists_bezout_sum_leftsecondentry * S ((S (pfrep_position_normalized_exists_bezout_sum_leftsecond)) * pfga_uc_normalized_exists_bezout_sum) + (pfrep_right_normalized_exists_bezout_sum_left)))))) \/ (((exists pfrep_gap_normalized_exists_bezout_sum_leftsecondoutside. pfrep_gap_normalized_exists_bezout_sum_leftsecondoutside+(pfga_K_normalized_exists_bezout_sum)=(pfrep_power_normalized_exists_bezout_sum_left)) /\ (((pfrep_right_normalized_exists_bezout_sum_left)=0))))) -> pfrep_left_normalized_exists_bezout_sum_left=pfrep_right_normalized_exists_bezout_sum_left) /\ ((forall pfrep_power_normalized_exists_bezout_sum_right pfrep_left_normalized_exists_bezout_sum_right pfrep_right_normalized_exists_bezout_sum_right. ((exists pfrep_position_normalized_exists_bezout_sum_rightfirst. ((pfrep_position_normalized_exists_bezout_sum_rightfirst+S (pfrep_power_normalized_exists_bezout_sum_right)=(pfgb_Q_normalized_exists_bezout)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_sum_rightfirstentry. ff_h_pfp_normalized_exists_bezout_sum_rightfirstentry + S (pfrep_left_normalized_exists_bezout_sum_right) = S ((S (pfrep_position_normalized_exists_bezout_sum_rightfirst)) * pfgb_qc_normalized_exists_bezout)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_rightfirstentry. pfgb_qb_normalized_exists_bezout = ff_q_pfp_normalized_exists_bezout_sum_rightfirstentry * S ((S (pfrep_position_normalized_exists_bezout_sum_rightfirst)) * pfgb_qc_normalized_exists_bezout) + (pfrep_left_normalized_exists_bezout_sum_right)))))) \/ (((exists pfrep_gap_normalized_exists_bezout_sum_rightfirstoutside. pfrep_gap_normalized_exists_bezout_sum_rightfirstoutside+(pfgb_Q_normalized_exists_bezout)=(pfrep_power_normalized_exists_bezout_sum_right)) /\ (((pfrep_left_normalized_exists_bezout_sum_right)=0))))) -> ((exists pfrep_position_normalized_exists_bezout_sum_rightsecond. ((pfrep_position_normalized_exists_bezout_sum_rightsecond+S (pfrep_power_normalized_exists_bezout_sum_right)=(pfga_K_normalized_exists_bezout_sum)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_sum_rightsecondentry. ff_h_pfp_normalized_exists_bezout_sum_rightsecondentry + S (pfrep_right_normalized_exists_bezout_sum_right) = S ((S (pfrep_position_normalized_exists_bezout_sum_rightsecond)) * pfga_vc_normalized_exists_bezout_sum)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_rightsecondentry. pfga_vb_normalized_exists_bezout_sum = ff_q_pfp_normalized_exists_bezout_sum_rightsecondentry * S ((S (pfrep_position_normalized_exists_bezout_sum_rightsecond)) * pfga_vc_normalized_exists_bezout_sum) + (pfrep_right_normalized_exists_bezout_sum_right)))))) \/ (((exists pfrep_gap_normalized_exists_bezout_sum_rightsecondoutside. pfrep_gap_normalized_exists_bezout_sum_rightsecondoutside+(pfga_K_normalized_exists_bezout_sum)=(pfrep_power_normalized_exists_bezout_sum_right)) /\ (((pfrep_right_normalized_exists_bezout_sum_right)=0))))) -> pfrep_left_normalized_exists_bezout_sum_right=pfrep_right_normalized_exists_bezout_sum_right)))) /\ (((forall pfp_index_normalized_exists_bezout_sum_add. (exists pfa_gap_normalized_exists_bezout_sum_addindex. pfa_gap_normalized_exists_bezout_sum_addindex + S (pfp_index_normalized_exists_bezout_sum_add) = (pfga_K_normalized_exists_bezout_sum)) -> exists pfp_left_normalized_exists_bezout_sum_add pfp_right_normalized_exists_bezout_sum_add pfp_value_normalized_exists_bezout_sum_add. ((((exists ff_h_pfp_normalized_exists_bezout_sum_addleft. ff_h_pfp_normalized_exists_bezout_sum_addleft + S (pfp_left_normalized_exists_bezout_sum_add) = S ((S (pfp_index_normalized_exists_bezout_sum_add)) * pfga_uc_normalized_exists_bezout_sum)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_addleft. pfga_ub_normalized_exists_bezout_sum = ff_q_pfp_normalized_exists_bezout_sum_addleft * S ((S (pfp_index_normalized_exists_bezout_sum_add)) * pfga_uc_normalized_exists_bezout_sum) + (pfp_left_normalized_exists_bezout_sum_add))) /\ (((((exists ff_h_pfp_normalized_exists_bezout_sum_addright. ff_h_pfp_normalized_exists_bezout_sum_addright + S (pfp_right_normalized_exists_bezout_sum_add) = S ((S (pfp_index_normalized_exists_bezout_sum_add)) * pfga_vc_normalized_exists_bezout_sum)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_addright. pfga_vb_normalized_exists_bezout_sum = ff_q_pfp_normalized_exists_bezout_sum_addright * S ((S (pfp_index_normalized_exists_bezout_sum_add)) * pfga_vc_normalized_exists_bezout_sum) + (pfp_right_normalized_exists_bezout_sum_add))) /\ (((((exists ff_h_pfp_normalized_exists_bezout_sum_addtarget. ff_h_pfp_normalized_exists_bezout_sum_addtarget + S (pfp_value_normalized_exists_bezout_sum_add) = S ((S (pfp_index_normalized_exists_bezout_sum_add)) * pfga_tc_normalized_exists_bezout_sum)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_addtarget. pfga_tb_normalized_exists_bezout_sum = ff_q_pfp_normalized_exists_bezout_sum_addtarget * S ((S (pfp_index_normalized_exists_bezout_sum_add)) * pfga_tc_normalized_exists_bezout_sum) + (pfp_value_normalized_exists_bezout_sum_add))) /\ ((((exists pfa_gap_normalized_exists_bezout_sum_addoperationleft. pfa_gap_normalized_exists_bezout_sum_addoperationleft + S (pfp_left_normalized_exists_bezout_sum_add) = (p)) /\ (((exists pfa_gap_normalized_exists_bezout_sum_addoperationright. pfa_gap_normalized_exists_bezout_sum_addoperationright + S (pfp_right_normalized_exists_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_normalized_exists_bezout_sum_addoperationresultbound. pfa_gap_normalized_exists_bezout_sum_addoperationresultbound + S (pfp_value_normalized_exists_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_normalized_exists_bezout_sum_addoperationresultcongruence pfa_offset_right_normalized_exists_bezout_sum_addoperationresultcongruence. ((pfp_left_normalized_exists_bezout_sum_add) + (pfp_right_normalized_exists_bezout_sum_add)) + (p) * pfa_offset_left_normalized_exists_bezout_sum_addoperationresultcongruence = (pfp_value_normalized_exists_bezout_sum_add) + (p) * pfa_offset_right_normalized_exists_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_normalized_exists_bezout_sum_result pfrep_left_normalized_exists_bezout_sum_result pfrep_right_normalized_exists_bezout_sum_result. ((exists pfrep_position_normalized_exists_bezout_sum_resultfirst. ((pfrep_position_normalized_exists_bezout_sum_resultfirst+S (pfrep_power_normalized_exists_bezout_sum_result)=(pfga_K_normalized_exists_bezout_sum)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_sum_resultfirstentry. ff_h_pfp_normalized_exists_bezout_sum_resultfirstentry + S (pfrep_left_normalized_exists_bezout_sum_result) = S ((S (pfrep_position_normalized_exists_bezout_sum_resultfirst)) * pfga_tc_normalized_exists_bezout_sum)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_resultfirstentry. pfga_tb_normalized_exists_bezout_sum = ff_q_pfp_normalized_exists_bezout_sum_resultfirstentry * S ((S (pfrep_position_normalized_exists_bezout_sum_resultfirst)) * pfga_tc_normalized_exists_bezout_sum) + (pfrep_left_normalized_exists_bezout_sum_result)))))) \/ (((exists pfrep_gap_normalized_exists_bezout_sum_resultfirstoutside. pfrep_gap_normalized_exists_bezout_sum_resultfirstoutside+(pfga_K_normalized_exists_bezout_sum)=(pfrep_power_normalized_exists_bezout_sum_result)) /\ (((pfrep_left_normalized_exists_bezout_sum_result)=0))))) -> ((exists pfrep_position_normalized_exists_bezout_sum_resultsecond. ((pfrep_position_normalized_exists_bezout_sum_resultsecond+S (pfrep_power_normalized_exists_bezout_sum_result)=(G)) /\ ((((exists ff_h_pfp_normalized_exists_bezout_sum_resultsecondentry. ff_h_pfp_normalized_exists_bezout_sum_resultsecondentry + S (pfrep_right_normalized_exists_bezout_sum_result) = S ((S (pfrep_position_normalized_exists_bezout_sum_resultsecond)) * gc)) /\ exists ff_q_pfp_normalized_exists_bezout_sum_resultsecondentry. gb = ff_q_pfp_normalized_exists_bezout_sum_resultsecondentry * S ((S (pfrep_position_normalized_exists_bezout_sum_resultsecond)) * gc) + (pfrep_right_normalized_exists_bezout_sum_result)))))) \/ (((exists pfrep_gap_normalized_exists_bezout_sum_resultsecondoutside. pfrep_gap_normalized_exists_bezout_sum_resultsecondoutside+(G)=(pfrep_power_normalized_exists_bezout_sum_result)) /\ (((pfrep_right_normalized_exists_bezout_sum_result)=0))))) -> pfrep_left_normalized_exists_bezout_sum_result=pfrep_right_normalized_exists_bezout_sum_result)))))))))))))))))))))Complete tactic proof in conservative notation
All 66 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
66 script commands · 10 reading checkpoints · 1 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 (2)
01Fix variables and assumptionsL1–10
02Establish hsL11–20
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial gcd bezout exists.
- L11Definitions: FpPolynomialZeroOrMonic(p,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution)FpPolynomialCommonRightDivisor(p,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution,ab,ac,L,bb,bc,M)FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,M,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution,pfgs_ub_normalized_exists_solution,pfgs_uc_normalized_exists_solution,pfgs_U_normalized_exists_solution,pfgs_vb_normalized_exists_solution,pfgs_vc_normalized_exists_solution,pfgs_V_normalized_exists_solution)Original native command in the exact edition
have hs · expand full local formula (1,003 characters)
have hs : ∃ pfgs_gb_normalized_exists_solution. ∃ pfgs_gc_normalized_exists_solution. ∃ pfgs_G_normalized_exists_solution. ∃ pfgs_ub_normalized_exists_solution. ∃ pfgs_uc_normalized_exists_solution. ∃ pfgs_U_normalized_exists_solution. ∃ pfgs_vb_normalized_exists_solution. ∃ pfgs_vc_normalized_exists_solution. ∃ pfgs_V_normalized_exists_solution. FpPolynomialZeroOrMonic(p,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution) ∧ (FpPolynomialCommonRightDivisor(p,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution,ab,ac,L,bb,bc,M) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,M,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution,pfgs_ub_normalized_exists_solution,pfgs_uc_normalized_exists_solution,pfgs_U_normalized_exists_solution,pfgs_vb_normalized_exists_solution,pfgs_vc_normalized_exists_solution,pfgs_V_normalized_exists_solution)) - L12
specialize prime_field_polynomial_gcd_bezout_exists (p) - L13
specialize prime_field_polynomial_gcd_bezout_exists (ab) - L14
specialize prime_field_polynomial_gcd_bezout_exists (ac) - L15
specialize prime_field_polynomial_gcd_bezout_exists (L) - L16
specialize prime_field_polynomial_gcd_bezout_exists (bb) - L17
specialize prime_field_polynomial_gcd_bezout_exists (bc) - L18
specialize prime_field_polynomial_gcd_bezout_exists (M) - L19
apply prime_field_polynomial_gcd_bezout_exists - L20
exact hp
03Use earlier factsL21–22
04Separate the logical casesL23–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L23
cases hs - L24
cases hs_witness - L25
cases hs_witness_witness - L26
cases hs_witness_witness_witness - L27
cases hs_witness_witness_witness_witness - L28
cases hs_witness_witness_witness_witness_witness - L29
cases hs_witness_witness_witness_witness_witness_witness - L30
cases hs_witness_witness_witness_witness_witness_witness_witness - L31
cases hs_witness_witness_witness_witness_witness_witness_witness_witness - L32
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness
05Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right
06Construct an explicit witnessL34–42
07Separate the logical casesL43–44
08Use earlier factsL45–54
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L45
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - L46
specialize prime_field_polynomial_bezout_is_right_gcd (p) - L47
specialize prime_field_polynomial_bezout_is_right_gcd (x) - L48
specialize prime_field_polynomial_bezout_is_right_gcd (x1) - L49
specialize prime_field_polynomial_bezout_is_right_gcd (x2) - L50
specialize prime_field_polynomial_bezout_is_right_gcd (ab) - L51
specialize prime_field_polynomial_bezout_is_right_gcd (ac) - L52
specialize prime_field_polynomial_bezout_is_right_gcd (L) - L53
specialize prime_field_polynomial_bezout_is_right_gcd (bb) - L54
specialize prime_field_polynomial_bezout_is_right_gcd (bc)
09Use earlier factsL55–64
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L55
specialize prime_field_polynomial_bezout_is_right_gcd (M) - L56
specialize prime_field_polynomial_bezout_is_right_gcd (x3) - L57
specialize prime_field_polynomial_bezout_is_right_gcd (x4) - L58
specialize prime_field_polynomial_bezout_is_right_gcd (x5) - L59
specialize prime_field_polynomial_bezout_is_right_gcd (x6) - L60
specialize prime_field_polynomial_bezout_is_right_gcd (x7) - L61
specialize prime_field_polynomial_bezout_is_right_gcd (x8) - L62
apply prime_field_polynomial_bezout_is_right_gcd - L63
exact hp - L64
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left
Original defined command ledger · 66 lines
- 0001
intro p - 0002
intro ab - 0003
intro ac - 0004
intro L - 0005
intro bb - 0006
intro bc - 0007
intro M - 0008
intro hp - 0009
intro hA - 0010
intro hB - 0011
have hs : ∃ pfgs_gb_normalized_exists_solution. ∃ pfgs_gc_normalized_exists_solution. ∃ pfgs_G_normalized_exists_solution. ∃ pfgs_ub_normalized_exists_solution. ∃ pfgs_uc_normalized_exists_solution. ∃ pfgs_U_normalized_exists_solution. ∃ pfgs_vb_normalized_exists_solution. ∃ pfgs_vc_normalized_exists_solution. ∃ pfgs_V_normalized_exists_solution. FpPolynomialZeroOrMonic(p,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution) ∧ (FpPolynomialCommonRightDivisor(p,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution,ab,ac,L,bb,bc,M) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,M,pfgs_gb_normalized_exists_solution,pfgs_gc_normalized_exists_solution,pfgs_G_normalized_exists_solution,pfgs_ub_normalized_exists_solution,pfgs_uc_normalized_exists_solution,pfgs_U_normalized_exists_solution,pfgs_vb_normalized_exists_solution,pfgs_vc_normalized_exists_solution,pfgs_V_normalized_exists_solution)) - 0012
specialize prime_field_polynomial_gcd_bezout_exists (p) - 0013
specialize prime_field_polynomial_gcd_bezout_exists (ab) - 0014
specialize prime_field_polynomial_gcd_bezout_exists (ac) - 0015
specialize prime_field_polynomial_gcd_bezout_exists (L) - 0016
specialize prime_field_polynomial_gcd_bezout_exists (bb) - 0017
specialize prime_field_polynomial_gcd_bezout_exists (bc) - 0018
specialize prime_field_polynomial_gcd_bezout_exists (M) - 0019
apply prime_field_polynomial_gcd_bezout_exists - 0020
exact hp - 0021
exact hA - 0022
exact hB - 0023
cases hs - 0024
cases hs_witness - 0025
cases hs_witness_witness - 0026
cases hs_witness_witness_witness - 0027
cases hs_witness_witness_witness_witness - 0028
cases hs_witness_witness_witness_witness_witness - 0029
cases hs_witness_witness_witness_witness_witness_witness - 0030
cases hs_witness_witness_witness_witness_witness_witness_witness - 0031
cases hs_witness_witness_witness_witness_witness_witness_witness_witness - 0032
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0033
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - 0034
exists x - 0035
exists x1 - 0036
exists x2 - 0037
exists x3 - 0038
exists x4 - 0039
exists x5 - 0040
exists x6 - 0041
exists x7 - 0042
exists x8 - 0043
split - 0044
split - 0045
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0046
specialize prime_field_polynomial_bezout_is_right_gcd (p) - 0047
specialize prime_field_polynomial_bezout_is_right_gcd (x) - 0048
specialize prime_field_polynomial_bezout_is_right_gcd (x1) - 0049
specialize prime_field_polynomial_bezout_is_right_gcd (x2) - 0050
specialize prime_field_polynomial_bezout_is_right_gcd (ab) - 0051
specialize prime_field_polynomial_bezout_is_right_gcd (ac) - 0052
specialize prime_field_polynomial_bezout_is_right_gcd (L) - 0053
specialize prime_field_polynomial_bezout_is_right_gcd (bb) - 0054
specialize prime_field_polynomial_bezout_is_right_gcd (bc) - 0055
specialize prime_field_polynomial_bezout_is_right_gcd (M) - 0056
specialize prime_field_polynomial_bezout_is_right_gcd (x3) - 0057
specialize prime_field_polynomial_bezout_is_right_gcd (x4) - 0058
specialize prime_field_polynomial_bezout_is_right_gcd (x5) - 0059
specialize prime_field_polynomial_bezout_is_right_gcd (x6) - 0060
specialize prime_field_polynomial_bezout_is_right_gcd (x7) - 0061
specialize prime_field_polynomial_bezout_is_right_gcd (x8) - 0062
apply prime_field_polynomial_bezout_is_right_gcd - 0063
exact hp - 0064
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0065
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0066
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right