Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.
Exact theorem in conservative defined notation
∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ d. ∀ qb. ∀ qc. ∀ N. ∀ b. ∀ pb. ∀ pc. ∀ L. ∀ ub. ∀ uc. Prime(p) → BetaAt(bb,bc,0,b) → FpInv(p,b,k) → FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,S d,qb,qc,N) → Le(N,L) → FpConvolutionPrefix(p,qb,qc,N,bb,bc,S d,pb,pc,L) → FpCoefficientSubtraction(p,ab,ac,pb,pc,ub,uc,L) → Repeat(ub,uc,0,N)
Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
FpInv(p,a,b) · 1FpConvolutionPrefix(p,ab,ac,L,bb,bc,M,cb,cc,l) · 1FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N) · 1Le(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1Repeat(b,c,a,l) · 1
Actual proof prerequisites
Original expanded first-order statement
forall p k ab ac bb bc d qb qc N b pb pc L ub uc. (~((p) = 1) /\ forall pfa_factor_left_division_zero_prime pfa_factor_right_division_zero_prime. (p) = pfa_factor_left_division_zero_prime * pfa_factor_right_division_zero_prime -> pfa_factor_left_division_zero_prime = 1 \/ pfa_factor_right_division_zero_prime = 1) -> (((exists ff_h_pfp_division_zero_head. ff_h_pfp_division_zero_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_zero_head. bb = ff_q_pfp_division_zero_head * S ((S (0)) * bc) + (b))) -> (((~((b) = 0)) /\ ((((exists pfa_gap_division_zero_inversemultiplicationleft. pfa_gap_division_zero_inversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_zero_inversemultiplicationright. pfa_gap_division_zero_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_zero_inversemultiplicationresultbound. pfa_gap_division_zero_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_zero_inversemultiplicationresultcongruence pfa_offset_right_division_zero_inversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_zero_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_zero_inversemultiplicationresultcongruence)))))))))))) -> (forall pfd_index_division_zero_execution. (exists pfa_gap_division_zero_executionbound. pfa_gap_division_zero_executionbound + S (pfd_index_division_zero_execution) = (N)) -> exists pfd_value_division_zero_execution. ((((exists ff_h_pfp_division_zero_executionentry. ff_h_pfp_division_zero_executionentry + S (pfd_value_division_zero_execution) = S ((S (pfd_index_division_zero_execution)) * qc)) /\ exists ff_q_pfp_division_zero_executionentry. qb = ff_q_pfp_division_zero_executionentry * S ((S (pfd_index_division_zero_execution)) * qc) + (pfd_value_division_zero_execution))) /\ ((exists pfd_input_division_zero_executionstep pfd_previous_division_zero_executionstep pfd_difference_division_zero_executionstep. ((((exists ff_h_pfp_division_zero_executionstepinput. ff_h_pfp_division_zero_executionstepinput + S (pfd_input_division_zero_executionstep) = S ((S (pfd_index_division_zero_execution)) * ac)) /\ exists ff_q_pfp_division_zero_executionstepinput. ab = ff_q_pfp_division_zero_executionstepinput * S ((S (pfd_index_division_zero_execution)) * ac) + (pfd_input_division_zero_executionstep))) /\ (((exists pfc_terms_code_division_zero_executionstepprevious pfc_terms_scale_division_zero_executionstepprevious pfc_natural_sum_division_zero_executionstepprevious. ((forall pfc_index_division_zero_executionsteppreviousdiagonal. (exists pfa_gap_division_zero_executionsteppreviousdiagonalbound. pfa_gap_division_zero_executionsteppreviousdiagonalbound + S (pfc_index_division_zero_executionsteppreviousdiagonal) = (S (pfd_index_division_zero_execution))) -> exists pfc_value_division_zero_executionsteppreviousdiagonal. ((((exists ff_h_pfp_division_zero_executionsteppreviousdiagonalentry. ff_h_pfp_division_zero_executionsteppreviousdiagonalentry + S (pfc_value_division_zero_executionsteppreviousdiagonal) = S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * pfc_terms_scale_division_zero_executionstepprevious)) /\ exists ff_q_pfp_division_zero_executionsteppreviousdiagonalentry. pfc_terms_code_division_zero_executionstepprevious = ff_q_pfp_division_zero_executionsteppreviousdiagonalentry * S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * pfc_terms_scale_division_zero_executionstepprevious) + (pfc_value_division_zero_executionsteppreviousdiagonal))) /\ ((exists pfc_complement_division_zero_executionsteppreviousdiagonalterm pfc_left_division_zero_executionsteppreviousdiagonalterm pfc_right_division_zero_executionsteppreviousdiagonalterm. (((pfc_index_division_zero_executionsteppreviousdiagonal)+pfc_complement_division_zero_executionsteppreviousdiagonalterm=(pfd_index_division_zero_execution)) /\ ((((((exists pfa_gap_division_zero_executionsteppreviousdiagonaltermleftinside. pfa_gap_division_zero_executionsteppreviousdiagonaltermleftinside + S (pfc_index_division_zero_executionsteppreviousdiagonal) = (pfd_index_division_zero_execution)) /\ ((((exists ff_h_pfp_division_zero_executionsteppreviousdiagonaltermleftentry. ff_h_pfp_division_zero_executionsteppreviousdiagonaltermleftentry + S (pfc_left_division_zero_executionsteppreviousdiagonalterm) = S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_zero_executionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_zero_executionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_zero_executionsteppreviousdiagonal)) * qc) + (pfc_left_division_zero_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_executionsteppreviousdiagonaltermleftoutside. pfc_gap_division_zero_executionsteppreviousdiagonaltermleftoutside+(pfd_index_division_zero_execution)=(pfc_index_division_zero_executionsteppreviousdiagonal)) /\ (((pfc_left_division_zero_executionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_zero_executionsteppreviousdiagonaltermrightinside. pfa_gap_division_zero_executionsteppreviousdiagonaltermrightinside + S (pfc_complement_division_zero_executionsteppreviousdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_zero_executionsteppreviousdiagonaltermrightentry. ff_h_pfp_division_zero_executionsteppreviousdiagonaltermrightentry + S (pfc_right_division_zero_executionsteppreviousdiagonalterm) = S ((S (pfc_complement_division_zero_executionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_zero_executionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_zero_executionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_zero_executionsteppreviousdiagonalterm)) * bc) + (pfc_right_division_zero_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_executionsteppreviousdiagonaltermrightoutside. pfc_gap_division_zero_executionsteppreviousdiagonaltermrightoutside+(S d)=(pfc_complement_division_zero_executionsteppreviousdiagonalterm)) /\ (((pfc_right_division_zero_executionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_zero_executionsteppreviousdiagonal)=pfc_left_division_zero_executionsteppreviousdiagonalterm*pfc_right_division_zero_executionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_zero_executionstepprevioussum fs_v_pfc_division_zero_executionstepprevioussum. ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_start. fs_h_pfc_division_zero_executionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_start. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_zero_executionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_terminal. fs_h_pfc_division_zero_executionstepprevioussum_body_terminal + S (pfc_natural_sum_division_zero_executionstepprevious) = S ((S (S (pfd_index_division_zero_execution))) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_terminal. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_terminal * S ((S (S (pfd_index_division_zero_execution))) * fs_v_pfc_division_zero_executionstepprevioussum) + (pfc_natural_sum_division_zero_executionstepprevious))) /\ forall fs_i_pfc_division_zero_executionstepprevioussum_body_steps. (exists fs_lt_pfc_division_zero_executionstepprevioussum_body_steps_bound. fs_lt_pfc_division_zero_executionstepprevioussum_body_steps_bound + S fs_i_pfc_division_zero_executionstepprevioussum_body_steps = S (pfd_index_division_zero_execution)) -> exists fs_a_pfc_division_zero_executionstepprevioussum_body_steps fs_r_pfc_division_zero_executionstepprevioussum_body_steps fs_s_pfc_division_zero_executionstepprevioussum_body_steps. ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_steps_summand. fs_h_pfc_division_zero_executionstepprevioussum_body_steps_summand + S (fs_a_pfc_division_zero_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_zero_executionstepprevious)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_steps_summand. pfc_terms_code_division_zero_executionstepprevious = fs_q_pfc_division_zero_executionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_zero_executionstepprevious) + (fs_a_pfc_division_zero_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_steps_partial. fs_h_pfc_division_zero_executionstepprevioussum_body_steps_partial + S (fs_r_pfc_division_zero_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_steps_partial. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum) + (fs_r_pfc_division_zero_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_executionstepprevioussum_body_steps_successor. fs_h_pfc_division_zero_executionstepprevioussum_body_steps_successor + S (fs_s_pfc_division_zero_executionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum)) /\ exists fs_q_pfc_division_zero_executionstepprevioussum_body_steps_successor. fs_u_pfc_division_zero_executionstepprevioussum = fs_q_pfc_division_zero_executionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_zero_executionstepprevioussum_body_steps)) * fs_v_pfc_division_zero_executionstepprevioussum) + (fs_s_pfc_division_zero_executionstepprevioussum_body_steps))) /\ fs_s_pfc_division_zero_executionstepprevioussum_body_steps = fs_r_pfc_division_zero_executionstepprevioussum_body_steps + fs_a_pfc_division_zero_executionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_zero_executionsteppreviousresiduebound. pfa_gap_division_zero_executionsteppreviousresiduebound + S (pfd_previous_division_zero_executionstep) = (p)) /\ ((exists pfa_offset_left_division_zero_executionsteppreviousresiduecongruence pfa_offset_right_division_zero_executionsteppreviousresiduecongruence. (pfc_natural_sum_division_zero_executionstepprevious) + (p) * pfa_offset_left_division_zero_executionsteppreviousresiduecongruence = (pfd_previous_division_zero_executionstep) + (p) * pfa_offset_right_division_zero_executionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_zero_executionstepsubtractleft. pfa_gap_division_zero_executionstepsubtractleft + S (pfd_previous_division_zero_executionstep) = (p)) /\ (((exists pfa_gap_division_zero_executionstepsubtractright. pfa_gap_division_zero_executionstepsubtractright + S (pfd_difference_division_zero_executionstep) = (p)) /\ ((((exists pfa_gap_division_zero_executionstepsubtractresultbound. pfa_gap_division_zero_executionstepsubtractresultbound + S (pfd_input_division_zero_executionstep) = (p)) /\ ((exists pfa_offset_left_division_zero_executionstepsubtractresultcongruence pfa_offset_right_division_zero_executionstepsubtractresultcongruence. ((pfd_previous_division_zero_executionstep) + (pfd_difference_division_zero_executionstep)) + (p) * pfa_offset_left_division_zero_executionstepsubtractresultcongruence = (pfd_input_division_zero_executionstep) + (p) * pfa_offset_right_division_zero_executionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_zero_executionstepmultiplyleft. pfa_gap_division_zero_executionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_zero_executionstepmultiplyright. pfa_gap_division_zero_executionstepmultiplyright + S (pfd_difference_division_zero_executionstep) = (p)) /\ ((((exists pfa_gap_division_zero_executionstepmultiplyresultbound. pfa_gap_division_zero_executionstepmultiplyresultbound + S (pfd_value_division_zero_execution) = (p)) /\ ((exists pfa_offset_left_division_zero_executionstepmultiplyresultcongruence pfa_offset_right_division_zero_executionstepmultiplyresultcongruence. ((k) * (pfd_difference_division_zero_executionstep)) + (p) * pfa_offset_left_division_zero_executionstepmultiplyresultcongruence = (pfd_value_division_zero_execution) + (p) * pfa_offset_right_division_zero_executionstepmultiplyresultcongruence))))))))))))))))))) -> (exists pfc_gap_division_zero_length. pfc_gap_division_zero_length+(N)=(L)) -> (forall pfc_index_division_zero_product. (exists pfa_gap_division_zero_productbound. pfa_gap_division_zero_productbound + S (pfc_index_division_zero_product) = (L)) -> exists pfc_value_division_zero_product. ((((exists ff_h_pfp_division_zero_productentry. ff_h_pfp_division_zero_productentry + S (pfc_value_division_zero_product) = S ((S (pfc_index_division_zero_product)) * pc)) /\ exists ff_q_pfp_division_zero_productentry. pb = ff_q_pfp_division_zero_productentry * S ((S (pfc_index_division_zero_product)) * pc) + (pfc_value_division_zero_product))) /\ ((exists pfc_terms_code_division_zero_productcoefficient pfc_terms_scale_division_zero_productcoefficient pfc_natural_sum_division_zero_productcoefficient. ((forall pfc_index_division_zero_productcoefficientdiagonal. (exists pfa_gap_division_zero_productcoefficientdiagonalbound. pfa_gap_division_zero_productcoefficientdiagonalbound + S (pfc_index_division_zero_productcoefficientdiagonal) = (S (pfc_index_division_zero_product))) -> exists pfc_value_division_zero_productcoefficientdiagonal. ((((exists ff_h_pfp_division_zero_productcoefficientdiagonalentry. ff_h_pfp_division_zero_productcoefficientdiagonalentry + S (pfc_value_division_zero_productcoefficientdiagonal) = S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * pfc_terms_scale_division_zero_productcoefficient)) /\ exists ff_q_pfp_division_zero_productcoefficientdiagonalentry. pfc_terms_code_division_zero_productcoefficient = ff_q_pfp_division_zero_productcoefficientdiagonalentry * S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * pfc_terms_scale_division_zero_productcoefficient) + (pfc_value_division_zero_productcoefficientdiagonal))) /\ ((exists pfc_complement_division_zero_productcoefficientdiagonalterm pfc_left_division_zero_productcoefficientdiagonalterm pfc_right_division_zero_productcoefficientdiagonalterm. (((pfc_index_division_zero_productcoefficientdiagonal)+pfc_complement_division_zero_productcoefficientdiagonalterm=(pfc_index_division_zero_product)) /\ ((((((exists pfa_gap_division_zero_productcoefficientdiagonaltermleftinside. pfa_gap_division_zero_productcoefficientdiagonaltermleftinside + S (pfc_index_division_zero_productcoefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_zero_productcoefficientdiagonaltermleftentry. ff_h_pfp_division_zero_productcoefficientdiagonaltermleftentry + S (pfc_left_division_zero_productcoefficientdiagonalterm) = S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_zero_productcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_zero_productcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_zero_productcoefficientdiagonal)) * qc) + (pfc_left_division_zero_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_productcoefficientdiagonaltermleftoutside. pfc_gap_division_zero_productcoefficientdiagonaltermleftoutside+(N)=(pfc_index_division_zero_productcoefficientdiagonal)) /\ (((pfc_left_division_zero_productcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_zero_productcoefficientdiagonaltermrightinside. pfa_gap_division_zero_productcoefficientdiagonaltermrightinside + S (pfc_complement_division_zero_productcoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_zero_productcoefficientdiagonaltermrightentry. ff_h_pfp_division_zero_productcoefficientdiagonaltermrightentry + S (pfc_right_division_zero_productcoefficientdiagonalterm) = S ((S (pfc_complement_division_zero_productcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_zero_productcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_zero_productcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_zero_productcoefficientdiagonalterm)) * bc) + (pfc_right_division_zero_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_zero_productcoefficientdiagonaltermrightoutside. pfc_gap_division_zero_productcoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_zero_productcoefficientdiagonalterm)) /\ (((pfc_right_division_zero_productcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_zero_productcoefficientdiagonal)=pfc_left_division_zero_productcoefficientdiagonalterm*pfc_right_division_zero_productcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_zero_productcoefficientsum fs_v_pfc_division_zero_productcoefficientsum. ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_start. fs_h_pfc_division_zero_productcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_start. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_zero_productcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_terminal. fs_h_pfc_division_zero_productcoefficientsum_body_terminal + S (pfc_natural_sum_division_zero_productcoefficient) = S ((S (S (pfc_index_division_zero_product))) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_terminal. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_terminal * S ((S (S (pfc_index_division_zero_product))) * fs_v_pfc_division_zero_productcoefficientsum) + (pfc_natural_sum_division_zero_productcoefficient))) /\ forall fs_i_pfc_division_zero_productcoefficientsum_body_steps. (exists fs_lt_pfc_division_zero_productcoefficientsum_body_steps_bound. fs_lt_pfc_division_zero_productcoefficientsum_body_steps_bound + S fs_i_pfc_division_zero_productcoefficientsum_body_steps = S (pfc_index_division_zero_product)) -> exists fs_a_pfc_division_zero_productcoefficientsum_body_steps fs_r_pfc_division_zero_productcoefficientsum_body_steps fs_s_pfc_division_zero_productcoefficientsum_body_steps. ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_steps_summand. fs_h_pfc_division_zero_productcoefficientsum_body_steps_summand + S (fs_a_pfc_division_zero_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * pfc_terms_scale_division_zero_productcoefficient)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_steps_summand. pfc_terms_code_division_zero_productcoefficient = fs_q_pfc_division_zero_productcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * pfc_terms_scale_division_zero_productcoefficient) + (fs_a_pfc_division_zero_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_steps_partial. fs_h_pfc_division_zero_productcoefficientsum_body_steps_partial + S (fs_r_pfc_division_zero_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_steps_partial. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum) + (fs_r_pfc_division_zero_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_zero_productcoefficientsum_body_steps_successor. fs_h_pfc_division_zero_productcoefficientsum_body_steps_successor + S (fs_s_pfc_division_zero_productcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum)) /\ exists fs_q_pfc_division_zero_productcoefficientsum_body_steps_successor. fs_u_pfc_division_zero_productcoefficientsum = fs_q_pfc_division_zero_productcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_zero_productcoefficientsum_body_steps)) * fs_v_pfc_division_zero_productcoefficientsum) + (fs_s_pfc_division_zero_productcoefficientsum_body_steps))) /\ fs_s_pfc_division_zero_productcoefficientsum_body_steps = fs_r_pfc_division_zero_productcoefficientsum_body_steps + fs_a_pfc_division_zero_productcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_zero_productcoefficientresiduebound. pfa_gap_division_zero_productcoefficientresiduebound + S (pfc_value_division_zero_product) = (p)) /\ ((exists pfa_offset_left_division_zero_productcoefficientresiduecongruence pfa_offset_right_division_zero_productcoefficientresiduecongruence. (pfc_natural_sum_division_zero_productcoefficient) + (p) * pfa_offset_left_division_zero_productcoefficientresiduecongruence = (pfc_value_division_zero_product) + (p) * pfa_offset_right_division_zero_productcoefficientresiduecongruence)))))))))))) -> (forall pfs_index_division_zero_subtraction. (exists pfa_gap_division_zero_subtractionindex. pfa_gap_division_zero_subtractionindex + S (pfs_index_division_zero_subtraction) = (L)) -> exists pfs_left_division_zero_subtraction pfs_right_division_zero_subtraction pfs_result_division_zero_subtraction. ((((exists ff_h_pfp_division_zero_subtractionleft. ff_h_pfp_division_zero_subtractionleft + S (pfs_left_division_zero_subtraction) = S ((S (pfs_index_division_zero_subtraction)) * ac)) /\ exists ff_q_pfp_division_zero_subtractionleft. ab = ff_q_pfp_division_zero_subtractionleft * S ((S (pfs_index_division_zero_subtraction)) * ac) + (pfs_left_division_zero_subtraction))) /\ (((((exists ff_h_pfp_division_zero_subtractionright. ff_h_pfp_division_zero_subtractionright + S (pfs_right_division_zero_subtraction) = S ((S (pfs_index_division_zero_subtraction)) * pc)) /\ exists ff_q_pfp_division_zero_subtractionright. pb = ff_q_pfp_division_zero_subtractionright * S ((S (pfs_index_division_zero_subtraction)) * pc) + (pfs_right_division_zero_subtraction))) /\ (((((exists ff_h_pfp_division_zero_subtractionresult. ff_h_pfp_division_zero_subtractionresult + S (pfs_result_division_zero_subtraction) = S ((S (pfs_index_division_zero_subtraction)) * uc)) /\ exists ff_q_pfp_division_zero_subtractionresult. ub = ff_q_pfp_division_zero_subtractionresult * S ((S (pfs_index_division_zero_subtraction)) * uc) + (pfs_result_division_zero_subtraction))) /\ ((((exists pfa_gap_division_zero_subtractionoperationleft. pfa_gap_division_zero_subtractionoperationleft + S (pfs_right_division_zero_subtraction) = (p)) /\ (((exists pfa_gap_division_zero_subtractionoperationright. pfa_gap_division_zero_subtractionoperationright + S (pfs_result_division_zero_subtraction) = (p)) /\ ((((exists pfa_gap_division_zero_subtractionoperationresultbound. pfa_gap_division_zero_subtractionoperationresultbound + S (pfs_left_division_zero_subtraction) = (p)) /\ ((exists pfa_offset_left_division_zero_subtractionoperationresultcongruence pfa_offset_right_division_zero_subtractionoperationresultcongruence. ((pfs_right_division_zero_subtraction) + (pfs_result_division_zero_subtraction)) + (p) * pfa_offset_left_division_zero_subtractionoperationresultcongruence = (pfs_left_division_zero_subtraction) + (p) * pfa_offset_right_division_zero_subtractionoperationresultcongruence)))))))))))))))) -> (forall pfp_repeat_index_division_zero_result. (exists pfa_gap_division_zero_resultindex. pfa_gap_division_zero_resultindex + S (pfp_repeat_index_division_zero_result) = (N)) -> (((exists ff_h_pfp_division_zero_resultentry. ff_h_pfp_division_zero_resultentry + S (0) = S ((S (pfp_repeat_index_division_zero_result)) * uc)) /\ exists ff_q_pfp_division_zero_resultentry. ub = ff_q_pfp_division_zero_resultentry * S ((S (pfp_repeat_index_division_zero_result)) * uc) + (0))))