Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
Exact theorem in conservative defined notation
∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. Prime(p) → BetaPrefixInto(ab,ac,L,p) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. FpPolynomialZeroOrMonic(p,x,y,z) ∧ (FpPolynomialCommonRightDivisor(p,x,y,z,ab,ac,L,bb,bc,0) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,0,x,y,z,n,m,k,i,j,u))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall p ab ac L bb bc. (~((p) = 1) /\ forall pfa_factor_left_gcd_terminal_prime pfa_factor_right_gcd_terminal_prime. (p) = pfa_factor_left_gcd_terminal_prime * pfa_factor_right_gcd_terminal_prime -> pfa_factor_left_gcd_terminal_prime = 1 \/ pfa_factor_right_gcd_terminal_prime = 1) -> (forall fom_index_pfp_gcd_terminal_input. (exists fom_gap_pfp_gcd_terminal_input_index_bound. fom_gap_pfp_gcd_terminal_input_index_bound + S (fom_index_pfp_gcd_terminal_input) = L) -> exists fom_value_pfp_gcd_terminal_input. ((((exists fom_beta_height_pfp_gcd_terminal_input_entry. fom_beta_height_pfp_gcd_terminal_input_entry + S (fom_value_pfp_gcd_terminal_input) = S ((S (fom_index_pfp_gcd_terminal_input)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_terminal_input_entry. ab = fom_beta_quotient_pfp_gcd_terminal_input_entry * S ((S (fom_index_pfp_gcd_terminal_input)) * ac) + (fom_value_pfp_gcd_terminal_input))) /\ (exists fom_gap_pfp_gcd_terminal_input_value_bound. fom_gap_pfp_gcd_terminal_input_value_bound + S (fom_value_pfp_gcd_terminal_input) = p))) -> (exists pfgs_gb_gcd_terminal_result pfgs_gc_gcd_terminal_result pfgs_G_gcd_terminal_result pfgs_ub_gcd_terminal_result pfgs_uc_gcd_terminal_result pfgs_U_gcd_terminal_result pfgs_vb_gcd_terminal_result pfgs_vc_gcd_terminal_result pfgs_V_gcd_terminal_result. (((pfgs_G_gcd_terminal_result)=0 \/ (((~((pfgs_G_gcd_terminal_result) = 0)) /\ (((forall fom_index_pfp_gcd_terminal_result_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_terminal_result_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_terminal_result_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_normal_moniccoefficients) = pfgs_G_gcd_terminal_result) -> exists fom_value_pfp_gcd_terminal_result_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_terminal_result_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_terminal_result_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_terminal_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_terminal_result)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_terminal_result = fom_beta_quotient_pfp_gcd_terminal_result_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_terminal_result) + (fom_value_pfp_gcd_terminal_result_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_terminal_result_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_normal_monicleading. ff_h_pfp_gcd_terminal_result_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_terminal_result)) /\ exists ff_q_pfp_gcd_terminal_result_witness_normal_monicleading. pfgs_gb_gcd_terminal_result = ff_q_pfp_gcd_terminal_result_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_terminal_result) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_terminal_result_witness_common_left_bounded. (exists fom_gap_pfp_gcd_terminal_result_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_terminal_result_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_common_left_bounded) = L) -> exists fom_value_pfp_gcd_terminal_result_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_terminal_result_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_terminal_result_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_terminal_result_witness_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_terminal_result_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_common_left_bounded)) * ac) + (fom_value_pfp_gcd_terminal_result_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_terminal_result_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_terminal_result_witness_common_left pfgd_qc_gcd_terminal_result_witness_common_left pfgd_Q_gcd_terminal_result_witness_common_left pfgd_pb_gcd_terminal_result_witness_common_left pfgd_pc_gcd_terminal_result_witness_common_left pfgd_P_gcd_terminal_result_witness_common_left. ((((forall fom_index_pfp_gcd_terminal_result_witness_common_left_productleft. (exists fom_gap_pfp_gcd_terminal_result_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_terminal_result_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_common_left_productleft) = pfgd_Q_gcd_terminal_result_witness_common_left) -> exists fom_value_pfp_gcd_terminal_result_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_terminal_result_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_terminal_result_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_terminal_result_witness_common_left_productleft)) * pfgd_qc_gcd_terminal_result_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_common_left_productleft_entry. pfgd_qb_gcd_terminal_result_witness_common_left = fom_beta_quotient_pfp_gcd_terminal_result_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_common_left_productleft)) * pfgd_qc_gcd_terminal_result_witness_common_left) + (fom_value_pfp_gcd_terminal_result_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_terminal_result_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_terminal_result_witness_common_left_productright. (exists fom_gap_pfp_gcd_terminal_result_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_terminal_result_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_common_left_productright) = pfgs_G_gcd_terminal_result) -> exists fom_value_pfp_gcd_terminal_result_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_terminal_result_witness_common_left_productright_entry + S (fom_value_pfp_gcd_terminal_result_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_terminal_result_witness_common_left_productright)) * pfgs_gc_gcd_terminal_result)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_common_left_productright_entry. pfgs_gb_gcd_terminal_result = fom_beta_quotient_pfp_gcd_terminal_result_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_common_left_productright)) * pfgs_gc_gcd_terminal_result) + (fom_value_pfp_gcd_terminal_result_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_terminal_result_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_terminal_result_witness_common_left)=0 \/ (pfgs_G_gcd_terminal_result)=0) /\ (((pfgd_P_gcd_terminal_result_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_terminal_result_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_terminal_result)=0)) /\ (((pfgd_Q_gcd_terminal_result_witness_common_left)+(pfgs_G_gcd_terminal_result)=S (pfgd_P_gcd_terminal_result_witness_common_left)))))))) /\ ((forall pfc_index_gcd_terminal_result_witness_common_left_productcoefficients. (exists pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientsbound. pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficients) = (pfgd_P_gcd_terminal_result_witness_common_left)) -> exists pfc_value_gcd_terminal_result_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_terminal_result_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_terminal_result_witness_common_left)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_terminal_result_witness_common_left = ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_terminal_result_witness_common_left) + (pfc_value_gcd_terminal_result_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_terminal_result_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_terminal_result_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_terminal_result_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_terminal_result_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_terminal_result_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_terminal_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_terminal_result_witness_common_left)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_terminal_result_witness_common_left = ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_terminal_result_witness_common_left) + (pfc_left_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_terminal_result_witness_common_left)=(pfc_index_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_terminal_result)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_terminal_result)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_terminal_result = ff_q_pfp_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_terminal_result) + (pfc_right_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_terminal_result)=(pfc_complement_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_terminal_result_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_terminal_result_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_terminal_result_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_terminal_result_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_terminal_result_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_terminal_result_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_terminal_result_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_terminal_result_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_terminal_result_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_terminal_result_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_terminal_result_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_terminal_result_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_terminal_result_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_terminal_result_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_terminal_result_witness_common_left_equivalent pfrep_left_gcd_terminal_result_witness_common_left_equivalent pfrep_right_gcd_terminal_result_witness_common_left_equivalent. ((exists pfrep_position_gcd_terminal_result_witness_common_left_equivalentfirst. ((pfrep_position_gcd_terminal_result_witness_common_left_equivalentfirst+S (pfrep_power_gcd_terminal_result_witness_common_left_equivalent)=(pfgd_P_gcd_terminal_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_terminal_result_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_terminal_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_terminal_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_terminal_result_witness_common_left)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_terminal_result_witness_common_left = ff_q_pfp_gcd_terminal_result_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_terminal_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_terminal_result_witness_common_left) + (pfrep_left_gcd_terminal_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_terminal_result_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_terminal_result_witness_common_left)=(pfrep_power_gcd_terminal_result_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_terminal_result_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_terminal_result_witness_common_left_equivalentsecond. ((pfrep_position_gcd_terminal_result_witness_common_left_equivalentsecond+S (pfrep_power_gcd_terminal_result_witness_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_terminal_result_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_terminal_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_terminal_result_witness_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_terminal_result_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_terminal_result_witness_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_terminal_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_terminal_result_witness_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_terminal_result_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_terminal_result_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_terminal_result_witness_common_left_equivalent=pfrep_right_gcd_terminal_result_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_terminal_result_witness_common_right_bounded. (exists fom_gap_pfp_gcd_terminal_result_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_terminal_result_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_common_right_bounded) = 0) -> exists fom_value_pfp_gcd_terminal_result_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_terminal_result_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_terminal_result_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_terminal_result_witness_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_common_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_terminal_result_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_common_right_bounded)) * bc) + (fom_value_pfp_gcd_terminal_result_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_terminal_result_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_terminal_result_witness_common_right pfgd_qc_gcd_terminal_result_witness_common_right pfgd_Q_gcd_terminal_result_witness_common_right pfgd_pb_gcd_terminal_result_witness_common_right pfgd_pc_gcd_terminal_result_witness_common_right pfgd_P_gcd_terminal_result_witness_common_right. ((((forall fom_index_pfp_gcd_terminal_result_witness_common_right_productleft. (exists fom_gap_pfp_gcd_terminal_result_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_terminal_result_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_common_right_productleft) = pfgd_Q_gcd_terminal_result_witness_common_right) -> exists fom_value_pfp_gcd_terminal_result_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_terminal_result_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_terminal_result_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_terminal_result_witness_common_right_productleft)) * pfgd_qc_gcd_terminal_result_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_common_right_productleft_entry. pfgd_qb_gcd_terminal_result_witness_common_right = fom_beta_quotient_pfp_gcd_terminal_result_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_common_right_productleft)) * pfgd_qc_gcd_terminal_result_witness_common_right) + (fom_value_pfp_gcd_terminal_result_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_terminal_result_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_terminal_result_witness_common_right_productright. (exists fom_gap_pfp_gcd_terminal_result_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_terminal_result_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_common_right_productright) = pfgs_G_gcd_terminal_result) -> exists fom_value_pfp_gcd_terminal_result_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_terminal_result_witness_common_right_productright_entry + S (fom_value_pfp_gcd_terminal_result_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_terminal_result_witness_common_right_productright)) * pfgs_gc_gcd_terminal_result)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_common_right_productright_entry. pfgs_gb_gcd_terminal_result = fom_beta_quotient_pfp_gcd_terminal_result_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_common_right_productright)) * pfgs_gc_gcd_terminal_result) + (fom_value_pfp_gcd_terminal_result_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_terminal_result_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_terminal_result_witness_common_right)=0 \/ (pfgs_G_gcd_terminal_result)=0) /\ (((pfgd_P_gcd_terminal_result_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_terminal_result_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_terminal_result)=0)) /\ (((pfgd_Q_gcd_terminal_result_witness_common_right)+(pfgs_G_gcd_terminal_result)=S (pfgd_P_gcd_terminal_result_witness_common_right)))))))) /\ ((forall pfc_index_gcd_terminal_result_witness_common_right_productcoefficients. (exists pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientsbound. pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficients) = (pfgd_P_gcd_terminal_result_witness_common_right)) -> exists pfc_value_gcd_terminal_result_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_terminal_result_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_terminal_result_witness_common_right)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_terminal_result_witness_common_right = ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_terminal_result_witness_common_right) + (pfc_value_gcd_terminal_result_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_terminal_result_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_terminal_result_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_terminal_result_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_terminal_result_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_terminal_result_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_terminal_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_terminal_result_witness_common_right)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_terminal_result_witness_common_right = ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_terminal_result_witness_common_right) + (pfc_left_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_terminal_result_witness_common_right)=(pfc_index_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_terminal_result)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_terminal_result)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_terminal_result = ff_q_pfp_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_terminal_result) + (pfc_right_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_terminal_result)=(pfc_complement_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_terminal_result_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_terminal_result_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_terminal_result_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_terminal_result_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_terminal_result_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_terminal_result_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_terminal_result_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_terminal_result_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_terminal_result_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_terminal_result_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_terminal_result_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_terminal_result_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_terminal_result_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_terminal_result_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_terminal_result_witness_common_right_equivalent pfrep_left_gcd_terminal_result_witness_common_right_equivalent pfrep_right_gcd_terminal_result_witness_common_right_equivalent. ((exists pfrep_position_gcd_terminal_result_witness_common_right_equivalentfirst. ((pfrep_position_gcd_terminal_result_witness_common_right_equivalentfirst+S (pfrep_power_gcd_terminal_result_witness_common_right_equivalent)=(pfgd_P_gcd_terminal_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_terminal_result_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_terminal_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_terminal_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_terminal_result_witness_common_right)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_terminal_result_witness_common_right = ff_q_pfp_gcd_terminal_result_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_terminal_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_terminal_result_witness_common_right) + (pfrep_left_gcd_terminal_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_terminal_result_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_terminal_result_witness_common_right)=(pfrep_power_gcd_terminal_result_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_terminal_result_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_terminal_result_witness_common_right_equivalentsecond. ((pfrep_position_gcd_terminal_result_witness_common_right_equivalentsecond+S (pfrep_power_gcd_terminal_result_witness_common_right_equivalent)=(0)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_terminal_result_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_terminal_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_terminal_result_witness_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_terminal_result_witness_common_right_equivalentsecondentry. bb = ff_q_pfp_gcd_terminal_result_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_terminal_result_witness_common_right_equivalentsecond)) * bc) + (pfrep_right_gcd_terminal_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_terminal_result_witness_common_right_equivalentsecondoutside+(0)=(pfrep_power_gcd_terminal_result_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_terminal_result_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_terminal_result_witness_common_right_equivalent=pfrep_right_gcd_terminal_result_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_terminal_result_witness_bezout pfgb_pc_gcd_terminal_result_witness_bezout pfgb_P_gcd_terminal_result_witness_bezout pfgb_qb_gcd_terminal_result_witness_bezout pfgb_qc_gcd_terminal_result_witness_bezout pfgb_Q_gcd_terminal_result_witness_bezout. ((((forall fom_index_pfp_gcd_terminal_result_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_bezout_leftleft) = pfgs_U_gcd_terminal_result) -> exists fom_value_pfp_gcd_terminal_result_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_terminal_result_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_terminal_result_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_leftleft)) * pfgs_uc_gcd_terminal_result)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_leftleft_entry. pfgs_ub_gcd_terminal_result = fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_leftleft)) * pfgs_uc_gcd_terminal_result) + (fom_value_pfp_gcd_terminal_result_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_terminal_result_witness_bezout_leftright. (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_bezout_leftright) = L) -> exists fom_value_pfp_gcd_terminal_result_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_terminal_result_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_terminal_result_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_leftright_entry. ab = fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_leftright)) * ac) + (fom_value_pfp_gcd_terminal_result_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_terminal_result)=0 \/ (L)=0) /\ (((pfgb_P_gcd_terminal_result_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_terminal_result)=0)) /\ (((~((L)=0)) /\ (((pfgs_U_gcd_terminal_result)+(L)=S (pfgb_P_gcd_terminal_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients) = (pfgb_P_gcd_terminal_result_witness_bezout)) -> exists pfc_value_gcd_terminal_result_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_terminal_result_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_terminal_result_witness_bezout)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_terminal_result_witness_bezout = ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_terminal_result_witness_bezout) + (pfc_value_gcd_terminal_result_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_terminal_result)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_terminal_result)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_terminal_result = ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_terminal_result) + (pfc_left_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_terminal_result)=(pfc_index_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_terminal_result_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_terminal_result_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_terminal_result_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_terminal_result_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_terminal_result_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_terminal_result_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_bezout_rightleft) = pfgs_V_gcd_terminal_result) -> exists fom_value_pfp_gcd_terminal_result_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_terminal_result_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_terminal_result_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_rightleft)) * pfgs_vc_gcd_terminal_result)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_rightleft_entry. pfgs_vb_gcd_terminal_result = fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_rightleft)) * pfgs_vc_gcd_terminal_result) + (fom_value_pfp_gcd_terminal_result_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_terminal_result_witness_bezout_rightright. (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_bezout_rightright) = 0) -> exists fom_value_pfp_gcd_terminal_result_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_terminal_result_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_terminal_result_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_rightright_entry. bb = fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_rightright)) * bc) + (fom_value_pfp_gcd_terminal_result_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_terminal_result)=0 \/ (0)=0) /\ (((pfgb_Q_gcd_terminal_result_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_terminal_result)=0)) /\ (((~((0)=0)) /\ (((pfgs_V_gcd_terminal_result)+(0)=S (pfgb_Q_gcd_terminal_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_terminal_result_witness_bezout)) -> exists pfc_value_gcd_terminal_result_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_terminal_result_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_terminal_result_witness_bezout)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_terminal_result_witness_bezout = ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_terminal_result_witness_bezout) + (pfc_value_gcd_terminal_result_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_terminal_result)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_terminal_result)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_terminal_result = ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_terminal_result) + (pfc_left_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_terminal_result)=(pfc_index_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (0)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(0)=(pfc_complement_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_terminal_result_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_terminal_result_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_terminal_result_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_terminal_result_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_terminal_result_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded) = pfgb_P_gcd_terminal_result_witness_bezout) -> exists fom_value_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_terminal_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_terminal_result_witness_bezout = fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_terminal_result_witness_bezout) + (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_terminal_result_witness_bezout) -> exists fom_value_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_terminal_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_terminal_result_witness_bezout = fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_terminal_result_witness_bezout) + (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded) = pfgs_G_gcd_terminal_result) -> exists fom_value_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_terminal_result)) /\ exists fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_terminal_result = fom_beta_quotient_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_terminal_result) + (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_terminal_result_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_terminal_result_witness_bezout_sum pfga_uc_gcd_terminal_result_witness_bezout_sum pfga_vb_gcd_terminal_result_witness_bezout_sum pfga_vc_gcd_terminal_result_witness_bezout_sum pfga_tb_gcd_terminal_result_witness_bezout_sum pfga_tc_gcd_terminal_result_witness_bezout_sum pfga_K_gcd_terminal_result_witness_bezout_sum. ((((forall pfrep_power_gcd_terminal_result_witness_bezout_sum_left pfrep_left_gcd_terminal_result_witness_bezout_sum_left pfrep_right_gcd_terminal_result_witness_bezout_sum_left. ((exists pfrep_position_gcd_terminal_result_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_terminal_result_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_terminal_result_witness_bezout_sum_left)=(pfgb_P_gcd_terminal_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_terminal_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_terminal_result_witness_bezout)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_terminal_result_witness_bezout = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_terminal_result_witness_bezout) + (pfrep_left_gcd_terminal_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_terminal_result_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_terminal_result_witness_bezout)=(pfrep_power_gcd_terminal_result_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_terminal_result_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_terminal_result_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_terminal_result_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_terminal_result_witness_bezout_sum_left)=(pfga_K_gcd_terminal_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_terminal_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_terminal_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_terminal_result_witness_bezout_sum = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_terminal_result_witness_bezout_sum) + (pfrep_right_gcd_terminal_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_terminal_result_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_terminal_result_witness_bezout_sum)=(pfrep_power_gcd_terminal_result_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_terminal_result_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_terminal_result_witness_bezout_sum_left=pfrep_right_gcd_terminal_result_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_terminal_result_witness_bezout_sum_right pfrep_left_gcd_terminal_result_witness_bezout_sum_right pfrep_right_gcd_terminal_result_witness_bezout_sum_right. ((exists pfrep_position_gcd_terminal_result_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_terminal_result_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_terminal_result_witness_bezout_sum_right)=(pfgb_Q_gcd_terminal_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_terminal_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_terminal_result_witness_bezout)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_terminal_result_witness_bezout = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_terminal_result_witness_bezout) + (pfrep_left_gcd_terminal_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_terminal_result_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_terminal_result_witness_bezout)=(pfrep_power_gcd_terminal_result_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_terminal_result_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_terminal_result_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_terminal_result_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_terminal_result_witness_bezout_sum_right)=(pfga_K_gcd_terminal_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_terminal_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_terminal_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_terminal_result_witness_bezout_sum = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_terminal_result_witness_bezout_sum) + (pfrep_right_gcd_terminal_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_terminal_result_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_terminal_result_witness_bezout_sum)=(pfrep_power_gcd_terminal_result_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_terminal_result_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_terminal_result_witness_bezout_sum_right=pfrep_right_gcd_terminal_result_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_terminal_result_witness_bezout_sum_add. (exists pfa_gap_gcd_terminal_result_witness_bezout_sum_addindex. pfa_gap_gcd_terminal_result_witness_bezout_sum_addindex + S (pfp_index_gcd_terminal_result_witness_bezout_sum_add) = (pfga_K_gcd_terminal_result_witness_bezout_sum)) -> exists pfp_left_gcd_terminal_result_witness_bezout_sum_add pfp_right_gcd_terminal_result_witness_bezout_sum_add pfp_value_gcd_terminal_result_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_addleft. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_addleft + S (pfp_left_gcd_terminal_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_terminal_result_witness_bezout_sum_add)) * pfga_uc_gcd_terminal_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_addleft. pfga_ub_gcd_terminal_result_witness_bezout_sum = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_terminal_result_witness_bezout_sum_add)) * pfga_uc_gcd_terminal_result_witness_bezout_sum) + (pfp_left_gcd_terminal_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_addright. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_addright + S (pfp_right_gcd_terminal_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_terminal_result_witness_bezout_sum_add)) * pfga_vc_gcd_terminal_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_addright. pfga_vb_gcd_terminal_result_witness_bezout_sum = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_addright * S ((S (pfp_index_gcd_terminal_result_witness_bezout_sum_add)) * pfga_vc_gcd_terminal_result_witness_bezout_sum) + (pfp_right_gcd_terminal_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_addtarget. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_addtarget + S (pfp_value_gcd_terminal_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_terminal_result_witness_bezout_sum_add)) * pfga_tc_gcd_terminal_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_addtarget. pfga_tb_gcd_terminal_result_witness_bezout_sum = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_terminal_result_witness_bezout_sum_add)) * pfga_tc_gcd_terminal_result_witness_bezout_sum) + (pfp_value_gcd_terminal_result_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_terminal_result_witness_bezout_sum_addoperationleft. pfa_gap_gcd_terminal_result_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_terminal_result_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_terminal_result_witness_bezout_sum_addoperationright. pfa_gap_gcd_terminal_result_witness_bezout_sum_addoperationright + S (pfp_right_gcd_terminal_result_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_terminal_result_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_terminal_result_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_terminal_result_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_terminal_result_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_terminal_result_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_terminal_result_witness_bezout_sum_add) + (pfp_right_gcd_terminal_result_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_terminal_result_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_terminal_result_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_terminal_result_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_terminal_result_witness_bezout_sum_result pfrep_left_gcd_terminal_result_witness_bezout_sum_result pfrep_right_gcd_terminal_result_witness_bezout_sum_result. ((exists pfrep_position_gcd_terminal_result_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_terminal_result_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_terminal_result_witness_bezout_sum_result)=(pfga_K_gcd_terminal_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_terminal_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_terminal_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_terminal_result_witness_bezout_sum = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_terminal_result_witness_bezout_sum) + (pfrep_left_gcd_terminal_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_terminal_result_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_terminal_result_witness_bezout_sum)=(pfrep_power_gcd_terminal_result_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_terminal_result_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_terminal_result_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_terminal_result_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_terminal_result_witness_bezout_sum_result)=(pfgs_G_gcd_terminal_result)) /\ ((((exists ff_h_pfp_gcd_terminal_result_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_terminal_result_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_terminal_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_terminal_result)) /\ exists ff_q_pfp_gcd_terminal_result_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_terminal_result = ff_q_pfp_gcd_terminal_result_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_terminal_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_terminal_result) + (pfrep_right_gcd_terminal_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_terminal_result_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_terminal_result_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_terminal_result)=(pfrep_power_gcd_terminal_result_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_terminal_result_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_terminal_result_witness_bezout_sum_result=pfrep_right_gcd_terminal_result_witness_bezout_sum_result)))))))))))))))))))))))Complete tactic proof in conservative notation
All 75 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
75 script commands · 12 reading checkpoints · 3 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 (4)
01Fix variables and assumptionsL1–8
02Establish hnL9–16
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial normalized right associate exists.
- L9
have hn : ∃ gb. ∃ gc. ∃ G. FpPolynomialZeroOrMonic(p,gb,gc,G) ∧ (FpPolynomialRightDivides(p,ab,ac,L,gb,gc,G) ∧ FpPolynomialRightDivides(p,gb,gc,G,ab,ac,L))Definitions: FpPolynomialZeroOrMonic(p,gb,gc,G)FpPolynomialRightDivides(p,ab,ac,L,gb,gc,G)FpPolynomialRightDivides(p,gb,gc,G,ab,ac,L)Original native command in the exact edition - L10
specialize prime_field_polynomial_normalized_right_associate_exists (p) - L11
specialize prime_field_polynomial_normalized_right_associate_exists (ab) - L12
specialize prime_field_polynomial_normalized_right_associate_exists (ac) - L13
specialize prime_field_polynomial_normalized_right_associate_exists (L) - L14
apply prime_field_polynomial_normalized_right_associate_exists - L15
exact hp - L16
exact hA
03Separate the logical casesL17–21
04Establish hGL22–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial right divides divisor bounded.
- L22
have hG : BetaPrefixInto(x,x1,x2,p)Definitions: BetaPrefixInto(x,x1,x2,p)Original native command in the exact edition - L23
specialize prime_field_polynomial_right_divides_divisor_bounded (p) - L24
specialize prime_field_polynomial_right_divides_divisor_bounded (x) - L25
specialize prime_field_polynomial_right_divides_divisor_bounded (x1) - L26
specialize prime_field_polynomial_right_divides_divisor_bounded (x2) - L27
specialize prime_field_polynomial_right_divides_divisor_bounded (ab) - L28
specialize prime_field_polynomial_right_divides_divisor_bounded (ac) - L29
specialize prime_field_polynomial_right_divides_divisor_bounded (L) - L30
apply prime_field_polynomial_right_divides_divisor_bounded - L31
exact hn_witness_witness_witness_right_right
05Establish hbL32–41
Establish this local claim before using it. It is not an additional assumption.
- L32
have hb : ∃ ub. ∃ uc. ∃ U. FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,0,x,x1,x2,ub,uc,U,0,0,0)Definitions: FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,0,x,x1,x2,ub,uc,U,0,0,0)Original native command in the exact edition - L33
specialize prime_field_polynomial_bezout_from_right_multiple (p) - L34
specialize prime_field_polynomial_bezout_from_right_multiple (ab) - L35
specialize prime_field_polynomial_bezout_from_right_multiple (ac) - L36
specialize prime_field_polynomial_bezout_from_right_multiple (L) - L37
specialize prime_field_polynomial_bezout_from_right_multiple (bb) - L38
specialize prime_field_polynomial_bezout_from_right_multiple (bc) - L39
specialize prime_field_polynomial_bezout_from_right_multiple (0) - L40
specialize prime_field_polynomial_bezout_from_right_multiple (x) - L41
specialize prime_field_polynomial_bezout_from_right_multiple (x1)
06Use earlier factsL42–49
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L42
specialize prime_field_polynomial_bezout_from_right_multiple (x2) - L43
apply prime_field_polynomial_bezout_from_right_multiple - L44
exact hp - L45
specialize matrix_rank_bounded_prefix_empty (bb) - L46
specialize matrix_rank_bounded_prefix_empty (bc) - L47
specialize matrix_rank_bounded_prefix_empty (p) - L48
apply matrix_rank_bounded_prefix_empty - L49
exact hn_witness_witness_witness_right_left
07Separate the logical casesL50–52
08Construct an explicit witnessL53–61
09Separate the logical casesL62–62
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L62
split
10Use earlier factsL63–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L63
exact hn_witness_witness_witness_left
11Separate the logical casesL64–65
12Use earlier factsL66–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L66
exact hn_witness_witness_witness_right_right - L67
specialize prime_field_polynomial_right_divides_empty (p) - L68
specialize prime_field_polynomial_right_divides_empty (x) - L69
specialize prime_field_polynomial_right_divides_empty (x1) - L70
specialize prime_field_polynomial_right_divides_empty (x2) - L71
specialize prime_field_polynomial_right_divides_empty (bb) - L72
specialize prime_field_polynomial_right_divides_empty (bc) - L73
apply prime_field_polynomial_right_divides_empty - L74
exact hG - L75
exact hb_witness_witness_witness
Original defined command ledger · 75 lines
- 0001
intro p - 0002
intro ab - 0003
intro ac - 0004
intro L - 0005
intro bb - 0006
intro bc - 0007
intro hp - 0008
intro hA - 0009
have hn : ∃ gb. ∃ gc. ∃ G. FpPolynomialZeroOrMonic(p,gb,gc,G) ∧ (FpPolynomialRightDivides(p,ab,ac,L,gb,gc,G) ∧ FpPolynomialRightDivides(p,gb,gc,G,ab,ac,L)) - 0010
specialize prime_field_polynomial_normalized_right_associate_exists (p) - 0011
specialize prime_field_polynomial_normalized_right_associate_exists (ab) - 0012
specialize prime_field_polynomial_normalized_right_associate_exists (ac) - 0013
specialize prime_field_polynomial_normalized_right_associate_exists (L) - 0014
apply prime_field_polynomial_normalized_right_associate_exists - 0015
exact hp - 0016
exact hA - 0017
cases hn - 0018
cases hn_witness - 0019
cases hn_witness_witness - 0020
cases hn_witness_witness_witness - 0021
cases hn_witness_witness_witness_right - 0022
have hG : BetaPrefixInto(x,x1,x2,p) - 0023
specialize prime_field_polynomial_right_divides_divisor_bounded (p) - 0024
specialize prime_field_polynomial_right_divides_divisor_bounded (x) - 0025
specialize prime_field_polynomial_right_divides_divisor_bounded (x1) - 0026
specialize prime_field_polynomial_right_divides_divisor_bounded (x2) - 0027
specialize prime_field_polynomial_right_divides_divisor_bounded (ab) - 0028
specialize prime_field_polynomial_right_divides_divisor_bounded (ac) - 0029
specialize prime_field_polynomial_right_divides_divisor_bounded (L) - 0030
apply prime_field_polynomial_right_divides_divisor_bounded - 0031
exact hn_witness_witness_witness_right_right - 0032
have hb : ∃ ub. ∃ uc. ∃ U. FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,0,x,x1,x2,ub,uc,U,0,0,0) - 0033
specialize prime_field_polynomial_bezout_from_right_multiple (p) - 0034
specialize prime_field_polynomial_bezout_from_right_multiple (ab) - 0035
specialize prime_field_polynomial_bezout_from_right_multiple (ac) - 0036
specialize prime_field_polynomial_bezout_from_right_multiple (L) - 0037
specialize prime_field_polynomial_bezout_from_right_multiple (bb) - 0038
specialize prime_field_polynomial_bezout_from_right_multiple (bc) - 0039
specialize prime_field_polynomial_bezout_from_right_multiple (0) - 0040
specialize prime_field_polynomial_bezout_from_right_multiple (x) - 0041
specialize prime_field_polynomial_bezout_from_right_multiple (x1) - 0042
specialize prime_field_polynomial_bezout_from_right_multiple (x2) - 0043
apply prime_field_polynomial_bezout_from_right_multiple - 0044
exact hp - 0045
specialize matrix_rank_bounded_prefix_empty (bb) - 0046
specialize matrix_rank_bounded_prefix_empty (bc) - 0047
specialize matrix_rank_bounded_prefix_empty (p) - 0048
apply matrix_rank_bounded_prefix_empty - 0049
exact hn_witness_witness_witness_right_left - 0050
cases hb - 0051
cases hb_witness - 0052
cases hb_witness_witness - 0053
exists x - 0054
exists x1 - 0055
exists x2 - 0056
exists x3 - 0057
exists x4 - 0058
exists x5 - 0059
exists 0 - 0060
exists 0 - 0061
exists 0 - 0062
split - 0063
exact hn_witness_witness_witness_left - 0064
split - 0065
split - 0066
exact hn_witness_witness_witness_right_right - 0067
specialize prime_field_polynomial_right_divides_empty (p) - 0068
specialize prime_field_polynomial_right_divides_empty (x) - 0069
specialize prime_field_polynomial_right_divides_empty (x1) - 0070
specialize prime_field_polynomial_right_divides_empty (x2) - 0071
specialize prime_field_polynomial_right_divides_empty (bb) - 0072
specialize prime_field_polynomial_right_divides_empty (bc) - 0073
apply prime_field_polynomial_right_divides_empty - 0074
exact hG - 0075
exact hb_witness_witness_witness