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. ∀ La. ∀ bb. ∀ bc. ∀ Lb. ∀ rb. ∀ rc. ∀ Lr. ∀ qb. ∀ qc. ∀ Lq. ∀ pb. ∀ pc. ∀ Lp. ∀ gb. ∀ gc. ∀ Lg. ∀ ub. ∀ uc. ∀ Lu. ∀ vb. ∀ vc. ∀ Lv. Prime(p) → FpPolyProduct(p,qb,qc,Lq,bb,bc,Lb,pb,pc,Lp) → FpPolynomialAlignedAdd(p,pb,pc,Lp,rb,rc,Lr,ab,ac,La) → FpPolynomialBezoutRepresentation(p,bb,bc,Lb,rb,rc,Lr,gb,gc,Lg,ub,uc,Lu,vb,vc,Lv) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. FpPolyProduct(p,vb,vc,Lv,qb,qc,Lq,x,y,z) ∧ (FpPolynomialAlignedAdd(p,x,y,z,n,m,k,ub,uc,Lu) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,La,bb,bc,Lb,gb,gc,Lg,vb,vc,Lv,n,m,k) )Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG BetaPrefixInto(b,c,l,B) · 11 PolynomialProductLength(L,M,N) · 5 FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 15 FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 8 FpPolynomialBezoutRepresentation(p,ab,ac,A,bb,bc,B,gb,gc,G,ub,uc,U,vb,vc,V) · 2 Prime(p) · 2 Actual proof prerequisites Original expanded first-order statement
forall p ab ac La bb bc Lb rb rc Lr qb qc Lq pb pc Lp gb gc Lg ub uc Lu vb vc Lv. (~((p) = 1) /\ forall pfa_factor_left_bezout_backward_prime pfa_factor_right_bezout_backward_prime. (p) = pfa_factor_left_bezout_backward_prime * pfa_factor_right_bezout_backward_prime -> pfa_factor_left_bezout_backward_prime = 1 \/ pfa_factor_right_bezout_backward_prime = 1) -> (((forall fom_index_pfp_bezout_backward_productleft. (exists fom_gap_pfp_bezout_backward_productleft_index_bound. fom_gap_pfp_bezout_backward_productleft_index_bound + S (fom_index_pfp_bezout_backward_productleft) = Lq) -> exists fom_value_pfp_bezout_backward_productleft. ((((exists fom_beta_height_pfp_bezout_backward_productleft_entry. fom_beta_height_pfp_bezout_backward_productleft_entry + S (fom_value_pfp_bezout_backward_productleft) = S ((S (fom_index_pfp_bezout_backward_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_bezout_backward_productleft_entry. qb = fom_beta_quotient_pfp_bezout_backward_productleft_entry * S ((S (fom_index_pfp_bezout_backward_productleft)) * qc) + (fom_value_pfp_bezout_backward_productleft))) /\ (exists fom_gap_pfp_bezout_backward_productleft_value_bound. fom_gap_pfp_bezout_backward_productleft_value_bound + S (fom_value_pfp_bezout_backward_productleft) = p))) /\ (((forall fom_index_pfp_bezout_backward_productright. (exists fom_gap_pfp_bezout_backward_productright_index_bound. fom_gap_pfp_bezout_backward_productright_index_bound + S (fom_index_pfp_bezout_backward_productright) = Lb) -> exists fom_value_pfp_bezout_backward_productright. ((((exists fom_beta_height_pfp_bezout_backward_productright_entry. fom_beta_height_pfp_bezout_backward_productright_entry + S (fom_value_pfp_bezout_backward_productright) = S ((S (fom_index_pfp_bezout_backward_productright)) * bc)) /\ exists fom_beta_quotient_pfp_bezout_backward_productright_entry. bb = fom_beta_quotient_pfp_bezout_backward_productright_entry * S ((S (fom_index_pfp_bezout_backward_productright)) * bc) + (fom_value_pfp_bezout_backward_productright))) /\ (exists fom_gap_pfp_bezout_backward_productright_value_bound. fom_gap_pfp_bezout_backward_productright_value_bound + S (fom_value_pfp_bezout_backward_productright) = p))) /\ (((((((Lq)=0 \/ (Lb)=0) /\ (((Lp)=0)))) \/ (((~((Lq)=0)) /\ (((~((Lb)=0)) /\ (((Lq)+(Lb)=S (Lp)))))))) /\ ((forall pfc_index_bezout_backward_productcoefficients. (exists pfa_gap_bezout_backward_productcoefficientsbound. pfa_gap_bezout_backward_productcoefficientsbound + S (pfc_index_bezout_backward_productcoefficients) = (Lp)) -> exists pfc_value_bezout_backward_productcoefficients. ((((exists ff_h_pfp_bezout_backward_productcoefficientsentry. ff_h_pfp_bezout_backward_productcoefficientsentry + S (pfc_value_bezout_backward_productcoefficients) = S ((S (pfc_index_bezout_backward_productcoefficients)) * pc)) /\ exists ff_q_pfp_bezout_backward_productcoefficientsentry. pb = ff_q_pfp_bezout_backward_productcoefficientsentry * S ((S (pfc_index_bezout_backward_productcoefficients)) * pc) + (pfc_value_bezout_backward_productcoefficients))) /\ ((exists pfc_terms_code_bezout_backward_productcoefficientscoefficient pfc_terms_scale_bezout_backward_productcoefficientscoefficient pfc_natural_sum_bezout_backward_productcoefficientscoefficient. ((forall pfc_index_bezout_backward_productcoefficientscoefficientdiagonal. (exists pfa_gap_bezout_backward_productcoefficientscoefficientdiagonalbound. pfa_gap_bezout_backward_productcoefficientscoefficientdiagonalbound + S (pfc_index_bezout_backward_productcoefficientscoefficientdiagonal) = (S (pfc_index_bezout_backward_productcoefficients))) -> exists pfc_value_bezout_backward_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bezout_backward_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bezout_backward_productcoefficientscoefficientdiagonalentry + S (pfc_value_bezout_backward_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bezout_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_productcoefficientscoefficient)) /\ exists ff_q_pfp_bezout_backward_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bezout_backward_productcoefficientscoefficient = ff_q_pfp_bezout_backward_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bezout_backward_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_productcoefficientscoefficient) + (pfc_value_bezout_backward_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bezout_backward_productcoefficientscoefficientdiagonalterm pfc_left_bezout_backward_productcoefficientscoefficientdiagonalterm pfc_right_bezout_backward_productcoefficientscoefficientdiagonalterm. (((pfc_index_bezout_backward_productcoefficientscoefficientdiagonal)+pfc_complement_bezout_backward_productcoefficientscoefficientdiagonalterm=(pfc_index_bezout_backward_productcoefficients)) /\ ((((((exists pfa_gap_bezout_backward_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bezout_backward_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bezout_backward_productcoefficientscoefficientdiagonal) = (Lq)) /\ ((((exists ff_h_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bezout_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bezout_backward_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bezout_backward_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_bezout_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bezout_backward_productcoefficientscoefficientdiagonaltermleftoutside+(Lq)=(pfc_index_bezout_backward_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bezout_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bezout_backward_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bezout_backward_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bezout_backward_productcoefficientscoefficientdiagonalterm) = (Lb)) /\ ((((exists ff_h_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bezout_backward_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bezout_backward_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_bezout_backward_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bezout_backward_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_bezout_backward_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bezout_backward_productcoefficientscoefficientdiagonaltermrightoutside+(Lb)=(pfc_complement_bezout_backward_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bezout_backward_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bezout_backward_productcoefficientscoefficientdiagonal)=pfc_left_bezout_backward_productcoefficientscoefficientdiagonalterm*pfc_right_bezout_backward_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bezout_backward_productcoefficientscoefficientsum fs_v_pfc_bezout_backward_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_start. fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_start. fs_u_pfc_bezout_backward_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bezout_backward_productcoefficientscoefficient) = S ((S (S (pfc_index_bezout_backward_productcoefficients))) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bezout_backward_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bezout_backward_productcoefficients))) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum) + (pfc_natural_sum_bezout_backward_productcoefficientscoefficient))) /\ forall fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps = S (pfc_index_bezout_backward_productcoefficients)) -> exists fs_a_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps fs_r_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps fs_s_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_productcoefficientscoefficient)) /\ exists fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bezout_backward_productcoefficientscoefficient = fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_productcoefficientscoefficient) + (fs_a_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bezout_backward_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum) + (fs_r_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bezout_backward_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_productcoefficientscoefficientsum) + (fs_s_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bezout_backward_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bezout_backward_productcoefficientscoefficientresiduebound. pfa_gap_bezout_backward_productcoefficientscoefficientresiduebound + S (pfc_value_bezout_backward_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bezout_backward_productcoefficientscoefficientresiduecongruence pfa_offset_right_bezout_backward_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bezout_backward_productcoefficientscoefficient) + (p) * pfa_offset_left_bezout_backward_productcoefficientscoefficientresiduecongruence = (pfc_value_bezout_backward_productcoefficients) + (p) * pfa_offset_right_bezout_backward_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_bezout_backward_identity_left_bounded. (exists fom_gap_pfp_bezout_backward_identity_left_bounded_index_bound. fom_gap_pfp_bezout_backward_identity_left_bounded_index_bound + S (fom_index_pfp_bezout_backward_identity_left_bounded) = Lp) -> exists fom_value_pfp_bezout_backward_identity_left_bounded. ((((exists fom_beta_height_pfp_bezout_backward_identity_left_bounded_entry. fom_beta_height_pfp_bezout_backward_identity_left_bounded_entry + S (fom_value_pfp_bezout_backward_identity_left_bounded) = S ((S (fom_index_pfp_bezout_backward_identity_left_bounded)) * pc)) /\ exists fom_beta_quotient_pfp_bezout_backward_identity_left_bounded_entry. pb = fom_beta_quotient_pfp_bezout_backward_identity_left_bounded_entry * S ((S (fom_index_pfp_bezout_backward_identity_left_bounded)) * pc) + (fom_value_pfp_bezout_backward_identity_left_bounded))) /\ (exists fom_gap_pfp_bezout_backward_identity_left_bounded_value_bound. fom_gap_pfp_bezout_backward_identity_left_bounded_value_bound + S (fom_value_pfp_bezout_backward_identity_left_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_identity_right_bounded. (exists fom_gap_pfp_bezout_backward_identity_right_bounded_index_bound. fom_gap_pfp_bezout_backward_identity_right_bounded_index_bound + S (fom_index_pfp_bezout_backward_identity_right_bounded) = Lr) -> exists fom_value_pfp_bezout_backward_identity_right_bounded. ((((exists fom_beta_height_pfp_bezout_backward_identity_right_bounded_entry. fom_beta_height_pfp_bezout_backward_identity_right_bounded_entry + S (fom_value_pfp_bezout_backward_identity_right_bounded) = S ((S (fom_index_pfp_bezout_backward_identity_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_bezout_backward_identity_right_bounded_entry. rb = fom_beta_quotient_pfp_bezout_backward_identity_right_bounded_entry * S ((S (fom_index_pfp_bezout_backward_identity_right_bounded)) * rc) + (fom_value_pfp_bezout_backward_identity_right_bounded))) /\ (exists fom_gap_pfp_bezout_backward_identity_right_bounded_value_bound. fom_gap_pfp_bezout_backward_identity_right_bounded_value_bound + S (fom_value_pfp_bezout_backward_identity_right_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_identity_result_bounded. (exists fom_gap_pfp_bezout_backward_identity_result_bounded_index_bound. fom_gap_pfp_bezout_backward_identity_result_bounded_index_bound + S (fom_index_pfp_bezout_backward_identity_result_bounded) = La) -> exists fom_value_pfp_bezout_backward_identity_result_bounded. ((((exists fom_beta_height_pfp_bezout_backward_identity_result_bounded_entry. fom_beta_height_pfp_bezout_backward_identity_result_bounded_entry + S (fom_value_pfp_bezout_backward_identity_result_bounded) = S ((S (fom_index_pfp_bezout_backward_identity_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_bezout_backward_identity_result_bounded_entry. ab = fom_beta_quotient_pfp_bezout_backward_identity_result_bounded_entry * S ((S (fom_index_pfp_bezout_backward_identity_result_bounded)) * ac) + (fom_value_pfp_bezout_backward_identity_result_bounded))) /\ (exists fom_gap_pfp_bezout_backward_identity_result_bounded_value_bound. fom_gap_pfp_bezout_backward_identity_result_bounded_value_bound + S (fom_value_pfp_bezout_backward_identity_result_bounded) = p))) /\ ((exists pfaa_left_b_bezout_backward_identity pfaa_left_c_bezout_backward_identity pfaa_right_b_bezout_backward_identity pfaa_right_c_bezout_backward_identity pfaa_sum_b_bezout_backward_identity pfaa_sum_c_bezout_backward_identity pfaa_length_bezout_backward_identity. ((((forall pfrep_power_bezout_backward_identity_witness_common_left pfrep_left_bezout_backward_identity_witness_common_left pfrep_right_bezout_backward_identity_witness_common_left. ((exists pfrep_position_bezout_backward_identity_witness_common_leftfirst. ((pfrep_position_bezout_backward_identity_witness_common_leftfirst+S (pfrep_power_bezout_backward_identity_witness_common_left)=(Lp)) /\ ((((exists ff_h_pfp_bezout_backward_identity_witness_common_leftfirstentry. ff_h_pfp_bezout_backward_identity_witness_common_leftfirstentry + S (pfrep_left_bezout_backward_identity_witness_common_left) = S ((S (pfrep_position_bezout_backward_identity_witness_common_leftfirst)) * pc)) /\ exists ff_q_pfp_bezout_backward_identity_witness_common_leftfirstentry. pb = ff_q_pfp_bezout_backward_identity_witness_common_leftfirstentry * S ((S (pfrep_position_bezout_backward_identity_witness_common_leftfirst)) * pc) + (pfrep_left_bezout_backward_identity_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_identity_witness_common_leftfirstoutside. pfrep_gap_bezout_backward_identity_witness_common_leftfirstoutside+(Lp)=(pfrep_power_bezout_backward_identity_witness_common_left)) /\ (((pfrep_left_bezout_backward_identity_witness_common_left)=0))))) -> ((exists pfrep_position_bezout_backward_identity_witness_common_leftsecond. ((pfrep_position_bezout_backward_identity_witness_common_leftsecond+S (pfrep_power_bezout_backward_identity_witness_common_left)=(pfaa_length_bezout_backward_identity)) /\ ((((exists ff_h_pfp_bezout_backward_identity_witness_common_leftsecondentry. ff_h_pfp_bezout_backward_identity_witness_common_leftsecondentry + S (pfrep_right_bezout_backward_identity_witness_common_left) = S ((S (pfrep_position_bezout_backward_identity_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_identity)) /\ exists ff_q_pfp_bezout_backward_identity_witness_common_leftsecondentry. pfaa_left_b_bezout_backward_identity = ff_q_pfp_bezout_backward_identity_witness_common_leftsecondentry * S ((S (pfrep_position_bezout_backward_identity_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_identity) + (pfrep_right_bezout_backward_identity_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_identity_witness_common_leftsecondoutside. pfrep_gap_bezout_backward_identity_witness_common_leftsecondoutside+(pfaa_length_bezout_backward_identity)=(pfrep_power_bezout_backward_identity_witness_common_left)) /\ (((pfrep_right_bezout_backward_identity_witness_common_left)=0))))) -> pfrep_left_bezout_backward_identity_witness_common_left=pfrep_right_bezout_backward_identity_witness_common_left) /\ ((forall pfrep_power_bezout_backward_identity_witness_common_right pfrep_left_bezout_backward_identity_witness_common_right pfrep_right_bezout_backward_identity_witness_common_right. ((exists pfrep_position_bezout_backward_identity_witness_common_rightfirst. ((pfrep_position_bezout_backward_identity_witness_common_rightfirst+S (pfrep_power_bezout_backward_identity_witness_common_right)=(Lr)) /\ ((((exists ff_h_pfp_bezout_backward_identity_witness_common_rightfirstentry. ff_h_pfp_bezout_backward_identity_witness_common_rightfirstentry + S (pfrep_left_bezout_backward_identity_witness_common_right) = S ((S (pfrep_position_bezout_backward_identity_witness_common_rightfirst)) * rc)) /\ exists ff_q_pfp_bezout_backward_identity_witness_common_rightfirstentry. rb = ff_q_pfp_bezout_backward_identity_witness_common_rightfirstentry * S ((S (pfrep_position_bezout_backward_identity_witness_common_rightfirst)) * rc) + (pfrep_left_bezout_backward_identity_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_identity_witness_common_rightfirstoutside. pfrep_gap_bezout_backward_identity_witness_common_rightfirstoutside+(Lr)=(pfrep_power_bezout_backward_identity_witness_common_right)) /\ (((pfrep_left_bezout_backward_identity_witness_common_right)=0))))) -> ((exists pfrep_position_bezout_backward_identity_witness_common_rightsecond. ((pfrep_position_bezout_backward_identity_witness_common_rightsecond+S (pfrep_power_bezout_backward_identity_witness_common_right)=(pfaa_length_bezout_backward_identity)) /\ ((((exists ff_h_pfp_bezout_backward_identity_witness_common_rightsecondentry. ff_h_pfp_bezout_backward_identity_witness_common_rightsecondentry + S (pfrep_right_bezout_backward_identity_witness_common_right) = S ((S (pfrep_position_bezout_backward_identity_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_identity)) /\ exists ff_q_pfp_bezout_backward_identity_witness_common_rightsecondentry. pfaa_right_b_bezout_backward_identity = ff_q_pfp_bezout_backward_identity_witness_common_rightsecondentry * S ((S (pfrep_position_bezout_backward_identity_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_identity) + (pfrep_right_bezout_backward_identity_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_identity_witness_common_rightsecondoutside. pfrep_gap_bezout_backward_identity_witness_common_rightsecondoutside+(pfaa_length_bezout_backward_identity)=(pfrep_power_bezout_backward_identity_witness_common_right)) /\ (((pfrep_right_bezout_backward_identity_witness_common_right)=0))))) -> pfrep_left_bezout_backward_identity_witness_common_right=pfrep_right_bezout_backward_identity_witness_common_right)))) /\ (((forall pfp_index_bezout_backward_identity_witness_operation. (exists pfa_gap_bezout_backward_identity_witness_operationindex. pfa_gap_bezout_backward_identity_witness_operationindex + S (pfp_index_bezout_backward_identity_witness_operation) = (pfaa_length_bezout_backward_identity)) -> exists pfp_left_bezout_backward_identity_witness_operation pfp_right_bezout_backward_identity_witness_operation pfp_value_bezout_backward_identity_witness_operation. ((((exists ff_h_pfp_bezout_backward_identity_witness_operationleft. ff_h_pfp_bezout_backward_identity_witness_operationleft + S (pfp_left_bezout_backward_identity_witness_operation) = S ((S (pfp_index_bezout_backward_identity_witness_operation)) * pfaa_left_c_bezout_backward_identity)) /\ exists ff_q_pfp_bezout_backward_identity_witness_operationleft. pfaa_left_b_bezout_backward_identity = ff_q_pfp_bezout_backward_identity_witness_operationleft * S ((S (pfp_index_bezout_backward_identity_witness_operation)) * pfaa_left_c_bezout_backward_identity) + (pfp_left_bezout_backward_identity_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_identity_witness_operationright. ff_h_pfp_bezout_backward_identity_witness_operationright + S (pfp_right_bezout_backward_identity_witness_operation) = S ((S (pfp_index_bezout_backward_identity_witness_operation)) * pfaa_right_c_bezout_backward_identity)) /\ exists ff_q_pfp_bezout_backward_identity_witness_operationright. pfaa_right_b_bezout_backward_identity = ff_q_pfp_bezout_backward_identity_witness_operationright * S ((S (pfp_index_bezout_backward_identity_witness_operation)) * pfaa_right_c_bezout_backward_identity) + (pfp_right_bezout_backward_identity_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_identity_witness_operationtarget. ff_h_pfp_bezout_backward_identity_witness_operationtarget + S (pfp_value_bezout_backward_identity_witness_operation) = S ((S (pfp_index_bezout_backward_identity_witness_operation)) * pfaa_sum_c_bezout_backward_identity)) /\ exists ff_q_pfp_bezout_backward_identity_witness_operationtarget. pfaa_sum_b_bezout_backward_identity = ff_q_pfp_bezout_backward_identity_witness_operationtarget * S ((S (pfp_index_bezout_backward_identity_witness_operation)) * pfaa_sum_c_bezout_backward_identity) + (pfp_value_bezout_backward_identity_witness_operation))) /\ ((((exists pfa_gap_bezout_backward_identity_witness_operationoperationleft. pfa_gap_bezout_backward_identity_witness_operationoperationleft + S (pfp_left_bezout_backward_identity_witness_operation) = (p)) /\ (((exists pfa_gap_bezout_backward_identity_witness_operationoperationright. pfa_gap_bezout_backward_identity_witness_operationoperationright + S (pfp_right_bezout_backward_identity_witness_operation) = (p)) /\ ((((exists pfa_gap_bezout_backward_identity_witness_operationoperationresultbound. pfa_gap_bezout_backward_identity_witness_operationoperationresultbound + S (pfp_value_bezout_backward_identity_witness_operation) = (p)) /\ ((exists pfa_offset_left_bezout_backward_identity_witness_operationoperationresultcongruence pfa_offset_right_bezout_backward_identity_witness_operationoperationresultcongruence. ((pfp_left_bezout_backward_identity_witness_operation) + (pfp_right_bezout_backward_identity_witness_operation)) + (p) * pfa_offset_left_bezout_backward_identity_witness_operationoperationresultcongruence = (pfp_value_bezout_backward_identity_witness_operation) + (p) * pfa_offset_right_bezout_backward_identity_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_bezout_backward_identity_witness_output pfrep_left_bezout_backward_identity_witness_output pfrep_right_bezout_backward_identity_witness_output. ((exists pfrep_position_bezout_backward_identity_witness_outputfirst. ((pfrep_position_bezout_backward_identity_witness_outputfirst+S (pfrep_power_bezout_backward_identity_witness_output)=(pfaa_length_bezout_backward_identity)) /\ ((((exists ff_h_pfp_bezout_backward_identity_witness_outputfirstentry. ff_h_pfp_bezout_backward_identity_witness_outputfirstentry + S (pfrep_left_bezout_backward_identity_witness_output) = S ((S (pfrep_position_bezout_backward_identity_witness_outputfirst)) * pfaa_sum_c_bezout_backward_identity)) /\ exists ff_q_pfp_bezout_backward_identity_witness_outputfirstentry. pfaa_sum_b_bezout_backward_identity = ff_q_pfp_bezout_backward_identity_witness_outputfirstentry * S ((S (pfrep_position_bezout_backward_identity_witness_outputfirst)) * pfaa_sum_c_bezout_backward_identity) + (pfrep_left_bezout_backward_identity_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_identity_witness_outputfirstoutside. pfrep_gap_bezout_backward_identity_witness_outputfirstoutside+(pfaa_length_bezout_backward_identity)=(pfrep_power_bezout_backward_identity_witness_output)) /\ (((pfrep_left_bezout_backward_identity_witness_output)=0))))) -> ((exists pfrep_position_bezout_backward_identity_witness_outputsecond. ((pfrep_position_bezout_backward_identity_witness_outputsecond+S (pfrep_power_bezout_backward_identity_witness_output)=(La)) /\ ((((exists ff_h_pfp_bezout_backward_identity_witness_outputsecondentry. ff_h_pfp_bezout_backward_identity_witness_outputsecondentry + S (pfrep_right_bezout_backward_identity_witness_output) = S ((S (pfrep_position_bezout_backward_identity_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_bezout_backward_identity_witness_outputsecondentry. ab = ff_q_pfp_bezout_backward_identity_witness_outputsecondentry * S ((S (pfrep_position_bezout_backward_identity_witness_outputsecond)) * ac) + (pfrep_right_bezout_backward_identity_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_identity_witness_outputsecondoutside. pfrep_gap_bezout_backward_identity_witness_outputsecondoutside+(La)=(pfrep_power_bezout_backward_identity_witness_output)) /\ (((pfrep_right_bezout_backward_identity_witness_output)=0))))) -> pfrep_left_bezout_backward_identity_witness_output=pfrep_right_bezout_backward_identity_witness_output))))))))))))) -> (exists pfbz_left_code_bezout_backward_original pfbz_left_scale_bezout_backward_original pfbz_left_length_bezout_backward_original pfbz_right_code_bezout_backward_original pfbz_right_scale_bezout_backward_original pfbz_right_length_bezout_backward_original. ((((forall fom_index_pfp_bezout_backward_original_left_productleft. (exists fom_gap_pfp_bezout_backward_original_left_productleft_index_bound. fom_gap_pfp_bezout_backward_original_left_productleft_index_bound + S (fom_index_pfp_bezout_backward_original_left_productleft) = Lu) -> exists fom_value_pfp_bezout_backward_original_left_productleft. ((((exists fom_beta_height_pfp_bezout_backward_original_left_productleft_entry. fom_beta_height_pfp_bezout_backward_original_left_productleft_entry + S (fom_value_pfp_bezout_backward_original_left_productleft) = S ((S (fom_index_pfp_bezout_backward_original_left_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_bezout_backward_original_left_productleft_entry. ub = fom_beta_quotient_pfp_bezout_backward_original_left_productleft_entry * S ((S (fom_index_pfp_bezout_backward_original_left_productleft)) * uc) + (fom_value_pfp_bezout_backward_original_left_productleft))) /\ (exists fom_gap_pfp_bezout_backward_original_left_productleft_value_bound. fom_gap_pfp_bezout_backward_original_left_productleft_value_bound + S (fom_value_pfp_bezout_backward_original_left_productleft) = p))) /\ (((forall fom_index_pfp_bezout_backward_original_left_productright. (exists fom_gap_pfp_bezout_backward_original_left_productright_index_bound. fom_gap_pfp_bezout_backward_original_left_productright_index_bound + S (fom_index_pfp_bezout_backward_original_left_productright) = Lb) -> exists fom_value_pfp_bezout_backward_original_left_productright. ((((exists fom_beta_height_pfp_bezout_backward_original_left_productright_entry. fom_beta_height_pfp_bezout_backward_original_left_productright_entry + S (fom_value_pfp_bezout_backward_original_left_productright) = S ((S (fom_index_pfp_bezout_backward_original_left_productright)) * bc)) /\ exists fom_beta_quotient_pfp_bezout_backward_original_left_productright_entry. bb = fom_beta_quotient_pfp_bezout_backward_original_left_productright_entry * S ((S (fom_index_pfp_bezout_backward_original_left_productright)) * bc) + (fom_value_pfp_bezout_backward_original_left_productright))) /\ (exists fom_gap_pfp_bezout_backward_original_left_productright_value_bound. fom_gap_pfp_bezout_backward_original_left_productright_value_bound + S (fom_value_pfp_bezout_backward_original_left_productright) = p))) /\ (((((((Lu)=0 \/ (Lb)=0) /\ (((pfbz_left_length_bezout_backward_original)=0)))) \/ (((~((Lu)=0)) /\ (((~((Lb)=0)) /\ (((Lu)+(Lb)=S (pfbz_left_length_bezout_backward_original)))))))) /\ ((forall pfc_index_bezout_backward_original_left_productcoefficients. (exists pfa_gap_bezout_backward_original_left_productcoefficientsbound. pfa_gap_bezout_backward_original_left_productcoefficientsbound + S (pfc_index_bezout_backward_original_left_productcoefficients) = (pfbz_left_length_bezout_backward_original)) -> exists pfc_value_bezout_backward_original_left_productcoefficients. ((((exists ff_h_pfp_bezout_backward_original_left_productcoefficientsentry. ff_h_pfp_bezout_backward_original_left_productcoefficientsentry + S (pfc_value_bezout_backward_original_left_productcoefficients) = S ((S (pfc_index_bezout_backward_original_left_productcoefficients)) * pfbz_left_scale_bezout_backward_original)) /\ exists ff_q_pfp_bezout_backward_original_left_productcoefficientsentry. pfbz_left_code_bezout_backward_original = ff_q_pfp_bezout_backward_original_left_productcoefficientsentry * S ((S (pfc_index_bezout_backward_original_left_productcoefficients)) * pfbz_left_scale_bezout_backward_original) + (pfc_value_bezout_backward_original_left_productcoefficients))) /\ ((exists pfc_terms_code_bezout_backward_original_left_productcoefficientscoefficient pfc_terms_scale_bezout_backward_original_left_productcoefficientscoefficient pfc_natural_sum_bezout_backward_original_left_productcoefficientscoefficient. ((forall pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonalbound. pfa_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_bezout_backward_original_left_productcoefficients))) -> exists pfc_value_bezout_backward_original_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_bezout_backward_original_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_original_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bezout_backward_original_left_productcoefficientscoefficient = ff_q_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_original_left_productcoefficientscoefficient) + (pfc_value_bezout_backward_original_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm pfc_left_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm pfc_right_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal)+pfc_complement_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm=(pfc_index_bezout_backward_original_left_productcoefficients)) /\ ((((((exists pfa_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal) = (Lu)) /\ ((((exists ff_h_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermleftoutside+(Lu)=(pfc_index_bezout_backward_original_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm) = (Lb)) /\ ((((exists ff_h_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bezout_backward_original_left_productcoefficientscoefficientdiagonaltermrightoutside+(Lb)=(pfc_complement_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bezout_backward_original_left_productcoefficientscoefficientdiagonal)=pfc_left_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm*pfc_right_bezout_backward_original_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bezout_backward_original_left_productcoefficientscoefficientsum fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_bezout_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bezout_backward_original_left_productcoefficientscoefficient) = S ((S (S (pfc_index_bezout_backward_original_left_productcoefficients))) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bezout_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bezout_backward_original_left_productcoefficients))) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum) + (pfc_natural_sum_bezout_backward_original_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_bezout_backward_original_left_productcoefficients)) -> exists fs_a_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_original_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bezout_backward_original_left_productcoefficientscoefficient = fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_original_left_productcoefficientscoefficient) + (fs_a_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bezout_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum) + (fs_r_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bezout_backward_original_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_left_productcoefficientscoefficientsum) + (fs_s_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bezout_backward_original_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bezout_backward_original_left_productcoefficientscoefficientresiduebound. pfa_gap_bezout_backward_original_left_productcoefficientscoefficientresiduebound + S (pfc_value_bezout_backward_original_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bezout_backward_original_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_bezout_backward_original_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bezout_backward_original_left_productcoefficientscoefficient) + (p) * pfa_offset_left_bezout_backward_original_left_productcoefficientscoefficientresiduecongruence = (pfc_value_bezout_backward_original_left_productcoefficients) + (p) * pfa_offset_right_bezout_backward_original_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_bezout_backward_original_right_productleft. (exists fom_gap_pfp_bezout_backward_original_right_productleft_index_bound. fom_gap_pfp_bezout_backward_original_right_productleft_index_bound + S (fom_index_pfp_bezout_backward_original_right_productleft) = Lv) -> exists fom_value_pfp_bezout_backward_original_right_productleft. ((((exists fom_beta_height_pfp_bezout_backward_original_right_productleft_entry. fom_beta_height_pfp_bezout_backward_original_right_productleft_entry + S (fom_value_pfp_bezout_backward_original_right_productleft) = S ((S (fom_index_pfp_bezout_backward_original_right_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_bezout_backward_original_right_productleft_entry. vb = fom_beta_quotient_pfp_bezout_backward_original_right_productleft_entry * S ((S (fom_index_pfp_bezout_backward_original_right_productleft)) * vc) + (fom_value_pfp_bezout_backward_original_right_productleft))) /\ (exists fom_gap_pfp_bezout_backward_original_right_productleft_value_bound. fom_gap_pfp_bezout_backward_original_right_productleft_value_bound + S (fom_value_pfp_bezout_backward_original_right_productleft) = p))) /\ (((forall fom_index_pfp_bezout_backward_original_right_productright. (exists fom_gap_pfp_bezout_backward_original_right_productright_index_bound. fom_gap_pfp_bezout_backward_original_right_productright_index_bound + S (fom_index_pfp_bezout_backward_original_right_productright) = Lr) -> exists fom_value_pfp_bezout_backward_original_right_productright. ((((exists fom_beta_height_pfp_bezout_backward_original_right_productright_entry. fom_beta_height_pfp_bezout_backward_original_right_productright_entry + S (fom_value_pfp_bezout_backward_original_right_productright) = S ((S (fom_index_pfp_bezout_backward_original_right_productright)) * rc)) /\ exists fom_beta_quotient_pfp_bezout_backward_original_right_productright_entry. rb = fom_beta_quotient_pfp_bezout_backward_original_right_productright_entry * S ((S (fom_index_pfp_bezout_backward_original_right_productright)) * rc) + (fom_value_pfp_bezout_backward_original_right_productright))) /\ (exists fom_gap_pfp_bezout_backward_original_right_productright_value_bound. fom_gap_pfp_bezout_backward_original_right_productright_value_bound + S (fom_value_pfp_bezout_backward_original_right_productright) = p))) /\ (((((((Lv)=0 \/ (Lr)=0) /\ (((pfbz_right_length_bezout_backward_original)=0)))) \/ (((~((Lv)=0)) /\ (((~((Lr)=0)) /\ (((Lv)+(Lr)=S (pfbz_right_length_bezout_backward_original)))))))) /\ ((forall pfc_index_bezout_backward_original_right_productcoefficients. (exists pfa_gap_bezout_backward_original_right_productcoefficientsbound. pfa_gap_bezout_backward_original_right_productcoefficientsbound + S (pfc_index_bezout_backward_original_right_productcoefficients) = (pfbz_right_length_bezout_backward_original)) -> exists pfc_value_bezout_backward_original_right_productcoefficients. ((((exists ff_h_pfp_bezout_backward_original_right_productcoefficientsentry. ff_h_pfp_bezout_backward_original_right_productcoefficientsentry + S (pfc_value_bezout_backward_original_right_productcoefficients) = S ((S (pfc_index_bezout_backward_original_right_productcoefficients)) * pfbz_right_scale_bezout_backward_original)) /\ exists ff_q_pfp_bezout_backward_original_right_productcoefficientsentry. pfbz_right_code_bezout_backward_original = ff_q_pfp_bezout_backward_original_right_productcoefficientsentry * S ((S (pfc_index_bezout_backward_original_right_productcoefficients)) * pfbz_right_scale_bezout_backward_original) + (pfc_value_bezout_backward_original_right_productcoefficients))) /\ ((exists pfc_terms_code_bezout_backward_original_right_productcoefficientscoefficient pfc_terms_scale_bezout_backward_original_right_productcoefficientscoefficient pfc_natural_sum_bezout_backward_original_right_productcoefficientscoefficient. ((forall pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonalbound. pfa_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_bezout_backward_original_right_productcoefficients))) -> exists pfc_value_bezout_backward_original_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_bezout_backward_original_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_original_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bezout_backward_original_right_productcoefficientscoefficient = ff_q_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_original_right_productcoefficientscoefficient) + (pfc_value_bezout_backward_original_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm pfc_left_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm pfc_right_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal)+pfc_complement_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm=(pfc_index_bezout_backward_original_right_productcoefficients)) /\ ((((((exists pfa_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_bezout_backward_original_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm) = (Lr)) /\ ((((exists ff_h_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm)) * rc)) /\ exists ff_q_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry. rb = ff_q_pfp_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm)) * rc) + (pfc_right_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bezout_backward_original_right_productcoefficientscoefficientdiagonaltermrightoutside+(Lr)=(pfc_complement_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bezout_backward_original_right_productcoefficientscoefficientdiagonal)=pfc_left_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm*pfc_right_bezout_backward_original_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bezout_backward_original_right_productcoefficientscoefficientsum fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_bezout_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bezout_backward_original_right_productcoefficientscoefficient) = S ((S (S (pfc_index_bezout_backward_original_right_productcoefficients))) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bezout_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bezout_backward_original_right_productcoefficients))) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum) + (pfc_natural_sum_bezout_backward_original_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_bezout_backward_original_right_productcoefficients)) -> exists fs_a_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_original_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bezout_backward_original_right_productcoefficientscoefficient = fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_original_right_productcoefficientscoefficient) + (fs_a_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bezout_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum) + (fs_r_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bezout_backward_original_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_original_right_productcoefficientscoefficientsum) + (fs_s_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bezout_backward_original_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bezout_backward_original_right_productcoefficientscoefficientresiduebound. pfa_gap_bezout_backward_original_right_productcoefficientscoefficientresiduebound + S (pfc_value_bezout_backward_original_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bezout_backward_original_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_bezout_backward_original_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bezout_backward_original_right_productcoefficientscoefficient) + (p) * pfa_offset_left_bezout_backward_original_right_productcoefficientscoefficientresiduecongruence = (pfc_value_bezout_backward_original_right_productcoefficients) + (p) * pfa_offset_right_bezout_backward_original_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_bezout_backward_original_sum_left_bounded. (exists fom_gap_pfp_bezout_backward_original_sum_left_bounded_index_bound. fom_gap_pfp_bezout_backward_original_sum_left_bounded_index_bound + S (fom_index_pfp_bezout_backward_original_sum_left_bounded) = pfbz_left_length_bezout_backward_original) -> exists fom_value_pfp_bezout_backward_original_sum_left_bounded. ((((exists fom_beta_height_pfp_bezout_backward_original_sum_left_bounded_entry. fom_beta_height_pfp_bezout_backward_original_sum_left_bounded_entry + S (fom_value_pfp_bezout_backward_original_sum_left_bounded) = S ((S (fom_index_pfp_bezout_backward_original_sum_left_bounded)) * pfbz_left_scale_bezout_backward_original)) /\ exists fom_beta_quotient_pfp_bezout_backward_original_sum_left_bounded_entry. pfbz_left_code_bezout_backward_original = fom_beta_quotient_pfp_bezout_backward_original_sum_left_bounded_entry * S ((S (fom_index_pfp_bezout_backward_original_sum_left_bounded)) * pfbz_left_scale_bezout_backward_original) + (fom_value_pfp_bezout_backward_original_sum_left_bounded))) /\ (exists fom_gap_pfp_bezout_backward_original_sum_left_bounded_value_bound. fom_gap_pfp_bezout_backward_original_sum_left_bounded_value_bound + S (fom_value_pfp_bezout_backward_original_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_original_sum_right_bounded. (exists fom_gap_pfp_bezout_backward_original_sum_right_bounded_index_bound. fom_gap_pfp_bezout_backward_original_sum_right_bounded_index_bound + S (fom_index_pfp_bezout_backward_original_sum_right_bounded) = pfbz_right_length_bezout_backward_original) -> exists fom_value_pfp_bezout_backward_original_sum_right_bounded. ((((exists fom_beta_height_pfp_bezout_backward_original_sum_right_bounded_entry. fom_beta_height_pfp_bezout_backward_original_sum_right_bounded_entry + S (fom_value_pfp_bezout_backward_original_sum_right_bounded) = S ((S (fom_index_pfp_bezout_backward_original_sum_right_bounded)) * pfbz_right_scale_bezout_backward_original)) /\ exists fom_beta_quotient_pfp_bezout_backward_original_sum_right_bounded_entry. pfbz_right_code_bezout_backward_original = fom_beta_quotient_pfp_bezout_backward_original_sum_right_bounded_entry * S ((S (fom_index_pfp_bezout_backward_original_sum_right_bounded)) * pfbz_right_scale_bezout_backward_original) + (fom_value_pfp_bezout_backward_original_sum_right_bounded))) /\ (exists fom_gap_pfp_bezout_backward_original_sum_right_bounded_value_bound. fom_gap_pfp_bezout_backward_original_sum_right_bounded_value_bound + S (fom_value_pfp_bezout_backward_original_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_original_sum_result_bounded. (exists fom_gap_pfp_bezout_backward_original_sum_result_bounded_index_bound. fom_gap_pfp_bezout_backward_original_sum_result_bounded_index_bound + S (fom_index_pfp_bezout_backward_original_sum_result_bounded) = Lg) -> exists fom_value_pfp_bezout_backward_original_sum_result_bounded. ((((exists fom_beta_height_pfp_bezout_backward_original_sum_result_bounded_entry. fom_beta_height_pfp_bezout_backward_original_sum_result_bounded_entry + S (fom_value_pfp_bezout_backward_original_sum_result_bounded) = S ((S (fom_index_pfp_bezout_backward_original_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_bezout_backward_original_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_bezout_backward_original_sum_result_bounded_entry * S ((S (fom_index_pfp_bezout_backward_original_sum_result_bounded)) * gc) + (fom_value_pfp_bezout_backward_original_sum_result_bounded))) /\ (exists fom_gap_pfp_bezout_backward_original_sum_result_bounded_value_bound. fom_gap_pfp_bezout_backward_original_sum_result_bounded_value_bound + S (fom_value_pfp_bezout_backward_original_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_bezout_backward_original_sum pfaa_left_c_bezout_backward_original_sum pfaa_right_b_bezout_backward_original_sum pfaa_right_c_bezout_backward_original_sum pfaa_sum_b_bezout_backward_original_sum pfaa_sum_c_bezout_backward_original_sum pfaa_length_bezout_backward_original_sum. ((((forall pfrep_power_bezout_backward_original_sum_witness_common_left pfrep_left_bezout_backward_original_sum_witness_common_left pfrep_right_bezout_backward_original_sum_witness_common_left. ((exists pfrep_position_bezout_backward_original_sum_witness_common_leftfirst. ((pfrep_position_bezout_backward_original_sum_witness_common_leftfirst+S (pfrep_power_bezout_backward_original_sum_witness_common_left)=(pfbz_left_length_bezout_backward_original)) /\ ((((exists ff_h_pfp_bezout_backward_original_sum_witness_common_leftfirstentry. ff_h_pfp_bezout_backward_original_sum_witness_common_leftfirstentry + S (pfrep_left_bezout_backward_original_sum_witness_common_left) = S ((S (pfrep_position_bezout_backward_original_sum_witness_common_leftfirst)) * pfbz_left_scale_bezout_backward_original)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_common_leftfirstentry. pfbz_left_code_bezout_backward_original = ff_q_pfp_bezout_backward_original_sum_witness_common_leftfirstentry * S ((S (pfrep_position_bezout_backward_original_sum_witness_common_leftfirst)) * pfbz_left_scale_bezout_backward_original) + (pfrep_left_bezout_backward_original_sum_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_original_sum_witness_common_leftfirstoutside. pfrep_gap_bezout_backward_original_sum_witness_common_leftfirstoutside+(pfbz_left_length_bezout_backward_original)=(pfrep_power_bezout_backward_original_sum_witness_common_left)) /\ (((pfrep_left_bezout_backward_original_sum_witness_common_left)=0))))) -> ((exists pfrep_position_bezout_backward_original_sum_witness_common_leftsecond. ((pfrep_position_bezout_backward_original_sum_witness_common_leftsecond+S (pfrep_power_bezout_backward_original_sum_witness_common_left)=(pfaa_length_bezout_backward_original_sum)) /\ ((((exists ff_h_pfp_bezout_backward_original_sum_witness_common_leftsecondentry. ff_h_pfp_bezout_backward_original_sum_witness_common_leftsecondentry + S (pfrep_right_bezout_backward_original_sum_witness_common_left) = S ((S (pfrep_position_bezout_backward_original_sum_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_original_sum)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_common_leftsecondentry. pfaa_left_b_bezout_backward_original_sum = ff_q_pfp_bezout_backward_original_sum_witness_common_leftsecondentry * S ((S (pfrep_position_bezout_backward_original_sum_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_original_sum) + (pfrep_right_bezout_backward_original_sum_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_original_sum_witness_common_leftsecondoutside. pfrep_gap_bezout_backward_original_sum_witness_common_leftsecondoutside+(pfaa_length_bezout_backward_original_sum)=(pfrep_power_bezout_backward_original_sum_witness_common_left)) /\ (((pfrep_right_bezout_backward_original_sum_witness_common_left)=0))))) -> pfrep_left_bezout_backward_original_sum_witness_common_left=pfrep_right_bezout_backward_original_sum_witness_common_left) /\ ((forall pfrep_power_bezout_backward_original_sum_witness_common_right pfrep_left_bezout_backward_original_sum_witness_common_right pfrep_right_bezout_backward_original_sum_witness_common_right. ((exists pfrep_position_bezout_backward_original_sum_witness_common_rightfirst. ((pfrep_position_bezout_backward_original_sum_witness_common_rightfirst+S (pfrep_power_bezout_backward_original_sum_witness_common_right)=(pfbz_right_length_bezout_backward_original)) /\ ((((exists ff_h_pfp_bezout_backward_original_sum_witness_common_rightfirstentry. ff_h_pfp_bezout_backward_original_sum_witness_common_rightfirstentry + S (pfrep_left_bezout_backward_original_sum_witness_common_right) = S ((S (pfrep_position_bezout_backward_original_sum_witness_common_rightfirst)) * pfbz_right_scale_bezout_backward_original)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_common_rightfirstentry. pfbz_right_code_bezout_backward_original = ff_q_pfp_bezout_backward_original_sum_witness_common_rightfirstentry * S ((S (pfrep_position_bezout_backward_original_sum_witness_common_rightfirst)) * pfbz_right_scale_bezout_backward_original) + (pfrep_left_bezout_backward_original_sum_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_original_sum_witness_common_rightfirstoutside. pfrep_gap_bezout_backward_original_sum_witness_common_rightfirstoutside+(pfbz_right_length_bezout_backward_original)=(pfrep_power_bezout_backward_original_sum_witness_common_right)) /\ (((pfrep_left_bezout_backward_original_sum_witness_common_right)=0))))) -> ((exists pfrep_position_bezout_backward_original_sum_witness_common_rightsecond. ((pfrep_position_bezout_backward_original_sum_witness_common_rightsecond+S (pfrep_power_bezout_backward_original_sum_witness_common_right)=(pfaa_length_bezout_backward_original_sum)) /\ ((((exists ff_h_pfp_bezout_backward_original_sum_witness_common_rightsecondentry. ff_h_pfp_bezout_backward_original_sum_witness_common_rightsecondentry + S (pfrep_right_bezout_backward_original_sum_witness_common_right) = S ((S (pfrep_position_bezout_backward_original_sum_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_original_sum)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_common_rightsecondentry. pfaa_right_b_bezout_backward_original_sum = ff_q_pfp_bezout_backward_original_sum_witness_common_rightsecondentry * S ((S (pfrep_position_bezout_backward_original_sum_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_original_sum) + (pfrep_right_bezout_backward_original_sum_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_original_sum_witness_common_rightsecondoutside. pfrep_gap_bezout_backward_original_sum_witness_common_rightsecondoutside+(pfaa_length_bezout_backward_original_sum)=(pfrep_power_bezout_backward_original_sum_witness_common_right)) /\ (((pfrep_right_bezout_backward_original_sum_witness_common_right)=0))))) -> pfrep_left_bezout_backward_original_sum_witness_common_right=pfrep_right_bezout_backward_original_sum_witness_common_right)))) /\ (((forall pfp_index_bezout_backward_original_sum_witness_operation. (exists pfa_gap_bezout_backward_original_sum_witness_operationindex. pfa_gap_bezout_backward_original_sum_witness_operationindex + S (pfp_index_bezout_backward_original_sum_witness_operation) = (pfaa_length_bezout_backward_original_sum)) -> exists pfp_left_bezout_backward_original_sum_witness_operation pfp_right_bezout_backward_original_sum_witness_operation pfp_value_bezout_backward_original_sum_witness_operation. ((((exists ff_h_pfp_bezout_backward_original_sum_witness_operationleft. ff_h_pfp_bezout_backward_original_sum_witness_operationleft + S (pfp_left_bezout_backward_original_sum_witness_operation) = S ((S (pfp_index_bezout_backward_original_sum_witness_operation)) * pfaa_left_c_bezout_backward_original_sum)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_operationleft. pfaa_left_b_bezout_backward_original_sum = ff_q_pfp_bezout_backward_original_sum_witness_operationleft * S ((S (pfp_index_bezout_backward_original_sum_witness_operation)) * pfaa_left_c_bezout_backward_original_sum) + (pfp_left_bezout_backward_original_sum_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_original_sum_witness_operationright. ff_h_pfp_bezout_backward_original_sum_witness_operationright + S (pfp_right_bezout_backward_original_sum_witness_operation) = S ((S (pfp_index_bezout_backward_original_sum_witness_operation)) * pfaa_right_c_bezout_backward_original_sum)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_operationright. pfaa_right_b_bezout_backward_original_sum = ff_q_pfp_bezout_backward_original_sum_witness_operationright * S ((S (pfp_index_bezout_backward_original_sum_witness_operation)) * pfaa_right_c_bezout_backward_original_sum) + (pfp_right_bezout_backward_original_sum_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_original_sum_witness_operationtarget. ff_h_pfp_bezout_backward_original_sum_witness_operationtarget + S (pfp_value_bezout_backward_original_sum_witness_operation) = S ((S (pfp_index_bezout_backward_original_sum_witness_operation)) * pfaa_sum_c_bezout_backward_original_sum)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_operationtarget. pfaa_sum_b_bezout_backward_original_sum = ff_q_pfp_bezout_backward_original_sum_witness_operationtarget * S ((S (pfp_index_bezout_backward_original_sum_witness_operation)) * pfaa_sum_c_bezout_backward_original_sum) + (pfp_value_bezout_backward_original_sum_witness_operation))) /\ ((((exists pfa_gap_bezout_backward_original_sum_witness_operationoperationleft. pfa_gap_bezout_backward_original_sum_witness_operationoperationleft + S (pfp_left_bezout_backward_original_sum_witness_operation) = (p)) /\ (((exists pfa_gap_bezout_backward_original_sum_witness_operationoperationright. pfa_gap_bezout_backward_original_sum_witness_operationoperationright + S (pfp_right_bezout_backward_original_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_bezout_backward_original_sum_witness_operationoperationresultbound. pfa_gap_bezout_backward_original_sum_witness_operationoperationresultbound + S (pfp_value_bezout_backward_original_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_bezout_backward_original_sum_witness_operationoperationresultcongruence pfa_offset_right_bezout_backward_original_sum_witness_operationoperationresultcongruence. ((pfp_left_bezout_backward_original_sum_witness_operation) + (pfp_right_bezout_backward_original_sum_witness_operation)) + (p) * pfa_offset_left_bezout_backward_original_sum_witness_operationoperationresultcongruence = (pfp_value_bezout_backward_original_sum_witness_operation) + (p) * pfa_offset_right_bezout_backward_original_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_bezout_backward_original_sum_witness_output pfrep_left_bezout_backward_original_sum_witness_output pfrep_right_bezout_backward_original_sum_witness_output. ((exists pfrep_position_bezout_backward_original_sum_witness_outputfirst. ((pfrep_position_bezout_backward_original_sum_witness_outputfirst+S (pfrep_power_bezout_backward_original_sum_witness_output)=(pfaa_length_bezout_backward_original_sum)) /\ ((((exists ff_h_pfp_bezout_backward_original_sum_witness_outputfirstentry. ff_h_pfp_bezout_backward_original_sum_witness_outputfirstentry + S (pfrep_left_bezout_backward_original_sum_witness_output) = S ((S (pfrep_position_bezout_backward_original_sum_witness_outputfirst)) * pfaa_sum_c_bezout_backward_original_sum)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_outputfirstentry. pfaa_sum_b_bezout_backward_original_sum = ff_q_pfp_bezout_backward_original_sum_witness_outputfirstentry * S ((S (pfrep_position_bezout_backward_original_sum_witness_outputfirst)) * pfaa_sum_c_bezout_backward_original_sum) + (pfrep_left_bezout_backward_original_sum_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_original_sum_witness_outputfirstoutside. pfrep_gap_bezout_backward_original_sum_witness_outputfirstoutside+(pfaa_length_bezout_backward_original_sum)=(pfrep_power_bezout_backward_original_sum_witness_output)) /\ (((pfrep_left_bezout_backward_original_sum_witness_output)=0))))) -> ((exists pfrep_position_bezout_backward_original_sum_witness_outputsecond. ((pfrep_position_bezout_backward_original_sum_witness_outputsecond+S (pfrep_power_bezout_backward_original_sum_witness_output)=(Lg)) /\ ((((exists ff_h_pfp_bezout_backward_original_sum_witness_outputsecondentry. ff_h_pfp_bezout_backward_original_sum_witness_outputsecondentry + S (pfrep_right_bezout_backward_original_sum_witness_output) = S ((S (pfrep_position_bezout_backward_original_sum_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_bezout_backward_original_sum_witness_outputsecondentry. gb = ff_q_pfp_bezout_backward_original_sum_witness_outputsecondentry * S ((S (pfrep_position_bezout_backward_original_sum_witness_outputsecond)) * gc) + (pfrep_right_bezout_backward_original_sum_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_original_sum_witness_outputsecondoutside. pfrep_gap_bezout_backward_original_sum_witness_outputsecondoutside+(Lg)=(pfrep_power_bezout_backward_original_sum_witness_output)) /\ (((pfrep_right_bezout_backward_original_sum_witness_output)=0))))) -> pfrep_left_bezout_backward_original_sum_witness_output=pfrep_right_bezout_backward_original_sum_witness_output)))))))))))))))))) -> (exists pfbz_update_wb_bezout_backward_result pfbz_update_wc_bezout_backward_result pfbz_update_W_bezout_backward_result pfbz_update_tb_bezout_backward_result pfbz_update_tc_bezout_backward_result pfbz_update_T_bezout_backward_result. ((((forall fom_index_pfp_bezout_backward_result_coefficient_productleft. (exists fom_gap_pfp_bezout_backward_result_coefficient_productleft_index_bound. fom_gap_pfp_bezout_backward_result_coefficient_productleft_index_bound + S (fom_index_pfp_bezout_backward_result_coefficient_productleft) = Lv) -> exists fom_value_pfp_bezout_backward_result_coefficient_productleft. ((((exists fom_beta_height_pfp_bezout_backward_result_coefficient_productleft_entry. fom_beta_height_pfp_bezout_backward_result_coefficient_productleft_entry + S (fom_value_pfp_bezout_backward_result_coefficient_productleft) = S ((S (fom_index_pfp_bezout_backward_result_coefficient_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_coefficient_productleft_entry. vb = fom_beta_quotient_pfp_bezout_backward_result_coefficient_productleft_entry * S ((S (fom_index_pfp_bezout_backward_result_coefficient_productleft)) * vc) + (fom_value_pfp_bezout_backward_result_coefficient_productleft))) /\ (exists fom_gap_pfp_bezout_backward_result_coefficient_productleft_value_bound. fom_gap_pfp_bezout_backward_result_coefficient_productleft_value_bound + S (fom_value_pfp_bezout_backward_result_coefficient_productleft) = p))) /\ (((forall fom_index_pfp_bezout_backward_result_coefficient_productright. (exists fom_gap_pfp_bezout_backward_result_coefficient_productright_index_bound. fom_gap_pfp_bezout_backward_result_coefficient_productright_index_bound + S (fom_index_pfp_bezout_backward_result_coefficient_productright) = Lq) -> exists fom_value_pfp_bezout_backward_result_coefficient_productright. ((((exists fom_beta_height_pfp_bezout_backward_result_coefficient_productright_entry. fom_beta_height_pfp_bezout_backward_result_coefficient_productright_entry + S (fom_value_pfp_bezout_backward_result_coefficient_productright) = S ((S (fom_index_pfp_bezout_backward_result_coefficient_productright)) * qc)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_coefficient_productright_entry. qb = fom_beta_quotient_pfp_bezout_backward_result_coefficient_productright_entry * S ((S (fom_index_pfp_bezout_backward_result_coefficient_productright)) * qc) + (fom_value_pfp_bezout_backward_result_coefficient_productright))) /\ (exists fom_gap_pfp_bezout_backward_result_coefficient_productright_value_bound. fom_gap_pfp_bezout_backward_result_coefficient_productright_value_bound + S (fom_value_pfp_bezout_backward_result_coefficient_productright) = p))) /\ (((((((Lv)=0 \/ (Lq)=0) /\ (((pfbz_update_W_bezout_backward_result)=0)))) \/ (((~((Lv)=0)) /\ (((~((Lq)=0)) /\ (((Lv)+(Lq)=S (pfbz_update_W_bezout_backward_result)))))))) /\ ((forall pfc_index_bezout_backward_result_coefficient_productcoefficients. (exists pfa_gap_bezout_backward_result_coefficient_productcoefficientsbound. pfa_gap_bezout_backward_result_coefficient_productcoefficientsbound + S (pfc_index_bezout_backward_result_coefficient_productcoefficients) = (pfbz_update_W_bezout_backward_result)) -> exists pfc_value_bezout_backward_result_coefficient_productcoefficients. ((((exists ff_h_pfp_bezout_backward_result_coefficient_productcoefficientsentry. ff_h_pfp_bezout_backward_result_coefficient_productcoefficientsentry + S (pfc_value_bezout_backward_result_coefficient_productcoefficients) = S ((S (pfc_index_bezout_backward_result_coefficient_productcoefficients)) * pfbz_update_wc_bezout_backward_result)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_productcoefficientsentry. pfbz_update_wb_bezout_backward_result = ff_q_pfp_bezout_backward_result_coefficient_productcoefficientsentry * S ((S (pfc_index_bezout_backward_result_coefficient_productcoefficients)) * pfbz_update_wc_bezout_backward_result) + (pfc_value_bezout_backward_result_coefficient_productcoefficients))) /\ ((exists pfc_terms_code_bezout_backward_result_coefficient_productcoefficientscoefficient pfc_terms_scale_bezout_backward_result_coefficient_productcoefficientscoefficient pfc_natural_sum_bezout_backward_result_coefficient_productcoefficientscoefficient. ((forall pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal. (exists pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalbound. pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalbound + S (pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal) = (S (pfc_index_bezout_backward_result_coefficient_productcoefficients))) -> exists pfc_value_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalentry + S (pfc_value_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_result_coefficient_productcoefficientscoefficient)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bezout_backward_result_coefficient_productcoefficientscoefficient = ff_q_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_result_coefficient_productcoefficientscoefficient) + (pfc_value_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm pfc_left_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm pfc_right_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm. (((pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal)+pfc_complement_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm=(pfc_index_bezout_backward_result_coefficient_productcoefficients)) /\ ((((((exists pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm) = (Lq)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)) * qc)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry. qb = ff_q_pfp_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)) * qc) + (pfc_right_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonaltermrightoutside+(Lq)=(pfc_complement_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonal)=pfc_left_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm*pfc_right_bezout_backward_result_coefficient_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_start. fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_start. fs_u_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bezout_backward_result_coefficient_productcoefficientscoefficient) = S ((S (S (pfc_index_bezout_backward_result_coefficient_productcoefficients))) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bezout_backward_result_coefficient_productcoefficients))) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum) + (pfc_natural_sum_bezout_backward_result_coefficient_productcoefficientscoefficient))) /\ forall fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps = S (pfc_index_bezout_backward_result_coefficient_productcoefficients)) -> exists fs_a_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps fs_r_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps fs_s_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_result_coefficient_productcoefficientscoefficient)) /\ exists fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bezout_backward_result_coefficient_productcoefficientscoefficient = fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_result_coefficient_productcoefficientscoefficient) + (fs_a_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum) + (fs_r_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum) + (fs_s_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bezout_backward_result_coefficient_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientresiduebound. pfa_gap_bezout_backward_result_coefficient_productcoefficientscoefficientresiduebound + S (pfc_value_bezout_backward_result_coefficient_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bezout_backward_result_coefficient_productcoefficientscoefficientresiduecongruence pfa_offset_right_bezout_backward_result_coefficient_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bezout_backward_result_coefficient_productcoefficientscoefficient) + (p) * pfa_offset_left_bezout_backward_result_coefficient_productcoefficientscoefficientresiduecongruence = (pfc_value_bezout_backward_result_coefficient_productcoefficients) + (p) * pfa_offset_right_bezout_backward_result_coefficient_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_bezout_backward_result_coefficient_difference_left_bounded. (exists fom_gap_pfp_bezout_backward_result_coefficient_difference_left_bounded_index_bound. fom_gap_pfp_bezout_backward_result_coefficient_difference_left_bounded_index_bound + S (fom_index_pfp_bezout_backward_result_coefficient_difference_left_bounded) = pfbz_update_W_bezout_backward_result) -> exists fom_value_pfp_bezout_backward_result_coefficient_difference_left_bounded. ((((exists fom_beta_height_pfp_bezout_backward_result_coefficient_difference_left_bounded_entry. fom_beta_height_pfp_bezout_backward_result_coefficient_difference_left_bounded_entry + S (fom_value_pfp_bezout_backward_result_coefficient_difference_left_bounded) = S ((S (fom_index_pfp_bezout_backward_result_coefficient_difference_left_bounded)) * pfbz_update_wc_bezout_backward_result)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_coefficient_difference_left_bounded_entry. pfbz_update_wb_bezout_backward_result = fom_beta_quotient_pfp_bezout_backward_result_coefficient_difference_left_bounded_entry * S ((S (fom_index_pfp_bezout_backward_result_coefficient_difference_left_bounded)) * pfbz_update_wc_bezout_backward_result) + (fom_value_pfp_bezout_backward_result_coefficient_difference_left_bounded))) /\ (exists fom_gap_pfp_bezout_backward_result_coefficient_difference_left_bounded_value_bound. fom_gap_pfp_bezout_backward_result_coefficient_difference_left_bounded_value_bound + S (fom_value_pfp_bezout_backward_result_coefficient_difference_left_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_result_coefficient_difference_right_bounded. (exists fom_gap_pfp_bezout_backward_result_coefficient_difference_right_bounded_index_bound. fom_gap_pfp_bezout_backward_result_coefficient_difference_right_bounded_index_bound + S (fom_index_pfp_bezout_backward_result_coefficient_difference_right_bounded) = pfbz_update_T_bezout_backward_result) -> exists fom_value_pfp_bezout_backward_result_coefficient_difference_right_bounded. ((((exists fom_beta_height_pfp_bezout_backward_result_coefficient_difference_right_bounded_entry. fom_beta_height_pfp_bezout_backward_result_coefficient_difference_right_bounded_entry + S (fom_value_pfp_bezout_backward_result_coefficient_difference_right_bounded) = S ((S (fom_index_pfp_bezout_backward_result_coefficient_difference_right_bounded)) * pfbz_update_tc_bezout_backward_result)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_coefficient_difference_right_bounded_entry. pfbz_update_tb_bezout_backward_result = fom_beta_quotient_pfp_bezout_backward_result_coefficient_difference_right_bounded_entry * S ((S (fom_index_pfp_bezout_backward_result_coefficient_difference_right_bounded)) * pfbz_update_tc_bezout_backward_result) + (fom_value_pfp_bezout_backward_result_coefficient_difference_right_bounded))) /\ (exists fom_gap_pfp_bezout_backward_result_coefficient_difference_right_bounded_value_bound. fom_gap_pfp_bezout_backward_result_coefficient_difference_right_bounded_value_bound + S (fom_value_pfp_bezout_backward_result_coefficient_difference_right_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_result_coefficient_difference_result_bounded. (exists fom_gap_pfp_bezout_backward_result_coefficient_difference_result_bounded_index_bound. fom_gap_pfp_bezout_backward_result_coefficient_difference_result_bounded_index_bound + S (fom_index_pfp_bezout_backward_result_coefficient_difference_result_bounded) = Lu) -> exists fom_value_pfp_bezout_backward_result_coefficient_difference_result_bounded. ((((exists fom_beta_height_pfp_bezout_backward_result_coefficient_difference_result_bounded_entry. fom_beta_height_pfp_bezout_backward_result_coefficient_difference_result_bounded_entry + S (fom_value_pfp_bezout_backward_result_coefficient_difference_result_bounded) = S ((S (fom_index_pfp_bezout_backward_result_coefficient_difference_result_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_coefficient_difference_result_bounded_entry. ub = fom_beta_quotient_pfp_bezout_backward_result_coefficient_difference_result_bounded_entry * S ((S (fom_index_pfp_bezout_backward_result_coefficient_difference_result_bounded)) * uc) + (fom_value_pfp_bezout_backward_result_coefficient_difference_result_bounded))) /\ (exists fom_gap_pfp_bezout_backward_result_coefficient_difference_result_bounded_value_bound. fom_gap_pfp_bezout_backward_result_coefficient_difference_result_bounded_value_bound + S (fom_value_pfp_bezout_backward_result_coefficient_difference_result_bounded) = p))) /\ ((exists pfaa_left_b_bezout_backward_result_coefficient_difference pfaa_left_c_bezout_backward_result_coefficient_difference pfaa_right_b_bezout_backward_result_coefficient_difference pfaa_right_c_bezout_backward_result_coefficient_difference pfaa_sum_b_bezout_backward_result_coefficient_difference pfaa_sum_c_bezout_backward_result_coefficient_difference pfaa_length_bezout_backward_result_coefficient_difference. ((((forall pfrep_power_bezout_backward_result_coefficient_difference_witness_common_left pfrep_left_bezout_backward_result_coefficient_difference_witness_common_left pfrep_right_bezout_backward_result_coefficient_difference_witness_common_left. ((exists pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftfirst. ((pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftfirst+S (pfrep_power_bezout_backward_result_coefficient_difference_witness_common_left)=(pfbz_update_W_bezout_backward_result)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_leftfirstentry. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_leftfirstentry + S (pfrep_left_bezout_backward_result_coefficient_difference_witness_common_left) = S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftfirst)) * pfbz_update_wc_bezout_backward_result)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_leftfirstentry. pfbz_update_wb_bezout_backward_result = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_leftfirstentry * S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftfirst)) * pfbz_update_wc_bezout_backward_result) + (pfrep_left_bezout_backward_result_coefficient_difference_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_leftfirstoutside. pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_leftfirstoutside+(pfbz_update_W_bezout_backward_result)=(pfrep_power_bezout_backward_result_coefficient_difference_witness_common_left)) /\ (((pfrep_left_bezout_backward_result_coefficient_difference_witness_common_left)=0))))) -> ((exists pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftsecond. ((pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftsecond+S (pfrep_power_bezout_backward_result_coefficient_difference_witness_common_left)=(pfaa_length_bezout_backward_result_coefficient_difference)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_leftsecondentry. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_leftsecondentry + S (pfrep_right_bezout_backward_result_coefficient_difference_witness_common_left) = S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_result_coefficient_difference)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_leftsecondentry. pfaa_left_b_bezout_backward_result_coefficient_difference = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_leftsecondentry * S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_result_coefficient_difference) + (pfrep_right_bezout_backward_result_coefficient_difference_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_leftsecondoutside. pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_leftsecondoutside+(pfaa_length_bezout_backward_result_coefficient_difference)=(pfrep_power_bezout_backward_result_coefficient_difference_witness_common_left)) /\ (((pfrep_right_bezout_backward_result_coefficient_difference_witness_common_left)=0))))) -> pfrep_left_bezout_backward_result_coefficient_difference_witness_common_left=pfrep_right_bezout_backward_result_coefficient_difference_witness_common_left) /\ ((forall pfrep_power_bezout_backward_result_coefficient_difference_witness_common_right pfrep_left_bezout_backward_result_coefficient_difference_witness_common_right pfrep_right_bezout_backward_result_coefficient_difference_witness_common_right. ((exists pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightfirst. ((pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightfirst+S (pfrep_power_bezout_backward_result_coefficient_difference_witness_common_right)=(pfbz_update_T_bezout_backward_result)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_rightfirstentry. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_rightfirstentry + S (pfrep_left_bezout_backward_result_coefficient_difference_witness_common_right) = S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightfirst)) * pfbz_update_tc_bezout_backward_result)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_rightfirstentry. pfbz_update_tb_bezout_backward_result = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_rightfirstentry * S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightfirst)) * pfbz_update_tc_bezout_backward_result) + (pfrep_left_bezout_backward_result_coefficient_difference_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_rightfirstoutside. pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_rightfirstoutside+(pfbz_update_T_bezout_backward_result)=(pfrep_power_bezout_backward_result_coefficient_difference_witness_common_right)) /\ (((pfrep_left_bezout_backward_result_coefficient_difference_witness_common_right)=0))))) -> ((exists pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightsecond. ((pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightsecond+S (pfrep_power_bezout_backward_result_coefficient_difference_witness_common_right)=(pfaa_length_bezout_backward_result_coefficient_difference)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_rightsecondentry. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_common_rightsecondentry + S (pfrep_right_bezout_backward_result_coefficient_difference_witness_common_right) = S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_result_coefficient_difference)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_rightsecondentry. pfaa_right_b_bezout_backward_result_coefficient_difference = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_common_rightsecondentry * S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_result_coefficient_difference) + (pfrep_right_bezout_backward_result_coefficient_difference_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_rightsecondoutside. pfrep_gap_bezout_backward_result_coefficient_difference_witness_common_rightsecondoutside+(pfaa_length_bezout_backward_result_coefficient_difference)=(pfrep_power_bezout_backward_result_coefficient_difference_witness_common_right)) /\ (((pfrep_right_bezout_backward_result_coefficient_difference_witness_common_right)=0))))) -> pfrep_left_bezout_backward_result_coefficient_difference_witness_common_right=pfrep_right_bezout_backward_result_coefficient_difference_witness_common_right)))) /\ (((forall pfp_index_bezout_backward_result_coefficient_difference_witness_operation. (exists pfa_gap_bezout_backward_result_coefficient_difference_witness_operationindex. pfa_gap_bezout_backward_result_coefficient_difference_witness_operationindex + S (pfp_index_bezout_backward_result_coefficient_difference_witness_operation) = (pfaa_length_bezout_backward_result_coefficient_difference)) -> exists pfp_left_bezout_backward_result_coefficient_difference_witness_operation pfp_right_bezout_backward_result_coefficient_difference_witness_operation pfp_value_bezout_backward_result_coefficient_difference_witness_operation. ((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_operationleft. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_operationleft + S (pfp_left_bezout_backward_result_coefficient_difference_witness_operation) = S ((S (pfp_index_bezout_backward_result_coefficient_difference_witness_operation)) * pfaa_left_c_bezout_backward_result_coefficient_difference)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_operationleft. pfaa_left_b_bezout_backward_result_coefficient_difference = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_operationleft * S ((S (pfp_index_bezout_backward_result_coefficient_difference_witness_operation)) * pfaa_left_c_bezout_backward_result_coefficient_difference) + (pfp_left_bezout_backward_result_coefficient_difference_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_operationright. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_operationright + S (pfp_right_bezout_backward_result_coefficient_difference_witness_operation) = S ((S (pfp_index_bezout_backward_result_coefficient_difference_witness_operation)) * pfaa_right_c_bezout_backward_result_coefficient_difference)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_operationright. pfaa_right_b_bezout_backward_result_coefficient_difference = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_operationright * S ((S (pfp_index_bezout_backward_result_coefficient_difference_witness_operation)) * pfaa_right_c_bezout_backward_result_coefficient_difference) + (pfp_right_bezout_backward_result_coefficient_difference_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_operationtarget. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_operationtarget + S (pfp_value_bezout_backward_result_coefficient_difference_witness_operation) = S ((S (pfp_index_bezout_backward_result_coefficient_difference_witness_operation)) * pfaa_sum_c_bezout_backward_result_coefficient_difference)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_operationtarget. pfaa_sum_b_bezout_backward_result_coefficient_difference = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_operationtarget * S ((S (pfp_index_bezout_backward_result_coefficient_difference_witness_operation)) * pfaa_sum_c_bezout_backward_result_coefficient_difference) + (pfp_value_bezout_backward_result_coefficient_difference_witness_operation))) /\ ((((exists pfa_gap_bezout_backward_result_coefficient_difference_witness_operationoperationleft. pfa_gap_bezout_backward_result_coefficient_difference_witness_operationoperationleft + S (pfp_left_bezout_backward_result_coefficient_difference_witness_operation) = (p)) /\ (((exists pfa_gap_bezout_backward_result_coefficient_difference_witness_operationoperationright. pfa_gap_bezout_backward_result_coefficient_difference_witness_operationoperationright + S (pfp_right_bezout_backward_result_coefficient_difference_witness_operation) = (p)) /\ ((((exists pfa_gap_bezout_backward_result_coefficient_difference_witness_operationoperationresultbound. pfa_gap_bezout_backward_result_coefficient_difference_witness_operationoperationresultbound + S (pfp_value_bezout_backward_result_coefficient_difference_witness_operation) = (p)) /\ ((exists pfa_offset_left_bezout_backward_result_coefficient_difference_witness_operationoperationresultcongruence pfa_offset_right_bezout_backward_result_coefficient_difference_witness_operationoperationresultcongruence. ((pfp_left_bezout_backward_result_coefficient_difference_witness_operation) + (pfp_right_bezout_backward_result_coefficient_difference_witness_operation)) + (p) * pfa_offset_left_bezout_backward_result_coefficient_difference_witness_operationoperationresultcongruence = (pfp_value_bezout_backward_result_coefficient_difference_witness_operation) + (p) * pfa_offset_right_bezout_backward_result_coefficient_difference_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_bezout_backward_result_coefficient_difference_witness_output pfrep_left_bezout_backward_result_coefficient_difference_witness_output pfrep_right_bezout_backward_result_coefficient_difference_witness_output. ((exists pfrep_position_bezout_backward_result_coefficient_difference_witness_outputfirst. ((pfrep_position_bezout_backward_result_coefficient_difference_witness_outputfirst+S (pfrep_power_bezout_backward_result_coefficient_difference_witness_output)=(pfaa_length_bezout_backward_result_coefficient_difference)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_outputfirstentry. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_outputfirstentry + S (pfrep_left_bezout_backward_result_coefficient_difference_witness_output) = S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_outputfirst)) * pfaa_sum_c_bezout_backward_result_coefficient_difference)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_outputfirstentry. pfaa_sum_b_bezout_backward_result_coefficient_difference = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_outputfirstentry * S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_outputfirst)) * pfaa_sum_c_bezout_backward_result_coefficient_difference) + (pfrep_left_bezout_backward_result_coefficient_difference_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_result_coefficient_difference_witness_outputfirstoutside. pfrep_gap_bezout_backward_result_coefficient_difference_witness_outputfirstoutside+(pfaa_length_bezout_backward_result_coefficient_difference)=(pfrep_power_bezout_backward_result_coefficient_difference_witness_output)) /\ (((pfrep_left_bezout_backward_result_coefficient_difference_witness_output)=0))))) -> ((exists pfrep_position_bezout_backward_result_coefficient_difference_witness_outputsecond. ((pfrep_position_bezout_backward_result_coefficient_difference_witness_outputsecond+S (pfrep_power_bezout_backward_result_coefficient_difference_witness_output)=(Lu)) /\ ((((exists ff_h_pfp_bezout_backward_result_coefficient_difference_witness_outputsecondentry. ff_h_pfp_bezout_backward_result_coefficient_difference_witness_outputsecondentry + S (pfrep_right_bezout_backward_result_coefficient_difference_witness_output) = S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_outputsecond)) * uc)) /\ exists ff_q_pfp_bezout_backward_result_coefficient_difference_witness_outputsecondentry. ub = ff_q_pfp_bezout_backward_result_coefficient_difference_witness_outputsecondentry * S ((S (pfrep_position_bezout_backward_result_coefficient_difference_witness_outputsecond)) * uc) + (pfrep_right_bezout_backward_result_coefficient_difference_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_result_coefficient_difference_witness_outputsecondoutside. pfrep_gap_bezout_backward_result_coefficient_difference_witness_outputsecondoutside+(Lu)=(pfrep_power_bezout_backward_result_coefficient_difference_witness_output)) /\ (((pfrep_right_bezout_backward_result_coefficient_difference_witness_output)=0))))) -> pfrep_left_bezout_backward_result_coefficient_difference_witness_output=pfrep_right_bezout_backward_result_coefficient_difference_witness_output))))))))))))) /\ ((exists pfbz_left_code_bezout_backward_result_bezout pfbz_left_scale_bezout_backward_result_bezout pfbz_left_length_bezout_backward_result_bezout pfbz_right_code_bezout_backward_result_bezout pfbz_right_scale_bezout_backward_result_bezout pfbz_right_length_bezout_backward_result_bezout. ((((forall fom_index_pfp_bezout_backward_result_bezout_left_productleft. (exists fom_gap_pfp_bezout_backward_result_bezout_left_productleft_index_bound. fom_gap_pfp_bezout_backward_result_bezout_left_productleft_index_bound + S (fom_index_pfp_bezout_backward_result_bezout_left_productleft) = Lv) -> exists fom_value_pfp_bezout_backward_result_bezout_left_productleft. ((((exists fom_beta_height_pfp_bezout_backward_result_bezout_left_productleft_entry. fom_beta_height_pfp_bezout_backward_result_bezout_left_productleft_entry + S (fom_value_pfp_bezout_backward_result_bezout_left_productleft) = S ((S (fom_index_pfp_bezout_backward_result_bezout_left_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_bezout_left_productleft_entry. vb = fom_beta_quotient_pfp_bezout_backward_result_bezout_left_productleft_entry * S ((S (fom_index_pfp_bezout_backward_result_bezout_left_productleft)) * vc) + (fom_value_pfp_bezout_backward_result_bezout_left_productleft))) /\ (exists fom_gap_pfp_bezout_backward_result_bezout_left_productleft_value_bound. fom_gap_pfp_bezout_backward_result_bezout_left_productleft_value_bound + S (fom_value_pfp_bezout_backward_result_bezout_left_productleft) = p))) /\ (((forall fom_index_pfp_bezout_backward_result_bezout_left_productright. (exists fom_gap_pfp_bezout_backward_result_bezout_left_productright_index_bound. fom_gap_pfp_bezout_backward_result_bezout_left_productright_index_bound + S (fom_index_pfp_bezout_backward_result_bezout_left_productright) = La) -> exists fom_value_pfp_bezout_backward_result_bezout_left_productright. ((((exists fom_beta_height_pfp_bezout_backward_result_bezout_left_productright_entry. fom_beta_height_pfp_bezout_backward_result_bezout_left_productright_entry + S (fom_value_pfp_bezout_backward_result_bezout_left_productright) = S ((S (fom_index_pfp_bezout_backward_result_bezout_left_productright)) * ac)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_bezout_left_productright_entry. ab = fom_beta_quotient_pfp_bezout_backward_result_bezout_left_productright_entry * S ((S (fom_index_pfp_bezout_backward_result_bezout_left_productright)) * ac) + (fom_value_pfp_bezout_backward_result_bezout_left_productright))) /\ (exists fom_gap_pfp_bezout_backward_result_bezout_left_productright_value_bound. fom_gap_pfp_bezout_backward_result_bezout_left_productright_value_bound + S (fom_value_pfp_bezout_backward_result_bezout_left_productright) = p))) /\ (((((((Lv)=0 \/ (La)=0) /\ (((pfbz_left_length_bezout_backward_result_bezout)=0)))) \/ (((~((Lv)=0)) /\ (((~((La)=0)) /\ (((Lv)+(La)=S (pfbz_left_length_bezout_backward_result_bezout)))))))) /\ ((forall pfc_index_bezout_backward_result_bezout_left_productcoefficients. (exists pfa_gap_bezout_backward_result_bezout_left_productcoefficientsbound. pfa_gap_bezout_backward_result_bezout_left_productcoefficientsbound + S (pfc_index_bezout_backward_result_bezout_left_productcoefficients) = (pfbz_left_length_bezout_backward_result_bezout)) -> exists pfc_value_bezout_backward_result_bezout_left_productcoefficients. ((((exists ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientsentry. ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientsentry + S (pfc_value_bezout_backward_result_bezout_left_productcoefficients) = S ((S (pfc_index_bezout_backward_result_bezout_left_productcoefficients)) * pfbz_left_scale_bezout_backward_result_bezout)) /\ exists ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientsentry. pfbz_left_code_bezout_backward_result_bezout = ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientsentry * S ((S (pfc_index_bezout_backward_result_bezout_left_productcoefficients)) * pfbz_left_scale_bezout_backward_result_bezout) + (pfc_value_bezout_backward_result_bezout_left_productcoefficients))) /\ ((exists pfc_terms_code_bezout_backward_result_bezout_left_productcoefficientscoefficient pfc_terms_scale_bezout_backward_result_bezout_left_productcoefficientscoefficient pfc_natural_sum_bezout_backward_result_bezout_left_productcoefficientscoefficient. ((forall pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalbound. pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_bezout_backward_result_bezout_left_productcoefficients))) -> exists pfc_value_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_result_bezout_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bezout_backward_result_bezout_left_productcoefficientscoefficient = ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_result_bezout_left_productcoefficientscoefficient) + (pfc_value_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm pfc_left_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm pfc_right_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal)+pfc_complement_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm=(pfc_index_bezout_backward_result_bezout_left_productcoefficients)) /\ ((((((exists pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal) = (Lv)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermleftoutside+(Lv)=(pfc_index_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm) = (La)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonaltermrightoutside+(La)=(pfc_complement_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonal)=pfc_left_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm*pfc_right_bezout_backward_result_bezout_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bezout_backward_result_bezout_left_productcoefficientscoefficient) = S ((S (S (pfc_index_bezout_backward_result_bezout_left_productcoefficients))) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bezout_backward_result_bezout_left_productcoefficients))) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum) + (pfc_natural_sum_bezout_backward_result_bezout_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_bezout_backward_result_bezout_left_productcoefficients)) -> exists fs_a_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_result_bezout_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bezout_backward_result_bezout_left_productcoefficientscoefficient = fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_result_bezout_left_productcoefficientscoefficient) + (fs_a_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum) + (fs_r_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum) + (fs_s_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bezout_backward_result_bezout_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientresiduebound. pfa_gap_bezout_backward_result_bezout_left_productcoefficientscoefficientresiduebound + S (pfc_value_bezout_backward_result_bezout_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bezout_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_bezout_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bezout_backward_result_bezout_left_productcoefficientscoefficient) + (p) * pfa_offset_left_bezout_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence = (pfc_value_bezout_backward_result_bezout_left_productcoefficients) + (p) * pfa_offset_right_bezout_backward_result_bezout_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_bezout_backward_result_bezout_right_productleft. (exists fom_gap_pfp_bezout_backward_result_bezout_right_productleft_index_bound. fom_gap_pfp_bezout_backward_result_bezout_right_productleft_index_bound + S (fom_index_pfp_bezout_backward_result_bezout_right_productleft) = pfbz_update_T_bezout_backward_result) -> exists fom_value_pfp_bezout_backward_result_bezout_right_productleft. ((((exists fom_beta_height_pfp_bezout_backward_result_bezout_right_productleft_entry. fom_beta_height_pfp_bezout_backward_result_bezout_right_productleft_entry + S (fom_value_pfp_bezout_backward_result_bezout_right_productleft) = S ((S (fom_index_pfp_bezout_backward_result_bezout_right_productleft)) * pfbz_update_tc_bezout_backward_result)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_bezout_right_productleft_entry. pfbz_update_tb_bezout_backward_result = fom_beta_quotient_pfp_bezout_backward_result_bezout_right_productleft_entry * S ((S (fom_index_pfp_bezout_backward_result_bezout_right_productleft)) * pfbz_update_tc_bezout_backward_result) + (fom_value_pfp_bezout_backward_result_bezout_right_productleft))) /\ (exists fom_gap_pfp_bezout_backward_result_bezout_right_productleft_value_bound. fom_gap_pfp_bezout_backward_result_bezout_right_productleft_value_bound + S (fom_value_pfp_bezout_backward_result_bezout_right_productleft) = p))) /\ (((forall fom_index_pfp_bezout_backward_result_bezout_right_productright. (exists fom_gap_pfp_bezout_backward_result_bezout_right_productright_index_bound. fom_gap_pfp_bezout_backward_result_bezout_right_productright_index_bound + S (fom_index_pfp_bezout_backward_result_bezout_right_productright) = Lb) -> exists fom_value_pfp_bezout_backward_result_bezout_right_productright. ((((exists fom_beta_height_pfp_bezout_backward_result_bezout_right_productright_entry. fom_beta_height_pfp_bezout_backward_result_bezout_right_productright_entry + S (fom_value_pfp_bezout_backward_result_bezout_right_productright) = S ((S (fom_index_pfp_bezout_backward_result_bezout_right_productright)) * bc)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_bezout_right_productright_entry. bb = fom_beta_quotient_pfp_bezout_backward_result_bezout_right_productright_entry * S ((S (fom_index_pfp_bezout_backward_result_bezout_right_productright)) * bc) + (fom_value_pfp_bezout_backward_result_bezout_right_productright))) /\ (exists fom_gap_pfp_bezout_backward_result_bezout_right_productright_value_bound. fom_gap_pfp_bezout_backward_result_bezout_right_productright_value_bound + S (fom_value_pfp_bezout_backward_result_bezout_right_productright) = p))) /\ (((((((pfbz_update_T_bezout_backward_result)=0 \/ (Lb)=0) /\ (((pfbz_right_length_bezout_backward_result_bezout)=0)))) \/ (((~((pfbz_update_T_bezout_backward_result)=0)) /\ (((~((Lb)=0)) /\ (((pfbz_update_T_bezout_backward_result)+(Lb)=S (pfbz_right_length_bezout_backward_result_bezout)))))))) /\ ((forall pfc_index_bezout_backward_result_bezout_right_productcoefficients. (exists pfa_gap_bezout_backward_result_bezout_right_productcoefficientsbound. pfa_gap_bezout_backward_result_bezout_right_productcoefficientsbound + S (pfc_index_bezout_backward_result_bezout_right_productcoefficients) = (pfbz_right_length_bezout_backward_result_bezout)) -> exists pfc_value_bezout_backward_result_bezout_right_productcoefficients. ((((exists ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientsentry. ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientsentry + S (pfc_value_bezout_backward_result_bezout_right_productcoefficients) = S ((S (pfc_index_bezout_backward_result_bezout_right_productcoefficients)) * pfbz_right_scale_bezout_backward_result_bezout)) /\ exists ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientsentry. pfbz_right_code_bezout_backward_result_bezout = ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientsentry * S ((S (pfc_index_bezout_backward_result_bezout_right_productcoefficients)) * pfbz_right_scale_bezout_backward_result_bezout) + (pfc_value_bezout_backward_result_bezout_right_productcoefficients))) /\ ((exists pfc_terms_code_bezout_backward_result_bezout_right_productcoefficientscoefficient pfc_terms_scale_bezout_backward_result_bezout_right_productcoefficientscoefficient pfc_natural_sum_bezout_backward_result_bezout_right_productcoefficientscoefficient. ((forall pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalbound. pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_bezout_backward_result_bezout_right_productcoefficients))) -> exists pfc_value_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_result_bezout_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bezout_backward_result_bezout_right_productcoefficientscoefficient = ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bezout_backward_result_bezout_right_productcoefficientscoefficient) + (pfc_value_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm pfc_left_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm pfc_right_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal)+pfc_complement_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm=(pfc_index_bezout_backward_result_bezout_right_productcoefficients)) /\ ((((((exists pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal) = (pfbz_update_T_bezout_backward_result)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfbz_update_tc_bezout_backward_result)) /\ exists ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry. pfbz_update_tb_bezout_backward_result = ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) * pfbz_update_tc_bezout_backward_result) + (pfc_left_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfbz_update_T_bezout_backward_result)=(pfc_index_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm) = (Lb)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonaltermrightoutside+(Lb)=(pfc_complement_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonal)=pfc_left_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm*pfc_right_bezout_backward_result_bezout_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bezout_backward_result_bezout_right_productcoefficientscoefficient) = S ((S (S (pfc_index_bezout_backward_result_bezout_right_productcoefficients))) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bezout_backward_result_bezout_right_productcoefficients))) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum) + (pfc_natural_sum_bezout_backward_result_bezout_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_bezout_backward_result_bezout_right_productcoefficients)) -> exists fs_a_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_result_bezout_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bezout_backward_result_bezout_right_productcoefficientscoefficient = fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bezout_backward_result_bezout_right_productcoefficientscoefficient) + (fs_a_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum) + (fs_r_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum = fs_q_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum) + (fs_s_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bezout_backward_result_bezout_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientresiduebound. pfa_gap_bezout_backward_result_bezout_right_productcoefficientscoefficientresiduebound + S (pfc_value_bezout_backward_result_bezout_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bezout_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_bezout_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bezout_backward_result_bezout_right_productcoefficientscoefficient) + (p) * pfa_offset_left_bezout_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence = (pfc_value_bezout_backward_result_bezout_right_productcoefficients) + (p) * pfa_offset_right_bezout_backward_result_bezout_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_bezout_backward_result_bezout_sum_left_bounded. (exists fom_gap_pfp_bezout_backward_result_bezout_sum_left_bounded_index_bound. fom_gap_pfp_bezout_backward_result_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_bezout_backward_result_bezout_sum_left_bounded) = pfbz_left_length_bezout_backward_result_bezout) -> exists fom_value_pfp_bezout_backward_result_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_bezout_backward_result_bezout_sum_left_bounded_entry. fom_beta_height_pfp_bezout_backward_result_bezout_sum_left_bounded_entry + S (fom_value_pfp_bezout_backward_result_bezout_sum_left_bounded) = S ((S (fom_index_pfp_bezout_backward_result_bezout_sum_left_bounded)) * pfbz_left_scale_bezout_backward_result_bezout)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_bezout_sum_left_bounded_entry. pfbz_left_code_bezout_backward_result_bezout = fom_beta_quotient_pfp_bezout_backward_result_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_bezout_backward_result_bezout_sum_left_bounded)) * pfbz_left_scale_bezout_backward_result_bezout) + (fom_value_pfp_bezout_backward_result_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_bezout_backward_result_bezout_sum_left_bounded_value_bound. fom_gap_pfp_bezout_backward_result_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_bezout_backward_result_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_result_bezout_sum_right_bounded. (exists fom_gap_pfp_bezout_backward_result_bezout_sum_right_bounded_index_bound. fom_gap_pfp_bezout_backward_result_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_bezout_backward_result_bezout_sum_right_bounded) = pfbz_right_length_bezout_backward_result_bezout) -> exists fom_value_pfp_bezout_backward_result_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_bezout_backward_result_bezout_sum_right_bounded_entry. fom_beta_height_pfp_bezout_backward_result_bezout_sum_right_bounded_entry + S (fom_value_pfp_bezout_backward_result_bezout_sum_right_bounded) = S ((S (fom_index_pfp_bezout_backward_result_bezout_sum_right_bounded)) * pfbz_right_scale_bezout_backward_result_bezout)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_bezout_sum_right_bounded_entry. pfbz_right_code_bezout_backward_result_bezout = fom_beta_quotient_pfp_bezout_backward_result_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_bezout_backward_result_bezout_sum_right_bounded)) * pfbz_right_scale_bezout_backward_result_bezout) + (fom_value_pfp_bezout_backward_result_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_bezout_backward_result_bezout_sum_right_bounded_value_bound. fom_gap_pfp_bezout_backward_result_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_bezout_backward_result_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_bezout_backward_result_bezout_sum_result_bounded. (exists fom_gap_pfp_bezout_backward_result_bezout_sum_result_bounded_index_bound. fom_gap_pfp_bezout_backward_result_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_bezout_backward_result_bezout_sum_result_bounded) = Lg) -> exists fom_value_pfp_bezout_backward_result_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_bezout_backward_result_bezout_sum_result_bounded_entry. fom_beta_height_pfp_bezout_backward_result_bezout_sum_result_bounded_entry + S (fom_value_pfp_bezout_backward_result_bezout_sum_result_bounded) = S ((S (fom_index_pfp_bezout_backward_result_bezout_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_bezout_backward_result_bezout_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_bezout_backward_result_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_bezout_backward_result_bezout_sum_result_bounded)) * gc) + (fom_value_pfp_bezout_backward_result_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_bezout_backward_result_bezout_sum_result_bounded_value_bound. fom_gap_pfp_bezout_backward_result_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_bezout_backward_result_bezout_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_bezout_backward_result_bezout_sum pfaa_left_c_bezout_backward_result_bezout_sum pfaa_right_b_bezout_backward_result_bezout_sum pfaa_right_c_bezout_backward_result_bezout_sum pfaa_sum_b_bezout_backward_result_bezout_sum pfaa_sum_c_bezout_backward_result_bezout_sum pfaa_length_bezout_backward_result_bezout_sum. ((((forall pfrep_power_bezout_backward_result_bezout_sum_witness_common_left pfrep_left_bezout_backward_result_bezout_sum_witness_common_left pfrep_right_bezout_backward_result_bezout_sum_witness_common_left. ((exists pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftfirst. ((pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftfirst+S (pfrep_power_bezout_backward_result_bezout_sum_witness_common_left)=(pfbz_left_length_bezout_backward_result_bezout)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_leftfirstentry. ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_leftfirstentry + S (pfrep_left_bezout_backward_result_bezout_sum_witness_common_left) = S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftfirst)) * pfbz_left_scale_bezout_backward_result_bezout)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_leftfirstentry. pfbz_left_code_bezout_backward_result_bezout = ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_leftfirstentry * S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftfirst)) * pfbz_left_scale_bezout_backward_result_bezout) + (pfrep_left_bezout_backward_result_bezout_sum_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_result_bezout_sum_witness_common_leftfirstoutside. pfrep_gap_bezout_backward_result_bezout_sum_witness_common_leftfirstoutside+(pfbz_left_length_bezout_backward_result_bezout)=(pfrep_power_bezout_backward_result_bezout_sum_witness_common_left)) /\ (((pfrep_left_bezout_backward_result_bezout_sum_witness_common_left)=0))))) -> ((exists pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftsecond. ((pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftsecond+S (pfrep_power_bezout_backward_result_bezout_sum_witness_common_left)=(pfaa_length_bezout_backward_result_bezout_sum)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_leftsecondentry. ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_leftsecondentry + S (pfrep_right_bezout_backward_result_bezout_sum_witness_common_left) = S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_result_bezout_sum)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_leftsecondentry. pfaa_left_b_bezout_backward_result_bezout_sum = ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_leftsecondentry * S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_leftsecond)) * pfaa_left_c_bezout_backward_result_bezout_sum) + (pfrep_right_bezout_backward_result_bezout_sum_witness_common_left)))))) \/ (((exists pfrep_gap_bezout_backward_result_bezout_sum_witness_common_leftsecondoutside. pfrep_gap_bezout_backward_result_bezout_sum_witness_common_leftsecondoutside+(pfaa_length_bezout_backward_result_bezout_sum)=(pfrep_power_bezout_backward_result_bezout_sum_witness_common_left)) /\ (((pfrep_right_bezout_backward_result_bezout_sum_witness_common_left)=0))))) -> pfrep_left_bezout_backward_result_bezout_sum_witness_common_left=pfrep_right_bezout_backward_result_bezout_sum_witness_common_left) /\ ((forall pfrep_power_bezout_backward_result_bezout_sum_witness_common_right pfrep_left_bezout_backward_result_bezout_sum_witness_common_right pfrep_right_bezout_backward_result_bezout_sum_witness_common_right. ((exists pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightfirst. ((pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightfirst+S (pfrep_power_bezout_backward_result_bezout_sum_witness_common_right)=(pfbz_right_length_bezout_backward_result_bezout)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_rightfirstentry. ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_rightfirstentry + S (pfrep_left_bezout_backward_result_bezout_sum_witness_common_right) = S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightfirst)) * pfbz_right_scale_bezout_backward_result_bezout)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_rightfirstentry. pfbz_right_code_bezout_backward_result_bezout = ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_rightfirstentry * S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightfirst)) * pfbz_right_scale_bezout_backward_result_bezout) + (pfrep_left_bezout_backward_result_bezout_sum_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_result_bezout_sum_witness_common_rightfirstoutside. pfrep_gap_bezout_backward_result_bezout_sum_witness_common_rightfirstoutside+(pfbz_right_length_bezout_backward_result_bezout)=(pfrep_power_bezout_backward_result_bezout_sum_witness_common_right)) /\ (((pfrep_left_bezout_backward_result_bezout_sum_witness_common_right)=0))))) -> ((exists pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightsecond. ((pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightsecond+S (pfrep_power_bezout_backward_result_bezout_sum_witness_common_right)=(pfaa_length_bezout_backward_result_bezout_sum)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_rightsecondentry. ff_h_pfp_bezout_backward_result_bezout_sum_witness_common_rightsecondentry + S (pfrep_right_bezout_backward_result_bezout_sum_witness_common_right) = S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_result_bezout_sum)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_rightsecondentry. pfaa_right_b_bezout_backward_result_bezout_sum = ff_q_pfp_bezout_backward_result_bezout_sum_witness_common_rightsecondentry * S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_common_rightsecond)) * pfaa_right_c_bezout_backward_result_bezout_sum) + (pfrep_right_bezout_backward_result_bezout_sum_witness_common_right)))))) \/ (((exists pfrep_gap_bezout_backward_result_bezout_sum_witness_common_rightsecondoutside. pfrep_gap_bezout_backward_result_bezout_sum_witness_common_rightsecondoutside+(pfaa_length_bezout_backward_result_bezout_sum)=(pfrep_power_bezout_backward_result_bezout_sum_witness_common_right)) /\ (((pfrep_right_bezout_backward_result_bezout_sum_witness_common_right)=0))))) -> pfrep_left_bezout_backward_result_bezout_sum_witness_common_right=pfrep_right_bezout_backward_result_bezout_sum_witness_common_right)))) /\ (((forall pfp_index_bezout_backward_result_bezout_sum_witness_operation. (exists pfa_gap_bezout_backward_result_bezout_sum_witness_operationindex. pfa_gap_bezout_backward_result_bezout_sum_witness_operationindex + S (pfp_index_bezout_backward_result_bezout_sum_witness_operation) = (pfaa_length_bezout_backward_result_bezout_sum)) -> exists pfp_left_bezout_backward_result_bezout_sum_witness_operation pfp_right_bezout_backward_result_bezout_sum_witness_operation pfp_value_bezout_backward_result_bezout_sum_witness_operation. ((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_operationleft. ff_h_pfp_bezout_backward_result_bezout_sum_witness_operationleft + S (pfp_left_bezout_backward_result_bezout_sum_witness_operation) = S ((S (pfp_index_bezout_backward_result_bezout_sum_witness_operation)) * pfaa_left_c_bezout_backward_result_bezout_sum)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_operationleft. pfaa_left_b_bezout_backward_result_bezout_sum = ff_q_pfp_bezout_backward_result_bezout_sum_witness_operationleft * S ((S (pfp_index_bezout_backward_result_bezout_sum_witness_operation)) * pfaa_left_c_bezout_backward_result_bezout_sum) + (pfp_left_bezout_backward_result_bezout_sum_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_operationright. ff_h_pfp_bezout_backward_result_bezout_sum_witness_operationright + S (pfp_right_bezout_backward_result_bezout_sum_witness_operation) = S ((S (pfp_index_bezout_backward_result_bezout_sum_witness_operation)) * pfaa_right_c_bezout_backward_result_bezout_sum)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_operationright. pfaa_right_b_bezout_backward_result_bezout_sum = ff_q_pfp_bezout_backward_result_bezout_sum_witness_operationright * S ((S (pfp_index_bezout_backward_result_bezout_sum_witness_operation)) * pfaa_right_c_bezout_backward_result_bezout_sum) + (pfp_right_bezout_backward_result_bezout_sum_witness_operation))) /\ (((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_operationtarget. ff_h_pfp_bezout_backward_result_bezout_sum_witness_operationtarget + S (pfp_value_bezout_backward_result_bezout_sum_witness_operation) = S ((S (pfp_index_bezout_backward_result_bezout_sum_witness_operation)) * pfaa_sum_c_bezout_backward_result_bezout_sum)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_operationtarget. pfaa_sum_b_bezout_backward_result_bezout_sum = ff_q_pfp_bezout_backward_result_bezout_sum_witness_operationtarget * S ((S (pfp_index_bezout_backward_result_bezout_sum_witness_operation)) * pfaa_sum_c_bezout_backward_result_bezout_sum) + (pfp_value_bezout_backward_result_bezout_sum_witness_operation))) /\ ((((exists pfa_gap_bezout_backward_result_bezout_sum_witness_operationoperationleft. pfa_gap_bezout_backward_result_bezout_sum_witness_operationoperationleft + S (pfp_left_bezout_backward_result_bezout_sum_witness_operation) = (p)) /\ (((exists pfa_gap_bezout_backward_result_bezout_sum_witness_operationoperationright. pfa_gap_bezout_backward_result_bezout_sum_witness_operationoperationright + S (pfp_right_bezout_backward_result_bezout_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_bezout_backward_result_bezout_sum_witness_operationoperationresultbound. pfa_gap_bezout_backward_result_bezout_sum_witness_operationoperationresultbound + S (pfp_value_bezout_backward_result_bezout_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_bezout_backward_result_bezout_sum_witness_operationoperationresultcongruence pfa_offset_right_bezout_backward_result_bezout_sum_witness_operationoperationresultcongruence. ((pfp_left_bezout_backward_result_bezout_sum_witness_operation) + (pfp_right_bezout_backward_result_bezout_sum_witness_operation)) + (p) * pfa_offset_left_bezout_backward_result_bezout_sum_witness_operationoperationresultcongruence = (pfp_value_bezout_backward_result_bezout_sum_witness_operation) + (p) * pfa_offset_right_bezout_backward_result_bezout_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_bezout_backward_result_bezout_sum_witness_output pfrep_left_bezout_backward_result_bezout_sum_witness_output pfrep_right_bezout_backward_result_bezout_sum_witness_output. ((exists pfrep_position_bezout_backward_result_bezout_sum_witness_outputfirst. ((pfrep_position_bezout_backward_result_bezout_sum_witness_outputfirst+S (pfrep_power_bezout_backward_result_bezout_sum_witness_output)=(pfaa_length_bezout_backward_result_bezout_sum)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_outputfirstentry. ff_h_pfp_bezout_backward_result_bezout_sum_witness_outputfirstentry + S (pfrep_left_bezout_backward_result_bezout_sum_witness_output) = S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_outputfirst)) * pfaa_sum_c_bezout_backward_result_bezout_sum)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_outputfirstentry. pfaa_sum_b_bezout_backward_result_bezout_sum = ff_q_pfp_bezout_backward_result_bezout_sum_witness_outputfirstentry * S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_outputfirst)) * pfaa_sum_c_bezout_backward_result_bezout_sum) + (pfrep_left_bezout_backward_result_bezout_sum_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_result_bezout_sum_witness_outputfirstoutside. pfrep_gap_bezout_backward_result_bezout_sum_witness_outputfirstoutside+(pfaa_length_bezout_backward_result_bezout_sum)=(pfrep_power_bezout_backward_result_bezout_sum_witness_output)) /\ (((pfrep_left_bezout_backward_result_bezout_sum_witness_output)=0))))) -> ((exists pfrep_position_bezout_backward_result_bezout_sum_witness_outputsecond. ((pfrep_position_bezout_backward_result_bezout_sum_witness_outputsecond+S (pfrep_power_bezout_backward_result_bezout_sum_witness_output)=(Lg)) /\ ((((exists ff_h_pfp_bezout_backward_result_bezout_sum_witness_outputsecondentry. ff_h_pfp_bezout_backward_result_bezout_sum_witness_outputsecondentry + S (pfrep_right_bezout_backward_result_bezout_sum_witness_output) = S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_bezout_backward_result_bezout_sum_witness_outputsecondentry. gb = ff_q_pfp_bezout_backward_result_bezout_sum_witness_outputsecondentry * S ((S (pfrep_position_bezout_backward_result_bezout_sum_witness_outputsecond)) * gc) + (pfrep_right_bezout_backward_result_bezout_sum_witness_output)))))) \/ (((exists pfrep_gap_bezout_backward_result_bezout_sum_witness_outputsecondoutside. pfrep_gap_bezout_backward_result_bezout_sum_witness_outputsecondoutside+(Lg)=(pfrep_power_bezout_backward_result_bezout_sum_witness_output)) /\ (((pfrep_right_bezout_backward_result_bezout_sum_witness_output)=0))))) -> pfrep_left_bezout_backward_result_bezout_sum_witness_output=pfrep_right_bezout_backward_result_bezout_sum_witness_output)))))))))))))))))))))))Complete tactic proof in conservative notation
All 299 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 299 script commands · 77 reading checkpoints · 23 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) Expand checkpoints Collapse checkpoints Show original steps Find a step
01 Fix variables and assumptions L1–10 Work with arbitrary variables or the premises of the current implication.
L1 intro p
L2 intro ab
L3 intro ac
L4 intro La
L5 intro bb
L6 intro bc
L7 intro Lb
L8 intro rb
L9 intro rc
L10 intro Lr
02 Fix variables and assumptions L11–20 Work with arbitrary variables or the premises of the current implication.
L11 intro qb
L12 intro qc
L13 intro Lq
L14 intro pb
L15 intro pc
L16 intro Lp
L17 intro gb
L18 intro gc
L19 intro Lg
L20 intro ub
03 Fix variables and assumptions L21–25 Work with arbitrary variables or the premises of the current implication.
L21 intro uc
L22 intro Lu
L23 intro vb
L24 intro vc
L25 intro Lv
04 Establish hstep L26–35 Establish this local claim before using it. It is not an additional assumption.
L26 have hstep · expand full local formula (753 characters) have hstep : ∀ cb. ∀ cc. ∀ Lc. ∀ db. ∀ dc. ∀ Ld. ∀ wb. ∀ wc. ∀ Lw. ∀ tb. ∀ tc. ∀ Lt. ∀ xb. ∀ xc. ∀ Lx. ∀ yb. ∀ yc. ∀ Ly. ∀ zb. ∀ zc. ∀ Lz. ∀ hb. ∀ hc. ∀ Lh. Prime(p) → FpPolyProduct(p,qb,qc,Lq,bb,bc,Lb,pb,pc,Lp) → FpPolynomialAlignedAdd(p,pb,pc,Lp,rb,rc,Lr,ab,ac,La) → FpPolyProduct(p,ub,uc,Lu,bb,bc,Lb,cb,cc,Lc) → FpPolyProduct(p,vb,vc,Lv,rb,rc,Lr,db,dc,Ld) → FpPolynomialAlignedAdd(p,cb,cc,Lc,db,dc,Ld,gb,gc,Lg) → FpPolyProduct(p,vb,vc,Lv,qb,qc,Lq,wb,wc,Lw) → FpPolynomialAlignedAdd(p,wb,wc,Lw,tb,tc,Lt,ub,uc,Lu) → FpPolyProduct(p,vb,vc,Lv,ab,ac,La,xb,xc,Lx) → FpPolyProduct(p,tb,tc,Lt,bb,bc,Lb,yb,yc,Ly) → FpPolyProduct(p,wb,wc,Lw,bb,bc,Lb,zb,zc,Lz) → FpPolyProduct(p,vb,vc,Lv,pb,pc,Lp,hb,hc,Lh) → FpPolynomialAlignedAdd(p,xb,xc,Lx,yb,yc,Ly,gb,gc,Lg)Definitions: Prime(p) FpPolyProduct(p,qb,qc,Lq,bb,bc,Lb,pb,pc,Lp) FpPolynomialAlignedAdd(p,pb,pc,Lp,rb,rc,Lr,ab,ac,La) FpPolyProduct(p,ub,uc,Lu,bb,bc,Lb,cb,cc,Lc) FpPolyProduct(p,vb,vc,Lv,rb,rc,Lr,db,dc,Ld) FpPolynomialAlignedAdd(p,cb,cc,Lc,db,dc,Ld,gb,gc,Lg) FpPolyProduct(p,vb,vc,Lv,qb,qc,Lq,wb,wc,Lw) FpPolynomialAlignedAdd(p,wb,wc,Lw,tb,tc,Lt,ub,uc,Lu) FpPolyProduct(p,vb,vc,Lv,ab,ac,La,xb,xc,Lx) FpPolyProduct(p,tb,tc,Lt,bb,bc,Lb,yb,yc,Ly) FpPolyProduct(p,wb,wc,Lw,bb,bc,Lb,zb,zc,Lz) FpPolyProduct(p,vb,vc,Lv,pb,pc,Lp,hb,hc,Lh) FpPolynomialAlignedAdd(p,xb,xc,Lx,yb,yc,Ly,gb,gc,Lg) Original native command in the exact edition L27 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (p)
L28 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (ab)
L29 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (ac)
L30 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (La)
L31 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (bb)
L32 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (bc)
L33 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lb)
L34 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (rb)
L35 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (rc)
05 Use earlier facts L36–45 Instantiate or apply named facts and discharge the corresponding proof obligations.
L36 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lr)
L37 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (qb)
L38 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (qc)
L39 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lq)
L40 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (pb)
L41 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (pc)
L42 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lp)
L43 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (ub)
L44 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (uc)
L45 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lu)
06 Use earlier facts L46–52 Instantiate or apply named facts and discharge the corresponding proof obligations.
L46 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (vb)
L47 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (vc)
L48 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lv)
L49 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (gb)
L50 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (gc)
L51 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lg)
L52 exact prime_field_polynomial_euclidean_backward_coefficient_identity
07 Fix variables and assumptions L53–56 Work with arbitrary variables or the premises of the current implication.
L53 intro hp
L54 intro hQB
L55 intro hdivision
L56 intro hbezout
08 Establish hp0 L57–62 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.
L57 have hp0 : ~(p=0)
L58 intro hz
L59 specialize prime_nonzero (p)
L60 apply prime_nonzero
L61 exact hp
L62 exact hz
09 Separate the logical cases L63–70 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L63 cases hbezout
L64 cases hbezout_witness
L65 cases hbezout_witness_witness
L66 cases hbezout_witness_witness_witness
L67 cases hbezout_witness_witness_witness_witness
L68 cases hbezout_witness_witness_witness_witness_witness
L69 cases hbezout_witness_witness_witness_witness_witness_witness
L70 cases hbezout_witness_witness_witness_witness_witness_witness_right
10 Establish hUbound L71–71 Establish this local claim before using it. It is not an additional assumption.
L71 11 Separate the logical cases L72–72 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L72 cases hbezout_witness_witness_witness_witness_witness_witness_left
12 Use earlier facts L73–73 Instantiate or apply named facts and discharge the corresponding proof obligations.
L73 exact hbezout_witness_witness_witness_witness_witness_witness_left_left
13 Establish hBbound L74–74 Establish this local claim before using it. It is not an additional assumption.
L74 14 Separate the logical cases L75–76 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L75 cases hbezout_witness_witness_witness_witness_witness_witness_left
L76 cases hbezout_witness_witness_witness_witness_witness_witness_left_right
15 Use earlier facts L77–77 Instantiate or apply named facts and discharge the corresponding proof obligations.
L77 exact hbezout_witness_witness_witness_witness_witness_witness_left_right_left
16 Establish hVbound L78–78 Establish this local claim before using it. It is not an additional assumption.
L78 17 Separate the logical cases L79–79 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L79 cases hbezout_witness_witness_witness_witness_witness_witness_right_left
18 Use earlier facts L80–80 Instantiate or apply named facts and discharge the corresponding proof obligations.
L80 exact hbezout_witness_witness_witness_witness_witness_witness_right_left_left
19 Establish hQbound L81–81 Establish this local claim before using it. It is not an additional assumption.
L81 20 Separate the logical cases L82–82 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L82 cases hQB
21 Use earlier facts L83–83 Instantiate or apply named facts and discharge the corresponding proof obligations.
L83 exact hQB_left
22 Establish hPbound L84–84 Establish this local claim before using it. It is not an additional assumption.
L84 23 Separate the logical cases L85–85 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L85 cases hdivision
24 Use earlier facts L86–86 Instantiate or apply named facts and discharge the corresponding proof obligations.
L86 exact hdivision_left
25 Establish hAbound L87–87 Establish this local claim before using it. It is not an additional assumption.
L87 26 Separate the logical cases L88–90 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L88 cases hdivision
L89 cases hdivision_right
L90 cases hdivision_right_right
27 Use earlier facts L91–91 Instantiate or apply named facts and discharge the corresponding proof obligations.
L91 exact hdivision_right_right_left
28 Establish hcoefficient_length L92–95 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
L92 L93 specialize polynomial_product_length_exists (Lv)
L94 specialize polynomial_product_length_exists (Lq)
L95 apply polynomial_product_length_exists
29 Separate the logical cases L96–96 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L96 cases hcoefficient_length
30 Establish hcoefficient_product L97–106 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
L97 have hcoefficient_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,Lv,qb,qc,Lq,b,c,x6)Definitions: FpPolyProduct(p,vb,vc,Lv,qb,qc,Lq,b,c,x6) Original native command in the exact edition L98 specialize prime_field_polynomial_convolution_at_length_exists (p)
L99 specialize prime_field_polynomial_convolution_at_length_exists (vb)
L100 specialize prime_field_polynomial_convolution_at_length_exists (vc)
L101 specialize prime_field_polynomial_convolution_at_length_exists (Lv)
L102 specialize prime_field_polynomial_convolution_at_length_exists (qb)
L103 specialize prime_field_polynomial_convolution_at_length_exists (qc)
L104 specialize prime_field_polynomial_convolution_at_length_exists (Lq)
L105 specialize prime_field_polynomial_convolution_at_length_exists (x6)
L106 apply prime_field_polynomial_convolution_at_length_exists
31 Use earlier facts L107–110 Instantiate or apply named facts and discharge the corresponding proof obligations.
L107 exact hp0
L108 exact hVbound
L109 exact hQbound
L110 exact hcoefficient_length_witness
32 Separate the logical cases L111–112 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L111 cases hcoefficient_product
L112 cases hcoefficient_product_witness
33 Establish hWbound L113–122 Establish this local claim before using it. It is not an additional assumption.
L113 L114 specialize prime_field_polynomial_convolution_bounded (p)
L115 specialize prime_field_polynomial_convolution_bounded (vb)
L116 specialize prime_field_polynomial_convolution_bounded (vc)
L117 specialize prime_field_polynomial_convolution_bounded (Lv)
L118 specialize prime_field_polynomial_convolution_bounded (qb)
L119 specialize prime_field_polynomial_convolution_bounded (qc)
L120 specialize prime_field_polynomial_convolution_bounded (Lq)
L121 specialize prime_field_polynomial_convolution_bounded (x7)
L122 specialize prime_field_polynomial_convolution_bounded (x8)
34 Use earlier facts L123–125 Instantiate or apply named facts and discharge the corresponding proof obligations.
L123 specialize prime_field_polynomial_convolution_bounded (x6)
L124 apply prime_field_polynomial_convolution_bounded
L125 exact hcoefficient_product_witness_witness
35 Establish hdifference L126–135 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial aligned subtract exists.
L126 have hdifference : ∃ tb. ∃ tc. FpPolynomialAlignedAdd(p,x7,x8,x6,tb,tc,Lu + x6,ub,uc,Lu)Definitions: FpPolynomialAlignedAdd(p,x7,x8,x6,tb,tc,Lu + x6,ub,uc,Lu) Original native command in the exact edition L127 specialize prime_field_polynomial_aligned_subtract_exists (p)
L128 specialize prime_field_polynomial_aligned_subtract_exists (ub)
L129 specialize prime_field_polynomial_aligned_subtract_exists (uc)
L130 specialize prime_field_polynomial_aligned_subtract_exists (Lu)
L131 specialize prime_field_polynomial_aligned_subtract_exists (x7)
L132 specialize prime_field_polynomial_aligned_subtract_exists (x8)
L133 specialize prime_field_polynomial_aligned_subtract_exists (x6)
L134 apply prime_field_polynomial_aligned_subtract_exists
L135 exact hp
36 Use earlier facts L136–137 Instantiate or apply named facts and discharge the corresponding proof obligations.
L136 exact hUbound
L137 exact hWbound
37 Separate the logical cases L138–139 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L138 cases hdifference
L139 cases hdifference_witness
38 Establish htbound L140–140 Establish this local claim before using it. It is not an additional assumption.
L140 39 Establish hsmall L141–150 Establish this local claim before using it. It is not an additional assumption.
L141 have hsmall : BetaPrefixInto(x7,x8,x6,p) ∧ (BetaPrefixInto(x9,x10,Lu + x6,p) ∧ BetaPrefixInto(ub,uc,Lu,p))Definitions: BetaPrefixInto(x7,x8,x6,p) BetaPrefixInto(x9,x10,Lu + x6,p) BetaPrefixInto(ub,uc,Lu,p) Original native command in the exact edition L142 specialize prime_field_polynomial_aligned_add_bounded (p)
L143 specialize prime_field_polynomial_aligned_add_bounded (x7)
L144 specialize prime_field_polynomial_aligned_add_bounded (x8)
L145 specialize prime_field_polynomial_aligned_add_bounded (x6)
L146 specialize prime_field_polynomial_aligned_add_bounded (x9)
L147 specialize prime_field_polynomial_aligned_add_bounded (x10)
L148 specialize prime_field_polynomial_aligned_add_bounded ((Lu)+(x6))
L149 specialize prime_field_polynomial_aligned_add_bounded (ub)
L150 specialize prime_field_polynomial_aligned_add_bounded (uc)
40 Use earlier facts L151–153 Instantiate or apply named facts and discharge the corresponding proof obligations.
L151 specialize prime_field_polynomial_aligned_add_bounded (Lu)
L152 apply prime_field_polynomial_aligned_add_bounded
L153 exact hdifference_witness_witness
41 Separate the logical cases L154–155 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L154 cases hsmall
L155 cases hsmall_right
42 Use earlier facts L156–156 Instantiate or apply named facts and discharge the corresponding proof obligations.
L156 exact hsmall_right_left
43 Establish hnewleft_length L157–160 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
L157 L158 specialize polynomial_product_length_exists (Lv)
L159 specialize polynomial_product_length_exists (La)
L160 apply polynomial_product_length_exists
44 Separate the logical cases L161–161 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L161 cases hnewleft_length
45 Establish hnewleft_product L162–171 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
L162 have hnewleft_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,Lv,ab,ac,La,b,c,x11)Definitions: FpPolyProduct(p,vb,vc,Lv,ab,ac,La,b,c,x11) Original native command in the exact edition L163 specialize prime_field_polynomial_convolution_at_length_exists (p)
L164 specialize prime_field_polynomial_convolution_at_length_exists (vb)
L165 specialize prime_field_polynomial_convolution_at_length_exists (vc)
L166 specialize prime_field_polynomial_convolution_at_length_exists (Lv)
L167 specialize prime_field_polynomial_convolution_at_length_exists (ab)
L168 specialize prime_field_polynomial_convolution_at_length_exists (ac)
L169 specialize prime_field_polynomial_convolution_at_length_exists (La)
L170 specialize prime_field_polynomial_convolution_at_length_exists (x11)
L171 apply prime_field_polynomial_convolution_at_length_exists
46 Use earlier facts L172–175 Instantiate or apply named facts and discharge the corresponding proof obligations.
L172 exact hp0
L173 exact hVbound
L174 exact hAbound
L175 exact hnewleft_length_witness
47 Separate the logical cases L176–177 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L176 cases hnewleft_product
L177 cases hnewleft_product_witness
48 Establish hnewright_length L178–181 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
L178 L179 specialize polynomial_product_length_exists ((Lu)+(x6))
L180 specialize polynomial_product_length_exists (Lb)
L181 apply polynomial_product_length_exists
49 Separate the logical cases L182–182 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L182 cases hnewright_length
50 Establish hnewright_product L183–192 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
L183 have hnewright_product : ∃ b. ∃ c. FpPolyProduct(p,x9,x10,Lu + x6,bb,bc,Lb,b,c,x14)Definitions: FpPolyProduct(p,x9,x10,Lu + x6,bb,bc,Lb,b,c,x14) Original native command in the exact edition L184 specialize prime_field_polynomial_convolution_at_length_exists (p)
L185 specialize prime_field_polynomial_convolution_at_length_exists (x9)
L186 specialize prime_field_polynomial_convolution_at_length_exists (x10)
L187 specialize prime_field_polynomial_convolution_at_length_exists ((Lu)+(x6))
L188 specialize prime_field_polynomial_convolution_at_length_exists (bb)
L189 specialize prime_field_polynomial_convolution_at_length_exists (bc)
L190 specialize prime_field_polynomial_convolution_at_length_exists (Lb)
L191 specialize prime_field_polynomial_convolution_at_length_exists (x14)
L192 apply prime_field_polynomial_convolution_at_length_exists
51 Use earlier facts L193–196 Instantiate or apply named facts and discharge the corresponding proof obligations.
L193 exact hp0
L194 exact htbound
L195 exact hBbound
L196 exact hnewright_length_witness
52 Separate the logical cases L197–198 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L197 cases hnewright_product
L198 cases hnewright_product_witness
53 Establish hresult L199–199 Establish this local claim before using it. It is not an additional assumption.
L199 have hresult : FpPolynomialAlignedAdd(p,x12,x13,x11,x15,x16,x14,gb,gc,Lg)Definitions: FpPolynomialAlignedAdd(p,x12,x13,x11,x15,x16,x14,gb,gc,Lg) Original native command in the exact edition 54 Establish hassociate_length L200–203 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
L200 L201 specialize polynomial_product_length_exists (x6)
L202 specialize polynomial_product_length_exists (Lb)
L203 apply polynomial_product_length_exists
55 Separate the logical cases L204–204 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L204 cases hassociate_length
56 Establish hassociate_product L205–214 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
L205 have hassociate_product : ∃ b. ∃ c. FpPolyProduct(p,x7,x8,x6,bb,bc,Lb,b,c,x17)Definitions: FpPolyProduct(p,x7,x8,x6,bb,bc,Lb,b,c,x17) Original native command in the exact edition L206 specialize prime_field_polynomial_convolution_at_length_exists (p)
L207 specialize prime_field_polynomial_convolution_at_length_exists (x7)
L208 specialize prime_field_polynomial_convolution_at_length_exists (x8)
L209 specialize prime_field_polynomial_convolution_at_length_exists (x6)
L210 specialize prime_field_polynomial_convolution_at_length_exists (bb)
L211 specialize prime_field_polynomial_convolution_at_length_exists (bc)
L212 specialize prime_field_polynomial_convolution_at_length_exists (Lb)
L213 specialize prime_field_polynomial_convolution_at_length_exists (x17)
L214 apply prime_field_polynomial_convolution_at_length_exists
57 Use earlier facts L215–218 Instantiate or apply named facts and discharge the corresponding proof obligations.
L215 exact hp0
L216 exact hWbound
L217 exact hBbound
L218 exact hassociate_length_witness
58 Separate the logical cases L219–220 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L219 cases hassociate_product
L220 cases hassociate_product_witness
59 Establish hdistribute_length L221–224 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
L221 L222 specialize polynomial_product_length_exists (Lv)
L223 specialize polynomial_product_length_exists (Lp)
L224 apply polynomial_product_length_exists
60 Separate the logical cases L225–225 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L225 cases hdistribute_length
61 Establish hdistribute_product L226–235 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial convolution at length exists.
L226 have hdistribute_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,Lv,pb,pc,Lp,b,c,x20)Definitions: FpPolyProduct(p,vb,vc,Lv,pb,pc,Lp,b,c,x20) Original native command in the exact edition L227 specialize prime_field_polynomial_convolution_at_length_exists (p)
L228 specialize prime_field_polynomial_convolution_at_length_exists (vb)
L229 specialize prime_field_polynomial_convolution_at_length_exists (vc)
L230 specialize prime_field_polynomial_convolution_at_length_exists (Lv)
L231 specialize prime_field_polynomial_convolution_at_length_exists (pb)
L232 specialize prime_field_polynomial_convolution_at_length_exists (pc)
L233 specialize prime_field_polynomial_convolution_at_length_exists (Lp)
L234 specialize prime_field_polynomial_convolution_at_length_exists (x20)
L235 apply prime_field_polynomial_convolution_at_length_exists
62 Use earlier facts L236–239 Instantiate or apply named facts and discharge the corresponding proof obligations.
L236 exact hp0
L237 exact hVbound
L238 exact hPbound
L239 exact hdistribute_length_witness
63 Separate the logical cases L240–241 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L240 cases hdistribute_product
L241 cases hdistribute_product_witness
64 Use earlier facts L242–251 Instantiate or apply named facts and discharge the corresponding proof obligations.
L242 specialize hstep (x)
L243 specialize hstep (x1)
L244 specialize hstep (x2)
L245 specialize hstep (x3)
L246 specialize hstep (x4)
L247 specialize hstep (x5)
L248 specialize hstep (x7)
L249 specialize hstep (x8)
L250 specialize hstep (x6)
L251 specialize hstep (x9)
65 Use earlier facts L252–261 Instantiate or apply named facts and discharge the corresponding proof obligations.
L252 specialize hstep (x10)
L253 specialize hstep ((Lu)+(x6))
L254 specialize hstep (x12)
L255 specialize hstep (x13)
L256 specialize hstep (x11)
L257 specialize hstep (x15)
L258 specialize hstep (x16)
L259 specialize hstep (x14)
L260 specialize hstep (x18)
L261 specialize hstep (x19)
66 Use earlier facts L262–271 Instantiate or apply named facts and discharge the corresponding proof obligations.
L262 specialize hstep (x17)
L263 specialize hstep (x21)
L264 specialize hstep (x22)
L265 specialize hstep (x20)
L266 apply hstep
L267 exact hp
L268 exact hQB
L269 exact hdivision
L270 exact hbezout_witness_witness_witness_witness_witness_witness_left
L271 exact hbezout_witness_witness_witness_witness_witness_witness_right_left
67 Use earlier facts L272–278 Instantiate or apply named facts and discharge the corresponding proof obligations.
L272 exact hbezout_witness_witness_witness_witness_witness_witness_right_right
L273 exact hcoefficient_product_witness_witness
L274 exact hdifference_witness_witness
L275 exact hnewleft_product_witness_witness
L276 exact hnewright_product_witness_witness
L277 exact hassociate_product_witness_witness
L278 exact hdistribute_product_witness_witness
68 Construct an explicit witness L279–284 Supply the displayed value, then prove that it has the required property.
L279 exists x7
L280 exists x8
L281 exists x6
L282 exists x9
L283 exists x10
L284 exists (Lu)+(x6)
69 Separate the logical cases L285–285 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L285 split
70 Use earlier facts L286–286 Instantiate or apply named facts and discharge the corresponding proof obligations.
L286 exact hcoefficient_product_witness_witness
71 Separate the logical cases L287–287 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L287 split
72 Use earlier facts L288–288 Instantiate or apply named facts and discharge the corresponding proof obligations.
L288 exact hdifference_witness_witness
73 Construct an explicit witness L289–294 Supply the displayed value, then prove that it has the required property.
L289 exists x12
L290 exists x13
L291 exists x11
L292 exists x15
L293 exists x16
L294 exists x14
74 Separate the logical cases L295–295 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L295 split
75 Use earlier facts L296–296 Instantiate or apply named facts and discharge the corresponding proof obligations.
L296 exact hnewleft_product_witness_witness
76 Separate the logical cases L297–297 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L297 split
77 Use earlier facts L298–299 Instantiate or apply named facts and discharge the corresponding proof obligations.
L298 exact hnewright_product_witness_witness
L299 exact hresult
Library-wide reading audit
Original defined command ledger · 299 lines 0001 intro p0002 intro ab0003 intro ac0004 intro La0005 intro bb0006 intro bc0007 intro Lb0008 intro rb0009 intro rc0010 intro Lr0011 intro qb0012 intro qc0013 intro Lq0014 intro pb0015 intro pc0016 intro Lp0017 intro gb0018 intro gc0019 intro Lg0020 intro ub0021 intro uc0022 intro Lu0023 intro vb0024 intro vc0025 intro Lv0026 have hstep : ∀ cb. ∀ cc. ∀ Lc. ∀ db. ∀ dc. ∀ Ld. ∀ wb. ∀ wc. ∀ Lw. ∀ tb. ∀ tc. ∀ Lt. ∀ xb. ∀ xc. ∀ Lx. ∀ yb. ∀ yc. ∀ Ly. ∀ zb. ∀ zc. ∀ Lz. ∀ hb. ∀ hc. ∀ Lh. Prime(p) → FpPolyProduct(p,qb,qc,Lq,bb,bc,Lb,pb,pc,Lp) → FpPolynomialAlignedAdd(p,pb,pc,Lp,rb,rc,Lr,ab,ac,La) → FpPolyProduct(p,ub,uc,Lu,bb,bc,Lb,cb,cc,Lc) → FpPolyProduct(p,vb,vc,Lv,rb,rc,Lr,db,dc,Ld) → FpPolynomialAlignedAdd(p,cb,cc,Lc,db,dc,Ld,gb,gc,Lg) → FpPolyProduct(p,vb,vc,Lv,qb,qc,Lq,wb,wc,Lw) → FpPolynomialAlignedAdd(p,wb,wc,Lw,tb,tc,Lt,ub,uc,Lu) → FpPolyProduct(p,vb,vc,Lv,ab,ac,La,xb,xc,Lx) → FpPolyProduct(p,tb,tc,Lt,bb,bc,Lb,yb,yc,Ly) → FpPolyProduct(p,wb,wc,Lw,bb,bc,Lb,zb,zc,Lz) → FpPolyProduct(p,vb,vc,Lv,pb,pc,Lp,hb,hc,Lh) → FpPolynomialAlignedAdd(p,xb,xc,Lx,yb,yc,Ly,gb,gc,Lg) 0027 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (p)0028 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (ab)0029 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (ac)0030 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (La)0031 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (bb)0032 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (bc)0033 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lb)0034 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (rb)0035 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (rc)0036 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lr)0037 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (qb)0038 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (qc)0039 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lq)0040 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (pb)0041 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (pc)0042 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lp)0043 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (ub)0044 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (uc)0045 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lu)0046 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (vb)0047 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (vc)0048 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lv)0049 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (gb)0050 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (gc)0051 specialize prime_field_polynomial_euclidean_backward_coefficient_identity (Lg)0052 exact prime_field_polynomial_euclidean_backward_coefficient_identity 0053 intro hp0054 intro hQB0055 intro hdivision0056 intro hbezout0057 have hp0 : ~(p=0)0058 intro hz0059 specialize prime_nonzero (p)0060 apply prime_nonzero0061 exact hp0062 exact hz0063 cases hbezout0064 cases hbezout_witness0065 cases hbezout_witness_witness0066 cases hbezout_witness_witness_witness0067 cases hbezout_witness_witness_witness_witness0068 cases hbezout_witness_witness_witness_witness_witness0069 cases hbezout_witness_witness_witness_witness_witness_witness0070 cases hbezout_witness_witness_witness_witness_witness_witness_right0071 have hUbound : BetaPrefixInto(ub,uc,Lu,p) 0072 cases hbezout_witness_witness_witness_witness_witness_witness_left0073 exact hbezout_witness_witness_witness_witness_witness_witness_left_left0074 have hBbound : BetaPrefixInto(bb,bc,Lb,p) 0075 cases hbezout_witness_witness_witness_witness_witness_witness_left0076 cases hbezout_witness_witness_witness_witness_witness_witness_left_right0077 exact hbezout_witness_witness_witness_witness_witness_witness_left_right_left0078 have hVbound : BetaPrefixInto(vb,vc,Lv,p) 0079 cases hbezout_witness_witness_witness_witness_witness_witness_right_left0080 exact hbezout_witness_witness_witness_witness_witness_witness_right_left_left0081 have hQbound : BetaPrefixInto(qb,qc,Lq,p) 0082 cases hQB0083 exact hQB_left0084 have hPbound : BetaPrefixInto(pb,pc,Lp,p) 0085 cases hdivision0086 exact hdivision_left0087 have hAbound : BetaPrefixInto(ab,ac,La,p) 0088 cases hdivision0089 cases hdivision_right0090 cases hdivision_right_right0091 exact hdivision_right_right_left0092 have hcoefficient_length : ∃ n. PolynomialProductLength(Lv,Lq,n) 0093 specialize polynomial_product_length_exists (Lv)0094 specialize polynomial_product_length_exists (Lq)0095 apply polynomial_product_length_exists0096 cases hcoefficient_length0097 have hcoefficient_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,Lv,qb,qc,Lq,b,c,x6) 0098 specialize prime_field_polynomial_convolution_at_length_exists (p)0099 specialize prime_field_polynomial_convolution_at_length_exists (vb)0100 specialize prime_field_polynomial_convolution_at_length_exists (vc)0101 specialize prime_field_polynomial_convolution_at_length_exists (Lv)0102 specialize prime_field_polynomial_convolution_at_length_exists (qb)0103 specialize prime_field_polynomial_convolution_at_length_exists (qc)0104 specialize prime_field_polynomial_convolution_at_length_exists (Lq)0105 specialize prime_field_polynomial_convolution_at_length_exists (x6)0106 apply prime_field_polynomial_convolution_at_length_exists0107 exact hp00108 exact hVbound0109 exact hQbound0110 exact hcoefficient_length_witness0111 cases hcoefficient_product0112 cases hcoefficient_product_witness0113 have hWbound : BetaPrefixInto(x7,x8,x6,p) 0114 specialize prime_field_polynomial_convolution_bounded (p)0115 specialize prime_field_polynomial_convolution_bounded (vb)0116 specialize prime_field_polynomial_convolution_bounded (vc)0117 specialize prime_field_polynomial_convolution_bounded (Lv)0118 specialize prime_field_polynomial_convolution_bounded (qb)0119 specialize prime_field_polynomial_convolution_bounded (qc)0120 specialize prime_field_polynomial_convolution_bounded (Lq)0121 specialize prime_field_polynomial_convolution_bounded (x7)0122 specialize prime_field_polynomial_convolution_bounded (x8)0123 specialize prime_field_polynomial_convolution_bounded (x6)0124 apply prime_field_polynomial_convolution_bounded0125 exact hcoefficient_product_witness_witness0126 have hdifference : ∃ tb. ∃ tc. FpPolynomialAlignedAdd(p,x7,x8,x6,tb,tc,Lu + x6,ub,uc,Lu) 0127 specialize prime_field_polynomial_aligned_subtract_exists (p)0128 specialize prime_field_polynomial_aligned_subtract_exists (ub)0129 specialize prime_field_polynomial_aligned_subtract_exists (uc)0130 specialize prime_field_polynomial_aligned_subtract_exists (Lu)0131 specialize prime_field_polynomial_aligned_subtract_exists (x7)0132 specialize prime_field_polynomial_aligned_subtract_exists (x8)0133 specialize prime_field_polynomial_aligned_subtract_exists (x6)0134 apply prime_field_polynomial_aligned_subtract_exists 0135 exact hp0136 exact hUbound0137 exact hWbound0138 cases hdifference0139 cases hdifference_witness0140 have htbound : BetaPrefixInto(x9,x10,Lu + x6,p) 0141 have hsmall : BetaPrefixInto(x7,x8,x6,p) ∧ (BetaPrefixInto(x9,x10,Lu + x6,p) ∧ BetaPrefixInto(ub,uc,Lu,p) )0142 specialize prime_field_polynomial_aligned_add_bounded (p)0143 specialize prime_field_polynomial_aligned_add_bounded (x7)0144 specialize prime_field_polynomial_aligned_add_bounded (x8)0145 specialize prime_field_polynomial_aligned_add_bounded (x6)0146 specialize prime_field_polynomial_aligned_add_bounded (x9)0147 specialize prime_field_polynomial_aligned_add_bounded (x10)0148 specialize prime_field_polynomial_aligned_add_bounded ((Lu)+(x6))0149 specialize prime_field_polynomial_aligned_add_bounded (ub)0150 specialize prime_field_polynomial_aligned_add_bounded (uc)0151 specialize prime_field_polynomial_aligned_add_bounded (Lu)0152 apply prime_field_polynomial_aligned_add_bounded 0153 exact hdifference_witness_witness0154 cases hsmall0155 cases hsmall_right0156 exact hsmall_right_left0157 have hnewleft_length : ∃ n. PolynomialProductLength(Lv,La,n) 0158 specialize polynomial_product_length_exists (Lv)0159 specialize polynomial_product_length_exists (La)0160 apply polynomial_product_length_exists0161 cases hnewleft_length0162 have hnewleft_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,Lv,ab,ac,La,b,c,x11) 0163 specialize prime_field_polynomial_convolution_at_length_exists (p)0164 specialize prime_field_polynomial_convolution_at_length_exists (vb)0165 specialize prime_field_polynomial_convolution_at_length_exists (vc)0166 specialize prime_field_polynomial_convolution_at_length_exists (Lv)0167 specialize prime_field_polynomial_convolution_at_length_exists (ab)0168 specialize prime_field_polynomial_convolution_at_length_exists (ac)0169 specialize prime_field_polynomial_convolution_at_length_exists (La)0170 specialize prime_field_polynomial_convolution_at_length_exists (x11)0171 apply prime_field_polynomial_convolution_at_length_exists0172 exact hp00173 exact hVbound0174 exact hAbound0175 exact hnewleft_length_witness0176 cases hnewleft_product0177 cases hnewleft_product_witness0178 have hnewright_length : ∃ n. PolynomialProductLength(Lu + x6,Lb,n) 0179 specialize polynomial_product_length_exists ((Lu)+(x6))0180 specialize polynomial_product_length_exists (Lb)0181 apply polynomial_product_length_exists0182 cases hnewright_length0183 have hnewright_product : ∃ b. ∃ c. FpPolyProduct(p,x9,x10,Lu + x6,bb,bc,Lb,b,c,x14) 0184 specialize prime_field_polynomial_convolution_at_length_exists (p)0185 specialize prime_field_polynomial_convolution_at_length_exists (x9)0186 specialize prime_field_polynomial_convolution_at_length_exists (x10)0187 specialize prime_field_polynomial_convolution_at_length_exists ((Lu)+(x6))0188 specialize prime_field_polynomial_convolution_at_length_exists (bb)0189 specialize prime_field_polynomial_convolution_at_length_exists (bc)0190 specialize prime_field_polynomial_convolution_at_length_exists (Lb)0191 specialize prime_field_polynomial_convolution_at_length_exists (x14)0192 apply prime_field_polynomial_convolution_at_length_exists0193 exact hp00194 exact htbound0195 exact hBbound0196 exact hnewright_length_witness0197 cases hnewright_product0198 cases hnewright_product_witness0199 have hresult : FpPolynomialAlignedAdd(p,x12,x13,x11,x15,x16,x14,gb,gc,Lg) 0200 have hassociate_length : ∃ n. PolynomialProductLength(x6,Lb,n) 0201 specialize polynomial_product_length_exists (x6)0202 specialize polynomial_product_length_exists (Lb)0203 apply polynomial_product_length_exists0204 cases hassociate_length0205 have hassociate_product : ∃ b. ∃ c. FpPolyProduct(p,x7,x8,x6,bb,bc,Lb,b,c,x17) 0206 specialize prime_field_polynomial_convolution_at_length_exists (p)0207 specialize prime_field_polynomial_convolution_at_length_exists (x7)0208 specialize prime_field_polynomial_convolution_at_length_exists (x8)0209 specialize prime_field_polynomial_convolution_at_length_exists (x6)0210 specialize prime_field_polynomial_convolution_at_length_exists (bb)0211 specialize prime_field_polynomial_convolution_at_length_exists (bc)0212 specialize prime_field_polynomial_convolution_at_length_exists (Lb)0213 specialize prime_field_polynomial_convolution_at_length_exists (x17)0214 apply prime_field_polynomial_convolution_at_length_exists0215 exact hp00216 exact hWbound0217 exact hBbound0218 exact hassociate_length_witness0219 cases hassociate_product0220 cases hassociate_product_witness0221 have hdistribute_length : ∃ n. PolynomialProductLength(Lv,Lp,n) 0222 specialize polynomial_product_length_exists (Lv)0223 specialize polynomial_product_length_exists (Lp)0224 apply polynomial_product_length_exists0225 cases hdistribute_length0226 have hdistribute_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,Lv,pb,pc,Lp,b,c,x20) 0227 specialize prime_field_polynomial_convolution_at_length_exists (p)0228 specialize prime_field_polynomial_convolution_at_length_exists (vb)0229 specialize prime_field_polynomial_convolution_at_length_exists (vc)0230 specialize prime_field_polynomial_convolution_at_length_exists (Lv)0231 specialize prime_field_polynomial_convolution_at_length_exists (pb)0232 specialize prime_field_polynomial_convolution_at_length_exists (pc)0233 specialize prime_field_polynomial_convolution_at_length_exists (Lp)0234 specialize prime_field_polynomial_convolution_at_length_exists (x20)0235 apply prime_field_polynomial_convolution_at_length_exists0236 exact hp00237 exact hVbound0238 exact hPbound0239 exact hdistribute_length_witness0240 cases hdistribute_product0241 cases hdistribute_product_witness0242 specialize hstep (x)0243 specialize hstep (x1)0244 specialize hstep (x2)0245 specialize hstep (x3)0246 specialize hstep (x4)0247 specialize hstep (x5)0248 specialize hstep (x7)0249 specialize hstep (x8)0250 specialize hstep (x6)0251 specialize hstep (x9)0252 specialize hstep (x10)0253 specialize hstep ((Lu)+(x6))0254 specialize hstep (x12)0255 specialize hstep (x13)0256 specialize hstep (x11)0257 specialize hstep (x15)0258 specialize hstep (x16)0259 specialize hstep (x14)0260 specialize hstep (x18)0261 specialize hstep (x19)0262 specialize hstep (x17)0263 specialize hstep (x21)0264 specialize hstep (x22)0265 specialize hstep (x20)0266 apply hstep0267 exact hp0268 exact hQB0269 exact hdivision0270 exact hbezout_witness_witness_witness_witness_witness_witness_left0271 exact hbezout_witness_witness_witness_witness_witness_witness_right_left0272 exact hbezout_witness_witness_witness_witness_witness_witness_right_right0273 exact hcoefficient_product_witness_witness0274 exact hdifference_witness_witness0275 exact hnewleft_product_witness_witness0276 exact hnewright_product_witness_witness0277 exact hassociate_product_witness_witness0278 exact hdistribute_product_witness_witness0279 exists x70280 exists x80281 exists x60282 exists x90283 exists x100284 exists (Lu)+(x6)0285 split0286 exact hcoefficient_product_witness_witness0287 split0288 exact hdifference_witness_witness0289 exists x120290 exists x130291 exists x110292 exists x150293 exists x160294 exists x140295 split0296 exact hnewleft_product_witness_witness0297 split0298 exact hnewright_product_witness_witness0299 exact hresult