Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
Exact theorem in conservative defined notation
∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ d. ∀ qb. ∀ qc. ∀ q. ∀ rb. ∀ rc. ∀ R. Prime(p) → FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R) → (∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. FpPolynomialZeroOrMonic(p,x,y,z) ∧ (FpPolynomialCommonRightDivisor(p,x,y,z,bb,bc,S d,rb,rc,R) ∧ FpPolynomialBezoutRepresentation(p,bb,bc,S d,rb,rc,R,x,y,z,n,m,k,i,j,u))) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. FpPolynomialZeroOrMonic(p,x,y,z) ∧ (FpPolynomialCommonRightDivisor(p,x,y,z,ab,ac,L,bb,bc,S d) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,S d,x,y,z,n,m,k,i,j,u))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R) · 2FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 2FpPolynomialCommonRightDivisor(p,db,dc,D,ab,ac,L,bb,bc,M) · 7FpPolynomialBezoutRepresentation(p,ab,ac,A,bb,bc,B,gb,gc,G,ub,uc,U,vb,vc,V) · 5FpPolynomialZeroOrMonic(p,gb,gc,G) · 2Prime(p) · 2
Actual proof prerequisites
Original expanded first-order statement
forall p ab ac L bb bc d qb qc q rb rc R. (~((p) = 1) /\ forall pfa_factor_left_gcd_backward_prime pfa_factor_right_gcd_backward_prime. (p) = pfa_factor_left_gcd_backward_prime * pfa_factor_right_gcd_backward_prime -> pfa_factor_left_gcd_backward_prime = 1 \/ pfa_factor_right_gcd_backward_prime = 1) -> (((forall fom_index_pfp_gcd_backward_executioninput. (exists fom_gap_pfp_gcd_backward_executioninput_index_bound. fom_gap_pfp_gcd_backward_executioninput_index_bound + S (fom_index_pfp_gcd_backward_executioninput) = L) -> exists fom_value_pfp_gcd_backward_executioninput. ((((exists fom_beta_height_pfp_gcd_backward_executioninput_entry. fom_beta_height_pfp_gcd_backward_executioninput_entry + S (fom_value_pfp_gcd_backward_executioninput) = S ((S (fom_index_pfp_gcd_backward_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_backward_executioninput_entry. ab = fom_beta_quotient_pfp_gcd_backward_executioninput_entry * S ((S (fom_index_pfp_gcd_backward_executioninput)) * ac) + (fom_value_pfp_gcd_backward_executioninput))) /\ (exists fom_gap_pfp_gcd_backward_executioninput_value_bound. fom_gap_pfp_gcd_backward_executioninput_value_bound + S (fom_value_pfp_gcd_backward_executioninput) = p))) /\ (((forall fom_index_pfp_gcd_backward_executiondivisor. (exists fom_gap_pfp_gcd_backward_executiondivisor_index_bound. fom_gap_pfp_gcd_backward_executiondivisor_index_bound + S (fom_index_pfp_gcd_backward_executiondivisor) = S (d)) -> exists fom_value_pfp_gcd_backward_executiondivisor. ((((exists fom_beta_height_pfp_gcd_backward_executiondivisor_entry. fom_beta_height_pfp_gcd_backward_executiondivisor_entry + S (fom_value_pfp_gcd_backward_executiondivisor) = S ((S (fom_index_pfp_gcd_backward_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_executiondivisor_entry. bb = fom_beta_quotient_pfp_gcd_backward_executiondivisor_entry * S ((S (fom_index_pfp_gcd_backward_executiondivisor)) * bc) + (fom_value_pfp_gcd_backward_executiondivisor))) /\ (exists fom_gap_pfp_gcd_backward_executiondivisor_value_bound. fom_gap_pfp_gcd_backward_executiondivisor_value_bound + S (fom_value_pfp_gcd_backward_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_gcd_backward_executionlengthshort. pfc_gap_gcd_backward_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_gcd_backward_execution pfd_inverse_gcd_backward_execution pfd_product_code_gcd_backward_execution pfd_product_scale_gcd_backward_execution pfd_residual_code_gcd_backward_execution pfd_residual_scale_gcd_backward_execution pfd_cut_gcd_backward_execution. ((((exists ff_h_pfp_gcd_backward_executionhead. ff_h_pfp_gcd_backward_executionhead + S (pfd_head_gcd_backward_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_gcd_backward_executionhead. bb = ff_q_pfp_gcd_backward_executionhead * S ((S (0)) * bc) + (pfd_head_gcd_backward_execution))) /\ (((((~((pfd_head_gcd_backward_execution) = 0)) /\ ((((exists pfa_gap_gcd_backward_executioninversemultiplicationleft. pfa_gap_gcd_backward_executioninversemultiplicationleft + S (pfd_head_gcd_backward_execution) = (p)) /\ (((exists pfa_gap_gcd_backward_executioninversemultiplicationright. pfa_gap_gcd_backward_executioninversemultiplicationright + S (pfd_inverse_gcd_backward_execution) = (p)) /\ ((((exists pfa_gap_gcd_backward_executioninversemultiplicationresultbound. pfa_gap_gcd_backward_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executioninversemultiplicationresultcongruence pfa_offset_right_gcd_backward_executioninversemultiplicationresultcongruence. ((pfd_head_gcd_backward_execution) * (pfd_inverse_gcd_backward_execution)) + (p) * pfa_offset_left_gcd_backward_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_gcd_backward_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_gcd_backward_executionquotient. (exists pfa_gap_gcd_backward_executionquotientbound. pfa_gap_gcd_backward_executionquotientbound + S (pfd_index_gcd_backward_executionquotient) = (q)) -> exists pfd_value_gcd_backward_executionquotient. ((((exists ff_h_pfp_gcd_backward_executionquotiententry. ff_h_pfp_gcd_backward_executionquotiententry + S (pfd_value_gcd_backward_executionquotient) = S ((S (pfd_index_gcd_backward_executionquotient)) * qc)) /\ exists ff_q_pfp_gcd_backward_executionquotiententry. qb = ff_q_pfp_gcd_backward_executionquotiententry * S ((S (pfd_index_gcd_backward_executionquotient)) * qc) + (pfd_value_gcd_backward_executionquotient))) /\ ((exists pfd_input_gcd_backward_executionquotientstep pfd_previous_gcd_backward_executionquotientstep pfd_difference_gcd_backward_executionquotientstep. ((((exists ff_h_pfp_gcd_backward_executionquotientstepinput. ff_h_pfp_gcd_backward_executionquotientstepinput + S (pfd_input_gcd_backward_executionquotientstep) = S ((S (pfd_index_gcd_backward_executionquotient)) * ac)) /\ exists ff_q_pfp_gcd_backward_executionquotientstepinput. ab = ff_q_pfp_gcd_backward_executionquotientstepinput * S ((S (pfd_index_gcd_backward_executionquotient)) * ac) + (pfd_input_gcd_backward_executionquotientstep))) /\ (((exists pfc_terms_code_gcd_backward_executionquotientstepprevious pfc_terms_scale_gcd_backward_executionquotientstepprevious pfc_natural_sum_gcd_backward_executionquotientstepprevious. ((forall pfc_index_gcd_backward_executionquotientsteppreviousdiagonal. (exists pfa_gap_gcd_backward_executionquotientsteppreviousdiagonalbound. pfa_gap_gcd_backward_executionquotientsteppreviousdiagonalbound + S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal) = (S (pfd_index_gcd_backward_executionquotient))) -> exists pfc_value_gcd_backward_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry. ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry + S (pfc_value_gcd_backward_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious)) /\ exists ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry. pfc_terms_code_gcd_backward_executionquotientstepprevious = ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious) + (pfc_value_gcd_backward_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm. (((pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)+pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm=(pfd_index_gcd_backward_executionquotient)) /\ ((((((exists pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal) = (pfd_index_gcd_backward_executionquotient)) /\ ((((exists ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_gcd_backward_executionquotient)=(pfc_index_gcd_backward_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_gcd_backward_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_gcd_backward_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_executionquotientsteppreviousdiagonal)=pfc_left_gcd_backward_executionquotientsteppreviousdiagonalterm*pfc_right_gcd_backward_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_executionquotientstepprevioussum fs_v_pfc_gcd_backward_executionquotientstepprevioussum. ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_start. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_start. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_gcd_backward_executionquotientstepprevious) = S ((S (S (pfd_index_gcd_backward_executionquotient))) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_gcd_backward_executionquotient))) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (pfc_natural_sum_gcd_backward_executionquotientstepprevious))) /\ forall fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps = S (pfd_index_gcd_backward_executionquotient)) -> exists fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_gcd_backward_executionquotientstepprevious = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_gcd_backward_executionquotientstepprevious) + (fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum)) /\ exists fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_gcd_backward_executionquotientstepprevioussum = fs_q_pfc_gcd_backward_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_gcd_backward_executionquotientstepprevioussum) + (fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_gcd_backward_executionquotientstepprevioussum_body_steps = fs_r_pfc_gcd_backward_executionquotientstepprevioussum_body_steps + fs_a_pfc_gcd_backward_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_executionquotientsteppreviousresiduebound. pfa_gap_gcd_backward_executionquotientsteppreviousresiduebound + S (pfd_previous_gcd_backward_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionquotientsteppreviousresiduecongruence pfa_offset_right_gcd_backward_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_gcd_backward_executionquotientstepprevious) + (p) * pfa_offset_left_gcd_backward_executionquotientsteppreviousresiduecongruence = (pfd_previous_gcd_backward_executionquotientstep) + (p) * pfa_offset_right_gcd_backward_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_gcd_backward_executionquotientstepsubtractleft. pfa_gap_gcd_backward_executionquotientstepsubtractleft + S (pfd_previous_gcd_backward_executionquotientstep) = (p)) /\ (((exists pfa_gap_gcd_backward_executionquotientstepsubtractright. pfa_gap_gcd_backward_executionquotientstepsubtractright + S (pfd_difference_gcd_backward_executionquotientstep) = (p)) /\ ((((exists pfa_gap_gcd_backward_executionquotientstepsubtractresultbound. pfa_gap_gcd_backward_executionquotientstepsubtractresultbound + S (pfd_input_gcd_backward_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionquotientstepsubtractresultcongruence pfa_offset_right_gcd_backward_executionquotientstepsubtractresultcongruence. ((pfd_previous_gcd_backward_executionquotientstep) + (pfd_difference_gcd_backward_executionquotientstep)) + (p) * pfa_offset_left_gcd_backward_executionquotientstepsubtractresultcongruence = (pfd_input_gcd_backward_executionquotientstep) + (p) * pfa_offset_right_gcd_backward_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_gcd_backward_executionquotientstepmultiplyleft. pfa_gap_gcd_backward_executionquotientstepmultiplyleft + S (pfd_inverse_gcd_backward_execution) = (p)) /\ (((exists pfa_gap_gcd_backward_executionquotientstepmultiplyright. pfa_gap_gcd_backward_executionquotientstepmultiplyright + S (pfd_difference_gcd_backward_executionquotientstep) = (p)) /\ ((((exists pfa_gap_gcd_backward_executionquotientstepmultiplyresultbound. pfa_gap_gcd_backward_executionquotientstepmultiplyresultbound + S (pfd_value_gcd_backward_executionquotient) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionquotientstepmultiplyresultcongruence pfa_offset_right_gcd_backward_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_gcd_backward_execution) * (pfd_difference_gcd_backward_executionquotientstep)) + (p) * pfa_offset_left_gcd_backward_executionquotientstepmultiplyresultcongruence = (pfd_value_gcd_backward_executionquotient) + (p) * pfa_offset_right_gcd_backward_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_gcd_backward_executionproduct. (exists pfa_gap_gcd_backward_executionproductbound. pfa_gap_gcd_backward_executionproductbound + S (pfc_index_gcd_backward_executionproduct) = (L)) -> exists pfc_value_gcd_backward_executionproduct. ((((exists ff_h_pfp_gcd_backward_executionproductentry. ff_h_pfp_gcd_backward_executionproductentry + S (pfc_value_gcd_backward_executionproduct) = S ((S (pfc_index_gcd_backward_executionproduct)) * pfd_product_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executionproductentry. pfd_product_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executionproductentry * S ((S (pfc_index_gcd_backward_executionproduct)) * pfd_product_scale_gcd_backward_execution) + (pfc_value_gcd_backward_executionproduct))) /\ ((exists pfc_terms_code_gcd_backward_executionproductcoefficient pfc_terms_scale_gcd_backward_executionproductcoefficient pfc_natural_sum_gcd_backward_executionproductcoefficient. ((forall pfc_index_gcd_backward_executionproductcoefficientdiagonal. (exists pfa_gap_gcd_backward_executionproductcoefficientdiagonalbound. pfa_gap_gcd_backward_executionproductcoefficientdiagonalbound + S (pfc_index_gcd_backward_executionproductcoefficientdiagonal) = (S (pfc_index_gcd_backward_executionproduct))) -> exists pfc_value_gcd_backward_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_executionproductcoefficientdiagonalentry. ff_h_pfp_gcd_backward_executionproductcoefficientdiagonalentry + S (pfc_value_gcd_backward_executionproductcoefficientdiagonal) = S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * pfc_terms_scale_gcd_backward_executionproductcoefficient)) /\ exists ff_q_pfp_gcd_backward_executionproductcoefficientdiagonalentry. pfc_terms_code_gcd_backward_executionproductcoefficient = ff_q_pfp_gcd_backward_executionproductcoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * pfc_terms_scale_gcd_backward_executionproductcoefficient) + (pfc_value_gcd_backward_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm pfc_left_gcd_backward_executionproductcoefficientdiagonalterm pfc_right_gcd_backward_executionproductcoefficientdiagonalterm. (((pfc_index_gcd_backward_executionproductcoefficientdiagonal)+pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm=(pfc_index_gcd_backward_executionproduct)) /\ ((((((exists pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_executionproductcoefficientdiagonal)) * qc) + (pfc_left_gcd_backward_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_gcd_backward_executionproductcoefficientdiagonal)) /\ (((pfc_left_gcd_backward_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_gcd_backward_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_gcd_backward_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_executionproductcoefficientdiagonal)=pfc_left_gcd_backward_executionproductcoefficientdiagonalterm*pfc_right_gcd_backward_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_executionproductcoefficientsum fs_v_pfc_gcd_backward_executionproductcoefficientsum. ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_start. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_start. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_terminal. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_executionproductcoefficient) = S ((S (S (pfc_index_gcd_backward_executionproduct))) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_terminal. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_executionproduct))) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (pfc_natural_sum_gcd_backward_executionproductcoefficient))) /\ forall fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps = S (pfc_index_gcd_backward_executionproduct)) -> exists fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_executionproductcoefficient)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_executionproductcoefficient = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_executionproductcoefficient) + (fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum)) /\ exists fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_executionproductcoefficientsum = fs_q_pfc_gcd_backward_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_executionproductcoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_executionproductcoefficientsum) + (fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_executionproductcoefficientsum_body_steps = fs_r_pfc_gcd_backward_executionproductcoefficientsum_body_steps + fs_a_pfc_gcd_backward_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_executionproductcoefficientresiduebound. pfa_gap_gcd_backward_executionproductcoefficientresiduebound + S (pfc_value_gcd_backward_executionproduct) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executionproductcoefficientresiduecongruence pfa_offset_right_gcd_backward_executionproductcoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_executionproductcoefficient) + (p) * pfa_offset_left_gcd_backward_executionproductcoefficientresiduecongruence = (pfc_value_gcd_backward_executionproduct) + (p) * pfa_offset_right_gcd_backward_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_gcd_backward_executiondifference. (exists pfa_gap_gcd_backward_executiondifferenceindex. pfa_gap_gcd_backward_executiondifferenceindex + S (pfs_index_gcd_backward_executiondifference) = (L)) -> exists pfs_left_gcd_backward_executiondifference pfs_right_gcd_backward_executiondifference pfs_result_gcd_backward_executiondifference. ((((exists ff_h_pfp_gcd_backward_executiondifferenceleft. ff_h_pfp_gcd_backward_executiondifferenceleft + S (pfs_left_gcd_backward_executiondifference) = S ((S (pfs_index_gcd_backward_executiondifference)) * ac)) /\ exists ff_q_pfp_gcd_backward_executiondifferenceleft. ab = ff_q_pfp_gcd_backward_executiondifferenceleft * S ((S (pfs_index_gcd_backward_executiondifference)) * ac) + (pfs_left_gcd_backward_executiondifference))) /\ (((((exists ff_h_pfp_gcd_backward_executiondifferenceright. ff_h_pfp_gcd_backward_executiondifferenceright + S (pfs_right_gcd_backward_executiondifference) = S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_product_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiondifferenceright. pfd_product_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiondifferenceright * S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_product_scale_gcd_backward_execution) + (pfs_right_gcd_backward_executiondifference))) /\ (((((exists ff_h_pfp_gcd_backward_executiondifferenceresult. ff_h_pfp_gcd_backward_executiondifferenceresult + S (pfs_result_gcd_backward_executiondifference) = S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_residual_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiondifferenceresult. pfd_residual_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiondifferenceresult * S ((S (pfs_index_gcd_backward_executiondifference)) * pfd_residual_scale_gcd_backward_execution) + (pfs_result_gcd_backward_executiondifference))) /\ ((((exists pfa_gap_gcd_backward_executiondifferenceoperationleft. pfa_gap_gcd_backward_executiondifferenceoperationleft + S (pfs_right_gcd_backward_executiondifference) = (p)) /\ (((exists pfa_gap_gcd_backward_executiondifferenceoperationright. pfa_gap_gcd_backward_executiondifferenceoperationright + S (pfs_result_gcd_backward_executiondifference) = (p)) /\ ((((exists pfa_gap_gcd_backward_executiondifferenceoperationresultbound. pfa_gap_gcd_backward_executiondifferenceoperationresultbound + S (pfs_left_gcd_backward_executiondifference) = (p)) /\ ((exists pfa_offset_left_gcd_backward_executiondifferenceoperationresultcongruence pfa_offset_right_gcd_backward_executiondifferenceoperationresultcongruence. ((pfs_right_gcd_backward_executiondifference) + (pfs_result_gcd_backward_executiondifference)) + (p) * pfa_offset_left_gcd_backward_executiondifferenceoperationresultcongruence = (pfs_left_gcd_backward_executiondifference) + (p) * pfa_offset_right_gcd_backward_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_gcd_backward_execution)+(R)) /\ (((forall fom_index_pfp_gcd_backward_executiontriminput. (exists fom_gap_pfp_gcd_backward_executiontriminput_index_bound. fom_gap_pfp_gcd_backward_executiontriminput_index_bound + S (fom_index_pfp_gcd_backward_executiontriminput) = L) -> exists fom_value_pfp_gcd_backward_executiontriminput. ((((exists fom_beta_height_pfp_gcd_backward_executiontriminput_entry. fom_beta_height_pfp_gcd_backward_executiontriminput_entry + S (fom_value_pfp_gcd_backward_executiontriminput) = S ((S (fom_index_pfp_gcd_backward_executiontriminput)) * pfd_residual_scale_gcd_backward_execution)) /\ exists fom_beta_quotient_pfp_gcd_backward_executiontriminput_entry. pfd_residual_code_gcd_backward_execution = fom_beta_quotient_pfp_gcd_backward_executiontriminput_entry * S ((S (fom_index_pfp_gcd_backward_executiontriminput)) * pfd_residual_scale_gcd_backward_execution) + (fom_value_pfp_gcd_backward_executiontriminput))) /\ (exists fom_gap_pfp_gcd_backward_executiontriminput_value_bound. fom_gap_pfp_gcd_backward_executiontriminput_value_bound + S (fom_value_pfp_gcd_backward_executiontriminput) = p))) /\ (((forall pfp_repeat_index_gcd_backward_executiontrimremoved. (exists pfa_gap_gcd_backward_executiontrimremovedindex. pfa_gap_gcd_backward_executiontrimremovedindex + S (pfp_repeat_index_gcd_backward_executiontrimremoved) = (pfd_cut_gcd_backward_execution)) -> (((exists ff_h_pfp_gcd_backward_executiontrimremovedentry. ff_h_pfp_gcd_backward_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_gcd_backward_executiontrimremoved)) * pfd_residual_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiontrimremovedentry. pfd_residual_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiontrimremovedentry * S ((S (pfp_repeat_index_gcd_backward_executiontrimremoved)) * pfd_residual_scale_gcd_backward_execution) + (0)))) /\ (((forall pftrim_index_gcd_backward_executiontrimsuffix pftrim_value_gcd_backward_executiontrimsuffix. (exists pfa_gap_gcd_backward_executiontrimsuffixbound. pfa_gap_gcd_backward_executiontrimsuffixbound + S (pftrim_index_gcd_backward_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_gcd_backward_executiontrimsuffixsource. ff_h_pfp_gcd_backward_executiontrimsuffixsource + S (pftrim_value_gcd_backward_executiontrimsuffix) = S ((S ((pfd_cut_gcd_backward_execution)+pftrim_index_gcd_backward_executiontrimsuffix)) * pfd_residual_scale_gcd_backward_execution)) /\ exists ff_q_pfp_gcd_backward_executiontrimsuffixsource. pfd_residual_code_gcd_backward_execution = ff_q_pfp_gcd_backward_executiontrimsuffixsource * S ((S ((pfd_cut_gcd_backward_execution)+pftrim_index_gcd_backward_executiontrimsuffix)) * pfd_residual_scale_gcd_backward_execution) + (pftrim_value_gcd_backward_executiontrimsuffix))) -> (((exists ff_h_pfp_gcd_backward_executiontrimsuffixoutput. ff_h_pfp_gcd_backward_executiontrimsuffixoutput + S (pftrim_value_gcd_backward_executiontrimsuffix) = S ((S (pftrim_index_gcd_backward_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_gcd_backward_executiontrimsuffixoutput. rb = ff_q_pfp_gcd_backward_executiontrimsuffixoutput * S ((S (pftrim_index_gcd_backward_executiontrimsuffix)) * rc) + (pftrim_value_gcd_backward_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_gcd_backward_executiontrimnormal. ((((exists ff_h_pfp_gcd_backward_executiontrimnormalentry. ff_h_pfp_gcd_backward_executiontrimnormalentry + S (pftrim_leading_gcd_backward_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_gcd_backward_executiontrimnormalentry. rb = ff_q_pfp_gcd_backward_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_gcd_backward_executiontrimnormal))) /\ ((~(pftrim_leading_gcd_backward_executiontrimnormal=0))))))))))))))))))))))))))))))))) -> (exists pfgs_gb_gcd_backward_small pfgs_gc_gcd_backward_small pfgs_G_gcd_backward_small pfgs_ub_gcd_backward_small pfgs_uc_gcd_backward_small pfgs_U_gcd_backward_small pfgs_vb_gcd_backward_small pfgs_vc_gcd_backward_small pfgs_V_gcd_backward_small. (((pfgs_G_gcd_backward_small)=0 \/ (((~((pfgs_G_gcd_backward_small) = 0)) /\ (((forall fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_backward_small_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_backward_small_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_normal_monicleading. ff_h_pfp_gcd_backward_small_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_normal_monicleading. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_backward_small) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_backward_small_witness_common_left_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_left_bounded) = S d) -> exists fom_value_pfp_gcd_backward_small_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_bounded_entry. bb = fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_bounded)) * bc) + (fom_value_pfp_gcd_backward_small_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_small_witness_common_left pfgd_qc_gcd_backward_small_witness_common_left pfgd_Q_gcd_backward_small_witness_common_left pfgd_pb_gcd_backward_small_witness_common_left pfgd_pc_gcd_backward_small_witness_common_left pfgd_P_gcd_backward_small_witness_common_left. ((((forall fom_index_pfp_gcd_backward_small_witness_common_left_productleft. (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_left_productleft) = pfgd_Q_gcd_backward_small_witness_common_left) -> exists fom_value_pfp_gcd_backward_small_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_backward_small_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productleft)) * pfgd_qc_gcd_backward_small_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productleft_entry. pfgd_qb_gcd_backward_small_witness_common_left = fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productleft)) * pfgd_qc_gcd_backward_small_witness_common_left) + (fom_value_pfp_gcd_backward_small_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_common_left_productright. (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_left_productright) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_left_productright_entry + S (fom_value_pfp_gcd_backward_small_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productright)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productright_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_left_productright)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_small_witness_common_left)=0 \/ (pfgs_G_gcd_backward_small)=0) /\ (((pfgd_P_gcd_backward_small_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_backward_small_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_backward_small)=0)) /\ (((pfgd_Q_gcd_backward_small_witness_common_left)+(pfgs_G_gcd_backward_small)=S (pfgd_P_gcd_backward_small_witness_common_left)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_common_left_productcoefficients. (exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientsbound. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients) = (pfgd_P_gcd_backward_small_witness_common_left)) -> exists pfc_value_gcd_backward_small_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_backward_small_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_backward_small_witness_common_left = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_left) + (pfc_value_gcd_backward_small_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_small_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_small_witness_common_left = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_left) + (pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_small_witness_common_left)=(pfc_index_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small) + (pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_small)=(pfc_complement_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_small_witness_common_left_equivalent pfrep_left_gcd_backward_small_witness_common_left_equivalent pfrep_right_gcd_backward_small_witness_common_left_equivalent. ((exists pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst. ((pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst+S (pfrep_power_gcd_backward_small_witness_common_left_equivalent)=(pfgd_P_gcd_backward_small_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_backward_small_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_backward_small_witness_common_left = ff_q_pfp_gcd_backward_small_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_left) + (pfrep_left_gcd_backward_small_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_backward_small_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_backward_small_witness_common_left)=(pfrep_power_gcd_backward_small_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_backward_small_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond. ((pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond+S (pfrep_power_gcd_backward_small_witness_common_left_equivalent)=(S d)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_backward_small_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry. bb = ff_q_pfp_gcd_backward_small_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_common_left_equivalentsecond)) * bc) + (pfrep_right_gcd_backward_small_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_backward_small_witness_common_left_equivalentsecondoutside+(S d)=(pfrep_power_gcd_backward_small_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_backward_small_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_backward_small_witness_common_left_equivalent=pfrep_right_gcd_backward_small_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_backward_small_witness_common_right_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_right_bounded) = R) -> exists fom_value_pfp_gcd_backward_small_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_bounded_entry. rb = fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_bounded)) * rc) + (fom_value_pfp_gcd_backward_small_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_small_witness_common_right pfgd_qc_gcd_backward_small_witness_common_right pfgd_Q_gcd_backward_small_witness_common_right pfgd_pb_gcd_backward_small_witness_common_right pfgd_pc_gcd_backward_small_witness_common_right pfgd_P_gcd_backward_small_witness_common_right. ((((forall fom_index_pfp_gcd_backward_small_witness_common_right_productleft. (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_right_productleft) = pfgd_Q_gcd_backward_small_witness_common_right) -> exists fom_value_pfp_gcd_backward_small_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_backward_small_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productleft)) * pfgd_qc_gcd_backward_small_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productleft_entry. pfgd_qb_gcd_backward_small_witness_common_right = fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productleft)) * pfgd_qc_gcd_backward_small_witness_common_right) + (fom_value_pfp_gcd_backward_small_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_common_right_productright. (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_common_right_productright) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_backward_small_witness_common_right_productright_entry + S (fom_value_pfp_gcd_backward_small_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productright)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productright_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_common_right_productright)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_backward_small_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_small_witness_common_right)=0 \/ (pfgs_G_gcd_backward_small)=0) /\ (((pfgd_P_gcd_backward_small_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_backward_small_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_backward_small)=0)) /\ (((pfgd_Q_gcd_backward_small_witness_common_right)+(pfgs_G_gcd_backward_small)=S (pfgd_P_gcd_backward_small_witness_common_right)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_common_right_productcoefficients. (exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientsbound. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients) = (pfgd_P_gcd_backward_small_witness_common_right)) -> exists pfc_value_gcd_backward_small_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_backward_small_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_backward_small_witness_common_right = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_small_witness_common_right) + (pfc_value_gcd_backward_small_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_small_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_small_witness_common_right = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_small_witness_common_right) + (pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_small_witness_common_right)=(pfc_index_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_small) + (pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_small)=(pfc_complement_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_small_witness_common_right_equivalent pfrep_left_gcd_backward_small_witness_common_right_equivalent pfrep_right_gcd_backward_small_witness_common_right_equivalent. ((exists pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst. ((pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst+S (pfrep_power_gcd_backward_small_witness_common_right_equivalent)=(pfgd_P_gcd_backward_small_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_backward_small_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_backward_small_witness_common_right = ff_q_pfp_gcd_backward_small_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_small_witness_common_right) + (pfrep_left_gcd_backward_small_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_backward_small_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_backward_small_witness_common_right)=(pfrep_power_gcd_backward_small_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_backward_small_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond. ((pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond+S (pfrep_power_gcd_backward_small_witness_common_right_equivalent)=(R)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_backward_small_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond)) * rc)) /\ exists ff_q_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry. rb = ff_q_pfp_gcd_backward_small_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_common_right_equivalentsecond)) * rc) + (pfrep_right_gcd_backward_small_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_backward_small_witness_common_right_equivalentsecondoutside+(R)=(pfrep_power_gcd_backward_small_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_backward_small_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_backward_small_witness_common_right_equivalent=pfrep_right_gcd_backward_small_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_backward_small_witness_bezout pfgb_pc_gcd_backward_small_witness_bezout pfgb_P_gcd_backward_small_witness_bezout pfgb_qb_gcd_backward_small_witness_bezout pfgb_qc_gcd_backward_small_witness_bezout pfgb_Q_gcd_backward_small_witness_bezout. ((((forall fom_index_pfp_gcd_backward_small_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_leftleft) = pfgs_U_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftleft_entry. pfgs_ub_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_leftright. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_leftright) = S d) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftright_entry. bb = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_leftright)) * bc) + (fom_value_pfp_gcd_backward_small_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_backward_small)=0 \/ (S d)=0) /\ (((pfgb_P_gcd_backward_small_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_backward_small)=0)) /\ (((~((S d)=0)) /\ (((pfgs_U_gcd_backward_small)+(S d)=S (pfgb_P_gcd_backward_small_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients) = (pfgb_P_gcd_backward_small_witness_bezout)) -> exists pfc_value_gcd_backward_small_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_small_witness_bezout) + (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_small) + (pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_backward_small)=(pfc_index_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_backward_small_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_rightleft) = pfgs_V_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightleft_entry. pfgs_vb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_rightright. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_rightright) = R) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightright)) * rc)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightright_entry. rb = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_rightright)) * rc) + (fom_value_pfp_gcd_backward_small_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_backward_small)=0 \/ (R)=0) /\ (((pfgb_Q_gcd_backward_small_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_backward_small)=0)) /\ (((~((R)=0)) /\ (((pfgs_V_gcd_backward_small)+(R)=S (pfgb_Q_gcd_backward_small_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_small_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_backward_small_witness_bezout)) -> exists pfc_value_gcd_backward_small_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_small_witness_bezout) + (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_small_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_small_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_small) + (pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_backward_small)=(pfc_index_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (R)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * rc)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. rb = ff_q_pfp_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * rc) + (pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(R)=(pfc_complement_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_small_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_small_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_small_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_small_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_small_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_backward_small_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded) = pfgb_P_gcd_backward_small_witness_bezout) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_small_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_backward_small_witness_bezout = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_small_witness_bezout) + (fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_backward_small_witness_bezout) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_small_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_backward_small_witness_bezout = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_small_witness_bezout) + (fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded) = pfgs_G_gcd_backward_small) -> exists fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_small)) /\ exists fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_backward_small = fom_beta_quotient_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_backward_small_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_small) + (fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_backward_small_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_backward_small_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_backward_small_witness_bezout_sum pfga_uc_gcd_backward_small_witness_bezout_sum pfga_vb_gcd_backward_small_witness_bezout_sum pfga_vc_gcd_backward_small_witness_bezout_sum pfga_tb_gcd_backward_small_witness_bezout_sum pfga_tc_gcd_backward_small_witness_bezout_sum pfga_K_gcd_backward_small_witness_bezout_sum. ((((forall pfrep_power_gcd_backward_small_witness_bezout_sum_left pfrep_left_gcd_backward_small_witness_bezout_sum_left pfrep_right_gcd_backward_small_witness_bezout_sum_left. ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_backward_small_witness_bezout_sum_left)=(pfgb_P_gcd_backward_small_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_backward_small_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_small_witness_bezout) + (pfrep_left_gcd_backward_small_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_backward_small_witness_bezout)=(pfrep_power_gcd_backward_small_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_backward_small_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_backward_small_witness_bezout_sum_left)=(pfga_K_gcd_backward_small_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_backward_small_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_small_witness_bezout_sum) + (pfrep_right_gcd_backward_small_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_backward_small_witness_bezout_sum)=(pfrep_power_gcd_backward_small_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_backward_small_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_backward_small_witness_bezout_sum_left=pfrep_right_gcd_backward_small_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_backward_small_witness_bezout_sum_right pfrep_left_gcd_backward_small_witness_bezout_sum_right pfrep_right_gcd_backward_small_witness_bezout_sum_right. ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_backward_small_witness_bezout_sum_right)=(pfgb_Q_gcd_backward_small_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_backward_small_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_small_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_backward_small_witness_bezout = ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_small_witness_bezout) + (pfrep_left_gcd_backward_small_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_backward_small_witness_bezout)=(pfrep_power_gcd_backward_small_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_backward_small_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_backward_small_witness_bezout_sum_right)=(pfga_K_gcd_backward_small_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_backward_small_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_small_witness_bezout_sum) + (pfrep_right_gcd_backward_small_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_backward_small_witness_bezout_sum)=(pfrep_power_gcd_backward_small_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_backward_small_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_backward_small_witness_bezout_sum_right=pfrep_right_gcd_backward_small_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_backward_small_witness_bezout_sum_add. (exists pfa_gap_gcd_backward_small_witness_bezout_sum_addindex. pfa_gap_gcd_backward_small_witness_bezout_sum_addindex + S (pfp_index_gcd_backward_small_witness_bezout_sum_add) = (pfga_K_gcd_backward_small_witness_bezout_sum)) -> exists pfp_left_gcd_backward_small_witness_bezout_sum_add pfp_right_gcd_backward_small_witness_bezout_sum_add pfp_value_gcd_backward_small_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_addleft. ff_h_pfp_gcd_backward_small_witness_bezout_sum_addleft + S (pfp_left_gcd_backward_small_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_uc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_addleft. pfga_ub_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_uc_gcd_backward_small_witness_bezout_sum) + (pfp_left_gcd_backward_small_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_addright. ff_h_pfp_gcd_backward_small_witness_bezout_sum_addright + S (pfp_right_gcd_backward_small_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_vc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_addright. pfga_vb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_addright * S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_vc_gcd_backward_small_witness_bezout_sum) + (pfp_right_gcd_backward_small_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_addtarget. ff_h_pfp_gcd_backward_small_witness_bezout_sum_addtarget + S (pfp_value_gcd_backward_small_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_tc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_addtarget. pfga_tb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_backward_small_witness_bezout_sum_add)) * pfga_tc_gcd_backward_small_witness_bezout_sum) + (pfp_value_gcd_backward_small_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationleft. pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_backward_small_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationright. pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationright + S (pfp_right_gcd_backward_small_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_backward_small_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_backward_small_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_backward_small_witness_bezout_sum_add) + (pfp_right_gcd_backward_small_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_backward_small_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_backward_small_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_backward_small_witness_bezout_sum_result pfrep_left_gcd_backward_small_witness_bezout_sum_result pfrep_right_gcd_backward_small_witness_bezout_sum_result. ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_backward_small_witness_bezout_sum_result)=(pfga_K_gcd_backward_small_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_backward_small_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_small_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_backward_small_witness_bezout_sum = ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_small_witness_bezout_sum) + (pfrep_left_gcd_backward_small_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_backward_small_witness_bezout_sum)=(pfrep_power_gcd_backward_small_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_backward_small_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_backward_small_witness_bezout_sum_result)=(pfgs_G_gcd_backward_small)) /\ ((((exists ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_backward_small_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_small)) /\ exists ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_backward_small = ff_q_pfp_gcd_backward_small_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_backward_small_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_small) + (pfrep_right_gcd_backward_small_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_small_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_backward_small_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_backward_small)=(pfrep_power_gcd_backward_small_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_backward_small_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_backward_small_witness_bezout_sum_result=pfrep_right_gcd_backward_small_witness_bezout_sum_result))))))))))))))))))))))) -> (exists pfgs_gb_gcd_backward_result pfgs_gc_gcd_backward_result pfgs_G_gcd_backward_result pfgs_ub_gcd_backward_result pfgs_uc_gcd_backward_result pfgs_U_gcd_backward_result pfgs_vb_gcd_backward_result pfgs_vc_gcd_backward_result pfgs_V_gcd_backward_result. (((pfgs_G_gcd_backward_result)=0 \/ (((~((pfgs_G_gcd_backward_result) = 0)) /\ (((forall fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients. (exists fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_index_bound. fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_index_bound + S (fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry. fom_beta_height_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry + S (fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients) = S ((S (fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_normal_moniccoefficients_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_normal_moniccoefficients)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_value_bound. fom_gap_pfp_gcd_backward_result_witness_normal_moniccoefficients_value_bound + S (fom_value_pfp_gcd_backward_result_witness_normal_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_normal_monicleading. ff_h_pfp_gcd_backward_result_witness_normal_monicleading + S (1) = S ((S (0)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_normal_monicleading. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_normal_monicleading * S ((S (0)) * pfgs_gc_gcd_backward_result) + (1))))))))) /\ (((((((forall fom_index_pfp_gcd_backward_result_witness_common_left_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_left_bounded) = L) -> exists fom_value_pfp_gcd_backward_result_witness_common_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_left_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_left_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_common_left_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_bounded_entry. ab = fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_bounded)) * ac) + (fom_value_pfp_gcd_backward_result_witness_common_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_left_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_result_witness_common_left pfgd_qc_gcd_backward_result_witness_common_left pfgd_Q_gcd_backward_result_witness_common_left pfgd_pb_gcd_backward_result_witness_common_left pfgd_pc_gcd_backward_result_witness_common_left pfgd_P_gcd_backward_result_witness_common_left. ((((forall fom_index_pfp_gcd_backward_result_witness_common_left_productleft. (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_left_productleft) = pfgd_Q_gcd_backward_result_witness_common_left) -> exists fom_value_pfp_gcd_backward_result_witness_common_left_productleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_left_productleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_left_productleft_entry + S (fom_value_pfp_gcd_backward_result_witness_common_left_productleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productleft)) * pfgd_qc_gcd_backward_result_witness_common_left)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productleft_entry. pfgd_qb_gcd_backward_result_witness_common_left = fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productleft)) * pfgd_qc_gcd_backward_result_witness_common_left) + (fom_value_pfp_gcd_backward_result_witness_common_left_productleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_left_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_common_left_productright. (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productright_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_left_productright) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_common_left_productright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_left_productright_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_left_productright_entry + S (fom_value_pfp_gcd_backward_result_witness_common_left_productright) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productright)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productright_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_common_left_productright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_left_productright)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_common_left_productright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_left_productright_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_left_productright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_left_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_result_witness_common_left)=0 \/ (pfgs_G_gcd_backward_result)=0) /\ (((pfgd_P_gcd_backward_result_witness_common_left)=0)))) \/ (((~((pfgd_Q_gcd_backward_result_witness_common_left)=0)) /\ (((~((pfgs_G_gcd_backward_result)=0)) /\ (((pfgd_Q_gcd_backward_result_witness_common_left)+(pfgs_G_gcd_backward_result)=S (pfgd_P_gcd_backward_result_witness_common_left)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_common_left_productcoefficients. (exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientsbound. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientsbound + S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients) = (pfgd_P_gcd_backward_result_witness_common_left)) -> exists pfc_value_gcd_backward_result_witness_common_left_productcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry + S (pfc_value_gcd_backward_result_witness_common_left_productcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry. pfgd_pb_gcd_backward_result_witness_common_left = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_left) + (pfc_value_gcd_backward_result_witness_common_left_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_common_left_productcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients))) -> exists pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_common_left_productcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_result_witness_common_left = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_left) + (pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_result_witness_common_left)=(pfc_index_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result) + (pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_result)=(pfc_complement_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_common_left_productcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_common_left_productcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_left_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_common_left_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_common_left_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_common_left_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_common_left_productcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_common_left_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_result_witness_common_left_equivalent pfrep_left_gcd_backward_result_witness_common_left_equivalent pfrep_right_gcd_backward_result_witness_common_left_equivalent. ((exists pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst. ((pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst+S (pfrep_power_gcd_backward_result_witness_common_left_equivalent)=(pfgd_P_gcd_backward_result_witness_common_left)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry. ff_h_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry + S (pfrep_left_gcd_backward_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_left)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry. pfgd_pb_gcd_backward_result_witness_common_left = ff_q_pfp_gcd_backward_result_witness_common_left_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_left) + (pfrep_left_gcd_backward_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_left_equivalentfirstoutside. pfrep_gap_gcd_backward_result_witness_common_left_equivalentfirstoutside+(pfgd_P_gcd_backward_result_witness_common_left)=(pfrep_power_gcd_backward_result_witness_common_left_equivalent)) /\ (((pfrep_left_gcd_backward_result_witness_common_left_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond. ((pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond+S (pfrep_power_gcd_backward_result_witness_common_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry. ff_h_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry + S (pfrep_right_gcd_backward_result_witness_common_left_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond)) * ac)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry. ab = ff_q_pfp_gcd_backward_result_witness_common_left_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_common_left_equivalentsecond)) * ac) + (pfrep_right_gcd_backward_result_witness_common_left_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_left_equivalentsecondoutside. pfrep_gap_gcd_backward_result_witness_common_left_equivalentsecondoutside+(L)=(pfrep_power_gcd_backward_result_witness_common_left_equivalent)) /\ (((pfrep_right_gcd_backward_result_witness_common_left_equivalent)=0))))) -> pfrep_left_gcd_backward_result_witness_common_left_equivalent=pfrep_right_gcd_backward_result_witness_common_left_equivalent))))))) /\ ((((forall fom_index_pfp_gcd_backward_result_witness_common_right_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_right_bounded) = S d) -> exists fom_value_pfp_gcd_backward_result_witness_common_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_right_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_right_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_common_right_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_bounded_entry. bb = fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_bounded)) * bc) + (fom_value_pfp_gcd_backward_result_witness_common_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_right_bounded) = p))) /\ ((exists pfgd_qb_gcd_backward_result_witness_common_right pfgd_qc_gcd_backward_result_witness_common_right pfgd_Q_gcd_backward_result_witness_common_right pfgd_pb_gcd_backward_result_witness_common_right pfgd_pc_gcd_backward_result_witness_common_right pfgd_P_gcd_backward_result_witness_common_right. ((((forall fom_index_pfp_gcd_backward_result_witness_common_right_productleft. (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_right_productleft) = pfgd_Q_gcd_backward_result_witness_common_right) -> exists fom_value_pfp_gcd_backward_result_witness_common_right_productleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_right_productleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_right_productleft_entry + S (fom_value_pfp_gcd_backward_result_witness_common_right_productleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productleft)) * pfgd_qc_gcd_backward_result_witness_common_right)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productleft_entry. pfgd_qb_gcd_backward_result_witness_common_right = fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productleft)) * pfgd_qc_gcd_backward_result_witness_common_right) + (fom_value_pfp_gcd_backward_result_witness_common_right_productleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_right_productleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_common_right_productright. (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productright_index_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_common_right_productright) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_common_right_productright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_common_right_productright_entry. fom_beta_height_pfp_gcd_backward_result_witness_common_right_productright_entry + S (fom_value_pfp_gcd_backward_result_witness_common_right_productright) = S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productright)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productright_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_common_right_productright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_common_right_productright)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_common_right_productright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_common_right_productright_value_bound. fom_gap_pfp_gcd_backward_result_witness_common_right_productright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_common_right_productright) = p))) /\ (((((((pfgd_Q_gcd_backward_result_witness_common_right)=0 \/ (pfgs_G_gcd_backward_result)=0) /\ (((pfgd_P_gcd_backward_result_witness_common_right)=0)))) \/ (((~((pfgd_Q_gcd_backward_result_witness_common_right)=0)) /\ (((~((pfgs_G_gcd_backward_result)=0)) /\ (((pfgd_Q_gcd_backward_result_witness_common_right)+(pfgs_G_gcd_backward_result)=S (pfgd_P_gcd_backward_result_witness_common_right)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_common_right_productcoefficients. (exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientsbound. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientsbound + S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients) = (pfgd_P_gcd_backward_result_witness_common_right)) -> exists pfc_value_gcd_backward_result_witness_common_right_productcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry + S (pfc_value_gcd_backward_result_witness_common_right_productcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry. pfgd_pb_gcd_backward_result_witness_common_right = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) * pfgd_pc_gcd_backward_result_witness_common_right) + (pfc_value_gcd_backward_result_witness_common_right_productcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_common_right_productcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients))) -> exists pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_common_right_productcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal) = (pfgd_Q_gcd_backward_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry. pfgd_qb_gcd_backward_result_witness_common_right = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) * pfgd_qc_gcd_backward_result_witness_common_right) + (pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermleftoutside+(pfgd_Q_gcd_backward_result_witness_common_right)=(pfc_index_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = (pfgs_G_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) * pfgs_gc_gcd_backward_result) + (pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonaltermrightoutside+(pfgs_G_gcd_backward_result)=(pfc_complement_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients))) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_common_right_productcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_common_right_productcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_common_right_productcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_common_right_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_common_right_productcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_common_right_productcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_common_right_productcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_common_right_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_gcd_backward_result_witness_common_right_equivalent pfrep_left_gcd_backward_result_witness_common_right_equivalent pfrep_right_gcd_backward_result_witness_common_right_equivalent. ((exists pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst. ((pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst+S (pfrep_power_gcd_backward_result_witness_common_right_equivalent)=(pfgd_P_gcd_backward_result_witness_common_right)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry. ff_h_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry + S (pfrep_left_gcd_backward_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_right)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry. pfgd_pb_gcd_backward_result_witness_common_right = ff_q_pfp_gcd_backward_result_witness_common_right_equivalentfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentfirst)) * pfgd_pc_gcd_backward_result_witness_common_right) + (pfrep_left_gcd_backward_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_right_equivalentfirstoutside. pfrep_gap_gcd_backward_result_witness_common_right_equivalentfirstoutside+(pfgd_P_gcd_backward_result_witness_common_right)=(pfrep_power_gcd_backward_result_witness_common_right_equivalent)) /\ (((pfrep_left_gcd_backward_result_witness_common_right_equivalent)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond. ((pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond+S (pfrep_power_gcd_backward_result_witness_common_right_equivalent)=(S d)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry. ff_h_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry + S (pfrep_right_gcd_backward_result_witness_common_right_equivalent) = S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond)) * bc)) /\ exists ff_q_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry. bb = ff_q_pfp_gcd_backward_result_witness_common_right_equivalentsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_common_right_equivalentsecond)) * bc) + (pfrep_right_gcd_backward_result_witness_common_right_equivalent)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_common_right_equivalentsecondoutside. pfrep_gap_gcd_backward_result_witness_common_right_equivalentsecondoutside+(S d)=(pfrep_power_gcd_backward_result_witness_common_right_equivalent)) /\ (((pfrep_right_gcd_backward_result_witness_common_right_equivalent)=0))))) -> pfrep_left_gcd_backward_result_witness_common_right_equivalent=pfrep_right_gcd_backward_result_witness_common_right_equivalent)))))))))) /\ ((exists pfgb_pb_gcd_backward_result_witness_bezout pfgb_pc_gcd_backward_result_witness_bezout pfgb_P_gcd_backward_result_witness_bezout pfgb_qb_gcd_backward_result_witness_bezout pfgb_qc_gcd_backward_result_witness_bezout pfgb_Q_gcd_backward_result_witness_bezout. ((((forall fom_index_pfp_gcd_backward_result_witness_bezout_leftleft. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_leftleft) = pfgs_U_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_leftleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftleft_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftleft_entry. pfgs_ub_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftleft)) * pfgs_uc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_bezout_leftleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_leftright. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_leftright) = L) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_leftright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftright_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_leftright_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftright) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftright)) * ac)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftright_entry. ab = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_leftright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_leftright)) * ac) + (fom_value_pfp_gcd_backward_result_witness_bezout_leftright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_leftright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_leftright) = p))) /\ (((((((pfgs_U_gcd_backward_result)=0 \/ (L)=0) /\ (((pfgb_P_gcd_backward_result_witness_bezout)=0)))) \/ (((~((pfgs_U_gcd_backward_result)=0)) /\ (((~((L)=0)) /\ (((pfgs_U_gcd_backward_result)+(L)=S (pfgb_P_gcd_backward_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_bezout_leftcoefficients. (exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientsbound. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientsbound + S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients) = (pfgb_P_gcd_backward_result_witness_bezout)) -> exists pfc_value_gcd_backward_result_witness_bezout_leftcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry + S (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry. pfgb_pb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) * pfgb_pc_gcd_backward_result_witness_bezout) + (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_bezout_leftcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients))) -> exists pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_bezout_leftcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal) = (pfgs_U_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry. pfgs_ub_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) * pfgs_uc_gcd_backward_result) + (pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermleftoutside+(pfgs_U_gcd_backward_result)=(pfc_index_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_bezout_leftcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_bezout_leftcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_bezout_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_bezout_leftcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_bezout_leftcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_bezout_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall fom_index_pfp_gcd_backward_result_witness_bezout_rightleft. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_rightleft) = pfgs_V_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_rightleft. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightleft_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightleft_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightleft) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightleft_entry. pfgs_vb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightleft_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightleft)) * pfgs_vc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_bezout_rightleft))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightleft_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightleft) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_rightright. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_rightright) = S d) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_rightright. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightright_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_rightright_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightright) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightright_entry. bb = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_rightright_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_rightright)) * bc) + (fom_value_pfp_gcd_backward_result_witness_bezout_rightright))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_rightright_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_rightright) = p))) /\ (((((((pfgs_V_gcd_backward_result)=0 \/ (S d)=0) /\ (((pfgb_Q_gcd_backward_result_witness_bezout)=0)))) \/ (((~((pfgs_V_gcd_backward_result)=0)) /\ (((~((S d)=0)) /\ (((pfgs_V_gcd_backward_result)+(S d)=S (pfgb_Q_gcd_backward_result_witness_bezout)))))))) /\ ((forall pfc_index_gcd_backward_result_witness_bezout_rightcoefficients. (exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientsbound. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientsbound + S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients) = (pfgb_Q_gcd_backward_result_witness_bezout)) -> exists pfc_value_gcd_backward_result_witness_bezout_rightcoefficients. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry + S (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients) = S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry. pfgb_qb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientsentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) * pfgb_qc_gcd_backward_result_witness_bezout) + (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients))) /\ ((exists pfc_terms_code_gcd_backward_result_witness_bezout_rightcoefficientscoefficient pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient. ((forall pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal. (exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalbound. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalbound + S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients))) -> exists pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry + S (pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_gcd_backward_result_witness_bezout_rightcoefficientscoefficient = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) + (pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm. (((pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)+pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm=(pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal) = (pfgs_V_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry. pfgs_vb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) * pfgs_vc_gcd_backward_result) + (pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermleftoutside+(pfgs_V_gcd_backward_result)=(pfc_index_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonal)=pfc_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm*pfc_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) = S ((S (S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients))) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient))) /\ forall fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = S (pfc_index_gcd_backward_result_witness_bezout_rightcoefficients)) -> exists fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_gcd_backward_result_witness_bezout_rightcoefficientscoefficient = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) + (fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum = fs_q_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum) + (fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_gcd_backward_result_witness_bezout_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduebound. pfa_gap_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduebound + S (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence pfa_offset_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_gcd_backward_result_witness_bezout_rightcoefficientscoefficient) + (p) * pfa_offset_left_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence = (pfc_value_gcd_backward_result_witness_bezout_rightcoefficients) + (p) * pfa_offset_right_gcd_backward_result_witness_bezout_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((((forall fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded) = pfgb_P_gcd_backward_result_witness_bezout) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry. pfgb_pb_gcd_backward_result_witness_bezout = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_left_bounded)) * pfgb_pc_gcd_backward_result_witness_bezout) + (fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_left_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_left_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded) = pfgb_Q_gcd_backward_result_witness_bezout) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_result_witness_bezout)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry. pfgb_qb_gcd_backward_result_witness_bezout = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_right_bounded)) * pfgb_qc_gcd_backward_result_witness_bezout) + (fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_right_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_right_bounded) = p))) /\ (((forall fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded. (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_index_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_index_bound + S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded) = pfgs_G_gcd_backward_result) -> exists fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded. ((((exists fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry. fom_beta_height_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded) = S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_result)) /\ exists fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry. pfgs_gb_gcd_backward_result = fom_beta_quotient_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_entry * S ((S (fom_index_pfp_gcd_backward_result_witness_bezout_sum_result_bounded)) * pfgs_gc_gcd_backward_result) + (fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded))) /\ (exists fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_value_bound. fom_gap_pfp_gcd_backward_result_witness_bezout_sum_result_bounded_value_bound + S (fom_value_pfp_gcd_backward_result_witness_bezout_sum_result_bounded) = p))) /\ ((exists pfga_ub_gcd_backward_result_witness_bezout_sum pfga_uc_gcd_backward_result_witness_bezout_sum pfga_vb_gcd_backward_result_witness_bezout_sum pfga_vc_gcd_backward_result_witness_bezout_sum pfga_tb_gcd_backward_result_witness_bezout_sum pfga_tc_gcd_backward_result_witness_bezout_sum pfga_K_gcd_backward_result_witness_bezout_sum. ((((forall pfrep_power_gcd_backward_result_witness_bezout_sum_left pfrep_left_gcd_backward_result_witness_bezout_sum_left pfrep_right_gcd_backward_result_witness_bezout_sum_left. ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst. ((pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst+S (pfrep_power_gcd_backward_result_witness_bezout_sum_left)=(pfgb_P_gcd_backward_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry + S (pfrep_left_gcd_backward_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry. pfgb_pb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftfirst)) * pfgb_pc_gcd_backward_result_witness_bezout) + (pfrep_left_gcd_backward_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_leftfirstoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_leftfirstoutside+(pfgb_P_gcd_backward_result_witness_bezout)=(pfrep_power_gcd_backward_result_witness_bezout_sum_left)) /\ (((pfrep_left_gcd_backward_result_witness_bezout_sum_left)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond. ((pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond+S (pfrep_power_gcd_backward_result_witness_bezout_sum_left)=(pfga_K_gcd_backward_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry + S (pfrep_right_gcd_backward_result_witness_bezout_sum_left) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry. pfga_ub_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_leftsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_leftsecond)) * pfga_uc_gcd_backward_result_witness_bezout_sum) + (pfrep_right_gcd_backward_result_witness_bezout_sum_left)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_leftsecondoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_leftsecondoutside+(pfga_K_gcd_backward_result_witness_bezout_sum)=(pfrep_power_gcd_backward_result_witness_bezout_sum_left)) /\ (((pfrep_right_gcd_backward_result_witness_bezout_sum_left)=0))))) -> pfrep_left_gcd_backward_result_witness_bezout_sum_left=pfrep_right_gcd_backward_result_witness_bezout_sum_left) /\ ((forall pfrep_power_gcd_backward_result_witness_bezout_sum_right pfrep_left_gcd_backward_result_witness_bezout_sum_right pfrep_right_gcd_backward_result_witness_bezout_sum_right. ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst. ((pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst+S (pfrep_power_gcd_backward_result_witness_bezout_sum_right)=(pfgb_Q_gcd_backward_result_witness_bezout)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry + S (pfrep_left_gcd_backward_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_result_witness_bezout)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry. pfgb_qb_gcd_backward_result_witness_bezout = ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightfirst)) * pfgb_qc_gcd_backward_result_witness_bezout) + (pfrep_left_gcd_backward_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_rightfirstoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_rightfirstoutside+(pfgb_Q_gcd_backward_result_witness_bezout)=(pfrep_power_gcd_backward_result_witness_bezout_sum_right)) /\ (((pfrep_left_gcd_backward_result_witness_bezout_sum_right)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond. ((pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond+S (pfrep_power_gcd_backward_result_witness_bezout_sum_right)=(pfga_K_gcd_backward_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry + S (pfrep_right_gcd_backward_result_witness_bezout_sum_right) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry. pfga_vb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_rightsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_rightsecond)) * pfga_vc_gcd_backward_result_witness_bezout_sum) + (pfrep_right_gcd_backward_result_witness_bezout_sum_right)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_rightsecondoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_rightsecondoutside+(pfga_K_gcd_backward_result_witness_bezout_sum)=(pfrep_power_gcd_backward_result_witness_bezout_sum_right)) /\ (((pfrep_right_gcd_backward_result_witness_bezout_sum_right)=0))))) -> pfrep_left_gcd_backward_result_witness_bezout_sum_right=pfrep_right_gcd_backward_result_witness_bezout_sum_right)))) /\ (((forall pfp_index_gcd_backward_result_witness_bezout_sum_add. (exists pfa_gap_gcd_backward_result_witness_bezout_sum_addindex. pfa_gap_gcd_backward_result_witness_bezout_sum_addindex + S (pfp_index_gcd_backward_result_witness_bezout_sum_add) = (pfga_K_gcd_backward_result_witness_bezout_sum)) -> exists pfp_left_gcd_backward_result_witness_bezout_sum_add pfp_right_gcd_backward_result_witness_bezout_sum_add pfp_value_gcd_backward_result_witness_bezout_sum_add. ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_addleft. ff_h_pfp_gcd_backward_result_witness_bezout_sum_addleft + S (pfp_left_gcd_backward_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_uc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_addleft. pfga_ub_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_addleft * S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_uc_gcd_backward_result_witness_bezout_sum) + (pfp_left_gcd_backward_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_addright. ff_h_pfp_gcd_backward_result_witness_bezout_sum_addright + S (pfp_right_gcd_backward_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_vc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_addright. pfga_vb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_addright * S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_vc_gcd_backward_result_witness_bezout_sum) + (pfp_right_gcd_backward_result_witness_bezout_sum_add))) /\ (((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_addtarget. ff_h_pfp_gcd_backward_result_witness_bezout_sum_addtarget + S (pfp_value_gcd_backward_result_witness_bezout_sum_add) = S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_tc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_addtarget. pfga_tb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_addtarget * S ((S (pfp_index_gcd_backward_result_witness_bezout_sum_add)) * pfga_tc_gcd_backward_result_witness_bezout_sum) + (pfp_value_gcd_backward_result_witness_bezout_sum_add))) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationleft. pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationleft + S (pfp_left_gcd_backward_result_witness_bezout_sum_add) = (p)) /\ (((exists pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationright. pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationright + S (pfp_right_gcd_backward_result_witness_bezout_sum_add) = (p)) /\ ((((exists pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationresultbound. pfa_gap_gcd_backward_result_witness_bezout_sum_addoperationresultbound + S (pfp_value_gcd_backward_result_witness_bezout_sum_add) = (p)) /\ ((exists pfa_offset_left_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence pfa_offset_right_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence. ((pfp_left_gcd_backward_result_witness_bezout_sum_add) + (pfp_right_gcd_backward_result_witness_bezout_sum_add)) + (p) * pfa_offset_left_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence = (pfp_value_gcd_backward_result_witness_bezout_sum_add) + (p) * pfa_offset_right_gcd_backward_result_witness_bezout_sum_addoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_gcd_backward_result_witness_bezout_sum_result pfrep_left_gcd_backward_result_witness_bezout_sum_result pfrep_right_gcd_backward_result_witness_bezout_sum_result. ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst. ((pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst+S (pfrep_power_gcd_backward_result_witness_bezout_sum_result)=(pfga_K_gcd_backward_result_witness_bezout_sum)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry + S (pfrep_left_gcd_backward_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_result_witness_bezout_sum)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry. pfga_tb_gcd_backward_result_witness_bezout_sum = ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultfirstentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultfirst)) * pfga_tc_gcd_backward_result_witness_bezout_sum) + (pfrep_left_gcd_backward_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_resultfirstoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_resultfirstoutside+(pfga_K_gcd_backward_result_witness_bezout_sum)=(pfrep_power_gcd_backward_result_witness_bezout_sum_result)) /\ (((pfrep_left_gcd_backward_result_witness_bezout_sum_result)=0))))) -> ((exists pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond. ((pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond+S (pfrep_power_gcd_backward_result_witness_bezout_sum_result)=(pfgs_G_gcd_backward_result)) /\ ((((exists ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry. ff_h_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry + S (pfrep_right_gcd_backward_result_witness_bezout_sum_result) = S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_result)) /\ exists ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry. pfgs_gb_gcd_backward_result = ff_q_pfp_gcd_backward_result_witness_bezout_sum_resultsecondentry * S ((S (pfrep_position_gcd_backward_result_witness_bezout_sum_resultsecond)) * pfgs_gc_gcd_backward_result) + (pfrep_right_gcd_backward_result_witness_bezout_sum_result)))))) \/ (((exists pfrep_gap_gcd_backward_result_witness_bezout_sum_resultsecondoutside. pfrep_gap_gcd_backward_result_witness_bezout_sum_resultsecondoutside+(pfgs_G_gcd_backward_result)=(pfrep_power_gcd_backward_result_witness_bezout_sum_result)) /\ (((pfrep_right_gcd_backward_result_witness_bezout_sum_result)=0))))) -> pfrep_left_gcd_backward_result_witness_bezout_sum_result=pfrep_right_gcd_backward_result_witness_bezout_sum_result)))))))))))))))))))))))Complete tactic proof in conservative notation
All 102 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
102 script commands · 20 reading checkpoints · 4 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 (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–13
03Establish hupdateL14–23
Establish this local claim before using it. It is not an additional assumption.
- L14
have hupdate : ∀ gb. ∀ gc. ∀ G. ∀ ub. ∀ uc. ∀ U. ∀ vb. ∀ vc. ∀ V. Prime(p) → FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R) → FpPolynomialBezoutRepresentation(p,bb,bc,S d,rb,rc,R,gb,gc,G,ub,uc,U,vb,vc,V) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. FpPolyProduct(p,vb,vc,V,qb,qc,q,x,y,z) ∧ (FpPolynomialAlignedAdd(p,x,y,z,n,m,k,ub,uc,U) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,S d,gb,gc,G,vb,vc,V,n,m,k))Definitions: Prime(p)FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)FpPolynomialBezoutRepresentation(p,bb,bc,S d,rb,rc,R,gb,gc,G,ub,uc,U,vb,vc,V)FpPolyProduct(p,vb,vc,V,qb,qc,q,x,y,z)FpPolynomialAlignedAdd(p,x,y,z,n,m,k,ub,uc,U)FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,S d,gb,gc,G,vb,vc,V,n,m,k)Original native command in the exact edition - L15
specialize prime_field_polynomial_division_execution_bezout_backward (p) - L16
specialize prime_field_polynomial_division_execution_bezout_backward (ab) - L17
specialize prime_field_polynomial_division_execution_bezout_backward (ac) - L18
specialize prime_field_polynomial_division_execution_bezout_backward (L) - L19
specialize prime_field_polynomial_division_execution_bezout_backward (bb) - L20
specialize prime_field_polynomial_division_execution_bezout_backward (bc) - L21
specialize prime_field_polynomial_division_execution_bezout_backward (d) - L22
specialize prime_field_polynomial_division_execution_bezout_backward (qb) - L23
specialize prime_field_polynomial_division_execution_bezout_backward (qc)
04Use earlier factsL24–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L24
specialize prime_field_polynomial_division_execution_bezout_backward (q) - L25
specialize prime_field_polynomial_division_execution_bezout_backward (rb) - L26
specialize prime_field_polynomial_division_execution_bezout_backward (rc) - L27
specialize prime_field_polynomial_division_execution_bezout_backward (R) - L28
exact prime_field_polynomial_division_execution_bezout_backward
05Fix variables and assumptionsL29–31
06Separate the logical casesL32–41
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
cases hs - L33
cases hs_witness - L34
cases hs_witness_witness - L35
cases hs_witness_witness_witness - L36
cases hs_witness_witness_witness_witness - L37
cases hs_witness_witness_witness_witness_witness - L38
cases hs_witness_witness_witness_witness_witness_witness - L39
cases hs_witness_witness_witness_witness_witness_witness_witness - L40
cases hs_witness_witness_witness_witness_witness_witness_witness_witness - L41
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness
07Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right
08Establish hcL43–43
Establish this local claim before using it. It is not an additional assumption.
- L43
have hc : FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d)Definitions: FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d)Original native command in the exact edition
09Establish hmL44–53
Establish this local claim before using it. It is not an additional assumption.
- L44
have hm : (FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d) → FpPolynomialCommonRightDivisor(p,x,x1,x2,bb,bc,S d,rb,rc,R)) ∧ (FpPolynomialCommonRightDivisor(p,x,x1,x2,bb,bc,S d,rb,rc,R) → FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d))Definitions: FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d)FpPolynomialCommonRightDivisor(p,x,x1,x2,bb,bc,S d,rb,rc,R)Original native command in the exact edition - L45
specialize prime_field_polynomial_division_execution_common_right_divisors (p) - L46
specialize prime_field_polynomial_division_execution_common_right_divisors (ab) - L47
specialize prime_field_polynomial_division_execution_common_right_divisors (ac) - L48
specialize prime_field_polynomial_division_execution_common_right_divisors (L) - L49
specialize prime_field_polynomial_division_execution_common_right_divisors (bb) - L50
specialize prime_field_polynomial_division_execution_common_right_divisors (bc) - L51
specialize prime_field_polynomial_division_execution_common_right_divisors (d) - L52
specialize prime_field_polynomial_division_execution_common_right_divisors (qb) - L53
specialize prime_field_polynomial_division_execution_common_right_divisors (qc)
10Use earlier factsL54–63
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
specialize prime_field_polynomial_division_execution_common_right_divisors (q) - L55
specialize prime_field_polynomial_division_execution_common_right_divisors (rb) - L56
specialize prime_field_polynomial_division_execution_common_right_divisors (rc) - L57
specialize prime_field_polynomial_division_execution_common_right_divisors (R) - L58
specialize prime_field_polynomial_division_execution_common_right_divisors (x) - L59
specialize prime_field_polynomial_division_execution_common_right_divisors (x1) - L60
specialize prime_field_polynomial_division_execution_common_right_divisors (x2) - L61
apply prime_field_polynomial_division_execution_common_right_divisors - L62
exact hp - L63
exact he
11Separate the logical casesL64–64
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L64
cases hm
12Use earlier factsL65–66
13Establish hbL67–76
Establish this local claim before using it. It is not an additional assumption.
- L67Definitions: FpPolyProduct(p,x6,x7,x8,qb,qc,q,pfg_update_wb_gcd_backward_update,pfg_update_wc_gcd_backward_update,pfg_update_W_gcd_backward_update)FpPolynomialAlignedAdd(p,pfg_update_wb_gcd_backward_update,pfg_update_wc_gcd_backward_update,pfg_update_W_gcd_backward_update,pfg_update_tb_gcd_backward_update,pfg_update_tc_gcd_backward_update,pfg_update_T_gcd_backward_update,x3,x4,x5)FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,S d,x,x1,x2,x6,x7,x8,pfg_update_tb_gcd_backward_update,pfg_update_tc_gcd_backward_update,pfg_update_T_gcd_backward_update)Original native command in the exact edition
have hb · expand full local formula (779 characters)
have hb : ∃ pfg_update_wb_gcd_backward_update. ∃ pfg_update_wc_gcd_backward_update. ∃ pfg_update_W_gcd_backward_update. ∃ pfg_update_tb_gcd_backward_update. ∃ pfg_update_tc_gcd_backward_update. ∃ pfg_update_T_gcd_backward_update. FpPolyProduct(p,x6,x7,x8,qb,qc,q,pfg_update_wb_gcd_backward_update,pfg_update_wc_gcd_backward_update,pfg_update_W_gcd_backward_update) ∧ (FpPolynomialAlignedAdd(p,pfg_update_wb_gcd_backward_update,pfg_update_wc_gcd_backward_update,pfg_update_W_gcd_backward_update,pfg_update_tb_gcd_backward_update,pfg_update_tc_gcd_backward_update,pfg_update_T_gcd_backward_update,x3,x4,x5) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,S d,x,x1,x2,x6,x7,x8,pfg_update_tb_gcd_backward_update,pfg_update_tc_gcd_backward_update,pfg_update_T_gcd_backward_update)) - L68
specialize hupdate (x) - L69
specialize hupdate (x1) - L70
specialize hupdate (x2) - L71
specialize hupdate (x3) - L72
specialize hupdate (x4) - L73
specialize hupdate (x5) - L74
specialize hupdate (x6) - L75
specialize hupdate (x7) - L76
specialize hupdate (x8)
14Use earlier factsL77–80
15Separate the logical casesL81–88
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L81
cases hb - L82
cases hb_witness - L83
cases hb_witness_witness - L84
cases hb_witness_witness_witness - L85
cases hb_witness_witness_witness_witness - L86
cases hb_witness_witness_witness_witness_witness - L87
cases hb_witness_witness_witness_witness_witness_witness - L88
cases hb_witness_witness_witness_witness_witness_witness_right
16Construct an explicit witnessL89–97
17Separate the logical casesL98–98
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L98
split
18Use earlier factsL99–99
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L99
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_left
19Separate the logical casesL100–100
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L100
split
Original defined command ledger · 102 lines
- 0001
intro p - 0002
intro ab - 0003
intro ac - 0004
intro L - 0005
intro bb - 0006
intro bc - 0007
intro d - 0008
intro qb - 0009
intro qc - 0010
intro q - 0011
intro rb - 0012
intro rc - 0013
intro R - 0014
have hupdate : ∀ gb. ∀ gc. ∀ G. ∀ ub. ∀ uc. ∀ U. ∀ vb. ∀ vc. ∀ V. Prime(p) → FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R) → FpPolynomialBezoutRepresentation(p,bb,bc,S d,rb,rc,R,gb,gc,G,ub,uc,U,vb,vc,V) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. FpPolyProduct(p,vb,vc,V,qb,qc,q,x,y,z) ∧ (FpPolynomialAlignedAdd(p,x,y,z,n,m,k,ub,uc,U) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,S d,gb,gc,G,vb,vc,V,n,m,k)) - 0015
specialize prime_field_polynomial_division_execution_bezout_backward (p) - 0016
specialize prime_field_polynomial_division_execution_bezout_backward (ab) - 0017
specialize prime_field_polynomial_division_execution_bezout_backward (ac) - 0018
specialize prime_field_polynomial_division_execution_bezout_backward (L) - 0019
specialize prime_field_polynomial_division_execution_bezout_backward (bb) - 0020
specialize prime_field_polynomial_division_execution_bezout_backward (bc) - 0021
specialize prime_field_polynomial_division_execution_bezout_backward (d) - 0022
specialize prime_field_polynomial_division_execution_bezout_backward (qb) - 0023
specialize prime_field_polynomial_division_execution_bezout_backward (qc) - 0024
specialize prime_field_polynomial_division_execution_bezout_backward (q) - 0025
specialize prime_field_polynomial_division_execution_bezout_backward (rb) - 0026
specialize prime_field_polynomial_division_execution_bezout_backward (rc) - 0027
specialize prime_field_polynomial_division_execution_bezout_backward (R) - 0028
exact prime_field_polynomial_division_execution_bezout_backward - 0029
intro hp - 0030
intro he - 0031
intro hs - 0032
cases hs - 0033
cases hs_witness - 0034
cases hs_witness_witness - 0035
cases hs_witness_witness_witness - 0036
cases hs_witness_witness_witness_witness - 0037
cases hs_witness_witness_witness_witness_witness - 0038
cases hs_witness_witness_witness_witness_witness_witness - 0039
cases hs_witness_witness_witness_witness_witness_witness_witness - 0040
cases hs_witness_witness_witness_witness_witness_witness_witness_witness - 0041
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness - 0042
cases hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right - 0043
have hc : FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d) - 0044
have hm : (FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d) → FpPolynomialCommonRightDivisor(p,x,x1,x2,bb,bc,S d,rb,rc,R)) ∧ (FpPolynomialCommonRightDivisor(p,x,x1,x2,bb,bc,S d,rb,rc,R) → FpPolynomialCommonRightDivisor(p,x,x1,x2,ab,ac,L,bb,bc,S d)) - 0045
specialize prime_field_polynomial_division_execution_common_right_divisors (p) - 0046
specialize prime_field_polynomial_division_execution_common_right_divisors (ab) - 0047
specialize prime_field_polynomial_division_execution_common_right_divisors (ac) - 0048
specialize prime_field_polynomial_division_execution_common_right_divisors (L) - 0049
specialize prime_field_polynomial_division_execution_common_right_divisors (bb) - 0050
specialize prime_field_polynomial_division_execution_common_right_divisors (bc) - 0051
specialize prime_field_polynomial_division_execution_common_right_divisors (d) - 0052
specialize prime_field_polynomial_division_execution_common_right_divisors (qb) - 0053
specialize prime_field_polynomial_division_execution_common_right_divisors (qc) - 0054
specialize prime_field_polynomial_division_execution_common_right_divisors (q) - 0055
specialize prime_field_polynomial_division_execution_common_right_divisors (rb) - 0056
specialize prime_field_polynomial_division_execution_common_right_divisors (rc) - 0057
specialize prime_field_polynomial_division_execution_common_right_divisors (R) - 0058
specialize prime_field_polynomial_division_execution_common_right_divisors (x) - 0059
specialize prime_field_polynomial_division_execution_common_right_divisors (x1) - 0060
specialize prime_field_polynomial_division_execution_common_right_divisors (x2) - 0061
apply prime_field_polynomial_division_execution_common_right_divisors - 0062
exact hp - 0063
exact he - 0064
cases hm - 0065
apply hm_right - 0066
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left - 0067
have hb : ∃ pfg_update_wb_gcd_backward_update. ∃ pfg_update_wc_gcd_backward_update. ∃ pfg_update_W_gcd_backward_update. ∃ pfg_update_tb_gcd_backward_update. ∃ pfg_update_tc_gcd_backward_update. ∃ pfg_update_T_gcd_backward_update. FpPolyProduct(p,x6,x7,x8,qb,qc,q,pfg_update_wb_gcd_backward_update,pfg_update_wc_gcd_backward_update,pfg_update_W_gcd_backward_update) ∧ (FpPolynomialAlignedAdd(p,pfg_update_wb_gcd_backward_update,pfg_update_wc_gcd_backward_update,pfg_update_W_gcd_backward_update,pfg_update_tb_gcd_backward_update,pfg_update_tc_gcd_backward_update,pfg_update_T_gcd_backward_update,x3,x4,x5) ∧ FpPolynomialBezoutRepresentation(p,ab,ac,L,bb,bc,S d,x,x1,x2,x6,x7,x8,pfg_update_tb_gcd_backward_update,pfg_update_tc_gcd_backward_update,pfg_update_T_gcd_backward_update)) - 0068
specialize hupdate (x) - 0069
specialize hupdate (x1) - 0070
specialize hupdate (x2) - 0071
specialize hupdate (x3) - 0072
specialize hupdate (x4) - 0073
specialize hupdate (x5) - 0074
specialize hupdate (x6) - 0075
specialize hupdate (x7) - 0076
specialize hupdate (x8) - 0077
apply hupdate - 0078
exact hp - 0079
exact he - 0080
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right - 0081
cases hb - 0082
cases hb_witness - 0083
cases hb_witness_witness - 0084
cases hb_witness_witness_witness - 0085
cases hb_witness_witness_witness_witness - 0086
cases hb_witness_witness_witness_witness_witness - 0087
cases hb_witness_witness_witness_witness_witness_witness - 0088
cases hb_witness_witness_witness_witness_witness_witness_right - 0089
exists x - 0090
exists x1 - 0091
exists x2 - 0092
exists x6 - 0093
exists x7 - 0094
exists x8 - 0095
exists x12 - 0096
exists x13 - 0097
exists x14 - 0098
split - 0099
exact hs_witness_witness_witness_witness_witness_witness_witness_witness_witness_left - 0100
split - 0101
exact hc - 0102
exact hb_witness_witness_witness_witness_witness_witness_right_right