Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
Exact theorem in conservative defined notation
∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ bb2. ∀ bc2. ∀ M2. Prime(p) → BetaPrefixInto(ab,ac,L,p) → BetaPrefixInto(bb2,bc2,M2,p) → PolynomialEquivalent(bb,bc,M,bb2,bc2,M2) → (∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. FpPolynomialZeroOrMonic(p,x,y,z) ∧ (FpPolynomialCommonRightDivisor(p,x,y,z,ab,ac,L,bb,bc,M) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,M,x,y,z,n,m,k,i,j,u))) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. FpPolynomialZeroOrMonic(p,x,y,z) ∧ (FpPolynomialCommonRightDivisor(p,x,y,z,ab,ac,L,bb2,bc2,M2) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb2,bc2,M2,x,y,z,n,m,k,i,j,u))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall p ab ac L bb bc M bb2 bc2 M2. (~((p) = 1) /\ forall pfa_factor_left_gcd_transport_prime pfa_factor_right_gcd_transport_prime. (p) = pfa_factor_left_gcd_transport_prime * pfa_factor_right_gcd_transport_prime -> pfa_factor_left_gcd_transport_prime = 1 \/ pfa_factor_right_gcd_transport_prime = 1) -> (forall fom_index_pfp_gcd_transport_A. (exists fom_gap_pfp_gcd_transport_A_index_bound. fom_gap_pfp_gcd_transport_A_index_bound + S (fom_index_pfp_gcd_transport_A) = L) -> exists fom_value_pfp_gcd_transport_A. ((((exists fom_beta_height_pfp_gcd_transport_A_entry. fom_beta_height_pfp_gcd_transport_A_entry + S (fom_value_pfp_gcd_transport_A) = S ((S (fom_index_pfp_gcd_transport_A)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_transport_A_entry. ab = fom_beta_quotient_pfp_gcd_transport_A_entry * S ((S (fom_index_pfp_gcd_transport_A)) * ac) + (fom_value_pfp_gcd_transport_A))) /\ (exists fom_gap_pfp_gcd_transport_A_value_bound. fom_gap_pfp_gcd_transport_A_value_bound + S (fom_value_pfp_gcd_transport_A) = p))) -> (forall fom_index_pfp_gcd_transport_B. (exists fom_gap_pfp_gcd_transport_B_index_bound. fom_gap_pfp_gcd_transport_B_index_bound + S (fom_index_pfp_gcd_transport_B) = M2) -> exists fom_value_pfp_gcd_transport_B. ((((exists fom_beta_height_pfp_gcd_transport_B_entry. fom_beta_height_pfp_gcd_transport_B_entry + S (fom_value_pfp_gcd_transport_B) = S ((S (fom_index_pfp_gcd_transport_B)) * bc2)) /\ exists fom_beta_quotient_pfp_gcd_transport_B_entry. bb2 = fom_beta_quotient_pfp_gcd_transport_B_entry * S ((S (fom_index_pfp_gcd_transport_B)) * bc2) + (fom_value_pfp_gcd_transport_B))) /\ (exists fom_gap_pfp_gcd_transport_B_value_bound. fom_gap_pfp_gcd_transport_B_value_bound + S (fom_value_pfp_gcd_transport_B) = p))) -> (forall pfrep_power_gcd_transport_equivalent pfrep_left_gcd_transport_equivalent pfrep_right_gcd_transport_equivalent. ((exists pfrep_position_gcd_transport_equivalentfirst. ((pfrep_position_gcd_transport_equivalentfirst+S (pfrep_power_gcd_transport_equivalent)=(M)) /\ ((((exists ff_h_pfp_gcd_transport_equivalentfirstentry. ff_h_pfp_gcd_transport_equivalentfirstentry + S (pfrep_left_gcd_transport_equivalent) = S ((S (pfrep_position_gcd_transport_equivalentfirst)) * bc)) /\ exists ff_q_pfp_gcd_transport_equivalentfirstentry. bb = ff_q_pfp_gcd_transport_equivalentfirstentry * S ((S (pfrep_position_gcd_transport_equivalentfirst)) * bc) + (pfrep_left_gcd_transport_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_equivalentfirstoutside. pfrep_gap_gcd_transport_equivalentfirstoutside+(M)=(pfrep_power_gcd_transport_equivalent)) /\ (((pfrep_left_gcd_transport_equivalent)=0))))) -> ((exists pfrep_position_gcd_transport_equivalentsecond. ((pfrep_position_gcd_transport_equivalentsecond+S (pfrep_power_gcd_transport_equivalent)=(M2)) /\ ((((exists ff_h_pfp_gcd_transport_equivalentsecondentry. ff_h_pfp_gcd_transport_equivalentsecondentry + S (pfrep_right_gcd_transport_equivalent) = S ((S (pfrep_position_gcd_transport_equivalentsecond)) * bc2)) /\ exists ff_q_pfp_gcd_transport_equivalentsecondentry. bb2 = ff_q_pfp_gcd_transport_equivalentsecondentry * S ((S (pfrep_position_gcd_transport_equivalentsecond)) * bc2) + (pfrep_right_gcd_transport_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_equivalentsecondoutside. pfrep_gap_gcd_transport_equivalentsecondoutside+(M2)=(pfrep_power_gcd_transport_equivalent)) /\ (((pfrep_right_gcd_transport_equivalent)=0))))) -> pfrep_left_gcd_transport_equivalent=pfrep_right_gcd_transport_equivalent) -> (exists pfgs_gb_gcd_transport_source pfgs_gc_gcd_transport_source pfgs_G_gcd_transport_source pfgs_ub_gcd_transport_source pfgs_uc_gcd_transport_source pfgs_U_gcd_transport_source pfgs_vb_gcd_transport_source pfgs_vc_gcd_transport_source pfgs_V_gcd_transport_source. (((pfgs_G_gcd_transport_source)=0 \/ (((~((pfgs_G_gcd_transport_source) = 0)) /\ (((forall fom_index_pfp_gcd_transport_source_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_transport_source_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_transport_source_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_transport_source_witness_normal_moniccoefficients) = pfgs_G_gcd_transport_source) -> exists fom_value_pfp_gcd_transport_source_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_transport_source_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_transport_source_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_transport_source_witness_normal_moniccoefficients)) * pfgs_gc_gcd_transport_source)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_transport_source = fom_beta_quotient_pfp_gcd_transport_source_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_normal_moniccoefficients)) * pfgs_gc_gcd_transport_source) + (fom_value_pfp_gcd_transport_source_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_transport_source_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_transport_source_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_normal_monicleading. ff_h_pfp_gcd_transport_source_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_transport_source)) /\ exists ff_q_pfp_gcd_transport_source_witness_normal_monicleading. pfgs_gb_gcd_transport_source = ff_q_pfp_gcd_transport_source_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_transport_source) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_transport_source_witness_common_left_bounded. (exists fom_gap_pfp_gcd_transport_source_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_transport_source_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_transport_source_witness_common_left_bounded) = L) -> exists fom_value_pfp_gcd_transport_source_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_transport_source_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_transport_source_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_transport_source_witness_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_transport_source_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_common_left_bounded)) * ac) + (fom_value_pfp_gcd_transport_source_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_transport_source_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_transport_source_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_transport_source_witness_common_left pfgd_qc_gcd_transport_source_witness_common_left pfgd_Q_gcd_transport_source_witness_common_left pfgd_pb_gcd_transport_source_witness_common_left pfgd_pc_gcd_transport_source_witness_common_left pfgd_P_gcd_transport_source_witness_common_left. ((((forall fom_index_pfp_gcd_transport_source_witness_common_left_productleft. (exists fom_gap_pfp_gcd_transport_source_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_transport_source_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_transport_source_witness_common_left_productleft) = pfgd_Q_gcd_transport_source_witness_common_left) -> exists fom_value_pfp_gcd_transport_source_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_transport_source_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_transport_source_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_transport_source_witness_common_left_productleft)) * pfgd_qc_gcd_transport_source_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_common_left_productleft_entry. pfgd_qb_gcd_transport_source_witness_common_left = fom_beta_quotient_pfp_gcd_transport_source_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_common_left_productleft)) * pfgd_qc_gcd_transport_source_witness_common_left) + (fom_value_pfp_gcd_transport_source_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_transport_source_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_transport_source_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_source_witness_common_left_productright. (exists fom_gap_pfp_gcd_transport_source_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_transport_source_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_transport_source_witness_common_left_productright) = pfgs_G_gcd_transport_source) -> exists fom_value_pfp_gcd_transport_source_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_transport_source_witness_common_left_productright_entry + S (fom_value_pfp_gcd_transport_source_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_transport_source_witness_common_left_productright)) * pfgs_gc_gcd_transport_source)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_common_left_productright_entry. pfgs_gb_gcd_transport_source = fom_beta_quotient_pfp_gcd_transport_source_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_common_left_productright)) * pfgs_gc_gcd_transport_source) + (fom_value_pfp_gcd_transport_source_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_transport_source_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_transport_source_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_transport_source_witness_common_left)=0 \/ (pfgs_G_gcd_transport_source)=0) /\ (((pfgd_P_gcd_transport_source_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_transport_source_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_transport_source)=0)) /\ (((pfgd_Q_gcd_transport_source_witness_common_left)+(pfgs_G_gcd_transport_source)=S (pfgd_P_gcd_transport_source_witness_common_left)))))))) /\ ((forall pfc_index_gcd_transport_source_witness_common_left_productcoefficients. (exists pfa_gap_gcd_transport_source_witness_common_left_productcoefficientsbound. pfa_gap_gcd_transport_source_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_transport_source_witness_common_left_productcoefficients) = (pfgd_P_gcd_transport_source_witness_common_left)) -> exists pfc_value_gcd_transport_source_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_transport_source_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_transport_source_witness_common_left_productcoefficients)) * pfgd_pc_gcd_transport_source_witness_common_left)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_transport_source_witness_common_left = ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_transport_source_witness_common_left_productcoefficients)) * pfgd_pc_gcd_transport_source_witness_common_left) + (pfc_value_gcd_transport_source_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_source_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_transport_source_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_transport_source_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_source_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_source_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_source_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_transport_source_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_source_witness_common_left)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_transport_source_witness_common_left = ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_source_witness_common_left) + (pfc_left_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_transport_source_witness_common_left)=(pfc_index_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_transport_source)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_source)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_transport_source = ff_q_pfp_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_source) + (pfc_right_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_transport_source)=(pfc_complement_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_source_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_source_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_source_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_source_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_source_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_source_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_source_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_source_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_source_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_source_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_source_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_source_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_source_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_source_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_source_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_transport_source_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_transport_source_witness_common_left_equivalent pfrep_left_gcd_transport_source_witness_common_left_equivalent pfrep_right_gcd_transport_source_witness_common_left_equivalent. ((exists pfrep_position_gcd_transport_source_witness_common_left_equivalentfirst. ((pfrep_position_gcd_transport_source_witness_common_left_equivalentfirst+S (pfrep_power_gcd_transport_source_witness_common_left_equivalent)=(pfgd_P_gcd_transport_source_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_transport_source_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_transport_source_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_transport_source_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_transport_source_witness_common_left)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_transport_source_witness_common_left = ff_q_pfp_gcd_transport_source_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_transport_source_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_transport_source_witness_common_left) + (pfrep_left_gcd_transport_source_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_transport_source_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_transport_source_witness_common_left)=(pfrep_power_gcd_transport_source_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_transport_source_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_transport_source_witness_common_left_equivalentsecond. ((pfrep_position_gcd_transport_source_witness_common_left_equivalentsecond+S (pfrep_power_gcd_transport_source_witness_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_transport_source_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_transport_source_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_transport_source_witness_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_transport_source_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_transport_source_witness_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_transport_source_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_transport_source_witness_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_transport_source_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_transport_source_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_transport_source_witness_common_left_equivalent=pfrep_right_gcd_transport_source_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_transport_source_witness_common_right_bounded. (exists fom_gap_pfp_gcd_transport_source_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_transport_source_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_transport_source_witness_common_right_bounded) = M) -> exists fom_value_pfp_gcd_transport_source_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_transport_source_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_transport_source_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_transport_source_witness_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_common_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_transport_source_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_common_right_bounded)) * bc) + (fom_value_pfp_gcd_transport_source_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_transport_source_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_transport_source_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_transport_source_witness_common_right pfgd_qc_gcd_transport_source_witness_common_right pfgd_Q_gcd_transport_source_witness_common_right pfgd_pb_gcd_transport_source_witness_common_right pfgd_pc_gcd_transport_source_witness_common_right pfgd_P_gcd_transport_source_witness_common_right. ((((forall fom_index_pfp_gcd_transport_source_witness_common_right_productleft. (exists fom_gap_pfp_gcd_transport_source_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_transport_source_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_transport_source_witness_common_right_productleft) = pfgd_Q_gcd_transport_source_witness_common_right) -> exists fom_value_pfp_gcd_transport_source_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_transport_source_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_transport_source_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_transport_source_witness_common_right_productleft)) * pfgd_qc_gcd_transport_source_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_common_right_productleft_entry. pfgd_qb_gcd_transport_source_witness_common_right = fom_beta_quotient_pfp_gcd_transport_source_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_common_right_productleft)) * pfgd_qc_gcd_transport_source_witness_common_right) + (fom_value_pfp_gcd_transport_source_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_transport_source_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_transport_source_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_source_witness_common_right_productright. (exists fom_gap_pfp_gcd_transport_source_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_transport_source_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_transport_source_witness_common_right_productright) = pfgs_G_gcd_transport_source) -> exists fom_value_pfp_gcd_transport_source_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_transport_source_witness_common_right_productright_entry + S (fom_value_pfp_gcd_transport_source_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_transport_source_witness_common_right_productright)) * pfgs_gc_gcd_transport_source)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_common_right_productright_entry. pfgs_gb_gcd_transport_source = fom_beta_quotient_pfp_gcd_transport_source_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_common_right_productright)) * pfgs_gc_gcd_transport_source) + (fom_value_pfp_gcd_transport_source_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_transport_source_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_transport_source_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_transport_source_witness_common_right)=0 \/ (pfgs_G_gcd_transport_source)=0) /\ (((pfgd_P_gcd_transport_source_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_transport_source_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_transport_source)=0)) /\ (((pfgd_Q_gcd_transport_source_witness_common_right)+(pfgs_G_gcd_transport_source)=S (pfgd_P_gcd_transport_source_witness_common_right)))))))) /\ ((forall pfc_index_gcd_transport_source_witness_common_right_productcoefficients. (exists pfa_gap_gcd_transport_source_witness_common_right_productcoefficientsbound. pfa_gap_gcd_transport_source_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_transport_source_witness_common_right_productcoefficients) = (pfgd_P_gcd_transport_source_witness_common_right)) -> exists pfc_value_gcd_transport_source_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_transport_source_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_transport_source_witness_common_right_productcoefficients)) * pfgd_pc_gcd_transport_source_witness_common_right)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_transport_source_witness_common_right = ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_transport_source_witness_common_right_productcoefficients)) * pfgd_pc_gcd_transport_source_witness_common_right) + (pfc_value_gcd_transport_source_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_source_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_transport_source_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_transport_source_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_source_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_source_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_source_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_transport_source_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_source_witness_common_right)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_transport_source_witness_common_right = ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_source_witness_common_right) + (pfc_left_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_transport_source_witness_common_right)=(pfc_index_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_transport_source)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_source)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_transport_source = ff_q_pfp_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_source) + (pfc_right_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_transport_source)=(pfc_complement_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_source_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_source_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_source_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_source_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_source_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_source_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_source_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_source_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_source_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_source_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_source_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_source_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_source_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_source_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_source_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_transport_source_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_transport_source_witness_common_right_equivalent pfrep_left_gcd_transport_source_witness_common_right_equivalent pfrep_right_gcd_transport_source_witness_common_right_equivalent. ((exists pfrep_position_gcd_transport_source_witness_common_right_equivalentfirst. ((pfrep_position_gcd_transport_source_witness_common_right_equivalentfirst+S (pfrep_power_gcd_transport_source_witness_common_right_equivalent)=(pfgd_P_gcd_transport_source_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_transport_source_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_transport_source_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_transport_source_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_transport_source_witness_common_right)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_transport_source_witness_common_right = ff_q_pfp_gcd_transport_source_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_transport_source_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_transport_source_witness_common_right) + (pfrep_left_gcd_transport_source_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_transport_source_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_transport_source_witness_common_right)=(pfrep_power_gcd_transport_source_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_transport_source_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_transport_source_witness_common_right_equivalentsecond. ((pfrep_position_gcd_transport_source_witness_common_right_equivalentsecond+S (pfrep_power_gcd_transport_source_witness_common_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_transport_source_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_transport_source_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_transport_source_witness_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_transport_source_witness_common_right_equivalentsecondentry. bb = ff_q_pfp_gcd_transport_source_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_transport_source_witness_common_right_equivalentsecond)) * bc) + (pfrep_right_gcd_transport_source_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_transport_source_witness_common_right_equivalentsecondoutside+(M)=(pfrep_power_gcd_transport_source_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_transport_source_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_transport_source_witness_common_right_equivalent=pfrep_right_gcd_transport_source_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_transport_source_witness_bezout pfgb_pc_gcd_transport_source_witness_bezout pfgb_P_gcd_transport_source_witness_bezout pfgb_qb_gcd_transport_source_witness_bezout pfgb_qc_gcd_transport_source_witness_bezout pfgb_Q_gcd_transport_source_witness_bezout. ((((forall fom_index_pfp_gcd_transport_source_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_transport_source_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_transport_source_witness_bezout_leftleft) = pfgs_U_gcd_transport_source) -> exists fom_value_pfp_gcd_transport_source_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_transport_source_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_transport_source_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_leftleft)) * pfgs_uc_gcd_transport_source)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_leftleft_entry. pfgs_ub_gcd_transport_source = fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_leftleft)) * pfgs_uc_gcd_transport_source) + (fom_value_pfp_gcd_transport_source_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_transport_source_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_source_witness_bezout_leftright. (exists fom_gap_pfp_gcd_transport_source_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_transport_source_witness_bezout_leftright) = L) -> exists fom_value_pfp_gcd_transport_source_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_transport_source_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_transport_source_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_leftright_entry. ab = fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_leftright)) * ac) + (fom_value_pfp_gcd_transport_source_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_transport_source_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_transport_source)=0 \/ (L)=0) /\ (((pfgb_P_gcd_transport_source_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_transport_source)=0)) /\ (((~((L)=0)) /\ (((pfgs_U_gcd_transport_source)+(L)=S (pfgb_P_gcd_transport_source_witness_bezout)))))))) /\ ((forall pfc_index_gcd_transport_source_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficients) = (pfgb_P_gcd_transport_source_witness_bezout)) -> exists pfc_value_gcd_transport_source_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_transport_source_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_transport_source_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_transport_source_witness_bezout = ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_transport_source_witness_bezout) + (pfc_value_gcd_transport_source_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_source_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_transport_source_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_transport_source_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_source_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_source_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_transport_source)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_transport_source)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_transport_source = ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_transport_source) + (pfc_left_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_transport_source)=(pfc_index_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_source_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_source_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_source_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_source_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_source_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_source_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_source_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_source_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_source_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_source_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_source_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_source_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_source_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_transport_source_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_transport_source_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_transport_source_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_transport_source_witness_bezout_rightleft) = pfgs_V_gcd_transport_source) -> exists fom_value_pfp_gcd_transport_source_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_transport_source_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_transport_source_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_rightleft)) * pfgs_vc_gcd_transport_source)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_rightleft_entry. pfgs_vb_gcd_transport_source = fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_rightleft)) * pfgs_vc_gcd_transport_source) + (fom_value_pfp_gcd_transport_source_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_transport_source_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_source_witness_bezout_rightright. (exists fom_gap_pfp_gcd_transport_source_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_transport_source_witness_bezout_rightright) = M) -> exists fom_value_pfp_gcd_transport_source_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_transport_source_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_transport_source_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_rightright_entry. bb = fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_rightright)) * bc) + (fom_value_pfp_gcd_transport_source_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_transport_source_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_transport_source)=0 \/ (M)=0) /\ (((pfgb_Q_gcd_transport_source_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_transport_source)=0)) /\ (((~((M)=0)) /\ (((pfgs_V_gcd_transport_source)+(M)=S (pfgb_Q_gcd_transport_source_witness_bezout)))))))) /\ ((forall pfc_index_gcd_transport_source_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_transport_source_witness_bezout)) -> exists pfc_value_gcd_transport_source_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_transport_source_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_transport_source_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_transport_source_witness_bezout = ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_transport_source_witness_bezout) + (pfc_value_gcd_transport_source_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_source_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_transport_source_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_transport_source_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_source_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_source_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_source_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_transport_source)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_transport_source)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_transport_source = ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_transport_source) + (pfc_left_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_transport_source)=(pfc_index_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_source_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_source_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_source_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_source_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_source_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_source_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_source_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_source_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_source_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_source_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_source_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_source_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_source_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_source_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_transport_source_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_transport_source_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_left_bounded) = pfgb_P_gcd_transport_source_witness_bezout) -> exists fom_value_pfp_gcd_transport_source_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_transport_source_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_transport_source_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_transport_source_witness_bezout = fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_transport_source_witness_bezout) + (fom_value_pfp_gcd_transport_source_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_transport_source_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_transport_source_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_transport_source_witness_bezout) -> exists fom_value_pfp_gcd_transport_source_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_transport_source_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_transport_source_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_transport_source_witness_bezout = fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_transport_source_witness_bezout) + (fom_value_pfp_gcd_transport_source_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_transport_source_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_transport_source_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_result_bounded) = pfgs_G_gcd_transport_source) -> exists fom_value_pfp_gcd_transport_source_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_transport_source_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_transport_source)) /\ exists fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_transport_source = fom_beta_quotient_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_transport_source_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_transport_source) + (fom_value_pfp_gcd_transport_source_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_transport_source_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_transport_source_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_transport_source_witness_bezout_sum pfga_uc_gcd_transport_source_witness_bezout_sum pfga_vb_gcd_transport_source_witness_bezout_sum pfga_vc_gcd_transport_source_witness_bezout_sum pfga_tb_gcd_transport_source_witness_bezout_sum pfga_tc_gcd_transport_source_witness_bezout_sum pfga_K_gcd_transport_source_witness_bezout_sum. ((((forall pfrep_power_gcd_transport_source_witness_bezout_sum_left pfrep_left_gcd_transport_source_witness_bezout_sum_left pfrep_right_gcd_transport_source_witness_bezout_sum_left. ((exists pfrep_position_gcd_transport_source_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_transport_source_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_transport_source_witness_bezout_sum_left)=(pfgb_P_gcd_transport_source_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_transport_source_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_transport_source_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_transport_source_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_transport_source_witness_bezout = ff_q_pfp_gcd_transport_source_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_transport_source_witness_bezout) + (pfrep_left_gcd_transport_source_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_transport_source_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_transport_source_witness_bezout)=(pfrep_power_gcd_transport_source_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_transport_source_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_transport_source_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_transport_source_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_transport_source_witness_bezout_sum_left)=(pfga_K_gcd_transport_source_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_transport_source_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_transport_source_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_transport_source_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_transport_source_witness_bezout_sum = ff_q_pfp_gcd_transport_source_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_transport_source_witness_bezout_sum) + (pfrep_right_gcd_transport_source_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_transport_source_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_transport_source_witness_bezout_sum)=(pfrep_power_gcd_transport_source_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_transport_source_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_transport_source_witness_bezout_sum_left=pfrep_right_gcd_transport_source_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_transport_source_witness_bezout_sum_right pfrep_left_gcd_transport_source_witness_bezout_sum_right pfrep_right_gcd_transport_source_witness_bezout_sum_right. ((exists pfrep_position_gcd_transport_source_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_transport_source_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_transport_source_witness_bezout_sum_right)=(pfgb_Q_gcd_transport_source_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_transport_source_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_transport_source_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_transport_source_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_transport_source_witness_bezout = ff_q_pfp_gcd_transport_source_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_transport_source_witness_bezout) + (pfrep_left_gcd_transport_source_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_transport_source_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_transport_source_witness_bezout)=(pfrep_power_gcd_transport_source_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_transport_source_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_transport_source_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_transport_source_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_transport_source_witness_bezout_sum_right)=(pfga_K_gcd_transport_source_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_transport_source_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_transport_source_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_transport_source_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_transport_source_witness_bezout_sum = ff_q_pfp_gcd_transport_source_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_transport_source_witness_bezout_sum) + (pfrep_right_gcd_transport_source_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_transport_source_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_transport_source_witness_bezout_sum)=(pfrep_power_gcd_transport_source_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_transport_source_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_transport_source_witness_bezout_sum_right=pfrep_right_gcd_transport_source_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_transport_source_witness_bezout_sum_add. (exists pfa_gap_gcd_transport_source_witness_bezout_sum_addindex. pfa_gap_gcd_transport_source_witness_bezout_sum_addindex + S (pfp_index_gcd_transport_source_witness_bezout_sum_add) = (pfga_K_gcd_transport_source_witness_bezout_sum)) -> exists pfp_left_gcd_transport_source_witness_bezout_sum_add pfp_right_gcd_transport_source_witness_bezout_sum_add pfp_value_gcd_transport_source_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_addleft. ff_h_pfp_gcd_transport_source_witness_bezout_sum_addleft + S (pfp_left_gcd_transport_source_witness_bezout_sum_add) = S ((S (pfp_index_gcd_transport_source_witness_bezout_sum_add)) * pfga_uc_gcd_transport_source_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_addleft. pfga_ub_gcd_transport_source_witness_bezout_sum = ff_q_pfp_gcd_transport_source_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_transport_source_witness_bezout_sum_add)) * pfga_uc_gcd_transport_source_witness_bezout_sum) + (pfp_left_gcd_transport_source_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_addright. ff_h_pfp_gcd_transport_source_witness_bezout_sum_addright + S (pfp_right_gcd_transport_source_witness_bezout_sum_add) = S ((S (pfp_index_gcd_transport_source_witness_bezout_sum_add)) * pfga_vc_gcd_transport_source_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_addright. pfga_vb_gcd_transport_source_witness_bezout_sum = ff_q_pfp_gcd_transport_source_witness_bezout_sum_addright * S ((S (pfp_index_gcd_transport_source_witness_bezout_sum_add)) * pfga_vc_gcd_transport_source_witness_bezout_sum) + (pfp_right_gcd_transport_source_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_addtarget. ff_h_pfp_gcd_transport_source_witness_bezout_sum_addtarget + S (pfp_value_gcd_transport_source_witness_bezout_sum_add) = S ((S (pfp_index_gcd_transport_source_witness_bezout_sum_add)) * pfga_tc_gcd_transport_source_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_addtarget. pfga_tb_gcd_transport_source_witness_bezout_sum = ff_q_pfp_gcd_transport_source_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_transport_source_witness_bezout_sum_add)) * pfga_tc_gcd_transport_source_witness_bezout_sum) + (pfp_value_gcd_transport_source_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_transport_source_witness_bezout_sum_addoperationleft. pfa_gap_gcd_transport_source_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_transport_source_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_transport_source_witness_bezout_sum_addoperationright. pfa_gap_gcd_transport_source_witness_bezout_sum_addoperationright + S (pfp_right_gcd_transport_source_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_transport_source_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_transport_source_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_transport_source_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_transport_source_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_transport_source_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_transport_source_witness_bezout_sum_add) + (pfp_right_gcd_transport_source_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_transport_source_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_transport_source_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_transport_source_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_transport_source_witness_bezout_sum_result pfrep_left_gcd_transport_source_witness_bezout_sum_result pfrep_right_gcd_transport_source_witness_bezout_sum_result. ((exists pfrep_position_gcd_transport_source_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_transport_source_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_transport_source_witness_bezout_sum_result)=(pfga_K_gcd_transport_source_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_transport_source_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_transport_source_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_transport_source_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_transport_source_witness_bezout_sum = ff_q_pfp_gcd_transport_source_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_transport_source_witness_bezout_sum) + (pfrep_left_gcd_transport_source_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_transport_source_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_transport_source_witness_bezout_sum)=(pfrep_power_gcd_transport_source_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_transport_source_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_transport_source_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_transport_source_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_transport_source_witness_bezout_sum_result)=(pfgs_G_gcd_transport_source)) /\ ((((exists ff_h_pfp_gcd_transport_source_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_transport_source_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_transport_source_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_transport_source)) /\ exists ff_q_pfp_gcd_transport_source_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_transport_source = ff_q_pfp_gcd_transport_source_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_transport_source_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_transport_source) + (pfrep_right_gcd_transport_source_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_transport_source_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_transport_source_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_transport_source)=(pfrep_power_gcd_transport_source_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_transport_source_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_transport_source_witness_bezout_sum_result=pfrep_right_gcd_transport_source_witness_bezout_sum_result))))))))))))))))))))))) -> (exists pfgs_gb_gcd_transport_result pfgs_gc_gcd_transport_result pfgs_G_gcd_transport_result pfgs_ub_gcd_transport_result pfgs_uc_gcd_transport_result pfgs_U_gcd_transport_result pfgs_vb_gcd_transport_result pfgs_vc_gcd_transport_result pfgs_V_gcd_transport_result. (((pfgs_G_gcd_transport_result)=0 \/ (((~((pfgs_G_gcd_transport_result) = 0)) /\ (((forall fom_index_pfp_gcd_transport_result_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_transport_result_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_transport_result_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_transport_result_witness_normal_moniccoefficients) = pfgs_G_gcd_transport_result) -> exists fom_value_pfp_gcd_transport_result_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_transport_result_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_transport_result_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_transport_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_transport_result)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_transport_result = fom_beta_quotient_pfp_gcd_transport_result_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_transport_result) + (fom_value_pfp_gcd_transport_result_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_transport_result_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_transport_result_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_normal_monicleading. ff_h_pfp_gcd_transport_result_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_transport_result)) /\ exists ff_q_pfp_gcd_transport_result_witness_normal_monicleading. pfgs_gb_gcd_transport_result = ff_q_pfp_gcd_transport_result_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_transport_result) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_transport_result_witness_common_left_bounded. (exists fom_gap_pfp_gcd_transport_result_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_transport_result_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_transport_result_witness_common_left_bounded) = L) -> exists fom_value_pfp_gcd_transport_result_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_transport_result_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_transport_result_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_transport_result_witness_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_transport_result_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_common_left_bounded)) * ac) + (fom_value_pfp_gcd_transport_result_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_transport_result_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_transport_result_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_transport_result_witness_common_left pfgd_qc_gcd_transport_result_witness_common_left pfgd_Q_gcd_transport_result_witness_common_left pfgd_pb_gcd_transport_result_witness_common_left pfgd_pc_gcd_transport_result_witness_common_left pfgd_P_gcd_transport_result_witness_common_left. ((((forall fom_index_pfp_gcd_transport_result_witness_common_left_productleft. (exists fom_gap_pfp_gcd_transport_result_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_transport_result_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_transport_result_witness_common_left_productleft) = pfgd_Q_gcd_transport_result_witness_common_left) -> exists fom_value_pfp_gcd_transport_result_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_transport_result_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_transport_result_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_transport_result_witness_common_left_productleft)) * pfgd_qc_gcd_transport_result_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_common_left_productleft_entry. pfgd_qb_gcd_transport_result_witness_common_left = fom_beta_quotient_pfp_gcd_transport_result_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_common_left_productleft)) * pfgd_qc_gcd_transport_result_witness_common_left) + (fom_value_pfp_gcd_transport_result_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_transport_result_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_transport_result_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_result_witness_common_left_productright. (exists fom_gap_pfp_gcd_transport_result_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_transport_result_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_transport_result_witness_common_left_productright) = pfgs_G_gcd_transport_result) -> exists fom_value_pfp_gcd_transport_result_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_transport_result_witness_common_left_productright_entry + S (fom_value_pfp_gcd_transport_result_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_transport_result_witness_common_left_productright)) * pfgs_gc_gcd_transport_result)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_common_left_productright_entry. pfgs_gb_gcd_transport_result = fom_beta_quotient_pfp_gcd_transport_result_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_common_left_productright)) * pfgs_gc_gcd_transport_result) + (fom_value_pfp_gcd_transport_result_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_transport_result_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_transport_result_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_transport_result_witness_common_left)=0 \/ (pfgs_G_gcd_transport_result)=0) /\ (((pfgd_P_gcd_transport_result_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_transport_result_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_transport_result)=0)) /\ (((pfgd_Q_gcd_transport_result_witness_common_left)+(pfgs_G_gcd_transport_result)=S (pfgd_P_gcd_transport_result_witness_common_left)))))))) /\ ((forall pfc_index_gcd_transport_result_witness_common_left_productcoefficients. (exists pfa_gap_gcd_transport_result_witness_common_left_productcoefficientsbound. pfa_gap_gcd_transport_result_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_transport_result_witness_common_left_productcoefficients) = (pfgd_P_gcd_transport_result_witness_common_left)) -> exists pfc_value_gcd_transport_result_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_transport_result_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_transport_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_transport_result_witness_common_left)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_transport_result_witness_common_left = ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_transport_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_transport_result_witness_common_left) + (pfc_value_gcd_transport_result_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_result_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_transport_result_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_transport_result_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_result_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_result_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_result_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_transport_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_result_witness_common_left)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_transport_result_witness_common_left = ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_result_witness_common_left) + (pfc_left_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_transport_result_witness_common_left)=(pfc_index_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_transport_result)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_result)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_transport_result = ff_q_pfp_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_result) + (pfc_right_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_transport_result)=(pfc_complement_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_result_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_result_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_result_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_result_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_result_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_result_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_result_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_result_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_result_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_result_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_result_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_result_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_result_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_transport_result_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_transport_result_witness_common_left_equivalent pfrep_left_gcd_transport_result_witness_common_left_equivalent pfrep_right_gcd_transport_result_witness_common_left_equivalent. ((exists pfrep_position_gcd_transport_result_witness_common_left_equivalentfirst. ((pfrep_position_gcd_transport_result_witness_common_left_equivalentfirst+S (pfrep_power_gcd_transport_result_witness_common_left_equivalent)=(pfgd_P_gcd_transport_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_transport_result_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_transport_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_transport_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_transport_result_witness_common_left)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_transport_result_witness_common_left = ff_q_pfp_gcd_transport_result_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_transport_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_transport_result_witness_common_left) + (pfrep_left_gcd_transport_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_transport_result_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_transport_result_witness_common_left)=(pfrep_power_gcd_transport_result_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_transport_result_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_transport_result_witness_common_left_equivalentsecond. ((pfrep_position_gcd_transport_result_witness_common_left_equivalentsecond+S (pfrep_power_gcd_transport_result_witness_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_transport_result_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_transport_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_transport_result_witness_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_transport_result_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_transport_result_witness_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_transport_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_transport_result_witness_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_transport_result_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_transport_result_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_transport_result_witness_common_left_equivalent=pfrep_right_gcd_transport_result_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_transport_result_witness_common_right_bounded. (exists fom_gap_pfp_gcd_transport_result_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_transport_result_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_transport_result_witness_common_right_bounded) = M2) -> exists fom_value_pfp_gcd_transport_result_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_transport_result_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_transport_result_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_transport_result_witness_common_right_bounded)) * bc2)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_common_right_bounded_entry. bb2 = fom_beta_quotient_pfp_gcd_transport_result_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_common_right_bounded)) * bc2) + (fom_value_pfp_gcd_transport_result_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_transport_result_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_transport_result_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_transport_result_witness_common_right pfgd_qc_gcd_transport_result_witness_common_right pfgd_Q_gcd_transport_result_witness_common_right pfgd_pb_gcd_transport_result_witness_common_right pfgd_pc_gcd_transport_result_witness_common_right pfgd_P_gcd_transport_result_witness_common_right. ((((forall fom_index_pfp_gcd_transport_result_witness_common_right_productleft. (exists fom_gap_pfp_gcd_transport_result_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_transport_result_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_transport_result_witness_common_right_productleft) = pfgd_Q_gcd_transport_result_witness_common_right) -> exists fom_value_pfp_gcd_transport_result_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_transport_result_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_transport_result_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_transport_result_witness_common_right_productleft)) * pfgd_qc_gcd_transport_result_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_common_right_productleft_entry. pfgd_qb_gcd_transport_result_witness_common_right = fom_beta_quotient_pfp_gcd_transport_result_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_common_right_productleft)) * pfgd_qc_gcd_transport_result_witness_common_right) + (fom_value_pfp_gcd_transport_result_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_transport_result_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_transport_result_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_result_witness_common_right_productright. (exists fom_gap_pfp_gcd_transport_result_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_transport_result_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_transport_result_witness_common_right_productright) = pfgs_G_gcd_transport_result) -> exists fom_value_pfp_gcd_transport_result_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_transport_result_witness_common_right_productright_entry + S (fom_value_pfp_gcd_transport_result_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_transport_result_witness_common_right_productright)) * pfgs_gc_gcd_transport_result)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_common_right_productright_entry. pfgs_gb_gcd_transport_result = fom_beta_quotient_pfp_gcd_transport_result_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_common_right_productright)) * pfgs_gc_gcd_transport_result) + (fom_value_pfp_gcd_transport_result_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_transport_result_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_transport_result_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_transport_result_witness_common_right)=0 \/ (pfgs_G_gcd_transport_result)=0) /\ (((pfgd_P_gcd_transport_result_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_transport_result_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_transport_result)=0)) /\ (((pfgd_Q_gcd_transport_result_witness_common_right)+(pfgs_G_gcd_transport_result)=S (pfgd_P_gcd_transport_result_witness_common_right)))))))) /\ ((forall pfc_index_gcd_transport_result_witness_common_right_productcoefficients. (exists pfa_gap_gcd_transport_result_witness_common_right_productcoefficientsbound. pfa_gap_gcd_transport_result_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_transport_result_witness_common_right_productcoefficients) = (pfgd_P_gcd_transport_result_witness_common_right)) -> exists pfc_value_gcd_transport_result_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_transport_result_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_transport_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_transport_result_witness_common_right)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_transport_result_witness_common_right = ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_transport_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_transport_result_witness_common_right) + (pfc_value_gcd_transport_result_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_result_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_transport_result_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_transport_result_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_result_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_result_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_result_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_transport_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_result_witness_common_right)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_transport_result_witness_common_right = ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_transport_result_witness_common_right) + (pfc_left_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_transport_result_witness_common_right)=(pfc_index_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_transport_result)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_result)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_transport_result = ff_q_pfp_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_transport_result) + (pfc_right_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_transport_result)=(pfc_complement_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_result_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_result_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_result_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_result_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_result_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_result_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_result_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_result_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_result_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_result_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_result_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_result_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_result_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_transport_result_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_transport_result_witness_common_right_equivalent pfrep_left_gcd_transport_result_witness_common_right_equivalent pfrep_right_gcd_transport_result_witness_common_right_equivalent. ((exists pfrep_position_gcd_transport_result_witness_common_right_equivalentfirst. ((pfrep_position_gcd_transport_result_witness_common_right_equivalentfirst+S (pfrep_power_gcd_transport_result_witness_common_right_equivalent)=(pfgd_P_gcd_transport_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_transport_result_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_transport_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_transport_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_transport_result_witness_common_right)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_transport_result_witness_common_right = ff_q_pfp_gcd_transport_result_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_transport_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_transport_result_witness_common_right) + (pfrep_left_gcd_transport_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_transport_result_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_transport_result_witness_common_right)=(pfrep_power_gcd_transport_result_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_transport_result_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_transport_result_witness_common_right_equivalentsecond. ((pfrep_position_gcd_transport_result_witness_common_right_equivalentsecond+S (pfrep_power_gcd_transport_result_witness_common_right_equivalent)=(M2)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_transport_result_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_transport_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_transport_result_witness_common_right_equivalentsecond)) * bc2)) /\ exists ff_q_pfp_gcd_transport_result_witness_common_right_equivalentsecondentry. bb2 = ff_q_pfp_gcd_transport_result_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_transport_result_witness_common_right_equivalentsecond)) * bc2) + (pfrep_right_gcd_transport_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_transport_result_witness_common_right_equivalentsecondoutside+(M2)=(pfrep_power_gcd_transport_result_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_transport_result_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_transport_result_witness_common_right_equivalent=pfrep_right_gcd_transport_result_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_transport_result_witness_bezout pfgb_pc_gcd_transport_result_witness_bezout pfgb_P_gcd_transport_result_witness_bezout pfgb_qb_gcd_transport_result_witness_bezout pfgb_qc_gcd_transport_result_witness_bezout pfgb_Q_gcd_transport_result_witness_bezout. ((((forall fom_index_pfp_gcd_transport_result_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_transport_result_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_transport_result_witness_bezout_leftleft) = pfgs_U_gcd_transport_result) -> exists fom_value_pfp_gcd_transport_result_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_transport_result_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_transport_result_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_leftleft)) * pfgs_uc_gcd_transport_result)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_leftleft_entry. pfgs_ub_gcd_transport_result = fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_leftleft)) * pfgs_uc_gcd_transport_result) + (fom_value_pfp_gcd_transport_result_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_transport_result_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_result_witness_bezout_leftright. (exists fom_gap_pfp_gcd_transport_result_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_transport_result_witness_bezout_leftright) = L) -> exists fom_value_pfp_gcd_transport_result_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_transport_result_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_transport_result_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_leftright_entry. ab = fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_leftright)) * ac) + (fom_value_pfp_gcd_transport_result_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_transport_result_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_transport_result)=0 \/ (L)=0) /\ (((pfgb_P_gcd_transport_result_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_transport_result)=0)) /\ (((~((L)=0)) /\ (((pfgs_U_gcd_transport_result)+(L)=S (pfgb_P_gcd_transport_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_transport_result_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficients) = (pfgb_P_gcd_transport_result_witness_bezout)) -> exists pfc_value_gcd_transport_result_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_transport_result_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_transport_result_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_transport_result_witness_bezout = ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_transport_result_witness_bezout) + (pfc_value_gcd_transport_result_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_result_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_transport_result_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_transport_result_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_result_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_result_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_transport_result)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_transport_result)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_transport_result = ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_transport_result) + (pfc_left_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_transport_result)=(pfc_index_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_result_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_result_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_result_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_result_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_result_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_result_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_result_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_result_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_result_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_result_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_result_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_result_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_transport_result_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_transport_result_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_transport_result_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_transport_result_witness_bezout_rightleft) = pfgs_V_gcd_transport_result) -> exists fom_value_pfp_gcd_transport_result_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_transport_result_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_transport_result_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_rightleft)) * pfgs_vc_gcd_transport_result)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_rightleft_entry. pfgs_vb_gcd_transport_result = fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_rightleft)) * pfgs_vc_gcd_transport_result) + (fom_value_pfp_gcd_transport_result_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_transport_result_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_transport_result_witness_bezout_rightright. (exists fom_gap_pfp_gcd_transport_result_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_transport_result_witness_bezout_rightright) = M2) -> exists fom_value_pfp_gcd_transport_result_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_transport_result_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_transport_result_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_rightright)) * bc2)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_rightright_entry. bb2 = fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_rightright)) * bc2) + (fom_value_pfp_gcd_transport_result_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_transport_result_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_transport_result)=0 \/ (M2)=0) /\ (((pfgb_Q_gcd_transport_result_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_transport_result)=0)) /\ (((~((M2)=0)) /\ (((pfgs_V_gcd_transport_result)+(M2)=S (pfgb_Q_gcd_transport_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_transport_result_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_transport_result_witness_bezout)) -> exists pfc_value_gcd_transport_result_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_transport_result_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_transport_result_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_transport_result_witness_bezout = ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_transport_result_witness_bezout) + (pfc_value_gcd_transport_result_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_transport_result_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_transport_result_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_transport_result_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_transport_result_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_transport_result_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_transport_result_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_transport_result)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_transport_result)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_transport_result = ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_transport_result) + (pfc_left_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_transport_result)=(pfc_index_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (M2)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc2)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb2 = ff_q_pfp_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc2) + (pfc_right_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(M2)=(pfc_complement_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_transport_result_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_transport_result_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_transport_result_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_transport_result_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_transport_result_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_transport_result_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_transport_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_transport_result_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_transport_result_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_transport_result_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_transport_result_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_transport_result_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_transport_result_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_transport_result_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_transport_result_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_transport_result_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_left_bounded) = pfgb_P_gcd_transport_result_witness_bezout) -> exists fom_value_pfp_gcd_transport_result_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_transport_result_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_transport_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_transport_result_witness_bezout = fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_transport_result_witness_bezout) + (fom_value_pfp_gcd_transport_result_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_transport_result_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_transport_result_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_transport_result_witness_bezout) -> exists fom_value_pfp_gcd_transport_result_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_transport_result_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_transport_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_transport_result_witness_bezout = fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_transport_result_witness_bezout) + (fom_value_pfp_gcd_transport_result_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_transport_result_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_transport_result_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_result_bounded) = pfgs_G_gcd_transport_result) -> exists fom_value_pfp_gcd_transport_result_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_transport_result_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_transport_result)) /\ exists fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_transport_result = fom_beta_quotient_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_transport_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_transport_result) + (fom_value_pfp_gcd_transport_result_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_transport_result_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_transport_result_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_transport_result_witness_bezout_sum pfga_uc_gcd_transport_result_witness_bezout_sum pfga_vb_gcd_transport_result_witness_bezout_sum pfga_vc_gcd_transport_result_witness_bezout_sum pfga_tb_gcd_transport_result_witness_bezout_sum pfga_tc_gcd_transport_result_witness_bezout_sum pfga_K_gcd_transport_result_witness_bezout_sum. ((((forall pfrep_power_gcd_transport_result_witness_bezout_sum_left pfrep_left_gcd_transport_result_witness_bezout_sum_left pfrep_right_gcd_transport_result_witness_bezout_sum_left. ((exists pfrep_position_gcd_transport_result_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_transport_result_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_transport_result_witness_bezout_sum_left)=(pfgb_P_gcd_transport_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_transport_result_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_transport_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_transport_result_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_transport_result_witness_bezout = ff_q_pfp_gcd_transport_result_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_transport_result_witness_bezout) + (pfrep_left_gcd_transport_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_transport_result_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_transport_result_witness_bezout)=(pfrep_power_gcd_transport_result_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_transport_result_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_transport_result_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_transport_result_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_transport_result_witness_bezout_sum_left)=(pfga_K_gcd_transport_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_transport_result_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_transport_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_transport_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_transport_result_witness_bezout_sum = ff_q_pfp_gcd_transport_result_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_transport_result_witness_bezout_sum) + (pfrep_right_gcd_transport_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_transport_result_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_transport_result_witness_bezout_sum)=(pfrep_power_gcd_transport_result_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_transport_result_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_transport_result_witness_bezout_sum_left=pfrep_right_gcd_transport_result_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_transport_result_witness_bezout_sum_right pfrep_left_gcd_transport_result_witness_bezout_sum_right pfrep_right_gcd_transport_result_witness_bezout_sum_right. ((exists pfrep_position_gcd_transport_result_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_transport_result_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_transport_result_witness_bezout_sum_right)=(pfgb_Q_gcd_transport_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_transport_result_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_transport_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_transport_result_witness_bezout)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_transport_result_witness_bezout = ff_q_pfp_gcd_transport_result_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_transport_result_witness_bezout) + (pfrep_left_gcd_transport_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_transport_result_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_transport_result_witness_bezout)=(pfrep_power_gcd_transport_result_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_transport_result_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_transport_result_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_transport_result_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_transport_result_witness_bezout_sum_right)=(pfga_K_gcd_transport_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_transport_result_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_transport_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_transport_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_transport_result_witness_bezout_sum = ff_q_pfp_gcd_transport_result_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_transport_result_witness_bezout_sum) + (pfrep_right_gcd_transport_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_transport_result_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_transport_result_witness_bezout_sum)=(pfrep_power_gcd_transport_result_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_transport_result_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_transport_result_witness_bezout_sum_right=pfrep_right_gcd_transport_result_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_transport_result_witness_bezout_sum_add. (exists pfa_gap_gcd_transport_result_witness_bezout_sum_addindex. pfa_gap_gcd_transport_result_witness_bezout_sum_addindex + S (pfp_index_gcd_transport_result_witness_bezout_sum_add) = (pfga_K_gcd_transport_result_witness_bezout_sum)) -> exists pfp_left_gcd_transport_result_witness_bezout_sum_add pfp_right_gcd_transport_result_witness_bezout_sum_add pfp_value_gcd_transport_result_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_addleft. ff_h_pfp_gcd_transport_result_witness_bezout_sum_addleft + S (pfp_left_gcd_transport_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_transport_result_witness_bezout_sum_add)) * pfga_uc_gcd_transport_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_addleft. pfga_ub_gcd_transport_result_witness_bezout_sum = ff_q_pfp_gcd_transport_result_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_transport_result_witness_bezout_sum_add)) * pfga_uc_gcd_transport_result_witness_bezout_sum) + (pfp_left_gcd_transport_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_addright. ff_h_pfp_gcd_transport_result_witness_bezout_sum_addright + S (pfp_right_gcd_transport_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_transport_result_witness_bezout_sum_add)) * pfga_vc_gcd_transport_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_addright. pfga_vb_gcd_transport_result_witness_bezout_sum = ff_q_pfp_gcd_transport_result_witness_bezout_sum_addright * S ((S (pfp_index_gcd_transport_result_witness_bezout_sum_add)) * pfga_vc_gcd_transport_result_witness_bezout_sum) + (pfp_right_gcd_transport_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_addtarget. ff_h_pfp_gcd_transport_result_witness_bezout_sum_addtarget + S (pfp_value_gcd_transport_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_transport_result_witness_bezout_sum_add)) * pfga_tc_gcd_transport_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_addtarget. pfga_tb_gcd_transport_result_witness_bezout_sum = ff_q_pfp_gcd_transport_result_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_transport_result_witness_bezout_sum_add)) * pfga_tc_gcd_transport_result_witness_bezout_sum) + (pfp_value_gcd_transport_result_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_transport_result_witness_bezout_sum_addoperationleft. pfa_gap_gcd_transport_result_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_transport_result_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_transport_result_witness_bezout_sum_addoperationright. pfa_gap_gcd_transport_result_witness_bezout_sum_addoperationright + S (pfp_right_gcd_transport_result_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_transport_result_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_transport_result_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_transport_result_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_transport_result_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_transport_result_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_transport_result_witness_bezout_sum_add) + (pfp_right_gcd_transport_result_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_transport_result_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_transport_result_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_transport_result_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_transport_result_witness_bezout_sum_result pfrep_left_gcd_transport_result_witness_bezout_sum_result pfrep_right_gcd_transport_result_witness_bezout_sum_result. ((exists pfrep_position_gcd_transport_result_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_transport_result_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_transport_result_witness_bezout_sum_result)=(pfga_K_gcd_transport_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_transport_result_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_transport_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_transport_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_transport_result_witness_bezout_sum = ff_q_pfp_gcd_transport_result_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_transport_result_witness_bezout_sum) + (pfrep_left_gcd_transport_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_transport_result_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_transport_result_witness_bezout_sum)=(pfrep_power_gcd_transport_result_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_transport_result_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_transport_result_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_transport_result_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_transport_result_witness_bezout_sum_result)=(pfgs_G_gcd_transport_result)) /\ ((((exists ff_h_pfp_gcd_transport_result_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_transport_result_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_transport_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_transport_result)) /\ exists ff_q_pfp_gcd_transport_result_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_transport_result = ff_q_pfp_gcd_transport_result_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_transport_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_transport_result) + (pfrep_right_gcd_transport_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_transport_result_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_transport_result_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_transport_result)=(pfrep_power_gcd_transport_result_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_transport_result_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_transport_result_witness_bezout_sum_result=pfrep_right_gcd_transport_result_witness_bezout_sum_result)))))))))))))))))))))))Complete tactic proof in conservative notation
All 113 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
113 script commands · 17 reading checkpoints · 3 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (3)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–15
03Establish hp0L16–21
04Separate the logical casesL22–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
cases hs - L23
cases hs_witness - L24
cases hs_witness_witness - L25
cases hs_witness_witness_witness - L26
cases hs_witness_witness_witness_witness - L27
cases hs_witness_witness_witness_witness_witness - L28
cases hs_witness_witness_witness_witness_witness_witness - L29
cases hs_witness_witness_witness_witness_witness_witness_witness - L30
cases hs_witness_witness_witness_witness_witness_witness_witness_witness - L31
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness
05Separate the logical casesL32–33
06Establish hGL34–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial right divides divisor bounded.
- L34
have hG : BetaPrefixInto(x,x1,x2,p)Definitions: BetaPrefixInto(x,x1,x2,p)Original native command in the exact edition - L35
specialize prime_field_polynomial_right_divides_divisor_bounded (p) - L36
specialize prime_field_polynomial_right_divides_divisor_bounded (x) - L37
specialize prime_field_polynomial_right_divides_divisor_bounded (x1) - L38
specialize prime_field_polynomial_right_divides_divisor_bounded (x2) - L39
specialize prime_field_polynomial_right_divides_divisor_bounded (ab) - L40
specialize prime_field_polynomial_right_divides_divisor_bounded (ac) - L41
specialize prime_field_polynomial_right_divides_divisor_bounded (L) - L42
apply prime_field_polynomial_right_divides_divisor_bounded - L43
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left_left
07Establish hbL44–53
Establish this local claim before using it. It is not an additional assumption.
- L44
have hb : FpPolynomialBezoutRepresentation(p,ab,ac,L,bb2,bc2,M2,x,x1,x2,x3,x4,x5,x6,x7,x8)Definitions: FpPolynomialBezoutRepresentation(p,ab,ac,L,bb2,bc2,M2,x,x1,x2,x3,x4,x5,x6,x7,x8)Original native command in the exact edition - L45
specialize prime_field_polynomial_bezout_equivalent_transport (p) - L46
specialize prime_field_polynomial_bezout_equivalent_transport (ab) - L47
specialize prime_field_polynomial_bezout_equivalent_transport (ac) - L48
specialize prime_field_polynomial_bezout_equivalent_transport (L) - L49
specialize prime_field_polynomial_bezout_equivalent_transport (bb) - L50
specialize prime_field_polynomial_bezout_equivalent_transport (bc) - L51
specialize prime_field_polynomial_bezout_equivalent_transport (M) - L52
specialize prime_field_polynomial_bezout_equivalent_transport (x) - L53
specialize prime_field_polynomial_bezout_equivalent_transport (x1)
08Use earlier factsL54–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
specialize prime_field_polynomial_bezout_equivalent_transport (x2) - L55
specialize prime_field_polynomial_bezout_equivalent_transport (x3) - L56
specialize prime_field_polynomial_bezout_equivalent_transport (x4) - L57
specialize prime_field_polynomial_bezout_equivalent_transport (x5) - L58
specialize prime_field_polynomial_bezout_equivalent_transport (x6) - L59
specialize prime_field_polynomial_bezout_equivalent_transport (x7) - L60
specialize prime_field_polynomial_bezout_equivalent_transport (x8) - L61
specialize prime_field_polynomial_bezout_equivalent_transport (ab) - L62
specialize prime_field_polynomial_bezout_equivalent_transport (ac) - L63
specialize prime_field_polynomial_bezout_equivalent_transport (L)
09Use earlier factsL64–73
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L64
specialize prime_field_polynomial_bezout_equivalent_transport (bb2) - L65
specialize prime_field_polynomial_bezout_equivalent_transport (bc2) - L66
specialize prime_field_polynomial_bezout_equivalent_transport (M2) - L67
specialize prime_field_polynomial_bezout_equivalent_transport (x) - L68
specialize prime_field_polynomial_bezout_equivalent_transport (x1) - L69
specialize prime_field_polynomial_bezout_equivalent_transport (x2) - L70
apply prime_field_polynomial_bezout_equivalent_transport - L71
exact hp0 - L72
exact hA - L73
exact hBB
10Use earlier factsL74–83
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L74
exact hG - L75
specialize prime_field_polynomial_power_coefficient_functional (ab) - L76
specialize prime_field_polynomial_power_coefficient_functional (ac) - L77
specialize prime_field_polynomial_power_coefficient_functional (L) - L78
apply prime_field_polynomial_power_coefficient_functional - L79
exact heq - L80
specialize prime_field_polynomial_power_coefficient_functional (x) - L81
specialize prime_field_polynomial_power_coefficient_functional (x1) - L82
specialize prime_field_polynomial_power_coefficient_functional (x2) - L83
apply prime_field_polynomial_power_coefficient_functional
11Use earlier factsL84–84
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L84
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right
12Construct an explicit witnessL85–93
13Separate the logical casesL94–94
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L94
split
14Use earlier factsL95–95
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L95
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_left
15Separate the logical casesL96–97
16Use earlier factsL98–107
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L98
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left_left - L99
specialize prime_field_polynomial_right_divides_equivalent_target (p) - L100
specialize prime_field_polynomial_right_divides_equivalent_target (x) - L101
specialize prime_field_polynomial_right_divides_equivalent_target (x1) - L102
specialize prime_field_polynomial_right_divides_equivalent_target (x2) - L103
specialize prime_field_polynomial_right_divides_equivalent_target (bb) - L104
specialize prime_field_polynomial_right_divides_equivalent_target (bc) - L105
specialize prime_field_polynomial_right_divides_equivalent_target (M) - L106
specialize prime_field_polynomial_right_divides_equivalent_target (bb2) - L107
specialize prime_field_polynomial_right_divides_equivalent_target (bc2)
17Use earlier factsL108–113
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 113 lines
- 0001
intro p - 0002
intro ab - 0003
intro ac - 0004
intro L - 0005
intro bb - 0006
intro bc - 0007
intro M - 0008
intro bb2 - 0009
intro bc2 - 0010
intro M2 - 0011
intro hp - 0012
intro hA - 0013
intro hBB - 0014
intro heq - 0015
intro hs - 0016
have hp0 : ~(p=0) - 0017
intro hz - 0018
specialize prime_nonzero (p) - 0019
apply prime_nonzero - 0020
exact hp - 0021
exact hz - 0022
cases hs - 0023
cases hs_witness - 0024
cases hs_witness_witness - 0025
cases hs_witness_witness_witness - 0026
cases hs_witness_witness_witness_witness - 0027
cases hs_witness_witness_witness_witness_witness - 0028
cases hs_witness_witness_witness_witness_witness_witness - 0029
cases hs_witness_witness_witness_witness_witness_witness_witness - 0030
cases hs_witness_witness_witness_witness_witness_witness_witness_witness - 0031
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0032
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - 0033
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0034
have hG : BetaPrefixInto(x,x1,x2,p) - 0035
specialize prime_field_polynomial_right_divides_divisor_bounded (p) - 0036
specialize prime_field_polynomial_right_divides_divisor_bounded (x) - 0037
specialize prime_field_polynomial_right_divides_divisor_bounded (x1) - 0038
specialize prime_field_polynomial_right_divides_divisor_bounded (x2) - 0039
specialize prime_field_polynomial_right_divides_divisor_bounded (ab) - 0040
specialize prime_field_polynomial_right_divides_divisor_bounded (ac) - 0041
specialize prime_field_polynomial_right_divides_divisor_bounded (L) - 0042
apply prime_field_polynomial_right_divides_divisor_bounded - 0043
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left_left - 0044
have hb : FpPolynomialBezoutRepresentation(p,ab,ac,L,bb2,bc2,M2,x,x1,x2,x3,x4,x5,x6,x7,x8) - 0045
specialize prime_field_polynomial_bezout_equivalent_transport (p) - 0046
specialize prime_field_polynomial_bezout_equivalent_transport (ab) - 0047
specialize prime_field_polynomial_bezout_equivalent_transport (ac) - 0048
specialize prime_field_polynomial_bezout_equivalent_transport (L) - 0049
specialize prime_field_polynomial_bezout_equivalent_transport (bb) - 0050
specialize prime_field_polynomial_bezout_equivalent_transport (bc) - 0051
specialize prime_field_polynomial_bezout_equivalent_transport (M) - 0052
specialize prime_field_polynomial_bezout_equivalent_transport (x) - 0053
specialize prime_field_polynomial_bezout_equivalent_transport (x1) - 0054
specialize prime_field_polynomial_bezout_equivalent_transport (x2) - 0055
specialize prime_field_polynomial_bezout_equivalent_transport (x3) - 0056
specialize prime_field_polynomial_bezout_equivalent_transport (x4) - 0057
specialize prime_field_polynomial_bezout_equivalent_transport (x5) - 0058
specialize prime_field_polynomial_bezout_equivalent_transport (x6) - 0059
specialize prime_field_polynomial_bezout_equivalent_transport (x7) - 0060
specialize prime_field_polynomial_bezout_equivalent_transport (x8) - 0061
specialize prime_field_polynomial_bezout_equivalent_transport (ab) - 0062
specialize prime_field_polynomial_bezout_equivalent_transport (ac) - 0063
specialize prime_field_polynomial_bezout_equivalent_transport (L) - 0064
specialize prime_field_polynomial_bezout_equivalent_transport (bb2) - 0065
specialize prime_field_polynomial_bezout_equivalent_transport (bc2) - 0066
specialize prime_field_polynomial_bezout_equivalent_transport (M2) - 0067
specialize prime_field_polynomial_bezout_equivalent_transport (x) - 0068
specialize prime_field_polynomial_bezout_equivalent_transport (x1) - 0069
specialize prime_field_polynomial_bezout_equivalent_transport (x2) - 0070
apply prime_field_polynomial_bezout_equivalent_transport - 0071
exact hp0 - 0072
exact hA - 0073
exact hBB - 0074
exact hG - 0075
specialize prime_field_polynomial_power_coefficient_functional (ab) - 0076
specialize prime_field_polynomial_power_coefficient_functional (ac) - 0077
specialize prime_field_polynomial_power_coefficient_functional (L) - 0078
apply prime_field_polynomial_power_coefficient_functional - 0079
exact heq - 0080
specialize prime_field_polynomial_power_coefficient_functional (x) - 0081
specialize prime_field_polynomial_power_coefficient_functional (x1) - 0082
specialize prime_field_polynomial_power_coefficient_functional (x2) - 0083
apply prime_field_polynomial_power_coefficient_functional - 0084
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0085
exists x - 0086
exists x1 - 0087
exists x2 - 0088
exists x3 - 0089
exists x4 - 0090
exists x5 - 0091
exists x6 - 0092
exists x7 - 0093
exists x8 - 0094
split - 0095
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0096
split - 0097
split - 0098
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left_left - 0099
specialize prime_field_polynomial_right_divides_equivalent_target (p) - 0100
specialize prime_field_polynomial_right_divides_equivalent_target (x) - 0101
specialize prime_field_polynomial_right_divides_equivalent_target (x1) - 0102
specialize prime_field_polynomial_right_divides_equivalent_target (x2) - 0103
specialize prime_field_polynomial_right_divides_equivalent_target (bb) - 0104
specialize prime_field_polynomial_right_divides_equivalent_target (bc) - 0105
specialize prime_field_polynomial_right_divides_equivalent_target (M) - 0106
specialize prime_field_polynomial_right_divides_equivalent_target (bb2) - 0107
specialize prime_field_polynomial_right_divides_equivalent_target (bc2) - 0108
specialize prime_field_polynomial_right_divides_equivalent_target (M2) - 0109
apply prime_field_polynomial_right_divides_equivalent_target - 0110
exact hBB - 0111
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left_right - 0112
exact heq - 0113
exact hb