Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
Exact theorem in conservative defined notation
∀ p. ∀ gb. ∀ gc. ∀ G. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ ub. ∀ uc. ∀ U. ∀ vb. ∀ vc. ∀ V. Prime(p) → FpPolynomialCommonRightDivisor(p,gb,gc,G,ab,ac,L,bb,bc,M) → FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,M,gb,gc,G,ub,uc,U,vb,vc,V) → FpPolynomialRightGcd(p,gb,gc,G,ab,ac,L,bb,bc,M)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall p gb gc G ab ac L bb bc M ub uc U vb vc V. (~((p) = 1) /\ forall pfa_factor_left_gcd_greatest_prime pfa_factor_right_gcd_greatest_prime. (p) = pfa_factor_left_gcd_greatest_prime * pfa_factor_right_gcd_greatest_prime -> pfa_factor_left_gcd_greatest_prime = 1 \/ pfa_factor_right_gcd_greatest_prime = 1) -> (((((forall fom_index_pfp_gcd_greatest_common_left_bounded. (exists fom_gap_pfp_gcd_greatest_common_left_bounded_index_bound. fom_gap_pfp_gcd_greatest_common_left_bounded_index_bound + S (fom_index_pfp_gcd_greatest_common_left_bounded) = L) -> exists fom_value_pfp_gcd_greatest_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_common_left_bounded_entry. fom_beta_height_pfp_gcd_greatest_common_left_bounded_entry + S (fom_value_pfp_gcd_greatest_common_left_bounded) = S ((S (fom_index_pfp_gcd_greatest_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_greatest_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_greatest_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_common_left_bounded)) * ac) + (fom_value_pfp_gcd_greatest_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_common_left_bounded_value_bound. fom_gap_pfp_gcd_greatest_common_left_bounded_value_bound + S (fom_value_pfp_gcd_greatest_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_greatest_common_left pfgd_qc_gcd_greatest_common_left pfgd_Q_gcd_greatest_common_left pfgd_pb_gcd_greatest_common_left pfgd_pc_gcd_greatest_common_left pfgd_P_gcd_greatest_common_left. ((((forall fom_index_pfp_gcd_greatest_common_left_productleft. (exists fom_gap_pfp_gcd_greatest_common_left_productleft_index_bound. fom_gap_pfp_gcd_greatest_common_left_productleft_index_bound + S (fom_index_pfp_gcd_greatest_common_left_productleft) = pfgd_Q_gcd_greatest_common_left) -> exists fom_value_pfp_gcd_greatest_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_greatest_common_left_productleft_entry. fom_beta_height_pfp_gcd_greatest_common_left_productleft_entry + S (fom_value_pfp_gcd_greatest_common_left_productleft) = S ((S (fom_index_pfp_gcd_greatest_common_left_productleft)) * pfgd_qc_gcd_greatest_common_left)) /\ exists fom_beta_quotient_pfp_gcd_greatest_common_left_productleft_entry. pfgd_qb_gcd_greatest_common_left = fom_beta_quotient_pfp_gcd_greatest_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_greatest_common_left_productleft)) * pfgd_qc_gcd_greatest_common_left) + (fom_value_pfp_gcd_greatest_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_greatest_common_left_productleft_value_bound. fom_gap_pfp_gcd_greatest_common_left_productleft_value_bound + S (fom_value_pfp_gcd_greatest_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_common_left_productright. (exists fom_gap_pfp_gcd_greatest_common_left_productright_index_bound. fom_gap_pfp_gcd_greatest_common_left_productright_index_bound + S (fom_index_pfp_gcd_greatest_common_left_productright) = G) -> exists fom_value_pfp_gcd_greatest_common_left_productright. ((((exists fom_beta_height_pfp_gcd_greatest_common_left_productright_entry. fom_beta_height_pfp_gcd_greatest_common_left_productright_entry + S (fom_value_pfp_gcd_greatest_common_left_productright) = S ((S (fom_index_pfp_gcd_greatest_common_left_productright)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_common_left_productright_entry. gb = fom_beta_quotient_pfp_gcd_greatest_common_left_productright_entry * S ((S (fom_index_pfp_gcd_greatest_common_left_productright)) * gc) + (fom_value_pfp_gcd_greatest_common_left_productright))) /\ (exists fom_gap_pfp_gcd_greatest_common_left_productright_value_bound. fom_gap_pfp_gcd_greatest_common_left_productright_value_bound + S (fom_value_pfp_gcd_greatest_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_greatest_common_left)=0 \/ (G)=0) /\ (((pfgd_P_gcd_greatest_common_left)=0)))) \/ (((~((pfgd_Q_gcd_greatest_common_left)=0)) /\ (((~((G)=0)) /\ (((pfgd_Q_gcd_greatest_common_left)+(G)=S (pfgd_P_gcd_greatest_common_left)))))))) /\ ((forall pfc_index_gcd_greatest_common_left_productcoefficients. (exists pfa_gap_gcd_greatest_common_left_productcoefficientsbound. pfa_gap_gcd_greatest_common_left_productcoefficientsbound + S (pfc_index_gcd_greatest_common_left_productcoefficients) = (pfgd_P_gcd_greatest_common_left)) -> exists pfc_value_gcd_greatest_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_greatest_common_left_productcoefficientsentry. ff_h_pfp_gcd_greatest_common_left_productcoefficientsentry + S (pfc_value_gcd_greatest_common_left_productcoefficients) = S ((S (pfc_index_gcd_greatest_common_left_productcoefficients)) * pfgd_pc_gcd_greatest_common_left)) /\ exists ff_q_pfp_gcd_greatest_common_left_productcoefficientsentry. pfgd_pb_gcd_greatest_common_left = ff_q_pfp_gcd_greatest_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_greatest_common_left_productcoefficients)) * pfgd_pc_gcd_greatest_common_left) + (pfc_value_gcd_greatest_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_greatest_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_greatest_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_common_left_productcoefficients))) -> exists pfc_value_gcd_greatest_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_common_left_productcoefficientscoefficient) + (pfc_value_gcd_greatest_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_greatest_common_left)) /\ ((((exists ff_h_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_common_left)) /\ exists ff_q_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_greatest_common_left = ff_q_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_common_left) + (pfc_left_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_greatest_common_left)=(pfc_index_gcd_greatest_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_common_left_productcoefficients))) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_common_left_productcoefficients))) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_greatest_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_common_left_equivalent pfrep_left_gcd_greatest_common_left_equivalent pfrep_right_gcd_greatest_common_left_equivalent. ((exists pfrep_position_gcd_greatest_common_left_equivalentfirst. ((pfrep_position_gcd_greatest_common_left_equivalentfirst+S (pfrep_power_gcd_greatest_common_left_equivalent)=(pfgd_P_gcd_greatest_common_left)) /\ ((((exists ff_h_pfp_gcd_greatest_common_left_equivalentfirstentry. ff_h_pfp_gcd_greatest_common_left_equivalentfirstentry + S (pfrep_left_gcd_greatest_common_left_equivalent) = S ((S (pfrep_position_gcd_greatest_common_left_equivalentfirst)) * pfgd_pc_gcd_greatest_common_left)) /\ exists ff_q_pfp_gcd_greatest_common_left_equivalentfirstentry. pfgd_pb_gcd_greatest_common_left = ff_q_pfp_gcd_greatest_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_greatest_common_left_equivalentfirst)) * pfgd_pc_gcd_greatest_common_left) + (pfrep_left_gcd_greatest_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_common_left_equivalentfirstoutside. pfrep_gap_gcd_greatest_common_left_equivalentfirstoutside+(pfgd_P_gcd_greatest_common_left)=(pfrep_power_gcd_greatest_common_left_equivalent)) /\ (((pfrep_left_gcd_greatest_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_greatest_common_left_equivalentsecond. ((pfrep_position_gcd_greatest_common_left_equivalentsecond+S (pfrep_power_gcd_greatest_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_greatest_common_left_equivalentsecondentry. ff_h_pfp_gcd_greatest_common_left_equivalentsecondentry + S (pfrep_right_gcd_greatest_common_left_equivalent) = S ((S (pfrep_position_gcd_greatest_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_greatest_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_greatest_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_greatest_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_greatest_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_common_left_equivalentsecondoutside. pfrep_gap_gcd_greatest_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_greatest_common_left_equivalent)) /\ (((pfrep_right_gcd_greatest_common_left_equivalent)=0))))) -> pfrep_left_gcd_greatest_common_left_equivalent=pfrep_right_gcd_greatest_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_greatest_common_right_bounded. (exists fom_gap_pfp_gcd_greatest_common_right_bounded_index_bound. fom_gap_pfp_gcd_greatest_common_right_bounded_index_bound + S (fom_index_pfp_gcd_greatest_common_right_bounded) = M) -> exists fom_value_pfp_gcd_greatest_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_common_right_bounded_entry. fom_beta_height_pfp_gcd_greatest_common_right_bounded_entry + S (fom_value_pfp_gcd_greatest_common_right_bounded) = S ((S (fom_index_pfp_gcd_greatest_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_common_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_greatest_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_common_right_bounded)) * bc) + (fom_value_pfp_gcd_greatest_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_common_right_bounded_value_bound. fom_gap_pfp_gcd_greatest_common_right_bounded_value_bound + S (fom_value_pfp_gcd_greatest_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_greatest_common_right pfgd_qc_gcd_greatest_common_right pfgd_Q_gcd_greatest_common_right pfgd_pb_gcd_greatest_common_right pfgd_pc_gcd_greatest_common_right pfgd_P_gcd_greatest_common_right. ((((forall fom_index_pfp_gcd_greatest_common_right_productleft. (exists fom_gap_pfp_gcd_greatest_common_right_productleft_index_bound. fom_gap_pfp_gcd_greatest_common_right_productleft_index_bound + S (fom_index_pfp_gcd_greatest_common_right_productleft) = pfgd_Q_gcd_greatest_common_right) -> exists fom_value_pfp_gcd_greatest_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_greatest_common_right_productleft_entry. fom_beta_height_pfp_gcd_greatest_common_right_productleft_entry + S (fom_value_pfp_gcd_greatest_common_right_productleft) = S ((S (fom_index_pfp_gcd_greatest_common_right_productleft)) * pfgd_qc_gcd_greatest_common_right)) /\ exists fom_beta_quotient_pfp_gcd_greatest_common_right_productleft_entry. pfgd_qb_gcd_greatest_common_right = fom_beta_quotient_pfp_gcd_greatest_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_greatest_common_right_productleft)) * pfgd_qc_gcd_greatest_common_right) + (fom_value_pfp_gcd_greatest_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_greatest_common_right_productleft_value_bound. fom_gap_pfp_gcd_greatest_common_right_productleft_value_bound + S (fom_value_pfp_gcd_greatest_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_common_right_productright. (exists fom_gap_pfp_gcd_greatest_common_right_productright_index_bound. fom_gap_pfp_gcd_greatest_common_right_productright_index_bound + S (fom_index_pfp_gcd_greatest_common_right_productright) = G) -> exists fom_value_pfp_gcd_greatest_common_right_productright. ((((exists fom_beta_height_pfp_gcd_greatest_common_right_productright_entry. fom_beta_height_pfp_gcd_greatest_common_right_productright_entry + S (fom_value_pfp_gcd_greatest_common_right_productright) = S ((S (fom_index_pfp_gcd_greatest_common_right_productright)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_common_right_productright_entry. gb = fom_beta_quotient_pfp_gcd_greatest_common_right_productright_entry * S ((S (fom_index_pfp_gcd_greatest_common_right_productright)) * gc) + (fom_value_pfp_gcd_greatest_common_right_productright))) /\ (exists fom_gap_pfp_gcd_greatest_common_right_productright_value_bound. fom_gap_pfp_gcd_greatest_common_right_productright_value_bound + S (fom_value_pfp_gcd_greatest_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_greatest_common_right)=0 \/ (G)=0) /\ (((pfgd_P_gcd_greatest_common_right)=0)))) \/ (((~((pfgd_Q_gcd_greatest_common_right)=0)) /\ (((~((G)=0)) /\ (((pfgd_Q_gcd_greatest_common_right)+(G)=S (pfgd_P_gcd_greatest_common_right)))))))) /\ ((forall pfc_index_gcd_greatest_common_right_productcoefficients. (exists pfa_gap_gcd_greatest_common_right_productcoefficientsbound. pfa_gap_gcd_greatest_common_right_productcoefficientsbound + S (pfc_index_gcd_greatest_common_right_productcoefficients) = (pfgd_P_gcd_greatest_common_right)) -> exists pfc_value_gcd_greatest_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_greatest_common_right_productcoefficientsentry. ff_h_pfp_gcd_greatest_common_right_productcoefficientsentry + S (pfc_value_gcd_greatest_common_right_productcoefficients) = S ((S (pfc_index_gcd_greatest_common_right_productcoefficients)) * pfgd_pc_gcd_greatest_common_right)) /\ exists ff_q_pfp_gcd_greatest_common_right_productcoefficientsentry. pfgd_pb_gcd_greatest_common_right = ff_q_pfp_gcd_greatest_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_greatest_common_right_productcoefficients)) * pfgd_pc_gcd_greatest_common_right) + (pfc_value_gcd_greatest_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_greatest_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_greatest_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_common_right_productcoefficients))) -> exists pfc_value_gcd_greatest_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_common_right_productcoefficientscoefficient) + (pfc_value_gcd_greatest_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_greatest_common_right)) /\ ((((exists ff_h_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_common_right)) /\ exists ff_q_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_greatest_common_right = ff_q_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_common_right) + (pfc_left_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_greatest_common_right)=(pfc_index_gcd_greatest_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_common_right_productcoefficients))) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_common_right_productcoefficients))) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_greatest_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_common_right_equivalent pfrep_left_gcd_greatest_common_right_equivalent pfrep_right_gcd_greatest_common_right_equivalent. ((exists pfrep_position_gcd_greatest_common_right_equivalentfirst. ((pfrep_position_gcd_greatest_common_right_equivalentfirst+S (pfrep_power_gcd_greatest_common_right_equivalent)=(pfgd_P_gcd_greatest_common_right)) /\ ((((exists ff_h_pfp_gcd_greatest_common_right_equivalentfirstentry. ff_h_pfp_gcd_greatest_common_right_equivalentfirstentry + S (pfrep_left_gcd_greatest_common_right_equivalent) = S ((S (pfrep_position_gcd_greatest_common_right_equivalentfirst)) * pfgd_pc_gcd_greatest_common_right)) /\ exists ff_q_pfp_gcd_greatest_common_right_equivalentfirstentry. pfgd_pb_gcd_greatest_common_right = ff_q_pfp_gcd_greatest_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_greatest_common_right_equivalentfirst)) * pfgd_pc_gcd_greatest_common_right) + (pfrep_left_gcd_greatest_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_common_right_equivalentfirstoutside. pfrep_gap_gcd_greatest_common_right_equivalentfirstoutside+(pfgd_P_gcd_greatest_common_right)=(pfrep_power_gcd_greatest_common_right_equivalent)) /\ (((pfrep_left_gcd_greatest_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_greatest_common_right_equivalentsecond. ((pfrep_position_gcd_greatest_common_right_equivalentsecond+S (pfrep_power_gcd_greatest_common_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_gcd_greatest_common_right_equivalentsecondentry. ff_h_pfp_gcd_greatest_common_right_equivalentsecondentry + S (pfrep_right_gcd_greatest_common_right_equivalent) = S ((S (pfrep_position_gcd_greatest_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_greatest_common_right_equivalentsecondentry. bb = ff_q_pfp_gcd_greatest_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_greatest_common_right_equivalentsecond)) * bc) + (pfrep_right_gcd_greatest_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_common_right_equivalentsecondoutside. pfrep_gap_gcd_greatest_common_right_equivalentsecondoutside+(M)=(pfrep_power_gcd_greatest_common_right_equivalent)) /\ (((pfrep_right_gcd_greatest_common_right_equivalent)=0))))) -> pfrep_left_gcd_greatest_common_right_equivalent=pfrep_right_gcd_greatest_common_right_equivalent)))))))))) -> (exists pfgb_pb_gcd_greatest_bezout pfgb_pc_gcd_greatest_bezout pfgb_P_gcd_greatest_bezout pfgb_qb_gcd_greatest_bezout pfgb_qc_gcd_greatest_bezout pfgb_Q_gcd_greatest_bezout. ((((forall fom_index_pfp_gcd_greatest_bezout_leftleft. (exists fom_gap_pfp_gcd_greatest_bezout_leftleft_index_bound. fom_gap_pfp_gcd_greatest_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_greatest_bezout_leftleft) = U) -> exists fom_value_pfp_gcd_greatest_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_greatest_bezout_leftleft_entry. fom_beta_height_pfp_gcd_greatest_bezout_leftleft_entry + S (fom_value_pfp_gcd_greatest_bezout_leftleft) = S ((S (fom_index_pfp_gcd_greatest_bezout_leftleft)) * uc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_bezout_leftleft_entry. ub = fom_beta_quotient_pfp_gcd_greatest_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_greatest_bezout_leftleft)) * uc) + (fom_value_pfp_gcd_greatest_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_greatest_bezout_leftleft_value_bound. fom_gap_pfp_gcd_greatest_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_greatest_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_bezout_leftright. (exists fom_gap_pfp_gcd_greatest_bezout_leftright_index_bound. fom_gap_pfp_gcd_greatest_bezout_leftright_index_bound + S (fom_index_pfp_gcd_greatest_bezout_leftright) = L) -> exists fom_value_pfp_gcd_greatest_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_greatest_bezout_leftright_entry. fom_beta_height_pfp_gcd_greatest_bezout_leftright_entry + S (fom_value_pfp_gcd_greatest_bezout_leftright) = S ((S (fom_index_pfp_gcd_greatest_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_greatest_bezout_leftright_entry. ab = fom_beta_quotient_pfp_gcd_greatest_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_greatest_bezout_leftright)) * ac) + (fom_value_pfp_gcd_greatest_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_greatest_bezout_leftright_value_bound. fom_gap_pfp_gcd_greatest_bezout_leftright_value_bound + S (fom_value_pfp_gcd_greatest_bezout_leftright) = p))) /\ (((((((U)=0 \/ (L)=0) /\ (((pfgb_P_gcd_greatest_bezout)=0)))) \/ (((~((U)=0)) /\ (((~((L)=0)) /\ (((U)+(L)=S (pfgb_P_gcd_greatest_bezout)))))))) /\ ((forall pfc_index_gcd_greatest_bezout_leftcoefficients. (exists pfa_gap_gcd_greatest_bezout_leftcoefficientsbound. pfa_gap_gcd_greatest_bezout_leftcoefficientsbound + S (pfc_index_gcd_greatest_bezout_leftcoefficients) = (pfgb_P_gcd_greatest_bezout)) -> exists pfc_value_gcd_greatest_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_greatest_bezout_leftcoefficientsentry. ff_h_pfp_gcd_greatest_bezout_leftcoefficientsentry + S (pfc_value_gcd_greatest_bezout_leftcoefficients) = S ((S (pfc_index_gcd_greatest_bezout_leftcoefficients)) * pfgb_pc_gcd_greatest_bezout)) /\ exists ff_q_pfp_gcd_greatest_bezout_leftcoefficientsentry. pfgb_pb_gcd_greatest_bezout = ff_q_pfp_gcd_greatest_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_greatest_bezout_leftcoefficients)) * pfgb_pc_gcd_greatest_bezout) + (pfc_value_gcd_greatest_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_greatest_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_greatest_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_bezout_leftcoefficients))) -> exists pfc_value_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal) = (U)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal)) * uc) + (pfc_left_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(U)=(pfc_index_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_bezout_leftcoefficients))) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_bezout_leftcoefficients))) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_greatest_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_greatest_bezout_rightleft. (exists fom_gap_pfp_gcd_greatest_bezout_rightleft_index_bound. fom_gap_pfp_gcd_greatest_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_greatest_bezout_rightleft) = V) -> exists fom_value_pfp_gcd_greatest_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_greatest_bezout_rightleft_entry. fom_beta_height_pfp_gcd_greatest_bezout_rightleft_entry + S (fom_value_pfp_gcd_greatest_bezout_rightleft) = S ((S (fom_index_pfp_gcd_greatest_bezout_rightleft)) * vc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_bezout_rightleft_entry. vb = fom_beta_quotient_pfp_gcd_greatest_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_greatest_bezout_rightleft)) * vc) + (fom_value_pfp_gcd_greatest_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_greatest_bezout_rightleft_value_bound. fom_gap_pfp_gcd_greatest_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_greatest_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_bezout_rightright. (exists fom_gap_pfp_gcd_greatest_bezout_rightright_index_bound. fom_gap_pfp_gcd_greatest_bezout_rightright_index_bound + S (fom_index_pfp_gcd_greatest_bezout_rightright) = M) -> exists fom_value_pfp_gcd_greatest_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_greatest_bezout_rightright_entry. fom_beta_height_pfp_gcd_greatest_bezout_rightright_entry + S (fom_value_pfp_gcd_greatest_bezout_rightright) = S ((S (fom_index_pfp_gcd_greatest_bezout_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_bezout_rightright_entry. bb = fom_beta_quotient_pfp_gcd_greatest_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_greatest_bezout_rightright)) * bc) + (fom_value_pfp_gcd_greatest_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_greatest_bezout_rightright_value_bound. fom_gap_pfp_gcd_greatest_bezout_rightright_value_bound + S (fom_value_pfp_gcd_greatest_bezout_rightright) = p))) /\ (((((((V)=0 \/ (M)=0) /\ (((pfgb_Q_gcd_greatest_bezout)=0)))) \/ (((~((V)=0)) /\ (((~((M)=0)) /\ (((V)+(M)=S (pfgb_Q_gcd_greatest_bezout)))))))) /\ ((forall pfc_index_gcd_greatest_bezout_rightcoefficients. (exists pfa_gap_gcd_greatest_bezout_rightcoefficientsbound. pfa_gap_gcd_greatest_bezout_rightcoefficientsbound + S (pfc_index_gcd_greatest_bezout_rightcoefficients) = (pfgb_Q_gcd_greatest_bezout)) -> exists pfc_value_gcd_greatest_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_greatest_bezout_rightcoefficientsentry. ff_h_pfp_gcd_greatest_bezout_rightcoefficientsentry + S (pfc_value_gcd_greatest_bezout_rightcoefficients) = S ((S (pfc_index_gcd_greatest_bezout_rightcoefficients)) * pfgb_qc_gcd_greatest_bezout)) /\ exists ff_q_pfp_gcd_greatest_bezout_rightcoefficientsentry. pfgb_qb_gcd_greatest_bezout = ff_q_pfp_gcd_greatest_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_greatest_bezout_rightcoefficients)) * pfgb_qc_gcd_greatest_bezout) + (pfc_value_gcd_greatest_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_greatest_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_greatest_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_bezout_rightcoefficients))) -> exists pfc_value_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal) = (V)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal)) * vc) + (pfc_left_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(V)=(pfc_index_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_bezout_rightcoefficients))) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_bezout_rightcoefficients))) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_greatest_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_greatest_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_greatest_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_greatest_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_greatest_bezout_sum_left_bounded) = pfgb_P_gcd_greatest_bezout) -> exists fom_value_pfp_gcd_greatest_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_greatest_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_greatest_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_greatest_bezout_sum_left_bounded)) * pfgb_pc_gcd_greatest_bezout)) /\ exists fom_beta_quotient_pfp_gcd_greatest_bezout_sum_left_bounded_entry. pfgb_pb_gcd_greatest_bezout = fom_beta_quotient_pfp_gcd_greatest_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_bezout_sum_left_bounded)) * pfgb_pc_gcd_greatest_bezout) + (fom_value_pfp_gcd_greatest_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_greatest_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_greatest_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_greatest_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_greatest_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_greatest_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_greatest_bezout_sum_right_bounded) = pfgb_Q_gcd_greatest_bezout) -> exists fom_value_pfp_gcd_greatest_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_greatest_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_greatest_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_greatest_bezout_sum_right_bounded)) * pfgb_qc_gcd_greatest_bezout)) /\ exists fom_beta_quotient_pfp_gcd_greatest_bezout_sum_right_bounded_entry. pfgb_qb_gcd_greatest_bezout = fom_beta_quotient_pfp_gcd_greatest_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_bezout_sum_right_bounded)) * pfgb_qc_gcd_greatest_bezout) + (fom_value_pfp_gcd_greatest_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_greatest_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_greatest_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_greatest_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_greatest_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_greatest_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_greatest_bezout_sum_result_bounded) = G) -> exists fom_value_pfp_gcd_greatest_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_greatest_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_greatest_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_greatest_bezout_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_bezout_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_gcd_greatest_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_bezout_sum_result_bounded)) * gc) + (fom_value_pfp_gcd_greatest_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_greatest_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_greatest_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_greatest_bezout_sum pfga_uc_gcd_greatest_bezout_sum pfga_vb_gcd_greatest_bezout_sum pfga_vc_gcd_greatest_bezout_sum pfga_tb_gcd_greatest_bezout_sum pfga_tc_gcd_greatest_bezout_sum pfga_K_gcd_greatest_bezout_sum. ((((forall pfrep_power_gcd_greatest_bezout_sum_left pfrep_left_gcd_greatest_bezout_sum_left pfrep_right_gcd_greatest_bezout_sum_left. ((exists pfrep_position_gcd_greatest_bezout_sum_leftfirst. ((pfrep_position_gcd_greatest_bezout_sum_leftfirst+S (pfrep_power_gcd_greatest_bezout_sum_left)=(pfgb_P_gcd_greatest_bezout)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_sum_leftfirstentry. ff_h_pfp_gcd_greatest_bezout_sum_leftfirstentry + S (pfrep_left_gcd_greatest_bezout_sum_left) = S ((S (pfrep_position_gcd_greatest_bezout_sum_leftfirst)) * pfgb_pc_gcd_greatest_bezout)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_leftfirstentry. pfgb_pb_gcd_greatest_bezout = ff_q_pfp_gcd_greatest_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_greatest_bezout_sum_leftfirst)) * pfgb_pc_gcd_greatest_bezout) + (pfrep_left_gcd_greatest_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_greatest_bezout_sum_leftfirstoutside. pfrep_gap_gcd_greatest_bezout_sum_leftfirstoutside+(pfgb_P_gcd_greatest_bezout)=(pfrep_power_gcd_greatest_bezout_sum_left)) /\ (((pfrep_left_gcd_greatest_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_greatest_bezout_sum_leftsecond. ((pfrep_position_gcd_greatest_bezout_sum_leftsecond+S (pfrep_power_gcd_greatest_bezout_sum_left)=(pfga_K_gcd_greatest_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_sum_leftsecondentry. ff_h_pfp_gcd_greatest_bezout_sum_leftsecondentry + S (pfrep_right_gcd_greatest_bezout_sum_left) = S ((S (pfrep_position_gcd_greatest_bezout_sum_leftsecond)) * pfga_uc_gcd_greatest_bezout_sum)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_leftsecondentry. pfga_ub_gcd_greatest_bezout_sum = ff_q_pfp_gcd_greatest_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_greatest_bezout_sum_leftsecond)) * pfga_uc_gcd_greatest_bezout_sum) + (pfrep_right_gcd_greatest_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_greatest_bezout_sum_leftsecondoutside. pfrep_gap_gcd_greatest_bezout_sum_leftsecondoutside+(pfga_K_gcd_greatest_bezout_sum)=(pfrep_power_gcd_greatest_bezout_sum_left)) /\ (((pfrep_right_gcd_greatest_bezout_sum_left)=0))))) -> pfrep_left_gcd_greatest_bezout_sum_left=pfrep_right_gcd_greatest_bezout_sum_left) /\ ((forall pfrep_power_gcd_greatest_bezout_sum_right pfrep_left_gcd_greatest_bezout_sum_right pfrep_right_gcd_greatest_bezout_sum_right. ((exists pfrep_position_gcd_greatest_bezout_sum_rightfirst. ((pfrep_position_gcd_greatest_bezout_sum_rightfirst+S (pfrep_power_gcd_greatest_bezout_sum_right)=(pfgb_Q_gcd_greatest_bezout)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_sum_rightfirstentry. ff_h_pfp_gcd_greatest_bezout_sum_rightfirstentry + S (pfrep_left_gcd_greatest_bezout_sum_right) = S ((S (pfrep_position_gcd_greatest_bezout_sum_rightfirst)) * pfgb_qc_gcd_greatest_bezout)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_rightfirstentry. pfgb_qb_gcd_greatest_bezout = ff_q_pfp_gcd_greatest_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_greatest_bezout_sum_rightfirst)) * pfgb_qc_gcd_greatest_bezout) + (pfrep_left_gcd_greatest_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_greatest_bezout_sum_rightfirstoutside. pfrep_gap_gcd_greatest_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_greatest_bezout)=(pfrep_power_gcd_greatest_bezout_sum_right)) /\ (((pfrep_left_gcd_greatest_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_greatest_bezout_sum_rightsecond. ((pfrep_position_gcd_greatest_bezout_sum_rightsecond+S (pfrep_power_gcd_greatest_bezout_sum_right)=(pfga_K_gcd_greatest_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_sum_rightsecondentry. ff_h_pfp_gcd_greatest_bezout_sum_rightsecondentry + S (pfrep_right_gcd_greatest_bezout_sum_right) = S ((S (pfrep_position_gcd_greatest_bezout_sum_rightsecond)) * pfga_vc_gcd_greatest_bezout_sum)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_rightsecondentry. pfga_vb_gcd_greatest_bezout_sum = ff_q_pfp_gcd_greatest_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_greatest_bezout_sum_rightsecond)) * pfga_vc_gcd_greatest_bezout_sum) + (pfrep_right_gcd_greatest_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_greatest_bezout_sum_rightsecondoutside. pfrep_gap_gcd_greatest_bezout_sum_rightsecondoutside+(pfga_K_gcd_greatest_bezout_sum)=(pfrep_power_gcd_greatest_bezout_sum_right)) /\ (((pfrep_right_gcd_greatest_bezout_sum_right)=0))))) -> pfrep_left_gcd_greatest_bezout_sum_right=pfrep_right_gcd_greatest_bezout_sum_right)))) /\ (((forall pfp_index_gcd_greatest_bezout_sum_add. (exists pfa_gap_gcd_greatest_bezout_sum_addindex. pfa_gap_gcd_greatest_bezout_sum_addindex + S (pfp_index_gcd_greatest_bezout_sum_add) = (pfga_K_gcd_greatest_bezout_sum)) -> exists pfp_left_gcd_greatest_bezout_sum_add pfp_right_gcd_greatest_bezout_sum_add pfp_value_gcd_greatest_bezout_sum_add. ((((exists ff_h_pfp_gcd_greatest_bezout_sum_addleft. ff_h_pfp_gcd_greatest_bezout_sum_addleft + S (pfp_left_gcd_greatest_bezout_sum_add) = S ((S (pfp_index_gcd_greatest_bezout_sum_add)) * pfga_uc_gcd_greatest_bezout_sum)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_addleft. pfga_ub_gcd_greatest_bezout_sum = ff_q_pfp_gcd_greatest_bezout_sum_addleft * S ((S (pfp_index_gcd_greatest_bezout_sum_add)) * pfga_uc_gcd_greatest_bezout_sum) + (pfp_left_gcd_greatest_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_greatest_bezout_sum_addright. ff_h_pfp_gcd_greatest_bezout_sum_addright + S (pfp_right_gcd_greatest_bezout_sum_add) = S ((S (pfp_index_gcd_greatest_bezout_sum_add)) * pfga_vc_gcd_greatest_bezout_sum)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_addright. pfga_vb_gcd_greatest_bezout_sum = ff_q_pfp_gcd_greatest_bezout_sum_addright * S ((S (pfp_index_gcd_greatest_bezout_sum_add)) * pfga_vc_gcd_greatest_bezout_sum) + (pfp_right_gcd_greatest_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_greatest_bezout_sum_addtarget. ff_h_pfp_gcd_greatest_bezout_sum_addtarget + S (pfp_value_gcd_greatest_bezout_sum_add) = S ((S (pfp_index_gcd_greatest_bezout_sum_add)) * pfga_tc_gcd_greatest_bezout_sum)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_addtarget. pfga_tb_gcd_greatest_bezout_sum = ff_q_pfp_gcd_greatest_bezout_sum_addtarget * S ((S (pfp_index_gcd_greatest_bezout_sum_add)) * pfga_tc_gcd_greatest_bezout_sum) + (pfp_value_gcd_greatest_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_greatest_bezout_sum_addoperationleft. pfa_gap_gcd_greatest_bezout_sum_addoperationleft + S (pfp_left_gcd_greatest_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_greatest_bezout_sum_addoperationright. pfa_gap_gcd_greatest_bezout_sum_addoperationright + S (pfp_right_gcd_greatest_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_greatest_bezout_sum_addoperationresultbound. pfa_gap_gcd_greatest_bezout_sum_addoperationresultbound + S (pfp_value_gcd_greatest_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_greatest_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_greatest_bezout_sum_add) + (pfp_right_gcd_greatest_bezout_sum_add)) + (p) * pfa_offset_left_gcd_greatest_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_greatest_bezout_sum_add) + (p) * pfa_offset_right_gcd_greatest_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_bezout_sum_result pfrep_left_gcd_greatest_bezout_sum_result pfrep_right_gcd_greatest_bezout_sum_result. ((exists pfrep_position_gcd_greatest_bezout_sum_resultfirst. ((pfrep_position_gcd_greatest_bezout_sum_resultfirst+S (pfrep_power_gcd_greatest_bezout_sum_result)=(pfga_K_gcd_greatest_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_sum_resultfirstentry. ff_h_pfp_gcd_greatest_bezout_sum_resultfirstentry + S (pfrep_left_gcd_greatest_bezout_sum_result) = S ((S (pfrep_position_gcd_greatest_bezout_sum_resultfirst)) * pfga_tc_gcd_greatest_bezout_sum)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_resultfirstentry. pfga_tb_gcd_greatest_bezout_sum = ff_q_pfp_gcd_greatest_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_greatest_bezout_sum_resultfirst)) * pfga_tc_gcd_greatest_bezout_sum) + (pfrep_left_gcd_greatest_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_greatest_bezout_sum_resultfirstoutside. pfrep_gap_gcd_greatest_bezout_sum_resultfirstoutside+(pfga_K_gcd_greatest_bezout_sum)=(pfrep_power_gcd_greatest_bezout_sum_result)) /\ (((pfrep_left_gcd_greatest_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_greatest_bezout_sum_resultsecond. ((pfrep_position_gcd_greatest_bezout_sum_resultsecond+S (pfrep_power_gcd_greatest_bezout_sum_result)=(G)) /\ ((((exists ff_h_pfp_gcd_greatest_bezout_sum_resultsecondentry. ff_h_pfp_gcd_greatest_bezout_sum_resultsecondentry + S (pfrep_right_gcd_greatest_bezout_sum_result) = S ((S (pfrep_position_gcd_greatest_bezout_sum_resultsecond)) * gc)) /\ exists ff_q_pfp_gcd_greatest_bezout_sum_resultsecondentry. gb = ff_q_pfp_gcd_greatest_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_greatest_bezout_sum_resultsecond)) * gc) + (pfrep_right_gcd_greatest_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_greatest_bezout_sum_resultsecondoutside. pfrep_gap_gcd_greatest_bezout_sum_resultsecondoutside+(G)=(pfrep_power_gcd_greatest_bezout_sum_result)) /\ (((pfrep_right_gcd_greatest_bezout_sum_result)=0))))) -> pfrep_left_gcd_greatest_bezout_sum_result=pfrep_right_gcd_greatest_bezout_sum_result)))))))))))))))))) -> (((((((forall fom_index_pfp_gcd_greatest_result_common_left_bounded. (exists fom_gap_pfp_gcd_greatest_result_common_left_bounded_index_bound. fom_gap_pfp_gcd_greatest_result_common_left_bounded_index_bound + S (fom_index_pfp_gcd_greatest_result_common_left_bounded) = L) -> exists fom_value_pfp_gcd_greatest_result_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_result_common_left_bounded_entry. fom_beta_height_pfp_gcd_greatest_result_common_left_bounded_entry + S (fom_value_pfp_gcd_greatest_result_common_left_bounded) = S ((S (fom_index_pfp_gcd_greatest_result_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_greatest_result_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_result_common_left_bounded)) * ac) + (fom_value_pfp_gcd_greatest_result_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_result_common_left_bounded_value_bound. fom_gap_pfp_gcd_greatest_result_common_left_bounded_value_bound + S (fom_value_pfp_gcd_greatest_result_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_greatest_result_common_left pfgd_qc_gcd_greatest_result_common_left pfgd_Q_gcd_greatest_result_common_left pfgd_pb_gcd_greatest_result_common_left pfgd_pc_gcd_greatest_result_common_left pfgd_P_gcd_greatest_result_common_left. ((((forall fom_index_pfp_gcd_greatest_result_common_left_productleft. (exists fom_gap_pfp_gcd_greatest_result_common_left_productleft_index_bound. fom_gap_pfp_gcd_greatest_result_common_left_productleft_index_bound + S (fom_index_pfp_gcd_greatest_result_common_left_productleft) = pfgd_Q_gcd_greatest_result_common_left) -> exists fom_value_pfp_gcd_greatest_result_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_greatest_result_common_left_productleft_entry. fom_beta_height_pfp_gcd_greatest_result_common_left_productleft_entry + S (fom_value_pfp_gcd_greatest_result_common_left_productleft) = S ((S (fom_index_pfp_gcd_greatest_result_common_left_productleft)) * pfgd_qc_gcd_greatest_result_common_left)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_common_left_productleft_entry. pfgd_qb_gcd_greatest_result_common_left = fom_beta_quotient_pfp_gcd_greatest_result_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_greatest_result_common_left_productleft)) * pfgd_qc_gcd_greatest_result_common_left) + (fom_value_pfp_gcd_greatest_result_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_greatest_result_common_left_productleft_value_bound. fom_gap_pfp_gcd_greatest_result_common_left_productleft_value_bound + S (fom_value_pfp_gcd_greatest_result_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_result_common_left_productright. (exists fom_gap_pfp_gcd_greatest_result_common_left_productright_index_bound. fom_gap_pfp_gcd_greatest_result_common_left_productright_index_bound + S (fom_index_pfp_gcd_greatest_result_common_left_productright) = G) -> exists fom_value_pfp_gcd_greatest_result_common_left_productright. ((((exists fom_beta_height_pfp_gcd_greatest_result_common_left_productright_entry. fom_beta_height_pfp_gcd_greatest_result_common_left_productright_entry + S (fom_value_pfp_gcd_greatest_result_common_left_productright) = S ((S (fom_index_pfp_gcd_greatest_result_common_left_productright)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_common_left_productright_entry. gb = fom_beta_quotient_pfp_gcd_greatest_result_common_left_productright_entry * S ((S (fom_index_pfp_gcd_greatest_result_common_left_productright)) * gc) + (fom_value_pfp_gcd_greatest_result_common_left_productright))) /\ (exists fom_gap_pfp_gcd_greatest_result_common_left_productright_value_bound. fom_gap_pfp_gcd_greatest_result_common_left_productright_value_bound + S (fom_value_pfp_gcd_greatest_result_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_greatest_result_common_left)=0 \/ (G)=0) /\ (((pfgd_P_gcd_greatest_result_common_left)=0)))) \/ (((~((pfgd_Q_gcd_greatest_result_common_left)=0)) /\ (((~((G)=0)) /\ (((pfgd_Q_gcd_greatest_result_common_left)+(G)=S (pfgd_P_gcd_greatest_result_common_left)))))))) /\ ((forall pfc_index_gcd_greatest_result_common_left_productcoefficients. (exists pfa_gap_gcd_greatest_result_common_left_productcoefficientsbound. pfa_gap_gcd_greatest_result_common_left_productcoefficientsbound + S (pfc_index_gcd_greatest_result_common_left_productcoefficients) = (pfgd_P_gcd_greatest_result_common_left)) -> exists pfc_value_gcd_greatest_result_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_greatest_result_common_left_productcoefficientsentry. ff_h_pfp_gcd_greatest_result_common_left_productcoefficientsentry + S (pfc_value_gcd_greatest_result_common_left_productcoefficients) = S ((S (pfc_index_gcd_greatest_result_common_left_productcoefficients)) * pfgd_pc_gcd_greatest_result_common_left)) /\ exists ff_q_pfp_gcd_greatest_result_common_left_productcoefficientsentry. pfgd_pb_gcd_greatest_result_common_left = ff_q_pfp_gcd_greatest_result_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_greatest_result_common_left_productcoefficients)) * pfgd_pc_gcd_greatest_result_common_left) + (pfc_value_gcd_greatest_result_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_result_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_greatest_result_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_greatest_result_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_result_common_left_productcoefficients))) -> exists pfc_value_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_result_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_common_left_productcoefficientscoefficient) + (pfc_value_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_result_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_greatest_result_common_left)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_common_left)) /\ exists ff_q_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_greatest_result_common_left = ff_q_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_common_left) + (pfc_left_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_greatest_result_common_left)=(pfc_index_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_result_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_result_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_result_common_left_productcoefficients))) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_result_common_left_productcoefficients))) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_result_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_result_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_result_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_result_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_result_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_result_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_result_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_result_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_result_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_result_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_result_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_greatest_result_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_result_common_left_equivalent pfrep_left_gcd_greatest_result_common_left_equivalent pfrep_right_gcd_greatest_result_common_left_equivalent. ((exists pfrep_position_gcd_greatest_result_common_left_equivalentfirst. ((pfrep_position_gcd_greatest_result_common_left_equivalentfirst+S (pfrep_power_gcd_greatest_result_common_left_equivalent)=(pfgd_P_gcd_greatest_result_common_left)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_left_equivalentfirstentry. ff_h_pfp_gcd_greatest_result_common_left_equivalentfirstentry + S (pfrep_left_gcd_greatest_result_common_left_equivalent) = S ((S (pfrep_position_gcd_greatest_result_common_left_equivalentfirst)) * pfgd_pc_gcd_greatest_result_common_left)) /\ exists ff_q_pfp_gcd_greatest_result_common_left_equivalentfirstentry. pfgd_pb_gcd_greatest_result_common_left = ff_q_pfp_gcd_greatest_result_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_greatest_result_common_left_equivalentfirst)) * pfgd_pc_gcd_greatest_result_common_left) + (pfrep_left_gcd_greatest_result_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_common_left_equivalentfirstoutside. pfrep_gap_gcd_greatest_result_common_left_equivalentfirstoutside+(pfgd_P_gcd_greatest_result_common_left)=(pfrep_power_gcd_greatest_result_common_left_equivalent)) /\ (((pfrep_left_gcd_greatest_result_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_greatest_result_common_left_equivalentsecond. ((pfrep_position_gcd_greatest_result_common_left_equivalentsecond+S (pfrep_power_gcd_greatest_result_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_left_equivalentsecondentry. ff_h_pfp_gcd_greatest_result_common_left_equivalentsecondentry + S (pfrep_right_gcd_greatest_result_common_left_equivalent) = S ((S (pfrep_position_gcd_greatest_result_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_greatest_result_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_greatest_result_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_greatest_result_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_greatest_result_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_common_left_equivalentsecondoutside. pfrep_gap_gcd_greatest_result_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_greatest_result_common_left_equivalent)) /\ (((pfrep_right_gcd_greatest_result_common_left_equivalent)=0))))) -> pfrep_left_gcd_greatest_result_common_left_equivalent=pfrep_right_gcd_greatest_result_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_greatest_result_common_right_bounded. (exists fom_gap_pfp_gcd_greatest_result_common_right_bounded_index_bound. fom_gap_pfp_gcd_greatest_result_common_right_bounded_index_bound + S (fom_index_pfp_gcd_greatest_result_common_right_bounded) = M) -> exists fom_value_pfp_gcd_greatest_result_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_result_common_right_bounded_entry. fom_beta_height_pfp_gcd_greatest_result_common_right_bounded_entry + S (fom_value_pfp_gcd_greatest_result_common_right_bounded) = S ((S (fom_index_pfp_gcd_greatest_result_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_common_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_greatest_result_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_result_common_right_bounded)) * bc) + (fom_value_pfp_gcd_greatest_result_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_result_common_right_bounded_value_bound. fom_gap_pfp_gcd_greatest_result_common_right_bounded_value_bound + S (fom_value_pfp_gcd_greatest_result_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_greatest_result_common_right pfgd_qc_gcd_greatest_result_common_right pfgd_Q_gcd_greatest_result_common_right pfgd_pb_gcd_greatest_result_common_right pfgd_pc_gcd_greatest_result_common_right pfgd_P_gcd_greatest_result_common_right. ((((forall fom_index_pfp_gcd_greatest_result_common_right_productleft. (exists fom_gap_pfp_gcd_greatest_result_common_right_productleft_index_bound. fom_gap_pfp_gcd_greatest_result_common_right_productleft_index_bound + S (fom_index_pfp_gcd_greatest_result_common_right_productleft) = pfgd_Q_gcd_greatest_result_common_right) -> exists fom_value_pfp_gcd_greatest_result_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_greatest_result_common_right_productleft_entry. fom_beta_height_pfp_gcd_greatest_result_common_right_productleft_entry + S (fom_value_pfp_gcd_greatest_result_common_right_productleft) = S ((S (fom_index_pfp_gcd_greatest_result_common_right_productleft)) * pfgd_qc_gcd_greatest_result_common_right)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_common_right_productleft_entry. pfgd_qb_gcd_greatest_result_common_right = fom_beta_quotient_pfp_gcd_greatest_result_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_greatest_result_common_right_productleft)) * pfgd_qc_gcd_greatest_result_common_right) + (fom_value_pfp_gcd_greatest_result_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_greatest_result_common_right_productleft_value_bound. fom_gap_pfp_gcd_greatest_result_common_right_productleft_value_bound + S (fom_value_pfp_gcd_greatest_result_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_result_common_right_productright. (exists fom_gap_pfp_gcd_greatest_result_common_right_productright_index_bound. fom_gap_pfp_gcd_greatest_result_common_right_productright_index_bound + S (fom_index_pfp_gcd_greatest_result_common_right_productright) = G) -> exists fom_value_pfp_gcd_greatest_result_common_right_productright. ((((exists fom_beta_height_pfp_gcd_greatest_result_common_right_productright_entry. fom_beta_height_pfp_gcd_greatest_result_common_right_productright_entry + S (fom_value_pfp_gcd_greatest_result_common_right_productright) = S ((S (fom_index_pfp_gcd_greatest_result_common_right_productright)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_common_right_productright_entry. gb = fom_beta_quotient_pfp_gcd_greatest_result_common_right_productright_entry * S ((S (fom_index_pfp_gcd_greatest_result_common_right_productright)) * gc) + (fom_value_pfp_gcd_greatest_result_common_right_productright))) /\ (exists fom_gap_pfp_gcd_greatest_result_common_right_productright_value_bound. fom_gap_pfp_gcd_greatest_result_common_right_productright_value_bound + S (fom_value_pfp_gcd_greatest_result_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_greatest_result_common_right)=0 \/ (G)=0) /\ (((pfgd_P_gcd_greatest_result_common_right)=0)))) \/ (((~((pfgd_Q_gcd_greatest_result_common_right)=0)) /\ (((~((G)=0)) /\ (((pfgd_Q_gcd_greatest_result_common_right)+(G)=S (pfgd_P_gcd_greatest_result_common_right)))))))) /\ ((forall pfc_index_gcd_greatest_result_common_right_productcoefficients. (exists pfa_gap_gcd_greatest_result_common_right_productcoefficientsbound. pfa_gap_gcd_greatest_result_common_right_productcoefficientsbound + S (pfc_index_gcd_greatest_result_common_right_productcoefficients) = (pfgd_P_gcd_greatest_result_common_right)) -> exists pfc_value_gcd_greatest_result_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_greatest_result_common_right_productcoefficientsentry. ff_h_pfp_gcd_greatest_result_common_right_productcoefficientsentry + S (pfc_value_gcd_greatest_result_common_right_productcoefficients) = S ((S (pfc_index_gcd_greatest_result_common_right_productcoefficients)) * pfgd_pc_gcd_greatest_result_common_right)) /\ exists ff_q_pfp_gcd_greatest_result_common_right_productcoefficientsentry. pfgd_pb_gcd_greatest_result_common_right = ff_q_pfp_gcd_greatest_result_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_greatest_result_common_right_productcoefficients)) * pfgd_pc_gcd_greatest_result_common_right) + (pfc_value_gcd_greatest_result_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_result_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_greatest_result_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_greatest_result_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_result_common_right_productcoefficients))) -> exists pfc_value_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_result_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_common_right_productcoefficientscoefficient) + (pfc_value_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_result_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_greatest_result_common_right)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_common_right)) /\ exists ff_q_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_greatest_result_common_right = ff_q_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_common_right) + (pfc_left_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_greatest_result_common_right)=(pfc_index_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm) = (G)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm)) * gc)) /\ exists ff_q_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightentry. gb = ff_q_pfp_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm)) * gc) + (pfc_right_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(G)=(pfc_complement_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_result_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_result_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_result_common_right_productcoefficients))) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_result_common_right_productcoefficients))) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_result_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_result_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_result_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_result_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_result_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_result_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_result_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_result_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_result_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_result_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_result_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_greatest_result_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_result_common_right_equivalent pfrep_left_gcd_greatest_result_common_right_equivalent pfrep_right_gcd_greatest_result_common_right_equivalent. ((exists pfrep_position_gcd_greatest_result_common_right_equivalentfirst. ((pfrep_position_gcd_greatest_result_common_right_equivalentfirst+S (pfrep_power_gcd_greatest_result_common_right_equivalent)=(pfgd_P_gcd_greatest_result_common_right)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_right_equivalentfirstentry. ff_h_pfp_gcd_greatest_result_common_right_equivalentfirstentry + S (pfrep_left_gcd_greatest_result_common_right_equivalent) = S ((S (pfrep_position_gcd_greatest_result_common_right_equivalentfirst)) * pfgd_pc_gcd_greatest_result_common_right)) /\ exists ff_q_pfp_gcd_greatest_result_common_right_equivalentfirstentry. pfgd_pb_gcd_greatest_result_common_right = ff_q_pfp_gcd_greatest_result_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_greatest_result_common_right_equivalentfirst)) * pfgd_pc_gcd_greatest_result_common_right) + (pfrep_left_gcd_greatest_result_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_common_right_equivalentfirstoutside. pfrep_gap_gcd_greatest_result_common_right_equivalentfirstoutside+(pfgd_P_gcd_greatest_result_common_right)=(pfrep_power_gcd_greatest_result_common_right_equivalent)) /\ (((pfrep_left_gcd_greatest_result_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_greatest_result_common_right_equivalentsecond. ((pfrep_position_gcd_greatest_result_common_right_equivalentsecond+S (pfrep_power_gcd_greatest_result_common_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_gcd_greatest_result_common_right_equivalentsecondentry. ff_h_pfp_gcd_greatest_result_common_right_equivalentsecondentry + S (pfrep_right_gcd_greatest_result_common_right_equivalent) = S ((S (pfrep_position_gcd_greatest_result_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_greatest_result_common_right_equivalentsecondentry. bb = ff_q_pfp_gcd_greatest_result_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_greatest_result_common_right_equivalentsecond)) * bc) + (pfrep_right_gcd_greatest_result_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_common_right_equivalentsecondoutside. pfrep_gap_gcd_greatest_result_common_right_equivalentsecondoutside+(M)=(pfrep_power_gcd_greatest_result_common_right_equivalent)) /\ (((pfrep_right_gcd_greatest_result_common_right_equivalent)=0))))) -> pfrep_left_gcd_greatest_result_common_right_equivalent=pfrep_right_gcd_greatest_result_common_right_equivalent)))))))))) /\ ((forall pfgg_db_gcd_greatest_result pfgg_dc_gcd_greatest_result pfgg_D_gcd_greatest_result. (((((forall fom_index_pfp_gcd_greatest_result_divisor_left_bounded. (exists fom_gap_pfp_gcd_greatest_result_divisor_left_bounded_index_bound. fom_gap_pfp_gcd_greatest_result_divisor_left_bounded_index_bound + S (fom_index_pfp_gcd_greatest_result_divisor_left_bounded) = L) -> exists fom_value_pfp_gcd_greatest_result_divisor_left_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_result_divisor_left_bounded_entry. fom_beta_height_pfp_gcd_greatest_result_divisor_left_bounded_entry + S (fom_value_pfp_gcd_greatest_result_divisor_left_bounded) = S ((S (fom_index_pfp_gcd_greatest_result_divisor_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_divisor_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_greatest_result_divisor_left_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_result_divisor_left_bounded)) * ac) + (fom_value_pfp_gcd_greatest_result_divisor_left_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_result_divisor_left_bounded_value_bound. fom_gap_pfp_gcd_greatest_result_divisor_left_bounded_value_bound + S (fom_value_pfp_gcd_greatest_result_divisor_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_greatest_result_divisor_left pfgd_qc_gcd_greatest_result_divisor_left pfgd_Q_gcd_greatest_result_divisor_left pfgd_pb_gcd_greatest_result_divisor_left pfgd_pc_gcd_greatest_result_divisor_left pfgd_P_gcd_greatest_result_divisor_left. ((((forall fom_index_pfp_gcd_greatest_result_divisor_left_productleft. (exists fom_gap_pfp_gcd_greatest_result_divisor_left_productleft_index_bound. fom_gap_pfp_gcd_greatest_result_divisor_left_productleft_index_bound + S (fom_index_pfp_gcd_greatest_result_divisor_left_productleft) = pfgd_Q_gcd_greatest_result_divisor_left) -> exists fom_value_pfp_gcd_greatest_result_divisor_left_productleft. ((((exists fom_beta_height_pfp_gcd_greatest_result_divisor_left_productleft_entry. fom_beta_height_pfp_gcd_greatest_result_divisor_left_productleft_entry + S (fom_value_pfp_gcd_greatest_result_divisor_left_productleft) = S ((S (fom_index_pfp_gcd_greatest_result_divisor_left_productleft)) * pfgd_qc_gcd_greatest_result_divisor_left)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_divisor_left_productleft_entry. pfgd_qb_gcd_greatest_result_divisor_left = fom_beta_quotient_pfp_gcd_greatest_result_divisor_left_productleft_entry * S ((S (fom_index_pfp_gcd_greatest_result_divisor_left_productleft)) * pfgd_qc_gcd_greatest_result_divisor_left) + (fom_value_pfp_gcd_greatest_result_divisor_left_productleft))) /\ (exists fom_gap_pfp_gcd_greatest_result_divisor_left_productleft_value_bound. fom_gap_pfp_gcd_greatest_result_divisor_left_productleft_value_bound + S (fom_value_pfp_gcd_greatest_result_divisor_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_result_divisor_left_productright. (exists fom_gap_pfp_gcd_greatest_result_divisor_left_productright_index_bound. fom_gap_pfp_gcd_greatest_result_divisor_left_productright_index_bound + S (fom_index_pfp_gcd_greatest_result_divisor_left_productright) = pfgg_D_gcd_greatest_result) -> exists fom_value_pfp_gcd_greatest_result_divisor_left_productright. ((((exists fom_beta_height_pfp_gcd_greatest_result_divisor_left_productright_entry. fom_beta_height_pfp_gcd_greatest_result_divisor_left_productright_entry + S (fom_value_pfp_gcd_greatest_result_divisor_left_productright) = S ((S (fom_index_pfp_gcd_greatest_result_divisor_left_productright)) * pfgg_dc_gcd_greatest_result)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_divisor_left_productright_entry. pfgg_db_gcd_greatest_result = fom_beta_quotient_pfp_gcd_greatest_result_divisor_left_productright_entry * S ((S (fom_index_pfp_gcd_greatest_result_divisor_left_productright)) * pfgg_dc_gcd_greatest_result) + (fom_value_pfp_gcd_greatest_result_divisor_left_productright))) /\ (exists fom_gap_pfp_gcd_greatest_result_divisor_left_productright_value_bound. fom_gap_pfp_gcd_greatest_result_divisor_left_productright_value_bound + S (fom_value_pfp_gcd_greatest_result_divisor_left_productright) = p))) /\ (((((((pfgd_Q_gcd_greatest_result_divisor_left)=0 \/ (pfgg_D_gcd_greatest_result)=0) /\ (((pfgd_P_gcd_greatest_result_divisor_left)=0)))) \/ (((~((pfgd_Q_gcd_greatest_result_divisor_left)=0)) /\ (((~((pfgg_D_gcd_greatest_result)=0)) /\ (((pfgd_Q_gcd_greatest_result_divisor_left)+(pfgg_D_gcd_greatest_result)=S (pfgd_P_gcd_greatest_result_divisor_left)))))))) /\ ((forall pfc_index_gcd_greatest_result_divisor_left_productcoefficients. (exists pfa_gap_gcd_greatest_result_divisor_left_productcoefficientsbound. pfa_gap_gcd_greatest_result_divisor_left_productcoefficientsbound + S (pfc_index_gcd_greatest_result_divisor_left_productcoefficients) = (pfgd_P_gcd_greatest_result_divisor_left)) -> exists pfc_value_gcd_greatest_result_divisor_left_productcoefficients. ((((exists ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientsentry. ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientsentry + S (pfc_value_gcd_greatest_result_divisor_left_productcoefficients) = S ((S (pfc_index_gcd_greatest_result_divisor_left_productcoefficients)) * pfgd_pc_gcd_greatest_result_divisor_left)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientsentry. pfgd_pb_gcd_greatest_result_divisor_left = ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientsentry * S ((S (pfc_index_gcd_greatest_result_divisor_left_productcoefficients)) * pfgd_pc_gcd_greatest_result_divisor_left) + (pfc_value_gcd_greatest_result_divisor_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_result_divisor_left_productcoefficientscoefficient pfc_terms_scale_gcd_greatest_result_divisor_left_productcoefficientscoefficient pfc_natural_sum_gcd_greatest_result_divisor_left_productcoefficientscoefficient. ((forall pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_result_divisor_left_productcoefficients))) -> exists pfc_value_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_divisor_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_result_divisor_left_productcoefficientscoefficient = ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_divisor_left_productcoefficientscoefficient) + (pfc_value_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_result_divisor_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_greatest_result_divisor_left)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_divisor_left)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_greatest_result_divisor_left = ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_divisor_left) + (pfc_left_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_greatest_result_divisor_left)=(pfc_index_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm) = (pfgg_D_gcd_greatest_result)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_gcd_greatest_result)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightentry. pfgg_db_gcd_greatest_result = ff_q_pfp_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_gcd_greatest_result) + (pfc_right_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgg_D_gcd_greatest_result)=(pfc_complement_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_result_divisor_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_result_divisor_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_result_divisor_left_productcoefficients))) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_result_divisor_left_productcoefficients))) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_result_divisor_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_result_divisor_left_productcoefficients)) -> exists fs_a_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_divisor_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_result_divisor_left_productcoefficientscoefficient = fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_divisor_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_result_divisor_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_result_divisor_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_result_divisor_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_result_divisor_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_result_divisor_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_result_divisor_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_result_divisor_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_result_divisor_left_productcoefficients) + (p) * pfa_offset_right_gcd_greatest_result_divisor_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_result_divisor_left_equivalent pfrep_left_gcd_greatest_result_divisor_left_equivalent pfrep_right_gcd_greatest_result_divisor_left_equivalent. ((exists pfrep_position_gcd_greatest_result_divisor_left_equivalentfirst. ((pfrep_position_gcd_greatest_result_divisor_left_equivalentfirst+S (pfrep_power_gcd_greatest_result_divisor_left_equivalent)=(pfgd_P_gcd_greatest_result_divisor_left)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_left_equivalentfirstentry. ff_h_pfp_gcd_greatest_result_divisor_left_equivalentfirstentry + S (pfrep_left_gcd_greatest_result_divisor_left_equivalent) = S ((S (pfrep_position_gcd_greatest_result_divisor_left_equivalentfirst)) * pfgd_pc_gcd_greatest_result_divisor_left)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_left_equivalentfirstentry. pfgd_pb_gcd_greatest_result_divisor_left = ff_q_pfp_gcd_greatest_result_divisor_left_equivalentfirstentry * S ((S (pfrep_position_gcd_greatest_result_divisor_left_equivalentfirst)) * pfgd_pc_gcd_greatest_result_divisor_left) + (pfrep_left_gcd_greatest_result_divisor_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_divisor_left_equivalentfirstoutside. pfrep_gap_gcd_greatest_result_divisor_left_equivalentfirstoutside+(pfgd_P_gcd_greatest_result_divisor_left)=(pfrep_power_gcd_greatest_result_divisor_left_equivalent)) /\ (((pfrep_left_gcd_greatest_result_divisor_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_greatest_result_divisor_left_equivalentsecond. ((pfrep_position_gcd_greatest_result_divisor_left_equivalentsecond+S (pfrep_power_gcd_greatest_result_divisor_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_left_equivalentsecondentry. ff_h_pfp_gcd_greatest_result_divisor_left_equivalentsecondentry + S (pfrep_right_gcd_greatest_result_divisor_left_equivalent) = S ((S (pfrep_position_gcd_greatest_result_divisor_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_left_equivalentsecondentry. ab = ff_q_pfp_gcd_greatest_result_divisor_left_equivalentsecondentry * S ((S (pfrep_position_gcd_greatest_result_divisor_left_equivalentsecond)) * ac) + (pfrep_right_gcd_greatest_result_divisor_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_divisor_left_equivalentsecondoutside. pfrep_gap_gcd_greatest_result_divisor_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_greatest_result_divisor_left_equivalent)) /\ (((pfrep_right_gcd_greatest_result_divisor_left_equivalent)=0))))) -> pfrep_left_gcd_greatest_result_divisor_left_equivalent=pfrep_right_gcd_greatest_result_divisor_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_greatest_result_divisor_right_bounded. (exists fom_gap_pfp_gcd_greatest_result_divisor_right_bounded_index_bound. fom_gap_pfp_gcd_greatest_result_divisor_right_bounded_index_bound + S (fom_index_pfp_gcd_greatest_result_divisor_right_bounded) = M) -> exists fom_value_pfp_gcd_greatest_result_divisor_right_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_result_divisor_right_bounded_entry. fom_beta_height_pfp_gcd_greatest_result_divisor_right_bounded_entry + S (fom_value_pfp_gcd_greatest_result_divisor_right_bounded) = S ((S (fom_index_pfp_gcd_greatest_result_divisor_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_divisor_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_greatest_result_divisor_right_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_result_divisor_right_bounded)) * bc) + (fom_value_pfp_gcd_greatest_result_divisor_right_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_result_divisor_right_bounded_value_bound. fom_gap_pfp_gcd_greatest_result_divisor_right_bounded_value_bound + S (fom_value_pfp_gcd_greatest_result_divisor_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_greatest_result_divisor_right pfgd_qc_gcd_greatest_result_divisor_right pfgd_Q_gcd_greatest_result_divisor_right pfgd_pb_gcd_greatest_result_divisor_right pfgd_pc_gcd_greatest_result_divisor_right pfgd_P_gcd_greatest_result_divisor_right. ((((forall fom_index_pfp_gcd_greatest_result_divisor_right_productleft. (exists fom_gap_pfp_gcd_greatest_result_divisor_right_productleft_index_bound. fom_gap_pfp_gcd_greatest_result_divisor_right_productleft_index_bound + S (fom_index_pfp_gcd_greatest_result_divisor_right_productleft) = pfgd_Q_gcd_greatest_result_divisor_right) -> exists fom_value_pfp_gcd_greatest_result_divisor_right_productleft. ((((exists fom_beta_height_pfp_gcd_greatest_result_divisor_right_productleft_entry. fom_beta_height_pfp_gcd_greatest_result_divisor_right_productleft_entry + S (fom_value_pfp_gcd_greatest_result_divisor_right_productleft) = S ((S (fom_index_pfp_gcd_greatest_result_divisor_right_productleft)) * pfgd_qc_gcd_greatest_result_divisor_right)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_divisor_right_productleft_entry. pfgd_qb_gcd_greatest_result_divisor_right = fom_beta_quotient_pfp_gcd_greatest_result_divisor_right_productleft_entry * S ((S (fom_index_pfp_gcd_greatest_result_divisor_right_productleft)) * pfgd_qc_gcd_greatest_result_divisor_right) + (fom_value_pfp_gcd_greatest_result_divisor_right_productleft))) /\ (exists fom_gap_pfp_gcd_greatest_result_divisor_right_productleft_value_bound. fom_gap_pfp_gcd_greatest_result_divisor_right_productleft_value_bound + S (fom_value_pfp_gcd_greatest_result_divisor_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_result_divisor_right_productright. (exists fom_gap_pfp_gcd_greatest_result_divisor_right_productright_index_bound. fom_gap_pfp_gcd_greatest_result_divisor_right_productright_index_bound + S (fom_index_pfp_gcd_greatest_result_divisor_right_productright) = pfgg_D_gcd_greatest_result) -> exists fom_value_pfp_gcd_greatest_result_divisor_right_productright. ((((exists fom_beta_height_pfp_gcd_greatest_result_divisor_right_productright_entry. fom_beta_height_pfp_gcd_greatest_result_divisor_right_productright_entry + S (fom_value_pfp_gcd_greatest_result_divisor_right_productright) = S ((S (fom_index_pfp_gcd_greatest_result_divisor_right_productright)) * pfgg_dc_gcd_greatest_result)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_divisor_right_productright_entry. pfgg_db_gcd_greatest_result = fom_beta_quotient_pfp_gcd_greatest_result_divisor_right_productright_entry * S ((S (fom_index_pfp_gcd_greatest_result_divisor_right_productright)) * pfgg_dc_gcd_greatest_result) + (fom_value_pfp_gcd_greatest_result_divisor_right_productright))) /\ (exists fom_gap_pfp_gcd_greatest_result_divisor_right_productright_value_bound. fom_gap_pfp_gcd_greatest_result_divisor_right_productright_value_bound + S (fom_value_pfp_gcd_greatest_result_divisor_right_productright) = p))) /\ (((((((pfgd_Q_gcd_greatest_result_divisor_right)=0 \/ (pfgg_D_gcd_greatest_result)=0) /\ (((pfgd_P_gcd_greatest_result_divisor_right)=0)))) \/ (((~((pfgd_Q_gcd_greatest_result_divisor_right)=0)) /\ (((~((pfgg_D_gcd_greatest_result)=0)) /\ (((pfgd_Q_gcd_greatest_result_divisor_right)+(pfgg_D_gcd_greatest_result)=S (pfgd_P_gcd_greatest_result_divisor_right)))))))) /\ ((forall pfc_index_gcd_greatest_result_divisor_right_productcoefficients. (exists pfa_gap_gcd_greatest_result_divisor_right_productcoefficientsbound. pfa_gap_gcd_greatest_result_divisor_right_productcoefficientsbound + S (pfc_index_gcd_greatest_result_divisor_right_productcoefficients) = (pfgd_P_gcd_greatest_result_divisor_right)) -> exists pfc_value_gcd_greatest_result_divisor_right_productcoefficients. ((((exists ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientsentry. ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientsentry + S (pfc_value_gcd_greatest_result_divisor_right_productcoefficients) = S ((S (pfc_index_gcd_greatest_result_divisor_right_productcoefficients)) * pfgd_pc_gcd_greatest_result_divisor_right)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientsentry. pfgd_pb_gcd_greatest_result_divisor_right = ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientsentry * S ((S (pfc_index_gcd_greatest_result_divisor_right_productcoefficients)) * pfgd_pc_gcd_greatest_result_divisor_right) + (pfc_value_gcd_greatest_result_divisor_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_result_divisor_right_productcoefficientscoefficient pfc_terms_scale_gcd_greatest_result_divisor_right_productcoefficientscoefficient pfc_natural_sum_gcd_greatest_result_divisor_right_productcoefficientscoefficient. ((forall pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_result_divisor_right_productcoefficients))) -> exists pfc_value_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_divisor_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_result_divisor_right_productcoefficientscoefficient = ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_divisor_right_productcoefficientscoefficient) + (pfc_value_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_result_divisor_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_greatest_result_divisor_right)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_divisor_right)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_greatest_result_divisor_right = ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_divisor_right) + (pfc_left_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_greatest_result_divisor_right)=(pfc_index_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm) = (pfgg_D_gcd_greatest_result)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_gcd_greatest_result)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightentry. pfgg_db_gcd_greatest_result = ff_q_pfp_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_gcd_greatest_result) + (pfc_right_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgg_D_gcd_greatest_result)=(pfc_complement_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_result_divisor_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_result_divisor_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_result_divisor_right_productcoefficients))) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_result_divisor_right_productcoefficients))) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_result_divisor_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_result_divisor_right_productcoefficients)) -> exists fs_a_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_divisor_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_result_divisor_right_productcoefficientscoefficient = fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_divisor_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_result_divisor_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_result_divisor_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_result_divisor_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_result_divisor_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_result_divisor_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_result_divisor_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_result_divisor_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_result_divisor_right_productcoefficients) + (p) * pfa_offset_right_gcd_greatest_result_divisor_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_result_divisor_right_equivalent pfrep_left_gcd_greatest_result_divisor_right_equivalent pfrep_right_gcd_greatest_result_divisor_right_equivalent. ((exists pfrep_position_gcd_greatest_result_divisor_right_equivalentfirst. ((pfrep_position_gcd_greatest_result_divisor_right_equivalentfirst+S (pfrep_power_gcd_greatest_result_divisor_right_equivalent)=(pfgd_P_gcd_greatest_result_divisor_right)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_right_equivalentfirstentry. ff_h_pfp_gcd_greatest_result_divisor_right_equivalentfirstentry + S (pfrep_left_gcd_greatest_result_divisor_right_equivalent) = S ((S (pfrep_position_gcd_greatest_result_divisor_right_equivalentfirst)) * pfgd_pc_gcd_greatest_result_divisor_right)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_right_equivalentfirstentry. pfgd_pb_gcd_greatest_result_divisor_right = ff_q_pfp_gcd_greatest_result_divisor_right_equivalentfirstentry * S ((S (pfrep_position_gcd_greatest_result_divisor_right_equivalentfirst)) * pfgd_pc_gcd_greatest_result_divisor_right) + (pfrep_left_gcd_greatest_result_divisor_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_divisor_right_equivalentfirstoutside. pfrep_gap_gcd_greatest_result_divisor_right_equivalentfirstoutside+(pfgd_P_gcd_greatest_result_divisor_right)=(pfrep_power_gcd_greatest_result_divisor_right_equivalent)) /\ (((pfrep_left_gcd_greatest_result_divisor_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_greatest_result_divisor_right_equivalentsecond. ((pfrep_position_gcd_greatest_result_divisor_right_equivalentsecond+S (pfrep_power_gcd_greatest_result_divisor_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_gcd_greatest_result_divisor_right_equivalentsecondentry. ff_h_pfp_gcd_greatest_result_divisor_right_equivalentsecondentry + S (pfrep_right_gcd_greatest_result_divisor_right_equivalent) = S ((S (pfrep_position_gcd_greatest_result_divisor_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_greatest_result_divisor_right_equivalentsecondentry. bb = ff_q_pfp_gcd_greatest_result_divisor_right_equivalentsecondentry * S ((S (pfrep_position_gcd_greatest_result_divisor_right_equivalentsecond)) * bc) + (pfrep_right_gcd_greatest_result_divisor_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_divisor_right_equivalentsecondoutside. pfrep_gap_gcd_greatest_result_divisor_right_equivalentsecondoutside+(M)=(pfrep_power_gcd_greatest_result_divisor_right_equivalent)) /\ (((pfrep_right_gcd_greatest_result_divisor_right_equivalent)=0))))) -> pfrep_left_gcd_greatest_result_divisor_right_equivalent=pfrep_right_gcd_greatest_result_divisor_right_equivalent)))))))))) -> (((forall fom_index_pfp_gcd_greatest_result_greatest_bounded. (exists fom_gap_pfp_gcd_greatest_result_greatest_bounded_index_bound. fom_gap_pfp_gcd_greatest_result_greatest_bounded_index_bound + S (fom_index_pfp_gcd_greatest_result_greatest_bounded) = G) -> exists fom_value_pfp_gcd_greatest_result_greatest_bounded. ((((exists fom_beta_height_pfp_gcd_greatest_result_greatest_bounded_entry. fom_beta_height_pfp_gcd_greatest_result_greatest_bounded_entry + S (fom_value_pfp_gcd_greatest_result_greatest_bounded) = S ((S (fom_index_pfp_gcd_greatest_result_greatest_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_greatest_bounded_entry. gb = fom_beta_quotient_pfp_gcd_greatest_result_greatest_bounded_entry * S ((S (fom_index_pfp_gcd_greatest_result_greatest_bounded)) * gc) + (fom_value_pfp_gcd_greatest_result_greatest_bounded))) /\ (exists fom_gap_pfp_gcd_greatest_result_greatest_bounded_value_bound. fom_gap_pfp_gcd_greatest_result_greatest_bounded_value_bound + S (fom_value_pfp_gcd_greatest_result_greatest_bounded) = p))) /\ ((exists pfgd_qb_gcd_greatest_result_greatest pfgd_qc_gcd_greatest_result_greatest pfgd_Q_gcd_greatest_result_greatest pfgd_pb_gcd_greatest_result_greatest pfgd_pc_gcd_greatest_result_greatest pfgd_P_gcd_greatest_result_greatest. ((((forall fom_index_pfp_gcd_greatest_result_greatest_productleft. (exists fom_gap_pfp_gcd_greatest_result_greatest_productleft_index_bound. fom_gap_pfp_gcd_greatest_result_greatest_productleft_index_bound + S (fom_index_pfp_gcd_greatest_result_greatest_productleft) = pfgd_Q_gcd_greatest_result_greatest) -> exists fom_value_pfp_gcd_greatest_result_greatest_productleft. ((((exists fom_beta_height_pfp_gcd_greatest_result_greatest_productleft_entry. fom_beta_height_pfp_gcd_greatest_result_greatest_productleft_entry + S (fom_value_pfp_gcd_greatest_result_greatest_productleft) = S ((S (fom_index_pfp_gcd_greatest_result_greatest_productleft)) * pfgd_qc_gcd_greatest_result_greatest)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_greatest_productleft_entry. pfgd_qb_gcd_greatest_result_greatest = fom_beta_quotient_pfp_gcd_greatest_result_greatest_productleft_entry * S ((S (fom_index_pfp_gcd_greatest_result_greatest_productleft)) * pfgd_qc_gcd_greatest_result_greatest) + (fom_value_pfp_gcd_greatest_result_greatest_productleft))) /\ (exists fom_gap_pfp_gcd_greatest_result_greatest_productleft_value_bound. fom_gap_pfp_gcd_greatest_result_greatest_productleft_value_bound + S (fom_value_pfp_gcd_greatest_result_greatest_productleft) = p))) /\ (((forall fom_index_pfp_gcd_greatest_result_greatest_productright. (exists fom_gap_pfp_gcd_greatest_result_greatest_productright_index_bound. fom_gap_pfp_gcd_greatest_result_greatest_productright_index_bound + S (fom_index_pfp_gcd_greatest_result_greatest_productright) = pfgg_D_gcd_greatest_result) -> exists fom_value_pfp_gcd_greatest_result_greatest_productright. ((((exists fom_beta_height_pfp_gcd_greatest_result_greatest_productright_entry. fom_beta_height_pfp_gcd_greatest_result_greatest_productright_entry + S (fom_value_pfp_gcd_greatest_result_greatest_productright) = S ((S (fom_index_pfp_gcd_greatest_result_greatest_productright)) * pfgg_dc_gcd_greatest_result)) /\ exists fom_beta_quotient_pfp_gcd_greatest_result_greatest_productright_entry. pfgg_db_gcd_greatest_result = fom_beta_quotient_pfp_gcd_greatest_result_greatest_productright_entry * S ((S (fom_index_pfp_gcd_greatest_result_greatest_productright)) * pfgg_dc_gcd_greatest_result) + (fom_value_pfp_gcd_greatest_result_greatest_productright))) /\ (exists fom_gap_pfp_gcd_greatest_result_greatest_productright_value_bound. fom_gap_pfp_gcd_greatest_result_greatest_productright_value_bound + S (fom_value_pfp_gcd_greatest_result_greatest_productright) = p))) /\ (((((((pfgd_Q_gcd_greatest_result_greatest)=0 \/ (pfgg_D_gcd_greatest_result)=0) /\ (((pfgd_P_gcd_greatest_result_greatest)=0)))) \/ (((~((pfgd_Q_gcd_greatest_result_greatest)=0)) /\ (((~((pfgg_D_gcd_greatest_result)=0)) /\ (((pfgd_Q_gcd_greatest_result_greatest)+(pfgg_D_gcd_greatest_result)=S (pfgd_P_gcd_greatest_result_greatest)))))))) /\ ((forall pfc_index_gcd_greatest_result_greatest_productcoefficients. (exists pfa_gap_gcd_greatest_result_greatest_productcoefficientsbound. pfa_gap_gcd_greatest_result_greatest_productcoefficientsbound + S (pfc_index_gcd_greatest_result_greatest_productcoefficients) = (pfgd_P_gcd_greatest_result_greatest)) -> exists pfc_value_gcd_greatest_result_greatest_productcoefficients. ((((exists ff_h_pfp_gcd_greatest_result_greatest_productcoefficientsentry. ff_h_pfp_gcd_greatest_result_greatest_productcoefficientsentry + S (pfc_value_gcd_greatest_result_greatest_productcoefficients) = S ((S (pfc_index_gcd_greatest_result_greatest_productcoefficients)) * pfgd_pc_gcd_greatest_result_greatest)) /\ exists ff_q_pfp_gcd_greatest_result_greatest_productcoefficientsentry. pfgd_pb_gcd_greatest_result_greatest = ff_q_pfp_gcd_greatest_result_greatest_productcoefficientsentry * S ((S (pfc_index_gcd_greatest_result_greatest_productcoefficients)) * pfgd_pc_gcd_greatest_result_greatest) + (pfc_value_gcd_greatest_result_greatest_productcoefficients))) /\ ((exists pfc_terms_code_gcd_greatest_result_greatest_productcoefficientscoefficient pfc_terms_scale_gcd_greatest_result_greatest_productcoefficientscoefficient pfc_natural_sum_gcd_greatest_result_greatest_productcoefficientscoefficient. ((forall pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_greatest_result_greatest_productcoefficients))) -> exists pfc_value_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_greatest_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_greatest_result_greatest_productcoefficientscoefficient = ff_q_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_greatest_result_greatest_productcoefficientscoefficient) + (pfc_value_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm pfc_left_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm pfc_right_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_greatest_result_greatest_productcoefficients)) /\ ((((((exists pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_greatest_result_greatest)) /\ ((((exists ff_h_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_greatest)) /\ exists ff_q_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_greatest_result_greatest = ff_q_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_greatest_result_greatest) + (pfc_left_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_greatest_result_greatest)=(pfc_index_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm) = (pfgg_D_gcd_greatest_result)) /\ ((((exists ff_h_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_gcd_greatest_result)) /\ exists ff_q_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightentry. pfgg_db_gcd_greatest_result = ff_q_pfp_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm)) * pfgg_dc_gcd_greatest_result) + (pfc_right_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonaltermrightoutside+(pfgg_D_gcd_greatest_result)=(pfc_complement_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonal)=pfc_left_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_greatest_result_greatest_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_greatest_result_greatest_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_greatest_result_greatest_productcoefficients))) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_greatest_result_greatest_productcoefficients))) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_greatest_result_greatest_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_greatest_result_greatest_productcoefficients)) -> exists fs_a_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_greatest_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_greatest_result_greatest_productcoefficientscoefficient = fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_greatest_result_greatest_productcoefficientscoefficient) + (fs_a_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum = fs_q_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_greatest_result_greatest_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientresiduebound. pfa_gap_gcd_greatest_result_greatest_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_greatest_result_greatest_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_greatest_result_greatest_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_greatest_result_greatest_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_greatest_result_greatest_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_greatest_result_greatest_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_greatest_result_greatest_productcoefficients) + (p) * pfa_offset_right_gcd_greatest_result_greatest_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_greatest_result_greatest_equivalent pfrep_left_gcd_greatest_result_greatest_equivalent pfrep_right_gcd_greatest_result_greatest_equivalent. ((exists pfrep_position_gcd_greatest_result_greatest_equivalentfirst. ((pfrep_position_gcd_greatest_result_greatest_equivalentfirst+S (pfrep_power_gcd_greatest_result_greatest_equivalent)=(pfgd_P_gcd_greatest_result_greatest)) /\ ((((exists ff_h_pfp_gcd_greatest_result_greatest_equivalentfirstentry. ff_h_pfp_gcd_greatest_result_greatest_equivalentfirstentry + S (pfrep_left_gcd_greatest_result_greatest_equivalent) = S ((S (pfrep_position_gcd_greatest_result_greatest_equivalentfirst)) * pfgd_pc_gcd_greatest_result_greatest)) /\ exists ff_q_pfp_gcd_greatest_result_greatest_equivalentfirstentry. pfgd_pb_gcd_greatest_result_greatest = ff_q_pfp_gcd_greatest_result_greatest_equivalentfirstentry * S ((S (pfrep_position_gcd_greatest_result_greatest_equivalentfirst)) * pfgd_pc_gcd_greatest_result_greatest) + (pfrep_left_gcd_greatest_result_greatest_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_greatest_equivalentfirstoutside. pfrep_gap_gcd_greatest_result_greatest_equivalentfirstoutside+(pfgd_P_gcd_greatest_result_greatest)=(pfrep_power_gcd_greatest_result_greatest_equivalent)) /\ (((pfrep_left_gcd_greatest_result_greatest_equivalent)=0))))) -> ((exists pfrep_position_gcd_greatest_result_greatest_equivalentsecond. ((pfrep_position_gcd_greatest_result_greatest_equivalentsecond+S (pfrep_power_gcd_greatest_result_greatest_equivalent)=(G)) /\ ((((exists ff_h_pfp_gcd_greatest_result_greatest_equivalentsecondentry. ff_h_pfp_gcd_greatest_result_greatest_equivalentsecondentry + S (pfrep_right_gcd_greatest_result_greatest_equivalent) = S ((S (pfrep_position_gcd_greatest_result_greatest_equivalentsecond)) * gc)) /\ exists ff_q_pfp_gcd_greatest_result_greatest_equivalentsecondentry. gb = ff_q_pfp_gcd_greatest_result_greatest_equivalentsecondentry * S ((S (pfrep_position_gcd_greatest_result_greatest_equivalentsecond)) * gc) + (pfrep_right_gcd_greatest_result_greatest_equivalent)))))) \/ (((exists pfrep_gap_gcd_greatest_result_greatest_equivalentsecondoutside. pfrep_gap_gcd_greatest_result_greatest_equivalentsecondoutside+(G)=(pfrep_power_gcd_greatest_result_greatest_equivalent)) /\ (((pfrep_right_gcd_greatest_result_greatest_equivalent)=0))))) -> pfrep_left_gcd_greatest_result_greatest_equivalent=pfrep_right_gcd_greatest_result_greatest_equivalent)))))))))))Complete tactic proof in conservative notation
All 48 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
48 script commands · 8 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–19
03Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
split
04Use earlier factsL21–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
exact hc
05Fix variables and assumptionsL22–25
06Use earlier factsL26–35
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L26
specialize prime_field_polynomial_bezout_common_right_divisor (p) - L27
specialize prime_field_polynomial_bezout_common_right_divisor (db) - L28
specialize prime_field_polynomial_bezout_common_right_divisor (dc) - L29
specialize prime_field_polynomial_bezout_common_right_divisor (D) - L30
specialize prime_field_polynomial_bezout_common_right_divisor (ab) - L31
specialize prime_field_polynomial_bezout_common_right_divisor (ac) - L32
specialize prime_field_polynomial_bezout_common_right_divisor (L) - L33
specialize prime_field_polynomial_bezout_common_right_divisor (bb) - L34
specialize prime_field_polynomial_bezout_common_right_divisor (bc) - L35
specialize prime_field_polynomial_bezout_common_right_divisor (M)
07Use earlier factsL36–45
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
specialize prime_field_polynomial_bezout_common_right_divisor (gb) - L37
specialize prime_field_polynomial_bezout_common_right_divisor (gc) - L38
specialize prime_field_polynomial_bezout_common_right_divisor (G) - L39
specialize prime_field_polynomial_bezout_common_right_divisor (ub) - L40
specialize prime_field_polynomial_bezout_common_right_divisor (uc) - L41
specialize prime_field_polynomial_bezout_common_right_divisor (U) - L42
specialize prime_field_polynomial_bezout_common_right_divisor (vb) - L43
specialize prime_field_polynomial_bezout_common_right_divisor (vc) - L44
specialize prime_field_polynomial_bezout_common_right_divisor (V) - L45
apply prime_field_polynomial_bezout_common_right_divisor
Original defined command ledger · 48 lines
- 0001
intro p - 0002
intro gb - 0003
intro gc - 0004
intro G - 0005
intro ab - 0006
intro ac - 0007
intro L - 0008
intro bb - 0009
intro bc - 0010
intro M - 0011
intro ub - 0012
intro uc - 0013
intro U - 0014
intro vb - 0015
intro vc - 0016
intro V - 0017
intro hp - 0018
intro hc - 0019
intro hb - 0020
split - 0021
exact hc - 0022
intro db - 0023
intro dc - 0024
intro D - 0025
intro hd - 0026
specialize prime_field_polynomial_bezout_common_right_divisor (p) - 0027
specialize prime_field_polynomial_bezout_common_right_divisor (db) - 0028
specialize prime_field_polynomial_bezout_common_right_divisor (dc) - 0029
specialize prime_field_polynomial_bezout_common_right_divisor (D) - 0030
specialize prime_field_polynomial_bezout_common_right_divisor (ab) - 0031
specialize prime_field_polynomial_bezout_common_right_divisor (ac) - 0032
specialize prime_field_polynomial_bezout_common_right_divisor (L) - 0033
specialize prime_field_polynomial_bezout_common_right_divisor (bb) - 0034
specialize prime_field_polynomial_bezout_common_right_divisor (bc) - 0035
specialize prime_field_polynomial_bezout_common_right_divisor (M) - 0036
specialize prime_field_polynomial_bezout_common_right_divisor (gb) - 0037
specialize prime_field_polynomial_bezout_common_right_divisor (gc) - 0038
specialize prime_field_polynomial_bezout_common_right_divisor (G) - 0039
specialize prime_field_polynomial_bezout_common_right_divisor (ub) - 0040
specialize prime_field_polynomial_bezout_common_right_divisor (uc) - 0041
specialize prime_field_polynomial_bezout_common_right_divisor (U) - 0042
specialize prime_field_polynomial_bezout_common_right_divisor (vb) - 0043
specialize prime_field_polynomial_bezout_common_right_divisor (vc) - 0044
specialize prime_field_polynomial_bezout_common_right_divisor (V) - 0045
apply prime_field_polynomial_bezout_common_right_divisor - 0046
exact hp - 0047
exact hd - 0048
exact hb