Ordinary natural induction constructs actual normalized gcd and Bezout witnesses for every pair with second retained length at most n. Both input triples are generalized, a stored zero divisor is trimmed before division, and every genuine recursive call has a proved smaller bound.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable
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.
forall n. forall p ab ac L bb bc M. (~((p) = 1) /\ forall pfa_factor_left_gcd_induction_prime pfa_factor_right_gcd_induction_prime. (p) = pfa_factor_left_gcd_induction_prime * pfa_factor_right_gcd_induction_prime -> pfa_factor_left_gcd_induction_prime = 1 \/ pfa_factor_right_gcd_induction_prime = 1) -> (forall fom_index_pfp_gcd_induction_A. (exists fom_gap_pfp_gcd_induction_A_index_bound. fom_gap_pfp_gcd_induction_A_index_bound + S (fom_index_pfp_gcd_induction_A) = L) -> exists fom_value_pfp_gcd_induction_A. ((((exists fom_beta_height_pfp_gcd_induction_A_entry. fom_beta_height_pfp_gcd_induction_A_entry + S (fom_value_pfp_gcd_induction_A) = S ((S (fom_index_pfp_gcd_induction_A)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_induction_A_entry. ab = fom_beta_quotient_pfp_gcd_induction_A_entry * S ((S (fom_index_pfp_gcd_induction_A)) * ac) + (fom_value_pfp_gcd_induction_A))) /\ (exists fom_gap_pfp_gcd_induction_A_value_bound. fom_gap_pfp_gcd_induction_A_value_bound + S (fom_value_pfp_gcd_induction_A) = p))) -> (forall fom_index_pfp_gcd_induction_B. (exists fom_gap_pfp_gcd_induction_B_index_bound. fom_gap_pfp_gcd_induction_B_index_bound + S (fom_index_pfp_gcd_induction_B) = M) -> exists fom_value_pfp_gcd_induction_B. ((((exists fom_beta_height_pfp_gcd_induction_B_entry. fom_beta_height_pfp_gcd_induction_B_entry + S (fom_value_pfp_gcd_induction_B) = S ((S (fom_index_pfp_gcd_induction_B)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_induction_B_entry. bb = fom_beta_quotient_pfp_gcd_induction_B_entry * S ((S (fom_index_pfp_gcd_induction_B)) * bc) + (fom_value_pfp_gcd_induction_B))) /\ (exists fom_gap_pfp_gcd_induction_B_value_bound. fom_gap_pfp_gcd_induction_B_value_bound + S (fom_value_pfp_gcd_induction_B) = p))) -> (exists pfc_gap_gcd_induction_bound. pfc_gap_gcd_induction_bound+(M)=(n)) -> (exists pfgs_gb_gcd_induction_solution pfgs_gc_gcd_induction_solution pfgs_G_gcd_induction_solution pfgs_ub_gcd_induction_solution pfgs_uc_gcd_induction_solution pfgs_U_gcd_induction_solution pfgs_vb_gcd_induction_solution pfgs_vc_gcd_induction_solution pfgs_V_gcd_induction_solution. (((pfgs_G_gcd_induction_solution)=0 \/ (((~((pfgs_G_gcd_induction_solution) = 0)) /\ (((forall fom_index_pfp_gcd_induction_solution_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_induction_solution_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_induction_solution_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_normal_moniccoefficients) = pfgs_G_gcd_induction_solution) -> exists fom_value_pfp_gcd_induction_solution_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_induction_solution_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_induction_solution_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_induction_solution_witness_normal_moniccoefficients)) * pfgs_gc_gcd_induction_solution)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_induction_solution = fom_beta_quotient_pfp_gcd_induction_solution_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_normal_moniccoefficients)) * pfgs_gc_gcd_induction_solution) + (fom_value_pfp_gcd_induction_solution_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_induction_solution_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_normal_monicleading. ff_h_pfp_gcd_induction_solution_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_induction_solution)) /\ exists ff_q_pfp_gcd_induction_solution_witness_normal_monicleading. pfgs_gb_gcd_induction_solution = ff_q_pfp_gcd_induction_solution_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_induction_solution) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_induction_solution_witness_common_left_bounded. (exists fom_gap_pfp_gcd_induction_solution_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_induction_solution_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_common_left_bounded) = L) -> exists fom_value_pfp_gcd_induction_solution_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_induction_solution_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_induction_solution_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_induction_solution_witness_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_induction_solution_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_common_left_bounded)) * ac) + (fom_value_pfp_gcd_induction_solution_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_induction_solution_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_induction_solution_witness_common_left pfgd_qc_gcd_induction_solution_witness_common_left pfgd_Q_gcd_induction_solution_witness_common_left pfgd_pb_gcd_induction_solution_witness_common_left pfgd_pc_gcd_induction_solution_witness_common_left pfgd_P_gcd_induction_solution_witness_common_left. ((((forall fom_index_pfp_gcd_induction_solution_witness_common_left_productleft. (exists fom_gap_pfp_gcd_induction_solution_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_induction_solution_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_common_left_productleft) = pfgd_Q_gcd_induction_solution_witness_common_left) -> exists fom_value_pfp_gcd_induction_solution_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_induction_solution_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_induction_solution_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_induction_solution_witness_common_left_productleft)) * pfgd_qc_gcd_induction_solution_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_common_left_productleft_entry. pfgd_qb_gcd_induction_solution_witness_common_left = fom_beta_quotient_pfp_gcd_induction_solution_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_common_left_productleft)) * pfgd_qc_gcd_induction_solution_witness_common_left) + (fom_value_pfp_gcd_induction_solution_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_induction_solution_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_induction_solution_witness_common_left_productright. (exists fom_gap_pfp_gcd_induction_solution_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_induction_solution_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_common_left_productright) = pfgs_G_gcd_induction_solution) -> exists fom_value_pfp_gcd_induction_solution_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_induction_solution_witness_common_left_productright_entry + S (fom_value_pfp_gcd_induction_solution_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_induction_solution_witness_common_left_productright)) * pfgs_gc_gcd_induction_solution)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_common_left_productright_entry. pfgs_gb_gcd_induction_solution = fom_beta_quotient_pfp_gcd_induction_solution_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_common_left_productright)) * pfgs_gc_gcd_induction_solution) + (fom_value_pfp_gcd_induction_solution_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_induction_solution_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_induction_solution_witness_common_left)=0 \/ (pfgs_G_gcd_induction_solution)=0) /\ (((pfgd_P_gcd_induction_solution_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_induction_solution_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_induction_solution)=0)) /\ (((pfgd_Q_gcd_induction_solution_witness_common_left)+(pfgs_G_gcd_induction_solution)=S (pfgd_P_gcd_induction_solution_witness_common_left)))))))) /\ ((forall pfc_index_gcd_induction_solution_witness_common_left_productcoefficients. (exists pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientsbound. pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficients) = (pfgd_P_gcd_induction_solution_witness_common_left)) -> exists pfc_value_gcd_induction_solution_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_induction_solution_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficients)) * pfgd_pc_gcd_induction_solution_witness_common_left)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_induction_solution_witness_common_left = ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficients)) * pfgd_pc_gcd_induction_solution_witness_common_left) + (pfc_value_gcd_induction_solution_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_induction_solution_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_induction_solution_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_induction_solution_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_induction_solution_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_induction_solution_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_induction_solution_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_induction_solution_witness_common_left)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_induction_solution_witness_common_left = ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_induction_solution_witness_common_left) + (pfc_left_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_induction_solution_witness_common_left)=(pfc_index_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_induction_solution)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_induction_solution)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_induction_solution = ff_q_pfp_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_induction_solution) + (pfc_right_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_induction_solution)=(pfc_complement_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_induction_solution_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_induction_solution_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_induction_solution_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_induction_solution_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_induction_solution_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_induction_solution_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_induction_solution_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_induction_solution_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_induction_solution_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_induction_solution_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_induction_solution_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_induction_solution_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_induction_solution_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_induction_solution_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_induction_solution_witness_common_left_equivalent pfrep_left_gcd_induction_solution_witness_common_left_equivalent pfrep_right_gcd_induction_solution_witness_common_left_equivalent. ((exists pfrep_position_gcd_induction_solution_witness_common_left_equivalentfirst. ((pfrep_position_gcd_induction_solution_witness_common_left_equivalentfirst+S (pfrep_power_gcd_induction_solution_witness_common_left_equivalent)=(pfgd_P_gcd_induction_solution_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_induction_solution_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_induction_solution_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_induction_solution_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_induction_solution_witness_common_left)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_induction_solution_witness_common_left = ff_q_pfp_gcd_induction_solution_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_induction_solution_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_induction_solution_witness_common_left) + (pfrep_left_gcd_induction_solution_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_induction_solution_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_induction_solution_witness_common_left)=(pfrep_power_gcd_induction_solution_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_induction_solution_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_induction_solution_witness_common_left_equivalentsecond. ((pfrep_position_gcd_induction_solution_witness_common_left_equivalentsecond+S (pfrep_power_gcd_induction_solution_witness_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_induction_solution_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_induction_solution_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_induction_solution_witness_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_induction_solution_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_induction_solution_witness_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_induction_solution_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_induction_solution_witness_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_induction_solution_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_induction_solution_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_induction_solution_witness_common_left_equivalent=pfrep_right_gcd_induction_solution_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_induction_solution_witness_common_right_bounded. (exists fom_gap_pfp_gcd_induction_solution_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_induction_solution_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_common_right_bounded) = M) -> exists fom_value_pfp_gcd_induction_solution_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_induction_solution_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_induction_solution_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_induction_solution_witness_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_common_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_induction_solution_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_common_right_bounded)) * bc) + (fom_value_pfp_gcd_induction_solution_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_induction_solution_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_induction_solution_witness_common_right pfgd_qc_gcd_induction_solution_witness_common_right pfgd_Q_gcd_induction_solution_witness_common_right pfgd_pb_gcd_induction_solution_witness_common_right pfgd_pc_gcd_induction_solution_witness_common_right pfgd_P_gcd_induction_solution_witness_common_right. ((((forall fom_index_pfp_gcd_induction_solution_witness_common_right_productleft. (exists fom_gap_pfp_gcd_induction_solution_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_induction_solution_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_common_right_productleft) = pfgd_Q_gcd_induction_solution_witness_common_right) -> exists fom_value_pfp_gcd_induction_solution_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_induction_solution_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_induction_solution_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_induction_solution_witness_common_right_productleft)) * pfgd_qc_gcd_induction_solution_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_common_right_productleft_entry. pfgd_qb_gcd_induction_solution_witness_common_right = fom_beta_quotient_pfp_gcd_induction_solution_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_common_right_productleft)) * pfgd_qc_gcd_induction_solution_witness_common_right) + (fom_value_pfp_gcd_induction_solution_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_induction_solution_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_induction_solution_witness_common_right_productright. (exists fom_gap_pfp_gcd_induction_solution_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_induction_solution_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_common_right_productright) = pfgs_G_gcd_induction_solution) -> exists fom_value_pfp_gcd_induction_solution_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_induction_solution_witness_common_right_productright_entry + S (fom_value_pfp_gcd_induction_solution_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_induction_solution_witness_common_right_productright)) * pfgs_gc_gcd_induction_solution)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_common_right_productright_entry. pfgs_gb_gcd_induction_solution = fom_beta_quotient_pfp_gcd_induction_solution_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_common_right_productright)) * pfgs_gc_gcd_induction_solution) + (fom_value_pfp_gcd_induction_solution_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_induction_solution_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_induction_solution_witness_common_right)=0 \/ (pfgs_G_gcd_induction_solution)=0) /\ (((pfgd_P_gcd_induction_solution_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_induction_solution_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_induction_solution)=0)) /\ (((pfgd_Q_gcd_induction_solution_witness_common_right)+(pfgs_G_gcd_induction_solution)=S (pfgd_P_gcd_induction_solution_witness_common_right)))))))) /\ ((forall pfc_index_gcd_induction_solution_witness_common_right_productcoefficients. (exists pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientsbound. pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficients) = (pfgd_P_gcd_induction_solution_witness_common_right)) -> exists pfc_value_gcd_induction_solution_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_induction_solution_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficients)) * pfgd_pc_gcd_induction_solution_witness_common_right)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_induction_solution_witness_common_right = ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficients)) * pfgd_pc_gcd_induction_solution_witness_common_right) + (pfc_value_gcd_induction_solution_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_induction_solution_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_induction_solution_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_induction_solution_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_induction_solution_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_induction_solution_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_induction_solution_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_induction_solution_witness_common_right)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_induction_solution_witness_common_right = ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_induction_solution_witness_common_right) + (pfc_left_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_induction_solution_witness_common_right)=(pfc_index_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_induction_solution)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_induction_solution)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_induction_solution = ff_q_pfp_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_induction_solution) + (pfc_right_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_induction_solution)=(pfc_complement_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_induction_solution_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_induction_solution_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_induction_solution_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_induction_solution_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_induction_solution_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_induction_solution_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_induction_solution_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_induction_solution_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_induction_solution_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_induction_solution_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_induction_solution_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_induction_solution_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_induction_solution_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_induction_solution_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_induction_solution_witness_common_right_equivalent pfrep_left_gcd_induction_solution_witness_common_right_equivalent pfrep_right_gcd_induction_solution_witness_common_right_equivalent. ((exists pfrep_position_gcd_induction_solution_witness_common_right_equivalentfirst. ((pfrep_position_gcd_induction_solution_witness_common_right_equivalentfirst+S (pfrep_power_gcd_induction_solution_witness_common_right_equivalent)=(pfgd_P_gcd_induction_solution_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_induction_solution_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_induction_solution_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_induction_solution_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_induction_solution_witness_common_right)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_induction_solution_witness_common_right = ff_q_pfp_gcd_induction_solution_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_induction_solution_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_induction_solution_witness_common_right) + (pfrep_left_gcd_induction_solution_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_induction_solution_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_induction_solution_witness_common_right)=(pfrep_power_gcd_induction_solution_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_induction_solution_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_induction_solution_witness_common_right_equivalentsecond. ((pfrep_position_gcd_induction_solution_witness_common_right_equivalentsecond+S (pfrep_power_gcd_induction_solution_witness_common_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_induction_solution_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_induction_solution_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_induction_solution_witness_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_induction_solution_witness_common_right_equivalentsecondentry. bb = ff_q_pfp_gcd_induction_solution_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_induction_solution_witness_common_right_equivalentsecond)) * bc) + (pfrep_right_gcd_induction_solution_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_induction_solution_witness_common_right_equivalentsecondoutside+(M)=(pfrep_power_gcd_induction_solution_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_induction_solution_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_induction_solution_witness_common_right_equivalent=pfrep_right_gcd_induction_solution_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_induction_solution_witness_bezout pfgb_pc_gcd_induction_solution_witness_bezout pfgb_P_gcd_induction_solution_witness_bezout pfgb_qb_gcd_induction_solution_witness_bezout pfgb_qc_gcd_induction_solution_witness_bezout pfgb_Q_gcd_induction_solution_witness_bezout. ((((forall fom_index_pfp_gcd_induction_solution_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_bezout_leftleft) = pfgs_U_gcd_induction_solution) -> exists fom_value_pfp_gcd_induction_solution_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_induction_solution_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_induction_solution_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_leftleft)) * pfgs_uc_gcd_induction_solution)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_leftleft_entry. pfgs_ub_gcd_induction_solution = fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_leftleft)) * pfgs_uc_gcd_induction_solution) + (fom_value_pfp_gcd_induction_solution_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_induction_solution_witness_bezout_leftright. (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_bezout_leftright) = L) -> exists fom_value_pfp_gcd_induction_solution_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_induction_solution_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_induction_solution_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_leftright_entry. ab = fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_leftright)) * ac) + (fom_value_pfp_gcd_induction_solution_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_induction_solution)=0 \/ (L)=0) /\ (((pfgb_P_gcd_induction_solution_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_induction_solution)=0)) /\ (((~((L)=0)) /\ (((pfgs_U_gcd_induction_solution)+(L)=S (pfgb_P_gcd_induction_solution_witness_bezout)))))))) /\ ((forall pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients) = (pfgb_P_gcd_induction_solution_witness_bezout)) -> exists pfc_value_gcd_induction_solution_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_induction_solution_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_induction_solution_witness_bezout)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_induction_solution_witness_bezout = ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_induction_solution_witness_bezout) + (pfc_value_gcd_induction_solution_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_induction_solution)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_induction_solution)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_induction_solution = ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_induction_solution) + (pfc_left_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_induction_solution)=(pfc_index_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_induction_solution_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_induction_solution_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_induction_solution_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_induction_solution_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_induction_solution_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_induction_solution_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_bezout_rightleft) = pfgs_V_gcd_induction_solution) -> exists fom_value_pfp_gcd_induction_solution_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_induction_solution_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_induction_solution_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_rightleft)) * pfgs_vc_gcd_induction_solution)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_rightleft_entry. pfgs_vb_gcd_induction_solution = fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_rightleft)) * pfgs_vc_gcd_induction_solution) + (fom_value_pfp_gcd_induction_solution_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_induction_solution_witness_bezout_rightright. (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_bezout_rightright) = M) -> exists fom_value_pfp_gcd_induction_solution_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_induction_solution_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_induction_solution_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_rightright_entry. bb = fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_rightright)) * bc) + (fom_value_pfp_gcd_induction_solution_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_induction_solution)=0 \/ (M)=0) /\ (((pfgb_Q_gcd_induction_solution_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_induction_solution)=0)) /\ (((~((M)=0)) /\ (((pfgs_V_gcd_induction_solution)+(M)=S (pfgb_Q_gcd_induction_solution_witness_bezout)))))))) /\ ((forall pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_induction_solution_witness_bezout)) -> exists pfc_value_gcd_induction_solution_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_induction_solution_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_induction_solution_witness_bezout)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_induction_solution_witness_bezout = ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_induction_solution_witness_bezout) + (pfc_value_gcd_induction_solution_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_induction_solution)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_induction_solution)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_induction_solution = ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_induction_solution) + (pfc_left_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_induction_solution)=(pfc_index_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_induction_solution_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_induction_solution_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_induction_solution_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_induction_solution_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_induction_solution_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded) = pfgb_P_gcd_induction_solution_witness_bezout) -> exists fom_value_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_induction_solution_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_induction_solution_witness_bezout = fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_induction_solution_witness_bezout) + (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_induction_solution_witness_bezout) -> exists fom_value_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_induction_solution_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_induction_solution_witness_bezout = fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_induction_solution_witness_bezout) + (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded) = pfgs_G_gcd_induction_solution) -> exists fom_value_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_induction_solution)) /\ exists fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_induction_solution = fom_beta_quotient_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_induction_solution) + (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_induction_solution_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_induction_solution_witness_bezout_sum pfga_uc_gcd_induction_solution_witness_bezout_sum pfga_vb_gcd_induction_solution_witness_bezout_sum pfga_vc_gcd_induction_solution_witness_bezout_sum pfga_tb_gcd_induction_solution_witness_bezout_sum pfga_tc_gcd_induction_solution_witness_bezout_sum pfga_K_gcd_induction_solution_witness_bezout_sum. ((((forall pfrep_power_gcd_induction_solution_witness_bezout_sum_left pfrep_left_gcd_induction_solution_witness_bezout_sum_left pfrep_right_gcd_induction_solution_witness_bezout_sum_left. ((exists pfrep_position_gcd_induction_solution_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_induction_solution_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_induction_solution_witness_bezout_sum_left)=(pfgb_P_gcd_induction_solution_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_induction_solution_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_induction_solution_witness_bezout)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_induction_solution_witness_bezout = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_induction_solution_witness_bezout) + (pfrep_left_gcd_induction_solution_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_induction_solution_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_induction_solution_witness_bezout)=(pfrep_power_gcd_induction_solution_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_induction_solution_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_induction_solution_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_induction_solution_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_induction_solution_witness_bezout_sum_left)=(pfga_K_gcd_induction_solution_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_induction_solution_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_induction_solution_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_induction_solution_witness_bezout_sum = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_induction_solution_witness_bezout_sum) + (pfrep_right_gcd_induction_solution_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_induction_solution_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_induction_solution_witness_bezout_sum)=(pfrep_power_gcd_induction_solution_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_induction_solution_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_induction_solution_witness_bezout_sum_left=pfrep_right_gcd_induction_solution_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_induction_solution_witness_bezout_sum_right pfrep_left_gcd_induction_solution_witness_bezout_sum_right pfrep_right_gcd_induction_solution_witness_bezout_sum_right. ((exists pfrep_position_gcd_induction_solution_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_induction_solution_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_induction_solution_witness_bezout_sum_right)=(pfgb_Q_gcd_induction_solution_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_induction_solution_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_induction_solution_witness_bezout)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_induction_solution_witness_bezout = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_induction_solution_witness_bezout) + (pfrep_left_gcd_induction_solution_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_induction_solution_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_induction_solution_witness_bezout)=(pfrep_power_gcd_induction_solution_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_induction_solution_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_induction_solution_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_induction_solution_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_induction_solution_witness_bezout_sum_right)=(pfga_K_gcd_induction_solution_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_induction_solution_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_induction_solution_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_induction_solution_witness_bezout_sum = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_induction_solution_witness_bezout_sum) + (pfrep_right_gcd_induction_solution_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_induction_solution_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_induction_solution_witness_bezout_sum)=(pfrep_power_gcd_induction_solution_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_induction_solution_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_induction_solution_witness_bezout_sum_right=pfrep_right_gcd_induction_solution_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_induction_solution_witness_bezout_sum_add. (exists pfa_gap_gcd_induction_solution_witness_bezout_sum_addindex. pfa_gap_gcd_induction_solution_witness_bezout_sum_addindex + S (pfp_index_gcd_induction_solution_witness_bezout_sum_add) = (pfga_K_gcd_induction_solution_witness_bezout_sum)) -> exists pfp_left_gcd_induction_solution_witness_bezout_sum_add pfp_right_gcd_induction_solution_witness_bezout_sum_add pfp_value_gcd_induction_solution_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_addleft. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_addleft + S (pfp_left_gcd_induction_solution_witness_bezout_sum_add) = S ((S (pfp_index_gcd_induction_solution_witness_bezout_sum_add)) * pfga_uc_gcd_induction_solution_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_addleft. pfga_ub_gcd_induction_solution_witness_bezout_sum = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_induction_solution_witness_bezout_sum_add)) * pfga_uc_gcd_induction_solution_witness_bezout_sum) + (pfp_left_gcd_induction_solution_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_addright. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_addright + S (pfp_right_gcd_induction_solution_witness_bezout_sum_add) = S ((S (pfp_index_gcd_induction_solution_witness_bezout_sum_add)) * pfga_vc_gcd_induction_solution_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_addright. pfga_vb_gcd_induction_solution_witness_bezout_sum = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_addright * S ((S (pfp_index_gcd_induction_solution_witness_bezout_sum_add)) * pfga_vc_gcd_induction_solution_witness_bezout_sum) + (pfp_right_gcd_induction_solution_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_addtarget. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_addtarget + S (pfp_value_gcd_induction_solution_witness_bezout_sum_add) = S ((S (pfp_index_gcd_induction_solution_witness_bezout_sum_add)) * pfga_tc_gcd_induction_solution_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_addtarget. pfga_tb_gcd_induction_solution_witness_bezout_sum = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_induction_solution_witness_bezout_sum_add)) * pfga_tc_gcd_induction_solution_witness_bezout_sum) + (pfp_value_gcd_induction_solution_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_induction_solution_witness_bezout_sum_addoperationleft. pfa_gap_gcd_induction_solution_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_induction_solution_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_induction_solution_witness_bezout_sum_addoperationright. pfa_gap_gcd_induction_solution_witness_bezout_sum_addoperationright + S (pfp_right_gcd_induction_solution_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_induction_solution_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_induction_solution_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_induction_solution_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_induction_solution_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_induction_solution_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_induction_solution_witness_bezout_sum_add) + (pfp_right_gcd_induction_solution_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_induction_solution_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_induction_solution_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_induction_solution_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_induction_solution_witness_bezout_sum_result pfrep_left_gcd_induction_solution_witness_bezout_sum_result pfrep_right_gcd_induction_solution_witness_bezout_sum_result. ((exists pfrep_position_gcd_induction_solution_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_induction_solution_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_induction_solution_witness_bezout_sum_result)=(pfga_K_gcd_induction_solution_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_induction_solution_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_induction_solution_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_induction_solution_witness_bezout_sum = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_induction_solution_witness_bezout_sum) + (pfrep_left_gcd_induction_solution_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_induction_solution_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_induction_solution_witness_bezout_sum)=(pfrep_power_gcd_induction_solution_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_induction_solution_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_induction_solution_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_induction_solution_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_induction_solution_witness_bezout_sum_result)=(pfgs_G_gcd_induction_solution)) /\ ((((exists ff_h_pfp_gcd_induction_solution_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_induction_solution_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_induction_solution_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_induction_solution)) /\ exists ff_q_pfp_gcd_induction_solution_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_induction_solution = ff_q_pfp_gcd_induction_solution_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_induction_solution_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_induction_solution) + (pfrep_right_gcd_induction_solution_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_induction_solution_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_induction_solution_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_induction_solution)=(pfrep_power_gcd_induction_solution_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_induction_solution_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_induction_solution_witness_bezout_sum_result=pfrep_right_gcd_induction_solution_witness_bezout_sum_result)))))))))))))))))))))))
Complete tactic proof in conservative notation
All 205 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.
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.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial reduced representative exists.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial division execution exists.