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. ∀ A. ∀ bb. ∀ bc. ∀ B. ∀ gb. ∀ gc. ∀ G. ∀ ub. ∀ uc. ∀ U. ∀ vb. ∀ vc. ∀ V. ∀ ab2. ∀ ac2. ∀ A2. ∀ bb2. ∀ bc2. ∀ B2. ∀ gb2. ∀ gc2. ∀ G2. ¬p = 0 → BetaPrefixInto(ab2,ac2,A2,p) → BetaPrefixInto(bb2,bc2,B2,p) → BetaPrefixInto(gb2,gc2,G2,p) → PolynomialEquivalent(ab,ac,A,ab2,ac2,A2) → PolynomialEquivalent(bb,bc,B,bb2,bc2,B2) → PolynomialEquivalent(gb,gc,G,gb2,gc2,G2) → FpPolynomialBezoutRepresentation(p,ab,ac,A,bb,bc,B,gb,gc,G,ub,uc,U,vb,vc,V) → FpPolynomialBezoutRepresentation(p,ab2,ac2,A2,bb2,bc2,B2,gb2,gc2,G2,ub,uc,U,vb,vc,V) Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG BetaPrefixInto(b,c,l,B) · 7 PolynomialProductLength(L,M,N) · 2 FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2 PolynomialEquivalent(b,c,L,d,e,M) · 3 FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 1 FpPolynomialBezoutRepresentation(p,ab,ac,A,bb,bc,B,gb,gc,G,ub,uc,U,vb,vc,V) · 2 Actual proof prerequisites Original expanded first-order statement
forall p ab ac A bb bc B gb gc G ub uc U vb vc V ab2 ac2 A2 bb2 bc2 B2 gb2 gc2 G2. (~(p=0)) -> (forall fom_index_pfp_transport_a_bound. (exists fom_gap_pfp_transport_a_bound_index_bound. fom_gap_pfp_transport_a_bound_index_bound + S (fom_index_pfp_transport_a_bound) = A2) -> exists fom_value_pfp_transport_a_bound. ((((exists fom_beta_height_pfp_transport_a_bound_entry. fom_beta_height_pfp_transport_a_bound_entry + S (fom_value_pfp_transport_a_bound) = S ((S (fom_index_pfp_transport_a_bound)) * ac2)) /\ exists fom_beta_quotient_pfp_transport_a_bound_entry. ab2 = fom_beta_quotient_pfp_transport_a_bound_entry * S ((S (fom_index_pfp_transport_a_bound)) * ac2) + (fom_value_pfp_transport_a_bound))) /\ (exists fom_gap_pfp_transport_a_bound_value_bound. fom_gap_pfp_transport_a_bound_value_bound + S (fom_value_pfp_transport_a_bound) = p))) -> (forall fom_index_pfp_transport_b_bound. (exists fom_gap_pfp_transport_b_bound_index_bound. fom_gap_pfp_transport_b_bound_index_bound + S (fom_index_pfp_transport_b_bound) = B2) -> exists fom_value_pfp_transport_b_bound. ((((exists fom_beta_height_pfp_transport_b_bound_entry. fom_beta_height_pfp_transport_b_bound_entry + S (fom_value_pfp_transport_b_bound) = S ((S (fom_index_pfp_transport_b_bound)) * bc2)) /\ exists fom_beta_quotient_pfp_transport_b_bound_entry. bb2 = fom_beta_quotient_pfp_transport_b_bound_entry * S ((S (fom_index_pfp_transport_b_bound)) * bc2) + (fom_value_pfp_transport_b_bound))) /\ (exists fom_gap_pfp_transport_b_bound_value_bound. fom_gap_pfp_transport_b_bound_value_bound + S (fom_value_pfp_transport_b_bound) = p))) -> (forall fom_index_pfp_transport_g_bound. (exists fom_gap_pfp_transport_g_bound_index_bound. fom_gap_pfp_transport_g_bound_index_bound + S (fom_index_pfp_transport_g_bound) = G2) -> exists fom_value_pfp_transport_g_bound. ((((exists fom_beta_height_pfp_transport_g_bound_entry. fom_beta_height_pfp_transport_g_bound_entry + S (fom_value_pfp_transport_g_bound) = S ((S (fom_index_pfp_transport_g_bound)) * gc2)) /\ exists fom_beta_quotient_pfp_transport_g_bound_entry. gb2 = fom_beta_quotient_pfp_transport_g_bound_entry * S ((S (fom_index_pfp_transport_g_bound)) * gc2) + (fom_value_pfp_transport_g_bound))) /\ (exists fom_gap_pfp_transport_g_bound_value_bound. fom_gap_pfp_transport_g_bound_value_bound + S (fom_value_pfp_transport_g_bound) = p))) -> (forall pfrep_power_transport_a_equivalent pfrep_left_transport_a_equivalent pfrep_right_transport_a_equivalent. ((exists pfrep_position_transport_a_equivalentfirst. ((pfrep_position_transport_a_equivalentfirst+S (pfrep_power_transport_a_equivalent)=(A)) /\ ((((exists ff_h_pfp_transport_a_equivalentfirstentry. ff_h_pfp_transport_a_equivalentfirstentry + S (pfrep_left_transport_a_equivalent) = S ((S (pfrep_position_transport_a_equivalentfirst)) * ac)) /\ exists ff_q_pfp_transport_a_equivalentfirstentry. ab = ff_q_pfp_transport_a_equivalentfirstentry * S ((S (pfrep_position_transport_a_equivalentfirst)) * ac) + (pfrep_left_transport_a_equivalent)))))) \/ (((exists pfrep_gap_transport_a_equivalentfirstoutside. pfrep_gap_transport_a_equivalentfirstoutside+(A)=(pfrep_power_transport_a_equivalent)) /\ (((pfrep_left_transport_a_equivalent)=0))))) -> ((exists pfrep_position_transport_a_equivalentsecond. ((pfrep_position_transport_a_equivalentsecond+S (pfrep_power_transport_a_equivalent)=(A2)) /\ ((((exists ff_h_pfp_transport_a_equivalentsecondentry. ff_h_pfp_transport_a_equivalentsecondentry + S (pfrep_right_transport_a_equivalent) = S ((S (pfrep_position_transport_a_equivalentsecond)) * ac2)) /\ exists ff_q_pfp_transport_a_equivalentsecondentry. ab2 = ff_q_pfp_transport_a_equivalentsecondentry * S ((S (pfrep_position_transport_a_equivalentsecond)) * ac2) + (pfrep_right_transport_a_equivalent)))))) \/ (((exists pfrep_gap_transport_a_equivalentsecondoutside. pfrep_gap_transport_a_equivalentsecondoutside+(A2)=(pfrep_power_transport_a_equivalent)) /\ (((pfrep_right_transport_a_equivalent)=0))))) -> pfrep_left_transport_a_equivalent=pfrep_right_transport_a_equivalent) -> (forall pfrep_power_transport_b_equivalent pfrep_left_transport_b_equivalent pfrep_right_transport_b_equivalent. ((exists pfrep_position_transport_b_equivalentfirst. ((pfrep_position_transport_b_equivalentfirst+S (pfrep_power_transport_b_equivalent)=(B)) /\ ((((exists ff_h_pfp_transport_b_equivalentfirstentry. ff_h_pfp_transport_b_equivalentfirstentry + S (pfrep_left_transport_b_equivalent) = S ((S (pfrep_position_transport_b_equivalentfirst)) * bc)) /\ exists ff_q_pfp_transport_b_equivalentfirstentry. bb = ff_q_pfp_transport_b_equivalentfirstentry * S ((S (pfrep_position_transport_b_equivalentfirst)) * bc) + (pfrep_left_transport_b_equivalent)))))) \/ (((exists pfrep_gap_transport_b_equivalentfirstoutside. pfrep_gap_transport_b_equivalentfirstoutside+(B)=(pfrep_power_transport_b_equivalent)) /\ (((pfrep_left_transport_b_equivalent)=0))))) -> ((exists pfrep_position_transport_b_equivalentsecond. ((pfrep_position_transport_b_equivalentsecond+S (pfrep_power_transport_b_equivalent)=(B2)) /\ ((((exists ff_h_pfp_transport_b_equivalentsecondentry. ff_h_pfp_transport_b_equivalentsecondentry + S (pfrep_right_transport_b_equivalent) = S ((S (pfrep_position_transport_b_equivalentsecond)) * bc2)) /\ exists ff_q_pfp_transport_b_equivalentsecondentry. bb2 = ff_q_pfp_transport_b_equivalentsecondentry * S ((S (pfrep_position_transport_b_equivalentsecond)) * bc2) + (pfrep_right_transport_b_equivalent)))))) \/ (((exists pfrep_gap_transport_b_equivalentsecondoutside. pfrep_gap_transport_b_equivalentsecondoutside+(B2)=(pfrep_power_transport_b_equivalent)) /\ (((pfrep_right_transport_b_equivalent)=0))))) -> pfrep_left_transport_b_equivalent=pfrep_right_transport_b_equivalent) -> (forall pfrep_power_transport_g_equivalent pfrep_left_transport_g_equivalent pfrep_right_transport_g_equivalent. ((exists pfrep_position_transport_g_equivalentfirst. ((pfrep_position_transport_g_equivalentfirst+S (pfrep_power_transport_g_equivalent)=(G)) /\ ((((exists ff_h_pfp_transport_g_equivalentfirstentry. ff_h_pfp_transport_g_equivalentfirstentry + S (pfrep_left_transport_g_equivalent) = S ((S (pfrep_position_transport_g_equivalentfirst)) * gc)) /\ exists ff_q_pfp_transport_g_equivalentfirstentry. gb = ff_q_pfp_transport_g_equivalentfirstentry * S ((S (pfrep_position_transport_g_equivalentfirst)) * gc) + (pfrep_left_transport_g_equivalent)))))) \/ (((exists pfrep_gap_transport_g_equivalentfirstoutside. pfrep_gap_transport_g_equivalentfirstoutside+(G)=(pfrep_power_transport_g_equivalent)) /\ (((pfrep_left_transport_g_equivalent)=0))))) -> ((exists pfrep_position_transport_g_equivalentsecond. ((pfrep_position_transport_g_equivalentsecond+S (pfrep_power_transport_g_equivalent)=(G2)) /\ ((((exists ff_h_pfp_transport_g_equivalentsecondentry. ff_h_pfp_transport_g_equivalentsecondentry + S (pfrep_right_transport_g_equivalent) = S ((S (pfrep_position_transport_g_equivalentsecond)) * gc2)) /\ exists ff_q_pfp_transport_g_equivalentsecondentry. gb2 = ff_q_pfp_transport_g_equivalentsecondentry * S ((S (pfrep_position_transport_g_equivalentsecond)) * gc2) + (pfrep_right_transport_g_equivalent)))))) \/ (((exists pfrep_gap_transport_g_equivalentsecondoutside. pfrep_gap_transport_g_equivalentsecondoutside+(G2)=(pfrep_power_transport_g_equivalent)) /\ (((pfrep_right_transport_g_equivalent)=0))))) -> pfrep_left_transport_g_equivalent=pfrep_right_transport_g_equivalent) -> (exists pfbz_left_code_transport_old pfbz_left_scale_transport_old pfbz_left_length_transport_old pfbz_right_code_transport_old pfbz_right_scale_transport_old pfbz_right_length_transport_old. ((((forall fom_index_pfp_transport_old_left_productleft. (exists fom_gap_pfp_transport_old_left_productleft_index_bound. fom_gap_pfp_transport_old_left_productleft_index_bound + S (fom_index_pfp_transport_old_left_productleft) = U) -> exists fom_value_pfp_transport_old_left_productleft. ((((exists fom_beta_height_pfp_transport_old_left_productleft_entry. fom_beta_height_pfp_transport_old_left_productleft_entry + S (fom_value_pfp_transport_old_left_productleft) = S ((S (fom_index_pfp_transport_old_left_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_transport_old_left_productleft_entry. ub = fom_beta_quotient_pfp_transport_old_left_productleft_entry * S ((S (fom_index_pfp_transport_old_left_productleft)) * uc) + (fom_value_pfp_transport_old_left_productleft))) /\ (exists fom_gap_pfp_transport_old_left_productleft_value_bound. fom_gap_pfp_transport_old_left_productleft_value_bound + S (fom_value_pfp_transport_old_left_productleft) = p))) /\ (((forall fom_index_pfp_transport_old_left_productright. (exists fom_gap_pfp_transport_old_left_productright_index_bound. fom_gap_pfp_transport_old_left_productright_index_bound + S (fom_index_pfp_transport_old_left_productright) = A) -> exists fom_value_pfp_transport_old_left_productright. ((((exists fom_beta_height_pfp_transport_old_left_productright_entry. fom_beta_height_pfp_transport_old_left_productright_entry + S (fom_value_pfp_transport_old_left_productright) = S ((S (fom_index_pfp_transport_old_left_productright)) * ac)) /\ exists fom_beta_quotient_pfp_transport_old_left_productright_entry. ab = fom_beta_quotient_pfp_transport_old_left_productright_entry * S ((S (fom_index_pfp_transport_old_left_productright)) * ac) + (fom_value_pfp_transport_old_left_productright))) /\ (exists fom_gap_pfp_transport_old_left_productright_value_bound. fom_gap_pfp_transport_old_left_productright_value_bound + S (fom_value_pfp_transport_old_left_productright) = p))) /\ (((((((U)=0 \/ (A)=0) /\ (((pfbz_left_length_transport_old)=0)))) \/ (((~((U)=0)) /\ (((~((A)=0)) /\ (((U)+(A)=S (pfbz_left_length_transport_old)))))))) /\ ((forall pfc_index_transport_old_left_productcoefficients. (exists pfa_gap_transport_old_left_productcoefficientsbound. pfa_gap_transport_old_left_productcoefficientsbound + S (pfc_index_transport_old_left_productcoefficients) = (pfbz_left_length_transport_old)) -> exists pfc_value_transport_old_left_productcoefficients. ((((exists ff_h_pfp_transport_old_left_productcoefficientsentry. ff_h_pfp_transport_old_left_productcoefficientsentry + S (pfc_value_transport_old_left_productcoefficients) = S ((S (pfc_index_transport_old_left_productcoefficients)) * pfbz_left_scale_transport_old)) /\ exists ff_q_pfp_transport_old_left_productcoefficientsentry. pfbz_left_code_transport_old = ff_q_pfp_transport_old_left_productcoefficientsentry * S ((S (pfc_index_transport_old_left_productcoefficients)) * pfbz_left_scale_transport_old) + (pfc_value_transport_old_left_productcoefficients))) /\ ((exists pfc_terms_code_transport_old_left_productcoefficientscoefficient pfc_terms_scale_transport_old_left_productcoefficientscoefficient pfc_natural_sum_transport_old_left_productcoefficientscoefficient. ((forall pfc_index_transport_old_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_old_left_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_old_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_old_left_productcoefficients))) -> exists pfc_value_transport_old_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_old_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_old_left_productcoefficientscoefficient = ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient) + (pfc_value_transport_old_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)+pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_old_left_productcoefficients)) /\ ((((((exists pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal) = (U)) /\ ((((exists ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermleftoutside+(U)=(pfc_index_transport_old_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm) = (A)) /\ ((((exists ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_transport_old_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_old_left_productcoefficientscoefficientdiagonaltermrightoutside+(A)=(pfc_complement_transport_old_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_old_left_productcoefficientscoefficientdiagonal)=pfc_left_transport_old_left_productcoefficientscoefficientdiagonalterm*pfc_right_transport_old_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_old_left_productcoefficientscoefficientsum fs_v_pfc_transport_old_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_old_left_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_old_left_productcoefficients))) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_old_left_productcoefficients))) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_old_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_old_left_productcoefficients)) -> exists fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_old_left_productcoefficientscoefficient = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_left_productcoefficientscoefficient) + (fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_old_left_productcoefficientscoefficientsum = fs_q_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_left_productcoefficientscoefficientsum) + (fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_old_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_old_left_productcoefficientscoefficientresiduebound. pfa_gap_transport_old_left_productcoefficientscoefficientresiduebound + S (pfc_value_transport_old_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_old_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_old_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_old_left_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_old_left_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_old_left_productcoefficients) + (p) * pfa_offset_right_transport_old_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_transport_old_right_productleft. (exists fom_gap_pfp_transport_old_right_productleft_index_bound. fom_gap_pfp_transport_old_right_productleft_index_bound + S (fom_index_pfp_transport_old_right_productleft) = V) -> exists fom_value_pfp_transport_old_right_productleft. ((((exists fom_beta_height_pfp_transport_old_right_productleft_entry. fom_beta_height_pfp_transport_old_right_productleft_entry + S (fom_value_pfp_transport_old_right_productleft) = S ((S (fom_index_pfp_transport_old_right_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_transport_old_right_productleft_entry. vb = fom_beta_quotient_pfp_transport_old_right_productleft_entry * S ((S (fom_index_pfp_transport_old_right_productleft)) * vc) + (fom_value_pfp_transport_old_right_productleft))) /\ (exists fom_gap_pfp_transport_old_right_productleft_value_bound. fom_gap_pfp_transport_old_right_productleft_value_bound + S (fom_value_pfp_transport_old_right_productleft) = p))) /\ (((forall fom_index_pfp_transport_old_right_productright. (exists fom_gap_pfp_transport_old_right_productright_index_bound. fom_gap_pfp_transport_old_right_productright_index_bound + S (fom_index_pfp_transport_old_right_productright) = B) -> exists fom_value_pfp_transport_old_right_productright. ((((exists fom_beta_height_pfp_transport_old_right_productright_entry. fom_beta_height_pfp_transport_old_right_productright_entry + S (fom_value_pfp_transport_old_right_productright) = S ((S (fom_index_pfp_transport_old_right_productright)) * bc)) /\ exists fom_beta_quotient_pfp_transport_old_right_productright_entry. bb = fom_beta_quotient_pfp_transport_old_right_productright_entry * S ((S (fom_index_pfp_transport_old_right_productright)) * bc) + (fom_value_pfp_transport_old_right_productright))) /\ (exists fom_gap_pfp_transport_old_right_productright_value_bound. fom_gap_pfp_transport_old_right_productright_value_bound + S (fom_value_pfp_transport_old_right_productright) = p))) /\ (((((((V)=0 \/ (B)=0) /\ (((pfbz_right_length_transport_old)=0)))) \/ (((~((V)=0)) /\ (((~((B)=0)) /\ (((V)+(B)=S (pfbz_right_length_transport_old)))))))) /\ ((forall pfc_index_transport_old_right_productcoefficients. (exists pfa_gap_transport_old_right_productcoefficientsbound. pfa_gap_transport_old_right_productcoefficientsbound + S (pfc_index_transport_old_right_productcoefficients) = (pfbz_right_length_transport_old)) -> exists pfc_value_transport_old_right_productcoefficients. ((((exists ff_h_pfp_transport_old_right_productcoefficientsentry. ff_h_pfp_transport_old_right_productcoefficientsentry + S (pfc_value_transport_old_right_productcoefficients) = S ((S (pfc_index_transport_old_right_productcoefficients)) * pfbz_right_scale_transport_old)) /\ exists ff_q_pfp_transport_old_right_productcoefficientsentry. pfbz_right_code_transport_old = ff_q_pfp_transport_old_right_productcoefficientsentry * S ((S (pfc_index_transport_old_right_productcoefficients)) * pfbz_right_scale_transport_old) + (pfc_value_transport_old_right_productcoefficients))) /\ ((exists pfc_terms_code_transport_old_right_productcoefficientscoefficient pfc_terms_scale_transport_old_right_productcoefficientscoefficient pfc_natural_sum_transport_old_right_productcoefficientscoefficient. ((forall pfc_index_transport_old_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_old_right_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_old_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_old_right_productcoefficients))) -> exists pfc_value_transport_old_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_old_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_old_right_productcoefficientscoefficient = ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient) + (pfc_value_transport_old_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)+pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_old_right_productcoefficients)) /\ ((((((exists pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal) = (V)) /\ ((((exists ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermleftoutside+(V)=(pfc_index_transport_old_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm) = (B)) /\ ((((exists ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_transport_old_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_old_right_productcoefficientscoefficientdiagonaltermrightoutside+(B)=(pfc_complement_transport_old_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_old_right_productcoefficientscoefficientdiagonal)=pfc_left_transport_old_right_productcoefficientscoefficientdiagonalterm*pfc_right_transport_old_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_old_right_productcoefficientscoefficientsum fs_v_pfc_transport_old_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_old_right_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_old_right_productcoefficients))) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_old_right_productcoefficients))) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_old_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_old_right_productcoefficients)) -> exists fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_old_right_productcoefficientscoefficient = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_old_right_productcoefficientscoefficient) + (fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_old_right_productcoefficientscoefficientsum = fs_q_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_old_right_productcoefficientscoefficientsum) + (fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_old_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_old_right_productcoefficientscoefficientresiduebound. pfa_gap_transport_old_right_productcoefficientscoefficientresiduebound + S (pfc_value_transport_old_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_old_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_old_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_old_right_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_old_right_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_old_right_productcoefficients) + (p) * pfa_offset_right_transport_old_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_transport_old_sum_left_bounded. (exists fom_gap_pfp_transport_old_sum_left_bounded_index_bound. fom_gap_pfp_transport_old_sum_left_bounded_index_bound + S (fom_index_pfp_transport_old_sum_left_bounded) = pfbz_left_length_transport_old) -> exists fom_value_pfp_transport_old_sum_left_bounded. ((((exists fom_beta_height_pfp_transport_old_sum_left_bounded_entry. fom_beta_height_pfp_transport_old_sum_left_bounded_entry + S (fom_value_pfp_transport_old_sum_left_bounded) = S ((S (fom_index_pfp_transport_old_sum_left_bounded)) * pfbz_left_scale_transport_old)) /\ exists fom_beta_quotient_pfp_transport_old_sum_left_bounded_entry. pfbz_left_code_transport_old = fom_beta_quotient_pfp_transport_old_sum_left_bounded_entry * S ((S (fom_index_pfp_transport_old_sum_left_bounded)) * pfbz_left_scale_transport_old) + (fom_value_pfp_transport_old_sum_left_bounded))) /\ (exists fom_gap_pfp_transport_old_sum_left_bounded_value_bound. fom_gap_pfp_transport_old_sum_left_bounded_value_bound + S (fom_value_pfp_transport_old_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_transport_old_sum_right_bounded. (exists fom_gap_pfp_transport_old_sum_right_bounded_index_bound. fom_gap_pfp_transport_old_sum_right_bounded_index_bound + S (fom_index_pfp_transport_old_sum_right_bounded) = pfbz_right_length_transport_old) -> exists fom_value_pfp_transport_old_sum_right_bounded. ((((exists fom_beta_height_pfp_transport_old_sum_right_bounded_entry. fom_beta_height_pfp_transport_old_sum_right_bounded_entry + S (fom_value_pfp_transport_old_sum_right_bounded) = S ((S (fom_index_pfp_transport_old_sum_right_bounded)) * pfbz_right_scale_transport_old)) /\ exists fom_beta_quotient_pfp_transport_old_sum_right_bounded_entry. pfbz_right_code_transport_old = fom_beta_quotient_pfp_transport_old_sum_right_bounded_entry * S ((S (fom_index_pfp_transport_old_sum_right_bounded)) * pfbz_right_scale_transport_old) + (fom_value_pfp_transport_old_sum_right_bounded))) /\ (exists fom_gap_pfp_transport_old_sum_right_bounded_value_bound. fom_gap_pfp_transport_old_sum_right_bounded_value_bound + S (fom_value_pfp_transport_old_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_transport_old_sum_result_bounded. (exists fom_gap_pfp_transport_old_sum_result_bounded_index_bound. fom_gap_pfp_transport_old_sum_result_bounded_index_bound + S (fom_index_pfp_transport_old_sum_result_bounded) = G) -> exists fom_value_pfp_transport_old_sum_result_bounded. ((((exists fom_beta_height_pfp_transport_old_sum_result_bounded_entry. fom_beta_height_pfp_transport_old_sum_result_bounded_entry + S (fom_value_pfp_transport_old_sum_result_bounded) = S ((S (fom_index_pfp_transport_old_sum_result_bounded)) * gc)) /\ exists fom_beta_quotient_pfp_transport_old_sum_result_bounded_entry. gb = fom_beta_quotient_pfp_transport_old_sum_result_bounded_entry * S ((S (fom_index_pfp_transport_old_sum_result_bounded)) * gc) + (fom_value_pfp_transport_old_sum_result_bounded))) /\ (exists fom_gap_pfp_transport_old_sum_result_bounded_value_bound. fom_gap_pfp_transport_old_sum_result_bounded_value_bound + S (fom_value_pfp_transport_old_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_transport_old_sum pfaa_left_c_transport_old_sum pfaa_right_b_transport_old_sum pfaa_right_c_transport_old_sum pfaa_sum_b_transport_old_sum pfaa_sum_c_transport_old_sum pfaa_length_transport_old_sum. ((((forall pfrep_power_transport_old_sum_witness_common_left pfrep_left_transport_old_sum_witness_common_left pfrep_right_transport_old_sum_witness_common_left. ((exists pfrep_position_transport_old_sum_witness_common_leftfirst. ((pfrep_position_transport_old_sum_witness_common_leftfirst+S (pfrep_power_transport_old_sum_witness_common_left)=(pfbz_left_length_transport_old)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_leftfirstentry. ff_h_pfp_transport_old_sum_witness_common_leftfirstentry + S (pfrep_left_transport_old_sum_witness_common_left) = S ((S (pfrep_position_transport_old_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_old)) /\ exists ff_q_pfp_transport_old_sum_witness_common_leftfirstentry. pfbz_left_code_transport_old = ff_q_pfp_transport_old_sum_witness_common_leftfirstentry * S ((S (pfrep_position_transport_old_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_old) + (pfrep_left_transport_old_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_leftfirstoutside. pfrep_gap_transport_old_sum_witness_common_leftfirstoutside+(pfbz_left_length_transport_old)=(pfrep_power_transport_old_sum_witness_common_left)) /\ (((pfrep_left_transport_old_sum_witness_common_left)=0))))) -> ((exists pfrep_position_transport_old_sum_witness_common_leftsecond. ((pfrep_position_transport_old_sum_witness_common_leftsecond+S (pfrep_power_transport_old_sum_witness_common_left)=(pfaa_length_transport_old_sum)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_leftsecondentry. ff_h_pfp_transport_old_sum_witness_common_leftsecondentry + S (pfrep_right_transport_old_sum_witness_common_left) = S ((S (pfrep_position_transport_old_sum_witness_common_leftsecond)) * pfaa_left_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_common_leftsecondentry. pfaa_left_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_common_leftsecondentry * S ((S (pfrep_position_transport_old_sum_witness_common_leftsecond)) * pfaa_left_c_transport_old_sum) + (pfrep_right_transport_old_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_leftsecondoutside. pfrep_gap_transport_old_sum_witness_common_leftsecondoutside+(pfaa_length_transport_old_sum)=(pfrep_power_transport_old_sum_witness_common_left)) /\ (((pfrep_right_transport_old_sum_witness_common_left)=0))))) -> pfrep_left_transport_old_sum_witness_common_left=pfrep_right_transport_old_sum_witness_common_left) /\ ((forall pfrep_power_transport_old_sum_witness_common_right pfrep_left_transport_old_sum_witness_common_right pfrep_right_transport_old_sum_witness_common_right. ((exists pfrep_position_transport_old_sum_witness_common_rightfirst. ((pfrep_position_transport_old_sum_witness_common_rightfirst+S (pfrep_power_transport_old_sum_witness_common_right)=(pfbz_right_length_transport_old)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_rightfirstentry. ff_h_pfp_transport_old_sum_witness_common_rightfirstentry + S (pfrep_left_transport_old_sum_witness_common_right) = S ((S (pfrep_position_transport_old_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_old)) /\ exists ff_q_pfp_transport_old_sum_witness_common_rightfirstentry. pfbz_right_code_transport_old = ff_q_pfp_transport_old_sum_witness_common_rightfirstentry * S ((S (pfrep_position_transport_old_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_old) + (pfrep_left_transport_old_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_rightfirstoutside. pfrep_gap_transport_old_sum_witness_common_rightfirstoutside+(pfbz_right_length_transport_old)=(pfrep_power_transport_old_sum_witness_common_right)) /\ (((pfrep_left_transport_old_sum_witness_common_right)=0))))) -> ((exists pfrep_position_transport_old_sum_witness_common_rightsecond. ((pfrep_position_transport_old_sum_witness_common_rightsecond+S (pfrep_power_transport_old_sum_witness_common_right)=(pfaa_length_transport_old_sum)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_common_rightsecondentry. ff_h_pfp_transport_old_sum_witness_common_rightsecondentry + S (pfrep_right_transport_old_sum_witness_common_right) = S ((S (pfrep_position_transport_old_sum_witness_common_rightsecond)) * pfaa_right_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_common_rightsecondentry. pfaa_right_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_common_rightsecondentry * S ((S (pfrep_position_transport_old_sum_witness_common_rightsecond)) * pfaa_right_c_transport_old_sum) + (pfrep_right_transport_old_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_common_rightsecondoutside. pfrep_gap_transport_old_sum_witness_common_rightsecondoutside+(pfaa_length_transport_old_sum)=(pfrep_power_transport_old_sum_witness_common_right)) /\ (((pfrep_right_transport_old_sum_witness_common_right)=0))))) -> pfrep_left_transport_old_sum_witness_common_right=pfrep_right_transport_old_sum_witness_common_right)))) /\ (((forall pfp_index_transport_old_sum_witness_operation. (exists pfa_gap_transport_old_sum_witness_operationindex. pfa_gap_transport_old_sum_witness_operationindex + S (pfp_index_transport_old_sum_witness_operation) = (pfaa_length_transport_old_sum)) -> exists pfp_left_transport_old_sum_witness_operation pfp_right_transport_old_sum_witness_operation pfp_value_transport_old_sum_witness_operation. ((((exists ff_h_pfp_transport_old_sum_witness_operationleft. ff_h_pfp_transport_old_sum_witness_operationleft + S (pfp_left_transport_old_sum_witness_operation) = S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_left_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_operationleft. pfaa_left_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_operationleft * S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_left_c_transport_old_sum) + (pfp_left_transport_old_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_old_sum_witness_operationright. ff_h_pfp_transport_old_sum_witness_operationright + S (pfp_right_transport_old_sum_witness_operation) = S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_right_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_operationright. pfaa_right_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_operationright * S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_right_c_transport_old_sum) + (pfp_right_transport_old_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_old_sum_witness_operationtarget. ff_h_pfp_transport_old_sum_witness_operationtarget + S (pfp_value_transport_old_sum_witness_operation) = S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_sum_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_operationtarget. pfaa_sum_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_operationtarget * S ((S (pfp_index_transport_old_sum_witness_operation)) * pfaa_sum_c_transport_old_sum) + (pfp_value_transport_old_sum_witness_operation))) /\ ((((exists pfa_gap_transport_old_sum_witness_operationoperationleft. pfa_gap_transport_old_sum_witness_operationoperationleft + S (pfp_left_transport_old_sum_witness_operation) = (p)) /\ (((exists pfa_gap_transport_old_sum_witness_operationoperationright. pfa_gap_transport_old_sum_witness_operationoperationright + S (pfp_right_transport_old_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_transport_old_sum_witness_operationoperationresultbound. pfa_gap_transport_old_sum_witness_operationoperationresultbound + S (pfp_value_transport_old_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_transport_old_sum_witness_operationoperationresultcongruence pfa_offset_right_transport_old_sum_witness_operationoperationresultcongruence. ((pfp_left_transport_old_sum_witness_operation) + (pfp_right_transport_old_sum_witness_operation)) + (p) * pfa_offset_left_transport_old_sum_witness_operationoperationresultcongruence = (pfp_value_transport_old_sum_witness_operation) + (p) * pfa_offset_right_transport_old_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_transport_old_sum_witness_output pfrep_left_transport_old_sum_witness_output pfrep_right_transport_old_sum_witness_output. ((exists pfrep_position_transport_old_sum_witness_outputfirst. ((pfrep_position_transport_old_sum_witness_outputfirst+S (pfrep_power_transport_old_sum_witness_output)=(pfaa_length_transport_old_sum)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_outputfirstentry. ff_h_pfp_transport_old_sum_witness_outputfirstentry + S (pfrep_left_transport_old_sum_witness_output) = S ((S (pfrep_position_transport_old_sum_witness_outputfirst)) * pfaa_sum_c_transport_old_sum)) /\ exists ff_q_pfp_transport_old_sum_witness_outputfirstentry. pfaa_sum_b_transport_old_sum = ff_q_pfp_transport_old_sum_witness_outputfirstentry * S ((S (pfrep_position_transport_old_sum_witness_outputfirst)) * pfaa_sum_c_transport_old_sum) + (pfrep_left_transport_old_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_outputfirstoutside. pfrep_gap_transport_old_sum_witness_outputfirstoutside+(pfaa_length_transport_old_sum)=(pfrep_power_transport_old_sum_witness_output)) /\ (((pfrep_left_transport_old_sum_witness_output)=0))))) -> ((exists pfrep_position_transport_old_sum_witness_outputsecond. ((pfrep_position_transport_old_sum_witness_outputsecond+S (pfrep_power_transport_old_sum_witness_output)=(G)) /\ ((((exists ff_h_pfp_transport_old_sum_witness_outputsecondentry. ff_h_pfp_transport_old_sum_witness_outputsecondentry + S (pfrep_right_transport_old_sum_witness_output) = S ((S (pfrep_position_transport_old_sum_witness_outputsecond)) * gc)) /\ exists ff_q_pfp_transport_old_sum_witness_outputsecondentry. gb = ff_q_pfp_transport_old_sum_witness_outputsecondentry * S ((S (pfrep_position_transport_old_sum_witness_outputsecond)) * gc) + (pfrep_right_transport_old_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_old_sum_witness_outputsecondoutside. pfrep_gap_transport_old_sum_witness_outputsecondoutside+(G)=(pfrep_power_transport_old_sum_witness_output)) /\ (((pfrep_right_transport_old_sum_witness_output)=0))))) -> pfrep_left_transport_old_sum_witness_output=pfrep_right_transport_old_sum_witness_output)))))))))))))))))) -> (exists pfbz_left_code_transport_result pfbz_left_scale_transport_result pfbz_left_length_transport_result pfbz_right_code_transport_result pfbz_right_scale_transport_result pfbz_right_length_transport_result. ((((forall fom_index_pfp_transport_result_left_productleft. (exists fom_gap_pfp_transport_result_left_productleft_index_bound. fom_gap_pfp_transport_result_left_productleft_index_bound + S (fom_index_pfp_transport_result_left_productleft) = U) -> exists fom_value_pfp_transport_result_left_productleft. ((((exists fom_beta_height_pfp_transport_result_left_productleft_entry. fom_beta_height_pfp_transport_result_left_productleft_entry + S (fom_value_pfp_transport_result_left_productleft) = S ((S (fom_index_pfp_transport_result_left_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_transport_result_left_productleft_entry. ub = fom_beta_quotient_pfp_transport_result_left_productleft_entry * S ((S (fom_index_pfp_transport_result_left_productleft)) * uc) + (fom_value_pfp_transport_result_left_productleft))) /\ (exists fom_gap_pfp_transport_result_left_productleft_value_bound. fom_gap_pfp_transport_result_left_productleft_value_bound + S (fom_value_pfp_transport_result_left_productleft) = p))) /\ (((forall fom_index_pfp_transport_result_left_productright. (exists fom_gap_pfp_transport_result_left_productright_index_bound. fom_gap_pfp_transport_result_left_productright_index_bound + S (fom_index_pfp_transport_result_left_productright) = A2) -> exists fom_value_pfp_transport_result_left_productright. ((((exists fom_beta_height_pfp_transport_result_left_productright_entry. fom_beta_height_pfp_transport_result_left_productright_entry + S (fom_value_pfp_transport_result_left_productright) = S ((S (fom_index_pfp_transport_result_left_productright)) * ac2)) /\ exists fom_beta_quotient_pfp_transport_result_left_productright_entry. ab2 = fom_beta_quotient_pfp_transport_result_left_productright_entry * S ((S (fom_index_pfp_transport_result_left_productright)) * ac2) + (fom_value_pfp_transport_result_left_productright))) /\ (exists fom_gap_pfp_transport_result_left_productright_value_bound. fom_gap_pfp_transport_result_left_productright_value_bound + S (fom_value_pfp_transport_result_left_productright) = p))) /\ (((((((U)=0 \/ (A2)=0) /\ (((pfbz_left_length_transport_result)=0)))) \/ (((~((U)=0)) /\ (((~((A2)=0)) /\ (((U)+(A2)=S (pfbz_left_length_transport_result)))))))) /\ ((forall pfc_index_transport_result_left_productcoefficients. (exists pfa_gap_transport_result_left_productcoefficientsbound. pfa_gap_transport_result_left_productcoefficientsbound + S (pfc_index_transport_result_left_productcoefficients) = (pfbz_left_length_transport_result)) -> exists pfc_value_transport_result_left_productcoefficients. ((((exists ff_h_pfp_transport_result_left_productcoefficientsentry. ff_h_pfp_transport_result_left_productcoefficientsentry + S (pfc_value_transport_result_left_productcoefficients) = S ((S (pfc_index_transport_result_left_productcoefficients)) * pfbz_left_scale_transport_result)) /\ exists ff_q_pfp_transport_result_left_productcoefficientsentry. pfbz_left_code_transport_result = ff_q_pfp_transport_result_left_productcoefficientsentry * S ((S (pfc_index_transport_result_left_productcoefficients)) * pfbz_left_scale_transport_result) + (pfc_value_transport_result_left_productcoefficients))) /\ ((exists pfc_terms_code_transport_result_left_productcoefficientscoefficient pfc_terms_scale_transport_result_left_productcoefficientscoefficient pfc_natural_sum_transport_result_left_productcoefficientscoefficient. ((forall pfc_index_transport_result_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_result_left_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_result_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_result_left_productcoefficients))) -> exists pfc_value_transport_result_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_result_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_result_left_productcoefficientscoefficient = ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient) + (pfc_value_transport_result_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)+pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_result_left_productcoefficients)) /\ ((((((exists pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal) = (U)) /\ ((((exists ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermleftoutside+(U)=(pfc_index_transport_result_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm) = (A2)) /\ ((((exists ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm)) * ac2)) /\ exists ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry. ab2 = ff_q_pfp_transport_result_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm)) * ac2) + (pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_result_left_productcoefficientscoefficientdiagonaltermrightoutside+(A2)=(pfc_complement_transport_result_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_result_left_productcoefficientscoefficientdiagonal)=pfc_left_transport_result_left_productcoefficientscoefficientdiagonalterm*pfc_right_transport_result_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_result_left_productcoefficientscoefficientsum fs_v_pfc_transport_result_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_result_left_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_result_left_productcoefficients))) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_result_left_productcoefficients))) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_result_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_result_left_productcoefficients)) -> exists fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_result_left_productcoefficientscoefficient = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_left_productcoefficientscoefficient) + (fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_result_left_productcoefficientscoefficientsum = fs_q_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_left_productcoefficientscoefficientsum) + (fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_result_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_result_left_productcoefficientscoefficientresiduebound. pfa_gap_transport_result_left_productcoefficientscoefficientresiduebound + S (pfc_value_transport_result_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_result_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_result_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_result_left_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_result_left_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_result_left_productcoefficients) + (p) * pfa_offset_right_transport_result_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_transport_result_right_productleft. (exists fom_gap_pfp_transport_result_right_productleft_index_bound. fom_gap_pfp_transport_result_right_productleft_index_bound + S (fom_index_pfp_transport_result_right_productleft) = V) -> exists fom_value_pfp_transport_result_right_productleft. ((((exists fom_beta_height_pfp_transport_result_right_productleft_entry. fom_beta_height_pfp_transport_result_right_productleft_entry + S (fom_value_pfp_transport_result_right_productleft) = S ((S (fom_index_pfp_transport_result_right_productleft)) * vc)) /\ exists fom_beta_quotient_pfp_transport_result_right_productleft_entry. vb = fom_beta_quotient_pfp_transport_result_right_productleft_entry * S ((S (fom_index_pfp_transport_result_right_productleft)) * vc) + (fom_value_pfp_transport_result_right_productleft))) /\ (exists fom_gap_pfp_transport_result_right_productleft_value_bound. fom_gap_pfp_transport_result_right_productleft_value_bound + S (fom_value_pfp_transport_result_right_productleft) = p))) /\ (((forall fom_index_pfp_transport_result_right_productright. (exists fom_gap_pfp_transport_result_right_productright_index_bound. fom_gap_pfp_transport_result_right_productright_index_bound + S (fom_index_pfp_transport_result_right_productright) = B2) -> exists fom_value_pfp_transport_result_right_productright. ((((exists fom_beta_height_pfp_transport_result_right_productright_entry. fom_beta_height_pfp_transport_result_right_productright_entry + S (fom_value_pfp_transport_result_right_productright) = S ((S (fom_index_pfp_transport_result_right_productright)) * bc2)) /\ exists fom_beta_quotient_pfp_transport_result_right_productright_entry. bb2 = fom_beta_quotient_pfp_transport_result_right_productright_entry * S ((S (fom_index_pfp_transport_result_right_productright)) * bc2) + (fom_value_pfp_transport_result_right_productright))) /\ (exists fom_gap_pfp_transport_result_right_productright_value_bound. fom_gap_pfp_transport_result_right_productright_value_bound + S (fom_value_pfp_transport_result_right_productright) = p))) /\ (((((((V)=0 \/ (B2)=0) /\ (((pfbz_right_length_transport_result)=0)))) \/ (((~((V)=0)) /\ (((~((B2)=0)) /\ (((V)+(B2)=S (pfbz_right_length_transport_result)))))))) /\ ((forall pfc_index_transport_result_right_productcoefficients. (exists pfa_gap_transport_result_right_productcoefficientsbound. pfa_gap_transport_result_right_productcoefficientsbound + S (pfc_index_transport_result_right_productcoefficients) = (pfbz_right_length_transport_result)) -> exists pfc_value_transport_result_right_productcoefficients. ((((exists ff_h_pfp_transport_result_right_productcoefficientsentry. ff_h_pfp_transport_result_right_productcoefficientsentry + S (pfc_value_transport_result_right_productcoefficients) = S ((S (pfc_index_transport_result_right_productcoefficients)) * pfbz_right_scale_transport_result)) /\ exists ff_q_pfp_transport_result_right_productcoefficientsentry. pfbz_right_code_transport_result = ff_q_pfp_transport_result_right_productcoefficientsentry * S ((S (pfc_index_transport_result_right_productcoefficients)) * pfbz_right_scale_transport_result) + (pfc_value_transport_result_right_productcoefficients))) /\ ((exists pfc_terms_code_transport_result_right_productcoefficientscoefficient pfc_terms_scale_transport_result_right_productcoefficientscoefficient pfc_natural_sum_transport_result_right_productcoefficientscoefficient. ((forall pfc_index_transport_result_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_transport_result_right_productcoefficientscoefficientdiagonalbound. pfa_gap_transport_result_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_transport_result_right_productcoefficients))) -> exists pfc_value_transport_result_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_transport_result_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_transport_result_right_productcoefficientscoefficient = ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient) + (pfc_value_transport_result_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)+pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm=(pfc_index_transport_result_right_productcoefficients)) /\ ((((((exists pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal) = (V)) /\ ((((exists ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * vc)) /\ exists ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry. vb = ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) * vc) + (pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermleftoutside+(V)=(pfc_index_transport_result_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm) = (B2)) /\ ((((exists ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm)) * bc2)) /\ exists ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry. bb2 = ff_q_pfp_transport_result_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm)) * bc2) + (pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_transport_result_right_productcoefficientscoefficientdiagonaltermrightoutside+(B2)=(pfc_complement_transport_result_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_transport_result_right_productcoefficientscoefficientdiagonal)=pfc_left_transport_result_right_productcoefficientscoefficientdiagonalterm*pfc_right_transport_result_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_transport_result_right_productcoefficientscoefficientsum fs_v_pfc_transport_result_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_transport_result_right_productcoefficientscoefficient) = S ((S (S (pfc_index_transport_result_right_productcoefficients))) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_transport_result_right_productcoefficients))) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (pfc_natural_sum_transport_result_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_transport_result_right_productcoefficients)) -> exists fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_transport_result_right_productcoefficientscoefficient = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_transport_result_right_productcoefficientscoefficient) + (fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_transport_result_right_productcoefficientscoefficientsum = fs_q_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_transport_result_right_productcoefficientscoefficientsum) + (fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_transport_result_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_transport_result_right_productcoefficientscoefficientresiduebound. pfa_gap_transport_result_right_productcoefficientscoefficientresiduebound + S (pfc_value_transport_result_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_transport_result_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_transport_result_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_transport_result_right_productcoefficientscoefficient) + (p) * pfa_offset_left_transport_result_right_productcoefficientscoefficientresiduecongruence = (pfc_value_transport_result_right_productcoefficients) + (p) * pfa_offset_right_transport_result_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_transport_result_sum_left_bounded. (exists fom_gap_pfp_transport_result_sum_left_bounded_index_bound. fom_gap_pfp_transport_result_sum_left_bounded_index_bound + S (fom_index_pfp_transport_result_sum_left_bounded) = pfbz_left_length_transport_result) -> exists fom_value_pfp_transport_result_sum_left_bounded. ((((exists fom_beta_height_pfp_transport_result_sum_left_bounded_entry. fom_beta_height_pfp_transport_result_sum_left_bounded_entry + S (fom_value_pfp_transport_result_sum_left_bounded) = S ((S (fom_index_pfp_transport_result_sum_left_bounded)) * pfbz_left_scale_transport_result)) /\ exists fom_beta_quotient_pfp_transport_result_sum_left_bounded_entry. pfbz_left_code_transport_result = fom_beta_quotient_pfp_transport_result_sum_left_bounded_entry * S ((S (fom_index_pfp_transport_result_sum_left_bounded)) * pfbz_left_scale_transport_result) + (fom_value_pfp_transport_result_sum_left_bounded))) /\ (exists fom_gap_pfp_transport_result_sum_left_bounded_value_bound. fom_gap_pfp_transport_result_sum_left_bounded_value_bound + S (fom_value_pfp_transport_result_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_transport_result_sum_right_bounded. (exists fom_gap_pfp_transport_result_sum_right_bounded_index_bound. fom_gap_pfp_transport_result_sum_right_bounded_index_bound + S (fom_index_pfp_transport_result_sum_right_bounded) = pfbz_right_length_transport_result) -> exists fom_value_pfp_transport_result_sum_right_bounded. ((((exists fom_beta_height_pfp_transport_result_sum_right_bounded_entry. fom_beta_height_pfp_transport_result_sum_right_bounded_entry + S (fom_value_pfp_transport_result_sum_right_bounded) = S ((S (fom_index_pfp_transport_result_sum_right_bounded)) * pfbz_right_scale_transport_result)) /\ exists fom_beta_quotient_pfp_transport_result_sum_right_bounded_entry. pfbz_right_code_transport_result = fom_beta_quotient_pfp_transport_result_sum_right_bounded_entry * S ((S (fom_index_pfp_transport_result_sum_right_bounded)) * pfbz_right_scale_transport_result) + (fom_value_pfp_transport_result_sum_right_bounded))) /\ (exists fom_gap_pfp_transport_result_sum_right_bounded_value_bound. fom_gap_pfp_transport_result_sum_right_bounded_value_bound + S (fom_value_pfp_transport_result_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_transport_result_sum_result_bounded. (exists fom_gap_pfp_transport_result_sum_result_bounded_index_bound. fom_gap_pfp_transport_result_sum_result_bounded_index_bound + S (fom_index_pfp_transport_result_sum_result_bounded) = G2) -> exists fom_value_pfp_transport_result_sum_result_bounded. ((((exists fom_beta_height_pfp_transport_result_sum_result_bounded_entry. fom_beta_height_pfp_transport_result_sum_result_bounded_entry + S (fom_value_pfp_transport_result_sum_result_bounded) = S ((S (fom_index_pfp_transport_result_sum_result_bounded)) * gc2)) /\ exists fom_beta_quotient_pfp_transport_result_sum_result_bounded_entry. gb2 = fom_beta_quotient_pfp_transport_result_sum_result_bounded_entry * S ((S (fom_index_pfp_transport_result_sum_result_bounded)) * gc2) + (fom_value_pfp_transport_result_sum_result_bounded))) /\ (exists fom_gap_pfp_transport_result_sum_result_bounded_value_bound. fom_gap_pfp_transport_result_sum_result_bounded_value_bound + S (fom_value_pfp_transport_result_sum_result_bounded) = p))) /\ ((exists pfaa_left_b_transport_result_sum pfaa_left_c_transport_result_sum pfaa_right_b_transport_result_sum pfaa_right_c_transport_result_sum pfaa_sum_b_transport_result_sum pfaa_sum_c_transport_result_sum pfaa_length_transport_result_sum. ((((forall pfrep_power_transport_result_sum_witness_common_left pfrep_left_transport_result_sum_witness_common_left pfrep_right_transport_result_sum_witness_common_left. ((exists pfrep_position_transport_result_sum_witness_common_leftfirst. ((pfrep_position_transport_result_sum_witness_common_leftfirst+S (pfrep_power_transport_result_sum_witness_common_left)=(pfbz_left_length_transport_result)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_leftfirstentry. ff_h_pfp_transport_result_sum_witness_common_leftfirstentry + S (pfrep_left_transport_result_sum_witness_common_left) = S ((S (pfrep_position_transport_result_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_result)) /\ exists ff_q_pfp_transport_result_sum_witness_common_leftfirstentry. pfbz_left_code_transport_result = ff_q_pfp_transport_result_sum_witness_common_leftfirstentry * S ((S (pfrep_position_transport_result_sum_witness_common_leftfirst)) * pfbz_left_scale_transport_result) + (pfrep_left_transport_result_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_leftfirstoutside. pfrep_gap_transport_result_sum_witness_common_leftfirstoutside+(pfbz_left_length_transport_result)=(pfrep_power_transport_result_sum_witness_common_left)) /\ (((pfrep_left_transport_result_sum_witness_common_left)=0))))) -> ((exists pfrep_position_transport_result_sum_witness_common_leftsecond. ((pfrep_position_transport_result_sum_witness_common_leftsecond+S (pfrep_power_transport_result_sum_witness_common_left)=(pfaa_length_transport_result_sum)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_leftsecondentry. ff_h_pfp_transport_result_sum_witness_common_leftsecondentry + S (pfrep_right_transport_result_sum_witness_common_left) = S ((S (pfrep_position_transport_result_sum_witness_common_leftsecond)) * pfaa_left_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_common_leftsecondentry. pfaa_left_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_common_leftsecondentry * S ((S (pfrep_position_transport_result_sum_witness_common_leftsecond)) * pfaa_left_c_transport_result_sum) + (pfrep_right_transport_result_sum_witness_common_left)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_leftsecondoutside. pfrep_gap_transport_result_sum_witness_common_leftsecondoutside+(pfaa_length_transport_result_sum)=(pfrep_power_transport_result_sum_witness_common_left)) /\ (((pfrep_right_transport_result_sum_witness_common_left)=0))))) -> pfrep_left_transport_result_sum_witness_common_left=pfrep_right_transport_result_sum_witness_common_left) /\ ((forall pfrep_power_transport_result_sum_witness_common_right pfrep_left_transport_result_sum_witness_common_right pfrep_right_transport_result_sum_witness_common_right. ((exists pfrep_position_transport_result_sum_witness_common_rightfirst. ((pfrep_position_transport_result_sum_witness_common_rightfirst+S (pfrep_power_transport_result_sum_witness_common_right)=(pfbz_right_length_transport_result)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_rightfirstentry. ff_h_pfp_transport_result_sum_witness_common_rightfirstentry + S (pfrep_left_transport_result_sum_witness_common_right) = S ((S (pfrep_position_transport_result_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_result)) /\ exists ff_q_pfp_transport_result_sum_witness_common_rightfirstentry. pfbz_right_code_transport_result = ff_q_pfp_transport_result_sum_witness_common_rightfirstentry * S ((S (pfrep_position_transport_result_sum_witness_common_rightfirst)) * pfbz_right_scale_transport_result) + (pfrep_left_transport_result_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_rightfirstoutside. pfrep_gap_transport_result_sum_witness_common_rightfirstoutside+(pfbz_right_length_transport_result)=(pfrep_power_transport_result_sum_witness_common_right)) /\ (((pfrep_left_transport_result_sum_witness_common_right)=0))))) -> ((exists pfrep_position_transport_result_sum_witness_common_rightsecond. ((pfrep_position_transport_result_sum_witness_common_rightsecond+S (pfrep_power_transport_result_sum_witness_common_right)=(pfaa_length_transport_result_sum)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_common_rightsecondentry. ff_h_pfp_transport_result_sum_witness_common_rightsecondentry + S (pfrep_right_transport_result_sum_witness_common_right) = S ((S (pfrep_position_transport_result_sum_witness_common_rightsecond)) * pfaa_right_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_common_rightsecondentry. pfaa_right_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_common_rightsecondentry * S ((S (pfrep_position_transport_result_sum_witness_common_rightsecond)) * pfaa_right_c_transport_result_sum) + (pfrep_right_transport_result_sum_witness_common_right)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_common_rightsecondoutside. pfrep_gap_transport_result_sum_witness_common_rightsecondoutside+(pfaa_length_transport_result_sum)=(pfrep_power_transport_result_sum_witness_common_right)) /\ (((pfrep_right_transport_result_sum_witness_common_right)=0))))) -> pfrep_left_transport_result_sum_witness_common_right=pfrep_right_transport_result_sum_witness_common_right)))) /\ (((forall pfp_index_transport_result_sum_witness_operation. (exists pfa_gap_transport_result_sum_witness_operationindex. pfa_gap_transport_result_sum_witness_operationindex + S (pfp_index_transport_result_sum_witness_operation) = (pfaa_length_transport_result_sum)) -> exists pfp_left_transport_result_sum_witness_operation pfp_right_transport_result_sum_witness_operation pfp_value_transport_result_sum_witness_operation. ((((exists ff_h_pfp_transport_result_sum_witness_operationleft. ff_h_pfp_transport_result_sum_witness_operationleft + S (pfp_left_transport_result_sum_witness_operation) = S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_left_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_operationleft. pfaa_left_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_operationleft * S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_left_c_transport_result_sum) + (pfp_left_transport_result_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_result_sum_witness_operationright. ff_h_pfp_transport_result_sum_witness_operationright + S (pfp_right_transport_result_sum_witness_operation) = S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_right_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_operationright. pfaa_right_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_operationright * S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_right_c_transport_result_sum) + (pfp_right_transport_result_sum_witness_operation))) /\ (((((exists ff_h_pfp_transport_result_sum_witness_operationtarget. ff_h_pfp_transport_result_sum_witness_operationtarget + S (pfp_value_transport_result_sum_witness_operation) = S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_sum_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_operationtarget. pfaa_sum_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_operationtarget * S ((S (pfp_index_transport_result_sum_witness_operation)) * pfaa_sum_c_transport_result_sum) + (pfp_value_transport_result_sum_witness_operation))) /\ ((((exists pfa_gap_transport_result_sum_witness_operationoperationleft. pfa_gap_transport_result_sum_witness_operationoperationleft + S (pfp_left_transport_result_sum_witness_operation) = (p)) /\ (((exists pfa_gap_transport_result_sum_witness_operationoperationright. pfa_gap_transport_result_sum_witness_operationoperationright + S (pfp_right_transport_result_sum_witness_operation) = (p)) /\ ((((exists pfa_gap_transport_result_sum_witness_operationoperationresultbound. pfa_gap_transport_result_sum_witness_operationoperationresultbound + S (pfp_value_transport_result_sum_witness_operation) = (p)) /\ ((exists pfa_offset_left_transport_result_sum_witness_operationoperationresultcongruence pfa_offset_right_transport_result_sum_witness_operationoperationresultcongruence. ((pfp_left_transport_result_sum_witness_operation) + (pfp_right_transport_result_sum_witness_operation)) + (p) * pfa_offset_left_transport_result_sum_witness_operationoperationresultcongruence = (pfp_value_transport_result_sum_witness_operation) + (p) * pfa_offset_right_transport_result_sum_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_transport_result_sum_witness_output pfrep_left_transport_result_sum_witness_output pfrep_right_transport_result_sum_witness_output. ((exists pfrep_position_transport_result_sum_witness_outputfirst. ((pfrep_position_transport_result_sum_witness_outputfirst+S (pfrep_power_transport_result_sum_witness_output)=(pfaa_length_transport_result_sum)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_outputfirstentry. ff_h_pfp_transport_result_sum_witness_outputfirstentry + S (pfrep_left_transport_result_sum_witness_output) = S ((S (pfrep_position_transport_result_sum_witness_outputfirst)) * pfaa_sum_c_transport_result_sum)) /\ exists ff_q_pfp_transport_result_sum_witness_outputfirstentry. pfaa_sum_b_transport_result_sum = ff_q_pfp_transport_result_sum_witness_outputfirstentry * S ((S (pfrep_position_transport_result_sum_witness_outputfirst)) * pfaa_sum_c_transport_result_sum) + (pfrep_left_transport_result_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_outputfirstoutside. pfrep_gap_transport_result_sum_witness_outputfirstoutside+(pfaa_length_transport_result_sum)=(pfrep_power_transport_result_sum_witness_output)) /\ (((pfrep_left_transport_result_sum_witness_output)=0))))) -> ((exists pfrep_position_transport_result_sum_witness_outputsecond. ((pfrep_position_transport_result_sum_witness_outputsecond+S (pfrep_power_transport_result_sum_witness_output)=(G2)) /\ ((((exists ff_h_pfp_transport_result_sum_witness_outputsecondentry. ff_h_pfp_transport_result_sum_witness_outputsecondentry + S (pfrep_right_transport_result_sum_witness_output) = S ((S (pfrep_position_transport_result_sum_witness_outputsecond)) * gc2)) /\ exists ff_q_pfp_transport_result_sum_witness_outputsecondentry. gb2 = ff_q_pfp_transport_result_sum_witness_outputsecondentry * S ((S (pfrep_position_transport_result_sum_witness_outputsecond)) * gc2) + (pfrep_right_transport_result_sum_witness_output)))))) \/ (((exists pfrep_gap_transport_result_sum_witness_outputsecondoutside. pfrep_gap_transport_result_sum_witness_outputsecondoutside+(G2)=(pfrep_power_transport_result_sum_witness_output)) /\ (((pfrep_right_transport_result_sum_witness_output)=0))))) -> pfrep_left_transport_result_sum_witness_output=pfrep_right_transport_result_sum_witness_output))))))))))))))))))Complete tactic proof in conservative notation
All 208 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 208 script commands · 39 reading checkpoints · 9 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1) 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 A
L5 intro bb
L6 intro bc
L7 intro B
L8 intro gb
L9 intro gc
L10 intro G
02 Fix variables and assumptions L11–20 Work with arbitrary variables or the premises of the current implication.
L11 intro ub
L12 intro uc
L13 intro U
L14 intro vb
L15 intro vc
L16 intro V
L17 intro ab2
L18 intro ac2
L19 intro A2
L20 intro bb2
03 Fix variables and assumptions L21–30 Work with arbitrary variables or the premises of the current implication.
L21 intro bc2
L22 intro B2
L23 intro gb2
L24 intro gc2
L25 intro G2
L26 intro hp0
L27 intro ha2
L28 intro hb2
L29 intro hg2
L30 intro haeq
04 Fix variables and assumptions L31–33 Work with arbitrary variables or the premises of the current implication.
L31 intro hbeq
L32 intro hgeq
L33 intro hbezout
05 Separate the logical cases L34–41 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L34 cases hbezout
L35 cases hbezout_witness
L36 cases hbezout_witness_witness
L37 cases hbezout_witness_witness_witness
L38 cases hbezout_witness_witness_witness_witness
L39 cases hbezout_witness_witness_witness_witness_witness
L40 cases hbezout_witness_witness_witness_witness_witness_witness
L41 cases hbezout_witness_witness_witness_witness_witness_witness_right
06 Establish hub L42–42 Establish this local claim before using it. It is not an additional assumption.
L42 07 Separate the logical cases L43–43 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L43 cases hbezout_witness_witness_witness_witness_witness_witness_left
08 Use earlier facts L44–44 Instantiate or apply named facts and discharge the corresponding proof obligations.
L44 exact hbezout_witness_witness_witness_witness_witness_witness_left_left
09 Establish hvb L45–45 Establish this local claim before using it. It is not an additional assumption.
L45 10 Separate the logical cases L46–46 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L46 cases hbezout_witness_witness_witness_witness_witness_witness_right_left
11 Use earlier facts L47–47 Instantiate or apply named facts and discharge the corresponding proof obligations.
L47 exact hbezout_witness_witness_witness_witness_witness_witness_right_left_left
12 Establish hnew_left_length L48–51 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
L48 L49 specialize polynomial_product_length_exists (U)
L50 specialize polynomial_product_length_exists (A2)
L51 apply polynomial_product_length_exists
13 Separate the logical cases L52–52 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L52 cases hnew_left_length
14 Establish hnew_left_product L53–62 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.
L53 have hnew_left_product : ∃ b. ∃ c. FpPolyProduct(p,ub,uc,U,ab2,ac2,A2,b,c,x6)Definitions: FpPolyProduct(p,ub,uc,U,ab2,ac2,A2,b,c,x6) Original native command in the exact edition L54 specialize prime_field_polynomial_convolution_at_length_exists (p)
L55 specialize prime_field_polynomial_convolution_at_length_exists (ub)
L56 specialize prime_field_polynomial_convolution_at_length_exists (uc)
L57 specialize prime_field_polynomial_convolution_at_length_exists (U)
L58 specialize prime_field_polynomial_convolution_at_length_exists (ab2)
L59 specialize prime_field_polynomial_convolution_at_length_exists (ac2)
L60 specialize prime_field_polynomial_convolution_at_length_exists (A2)
L61 specialize prime_field_polynomial_convolution_at_length_exists (x6)
L62 apply prime_field_polynomial_convolution_at_length_exists
15 Use earlier facts L63–66 Instantiate or apply named facts and discharge the corresponding proof obligations.
L63 exact hp0
L64 exact hub
L65 exact ha2
L66 exact hnew_left_length_witness
16 Separate the logical cases L67–68 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L67 cases hnew_left_product
L68 cases hnew_left_product_witness
17 Establish hnew_right_length L69–72 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.
L69 L70 specialize polynomial_product_length_exists (V)
L71 specialize polynomial_product_length_exists (B2)
L72 apply polynomial_product_length_exists
18 Separate the logical cases L73–73 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L73 cases hnew_right_length
19 Establish hnew_right_product L74–83 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.
L74 have hnew_right_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,V,bb2,bc2,B2,b,c,x9)Definitions: FpPolyProduct(p,vb,vc,V,bb2,bc2,B2,b,c,x9) Original native command in the exact edition L75 specialize prime_field_polynomial_convolution_at_length_exists (p)
L76 specialize prime_field_polynomial_convolution_at_length_exists (vb)
L77 specialize prime_field_polynomial_convolution_at_length_exists (vc)
L78 specialize prime_field_polynomial_convolution_at_length_exists (V)
L79 specialize prime_field_polynomial_convolution_at_length_exists (bb2)
L80 specialize prime_field_polynomial_convolution_at_length_exists (bc2)
L81 specialize prime_field_polynomial_convolution_at_length_exists (B2)
L82 specialize prime_field_polynomial_convolution_at_length_exists (x9)
L83 apply prime_field_polynomial_convolution_at_length_exists
20 Use earlier facts L84–87 Instantiate or apply named facts and discharge the corresponding proof obligations.
L84 exact hp0
L85 exact hvb
L86 exact hb2
L87 exact hnew_right_length_witness
21 Separate the logical cases L88–89 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L88 cases hnew_right_product
L89 cases hnew_right_product_witness
22 Establish hpp L90–99 Establish this local claim before using it. It is not an additional assumption.
L90 L91 specialize prime_field_polynomial_convolution_bounded (p)
L92 specialize prime_field_polynomial_convolution_bounded (ub)
L93 specialize prime_field_polynomial_convolution_bounded (uc)
L94 specialize prime_field_polynomial_convolution_bounded (U)
L95 specialize prime_field_polynomial_convolution_bounded (ab2)
L96 specialize prime_field_polynomial_convolution_bounded (ac2)
L97 specialize prime_field_polynomial_convolution_bounded (A2)
L98 specialize prime_field_polynomial_convolution_bounded (x7)
L99 specialize prime_field_polynomial_convolution_bounded (x8)
23 Use earlier facts L100–102 Instantiate or apply named facts and discharge the corresponding proof obligations.
L100 specialize prime_field_polynomial_convolution_bounded (x6)
L101 apply prime_field_polynomial_convolution_bounded
L102 exact hnew_left_product_witness_witness
24 Establish hqq L103–112 Establish this local claim before using it. It is not an additional assumption.
L103 L104 specialize prime_field_polynomial_convolution_bounded (p)
L105 specialize prime_field_polynomial_convolution_bounded (vb)
L106 specialize prime_field_polynomial_convolution_bounded (vc)
L107 specialize prime_field_polynomial_convolution_bounded (V)
L108 specialize prime_field_polynomial_convolution_bounded (bb2)
L109 specialize prime_field_polynomial_convolution_bounded (bc2)
L110 specialize prime_field_polynomial_convolution_bounded (B2)
L111 specialize prime_field_polynomial_convolution_bounded (x10)
L112 specialize prime_field_polynomial_convolution_bounded (x11)
25 Use earlier facts L113–115 Instantiate or apply named facts and discharge the corresponding proof obligations.
L113 specialize prime_field_polynomial_convolution_bounded (x9)
L114 apply prime_field_polynomial_convolution_bounded
L115 exact hnew_right_product_witness_witness
26 Establish hsum L116–125 Establish this local claim before using it. It is not an additional assumption.
L116 have hsum : FpPolynomialAlignedAdd(p,x7,x8,x6,x10,x11,x9,gb2,gc2,G2)Definitions: FpPolynomialAlignedAdd(p,x7,x8,x6,x10,x11,x9,gb2,gc2,G2) Original native command in the exact edition L117 specialize prime_field_polynomial_aligned_add_transport (p)
L118 specialize prime_field_polynomial_aligned_add_transport (x)
L119 specialize prime_field_polynomial_aligned_add_transport (x1)
L120 specialize prime_field_polynomial_aligned_add_transport (x2)
L121 specialize prime_field_polynomial_aligned_add_transport (x3)
L122 specialize prime_field_polynomial_aligned_add_transport (x4)
L123 specialize prime_field_polynomial_aligned_add_transport (x5)
L124 specialize prime_field_polynomial_aligned_add_transport (gb)
L125 specialize prime_field_polynomial_aligned_add_transport (gc)
27 Use earlier facts L126–135 Instantiate or apply named facts and discharge the corresponding proof obligations.
L126 specialize prime_field_polynomial_aligned_add_transport (G)
L127 specialize prime_field_polynomial_aligned_add_transport (x7)
L128 specialize prime_field_polynomial_aligned_add_transport (x8)
L129 specialize prime_field_polynomial_aligned_add_transport (x6)
L130 specialize prime_field_polynomial_aligned_add_transport (x10)
L131 specialize prime_field_polynomial_aligned_add_transport (x11)
L132 specialize prime_field_polynomial_aligned_add_transport (x9)
L133 specialize prime_field_polynomial_aligned_add_transport (gb2)
L134 specialize prime_field_polynomial_aligned_add_transport (gc2)
L135 specialize prime_field_polynomial_aligned_add_transport (G2)
28 Use earlier facts L136–145 Instantiate or apply named facts and discharge the corresponding proof obligations.
L136 apply prime_field_polynomial_aligned_add_transport
L137 exact hpp
L138 exact hqq
L139 exact hg2
L140 specialize prime_field_polynomial_equivalent_symmetric (x)
L141 specialize prime_field_polynomial_equivalent_symmetric (x1)
L142 specialize prime_field_polynomial_equivalent_symmetric (x2)
L143 specialize prime_field_polynomial_equivalent_symmetric (x7)
L144 specialize prime_field_polynomial_equivalent_symmetric (x8)
L145 specialize prime_field_polynomial_equivalent_symmetric (x6)
29 Use earlier facts L146–155 Instantiate or apply named facts and discharge the corresponding proof obligations.
L146 apply prime_field_polynomial_equivalent_symmetric
L147 specialize prime_field_polynomial_convolution_equivalent_congruent_right (p)
L148 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ub)
L149 specialize prime_field_polynomial_convolution_equivalent_congruent_right (uc)
L150 specialize prime_field_polynomial_convolution_equivalent_congruent_right (U)
L151 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ab)
L152 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ac)
L153 specialize prime_field_polynomial_convolution_equivalent_congruent_right (A)
L154 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x)
L155 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x1)
30 Use earlier facts L156–165 Instantiate or apply named facts and discharge the corresponding proof obligations.
L156 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x2)
L157 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ab2)
L158 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ac2)
L159 specialize prime_field_polynomial_convolution_equivalent_congruent_right (A2)
L160 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x7)
L161 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x8)
L162 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x6)
L163 apply prime_field_polynomial_convolution_equivalent_congruent_right
L164 exact hp0
L165 exact haeq
31 Use earlier facts L166–175 Instantiate or apply named facts and discharge the corresponding proof obligations.
L166 exact hbezout_witness_witness_witness_witness_witness_witness_left
L167 exact hnew_left_product_witness_witness
L168 specialize prime_field_polynomial_equivalent_symmetric (x3)
L169 specialize prime_field_polynomial_equivalent_symmetric (x4)
L170 specialize prime_field_polynomial_equivalent_symmetric (x5)
L171 specialize prime_field_polynomial_equivalent_symmetric (x10)
L172 specialize prime_field_polynomial_equivalent_symmetric (x11)
L173 specialize prime_field_polynomial_equivalent_symmetric (x9)
L174 apply prime_field_polynomial_equivalent_symmetric
L175 specialize prime_field_polynomial_convolution_equivalent_congruent_right (p)
32 Use earlier facts L176–185 Instantiate or apply named facts and discharge the corresponding proof obligations.
L176 specialize prime_field_polynomial_convolution_equivalent_congruent_right (vb)
L177 specialize prime_field_polynomial_convolution_equivalent_congruent_right (vc)
L178 specialize prime_field_polynomial_convolution_equivalent_congruent_right (V)
L179 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bb)
L180 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bc)
L181 specialize prime_field_polynomial_convolution_equivalent_congruent_right (B)
L182 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x3)
L183 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x4)
L184 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x5)
L185 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bb2)
33 Use earlier facts L186–195 Instantiate or apply named facts and discharge the corresponding proof obligations.
L186 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bc2)
L187 specialize prime_field_polynomial_convolution_equivalent_congruent_right (B2)
L188 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x10)
L189 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x11)
L190 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x9)
L191 apply prime_field_polynomial_convolution_equivalent_congruent_right
L192 exact hp0
L193 exact hbeq
L194 exact hbezout_witness_witness_witness_witness_witness_witness_right_left
L195 exact hnew_right_product_witness_witness
34 Use earlier facts L196–197 Instantiate or apply named facts and discharge the corresponding proof obligations.
L196 exact hgeq
L197 exact hbezout_witness_witness_witness_witness_witness_witness_right_right
35 Construct an explicit witness L198–203 Supply the displayed value, then prove that it has the required property.
L198 exists x7
L199 exists x8
L200 exists x6
L201 exists x10
L202 exists x11
L203 exists x9
36 Separate the logical cases L204–204 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L204 split
37 Use earlier facts L205–205 Instantiate or apply named facts and discharge the corresponding proof obligations.
L205 exact hnew_left_product_witness_witness
38 Separate the logical cases L206–206 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L206 split
39 Use earlier facts L207–208 Instantiate or apply named facts and discharge the corresponding proof obligations.
L207 exact hnew_right_product_witness_witness
L208 exact hsum
Library-wide reading audit
Original defined command ledger · 208 lines 0001 intro p0002 intro ab0003 intro ac0004 intro A0005 intro bb0006 intro bc0007 intro B0008 intro gb0009 intro gc0010 intro G0011 intro ub0012 intro uc0013 intro U0014 intro vb0015 intro vc0016 intro V0017 intro ab20018 intro ac20019 intro A20020 intro bb20021 intro bc20022 intro B20023 intro gb20024 intro gc20025 intro G20026 intro hp00027 intro ha20028 intro hb20029 intro hg20030 intro haeq0031 intro hbeq0032 intro hgeq0033 intro hbezout0034 cases hbezout0035 cases hbezout_witness0036 cases hbezout_witness_witness0037 cases hbezout_witness_witness_witness0038 cases hbezout_witness_witness_witness_witness0039 cases hbezout_witness_witness_witness_witness_witness0040 cases hbezout_witness_witness_witness_witness_witness_witness0041 cases hbezout_witness_witness_witness_witness_witness_witness_right0042 have hub : BetaPrefixInto(ub,uc,U,p) 0043 cases hbezout_witness_witness_witness_witness_witness_witness_left0044 exact hbezout_witness_witness_witness_witness_witness_witness_left_left0045 have hvb : BetaPrefixInto(vb,vc,V,p) 0046 cases hbezout_witness_witness_witness_witness_witness_witness_right_left0047 exact hbezout_witness_witness_witness_witness_witness_witness_right_left_left0048 have hnew_left_length : ∃ n. PolynomialProductLength(U,A2,n) 0049 specialize polynomial_product_length_exists (U)0050 specialize polynomial_product_length_exists (A2)0051 apply polynomial_product_length_exists0052 cases hnew_left_length0053 have hnew_left_product : ∃ b. ∃ c. FpPolyProduct(p,ub,uc,U,ab2,ac2,A2,b,c,x6) 0054 specialize prime_field_polynomial_convolution_at_length_exists (p)0055 specialize prime_field_polynomial_convolution_at_length_exists (ub)0056 specialize prime_field_polynomial_convolution_at_length_exists (uc)0057 specialize prime_field_polynomial_convolution_at_length_exists (U)0058 specialize prime_field_polynomial_convolution_at_length_exists (ab2)0059 specialize prime_field_polynomial_convolution_at_length_exists (ac2)0060 specialize prime_field_polynomial_convolution_at_length_exists (A2)0061 specialize prime_field_polynomial_convolution_at_length_exists (x6)0062 apply prime_field_polynomial_convolution_at_length_exists0063 exact hp00064 exact hub0065 exact ha20066 exact hnew_left_length_witness0067 cases hnew_left_product0068 cases hnew_left_product_witness0069 have hnew_right_length : ∃ n. PolynomialProductLength(V,B2,n) 0070 specialize polynomial_product_length_exists (V)0071 specialize polynomial_product_length_exists (B2)0072 apply polynomial_product_length_exists0073 cases hnew_right_length0074 have hnew_right_product : ∃ b. ∃ c. FpPolyProduct(p,vb,vc,V,bb2,bc2,B2,b,c,x9) 0075 specialize prime_field_polynomial_convolution_at_length_exists (p)0076 specialize prime_field_polynomial_convolution_at_length_exists (vb)0077 specialize prime_field_polynomial_convolution_at_length_exists (vc)0078 specialize prime_field_polynomial_convolution_at_length_exists (V)0079 specialize prime_field_polynomial_convolution_at_length_exists (bb2)0080 specialize prime_field_polynomial_convolution_at_length_exists (bc2)0081 specialize prime_field_polynomial_convolution_at_length_exists (B2)0082 specialize prime_field_polynomial_convolution_at_length_exists (x9)0083 apply prime_field_polynomial_convolution_at_length_exists0084 exact hp00085 exact hvb0086 exact hb20087 exact hnew_right_length_witness0088 cases hnew_right_product0089 cases hnew_right_product_witness0090 have hpp : BetaPrefixInto(x7,x8,x6,p) 0091 specialize prime_field_polynomial_convolution_bounded (p)0092 specialize prime_field_polynomial_convolution_bounded (ub)0093 specialize prime_field_polynomial_convolution_bounded (uc)0094 specialize prime_field_polynomial_convolution_bounded (U)0095 specialize prime_field_polynomial_convolution_bounded (ab2)0096 specialize prime_field_polynomial_convolution_bounded (ac2)0097 specialize prime_field_polynomial_convolution_bounded (A2)0098 specialize prime_field_polynomial_convolution_bounded (x7)0099 specialize prime_field_polynomial_convolution_bounded (x8)0100 specialize prime_field_polynomial_convolution_bounded (x6)0101 apply prime_field_polynomial_convolution_bounded0102 exact hnew_left_product_witness_witness0103 have hqq : BetaPrefixInto(x10,x11,x9,p) 0104 specialize prime_field_polynomial_convolution_bounded (p)0105 specialize prime_field_polynomial_convolution_bounded (vb)0106 specialize prime_field_polynomial_convolution_bounded (vc)0107 specialize prime_field_polynomial_convolution_bounded (V)0108 specialize prime_field_polynomial_convolution_bounded (bb2)0109 specialize prime_field_polynomial_convolution_bounded (bc2)0110 specialize prime_field_polynomial_convolution_bounded (B2)0111 specialize prime_field_polynomial_convolution_bounded (x10)0112 specialize prime_field_polynomial_convolution_bounded (x11)0113 specialize prime_field_polynomial_convolution_bounded (x9)0114 apply prime_field_polynomial_convolution_bounded0115 exact hnew_right_product_witness_witness0116 have hsum : FpPolynomialAlignedAdd(p,x7,x8,x6,x10,x11,x9,gb2,gc2,G2) 0117 specialize prime_field_polynomial_aligned_add_transport (p)0118 specialize prime_field_polynomial_aligned_add_transport (x)0119 specialize prime_field_polynomial_aligned_add_transport (x1)0120 specialize prime_field_polynomial_aligned_add_transport (x2)0121 specialize prime_field_polynomial_aligned_add_transport (x3)0122 specialize prime_field_polynomial_aligned_add_transport (x4)0123 specialize prime_field_polynomial_aligned_add_transport (x5)0124 specialize prime_field_polynomial_aligned_add_transport (gb)0125 specialize prime_field_polynomial_aligned_add_transport (gc)0126 specialize prime_field_polynomial_aligned_add_transport (G)0127 specialize prime_field_polynomial_aligned_add_transport (x7)0128 specialize prime_field_polynomial_aligned_add_transport (x8)0129 specialize prime_field_polynomial_aligned_add_transport (x6)0130 specialize prime_field_polynomial_aligned_add_transport (x10)0131 specialize prime_field_polynomial_aligned_add_transport (x11)0132 specialize prime_field_polynomial_aligned_add_transport (x9)0133 specialize prime_field_polynomial_aligned_add_transport (gb2)0134 specialize prime_field_polynomial_aligned_add_transport (gc2)0135 specialize prime_field_polynomial_aligned_add_transport (G2)0136 apply prime_field_polynomial_aligned_add_transport 0137 exact hpp0138 exact hqq0139 exact hg20140 specialize prime_field_polynomial_equivalent_symmetric (x)0141 specialize prime_field_polynomial_equivalent_symmetric (x1)0142 specialize prime_field_polynomial_equivalent_symmetric (x2)0143 specialize prime_field_polynomial_equivalent_symmetric (x7)0144 specialize prime_field_polynomial_equivalent_symmetric (x8)0145 specialize prime_field_polynomial_equivalent_symmetric (x6)0146 apply prime_field_polynomial_equivalent_symmetric0147 specialize prime_field_polynomial_convolution_equivalent_congruent_right (p)0148 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ub)0149 specialize prime_field_polynomial_convolution_equivalent_congruent_right (uc)0150 specialize prime_field_polynomial_convolution_equivalent_congruent_right (U)0151 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ab)0152 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ac)0153 specialize prime_field_polynomial_convolution_equivalent_congruent_right (A)0154 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x)0155 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x1)0156 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x2)0157 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ab2)0158 specialize prime_field_polynomial_convolution_equivalent_congruent_right (ac2)0159 specialize prime_field_polynomial_convolution_equivalent_congruent_right (A2)0160 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x7)0161 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x8)0162 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x6)0163 apply prime_field_polynomial_convolution_equivalent_congruent_right0164 exact hp00165 exact haeq0166 exact hbezout_witness_witness_witness_witness_witness_witness_left0167 exact hnew_left_product_witness_witness0168 specialize prime_field_polynomial_equivalent_symmetric (x3)0169 specialize prime_field_polynomial_equivalent_symmetric (x4)0170 specialize prime_field_polynomial_equivalent_symmetric (x5)0171 specialize prime_field_polynomial_equivalent_symmetric (x10)0172 specialize prime_field_polynomial_equivalent_symmetric (x11)0173 specialize prime_field_polynomial_equivalent_symmetric (x9)0174 apply prime_field_polynomial_equivalent_symmetric0175 specialize prime_field_polynomial_convolution_equivalent_congruent_right (p)0176 specialize prime_field_polynomial_convolution_equivalent_congruent_right (vb)0177 specialize prime_field_polynomial_convolution_equivalent_congruent_right (vc)0178 specialize prime_field_polynomial_convolution_equivalent_congruent_right (V)0179 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bb)0180 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bc)0181 specialize prime_field_polynomial_convolution_equivalent_congruent_right (B)0182 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x3)0183 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x4)0184 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x5)0185 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bb2)0186 specialize prime_field_polynomial_convolution_equivalent_congruent_right (bc2)0187 specialize prime_field_polynomial_convolution_equivalent_congruent_right (B2)0188 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x10)0189 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x11)0190 specialize prime_field_polynomial_convolution_equivalent_congruent_right (x9)0191 apply prime_field_polynomial_convolution_equivalent_congruent_right0192 exact hp00193 exact hbeq0194 exact hbezout_witness_witness_witness_witness_witness_witness_right_left0195 exact hnew_right_product_witness_witness0196 exact hgeq0197 exact hbezout_witness_witness_witness_witness_witness_witness_right_right0198 exists x70199 exists x80200 exists x60201 exists x100202 exists x110203 exists x90204 split0205 exact hnew_left_product_witness_witness0206 split0207 exact hnew_right_product_witness_witness0208 exact hsum