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. ∀ M. ∀ qb. ∀ qc. ∀ QB. ∀ QC. ∀ i. ∀ q. ∀ r. BetaPrefixEqual(qb,qc,QB,QC,i) → FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q) → FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,QB,QC,i,r) → q = r
Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
BetaPrefixEqual(b,c,d,e,l) · 1FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q) · 2
Actual proof prerequisites
Original expanded first-order statement
forall p k ab ac bb bc M qb qc QB QC i q r. (forall mdr_i_pfp_step_unique_prefix mdr_a_pfp_step_unique_prefix. (exists mdr_gap_pfp_step_unique_prefixb. mdr_gap_pfp_step_unique_prefixb + S (mdr_i_pfp_step_unique_prefix) = (i)) -> (((exists ff_h_mdr_pfp_step_unique_prefixo. ff_h_mdr_pfp_step_unique_prefixo + S (mdr_a_pfp_step_unique_prefix) = S ((S (mdr_i_pfp_step_unique_prefix)) * qc)) /\ exists ff_q_mdr_pfp_step_unique_prefixo. qb = ff_q_mdr_pfp_step_unique_prefixo * S ((S (mdr_i_pfp_step_unique_prefix)) * qc) + (mdr_a_pfp_step_unique_prefix))) -> (((exists ff_h_mdr_pfp_step_unique_prefixn. ff_h_mdr_pfp_step_unique_prefixn + S (mdr_a_pfp_step_unique_prefix) = S ((S (mdr_i_pfp_step_unique_prefix)) * QC)) /\ exists ff_q_mdr_pfp_step_unique_prefixn. QB = ff_q_mdr_pfp_step_unique_prefixn * S ((S (mdr_i_pfp_step_unique_prefix)) * QC) + (mdr_a_pfp_step_unique_prefix)))) -> (exists pfd_input_step_unique_old pfd_previous_step_unique_old pfd_difference_step_unique_old. ((((exists ff_h_pfp_step_unique_oldinput. ff_h_pfp_step_unique_oldinput + S (pfd_input_step_unique_old) = S ((S (i)) * ac)) /\ exists ff_q_pfp_step_unique_oldinput. ab = ff_q_pfp_step_unique_oldinput * S ((S (i)) * ac) + (pfd_input_step_unique_old))) /\ (((exists pfc_terms_code_step_unique_oldprevious pfc_terms_scale_step_unique_oldprevious pfc_natural_sum_step_unique_oldprevious. ((forall pfc_index_step_unique_oldpreviousdiagonal. (exists pfa_gap_step_unique_oldpreviousdiagonalbound. pfa_gap_step_unique_oldpreviousdiagonalbound + S (pfc_index_step_unique_oldpreviousdiagonal) = (S (i))) -> exists pfc_value_step_unique_oldpreviousdiagonal. ((((exists ff_h_pfp_step_unique_oldpreviousdiagonalentry. ff_h_pfp_step_unique_oldpreviousdiagonalentry + S (pfc_value_step_unique_oldpreviousdiagonal) = S ((S (pfc_index_step_unique_oldpreviousdiagonal)) * pfc_terms_scale_step_unique_oldprevious)) /\ exists ff_q_pfp_step_unique_oldpreviousdiagonalentry. pfc_terms_code_step_unique_oldprevious = ff_q_pfp_step_unique_oldpreviousdiagonalentry * S ((S (pfc_index_step_unique_oldpreviousdiagonal)) * pfc_terms_scale_step_unique_oldprevious) + (pfc_value_step_unique_oldpreviousdiagonal))) /\ ((exists pfc_complement_step_unique_oldpreviousdiagonalterm pfc_left_step_unique_oldpreviousdiagonalterm pfc_right_step_unique_oldpreviousdiagonalterm. (((pfc_index_step_unique_oldpreviousdiagonal)+pfc_complement_step_unique_oldpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_step_unique_oldpreviousdiagonaltermleftinside. pfa_gap_step_unique_oldpreviousdiagonaltermleftinside + S (pfc_index_step_unique_oldpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_step_unique_oldpreviousdiagonaltermleftentry. ff_h_pfp_step_unique_oldpreviousdiagonaltermleftentry + S (pfc_left_step_unique_oldpreviousdiagonalterm) = S ((S (pfc_index_step_unique_oldpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_step_unique_oldpreviousdiagonaltermleftentry. qb = ff_q_pfp_step_unique_oldpreviousdiagonaltermleftentry * S ((S (pfc_index_step_unique_oldpreviousdiagonal)) * qc) + (pfc_left_step_unique_oldpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_oldpreviousdiagonaltermleftoutside. pfc_gap_step_unique_oldpreviousdiagonaltermleftoutside+(i)=(pfc_index_step_unique_oldpreviousdiagonal)) /\ (((pfc_left_step_unique_oldpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_unique_oldpreviousdiagonaltermrightinside. pfa_gap_step_unique_oldpreviousdiagonaltermrightinside + S (pfc_complement_step_unique_oldpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_step_unique_oldpreviousdiagonaltermrightentry. ff_h_pfp_step_unique_oldpreviousdiagonaltermrightentry + S (pfc_right_step_unique_oldpreviousdiagonalterm) = S ((S (pfc_complement_step_unique_oldpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_step_unique_oldpreviousdiagonaltermrightentry. bb = ff_q_pfp_step_unique_oldpreviousdiagonaltermrightentry * S ((S (pfc_complement_step_unique_oldpreviousdiagonalterm)) * bc) + (pfc_right_step_unique_oldpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_oldpreviousdiagonaltermrightoutside. pfc_gap_step_unique_oldpreviousdiagonaltermrightoutside+(M)=(pfc_complement_step_unique_oldpreviousdiagonalterm)) /\ (((pfc_right_step_unique_oldpreviousdiagonalterm)=0))))) /\ (((pfc_value_step_unique_oldpreviousdiagonal)=pfc_left_step_unique_oldpreviousdiagonalterm*pfc_right_step_unique_oldpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_unique_oldprevioussum fs_v_pfc_step_unique_oldprevioussum. ((((exists fs_h_pfc_step_unique_oldprevioussum_body_start. fs_h_pfc_step_unique_oldprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_unique_oldprevioussum)) /\ exists fs_q_pfc_step_unique_oldprevioussum_body_start. fs_u_pfc_step_unique_oldprevioussum = fs_q_pfc_step_unique_oldprevioussum_body_start * S ((S (0)) * fs_v_pfc_step_unique_oldprevioussum) + (0))) /\ ((((exists fs_h_pfc_step_unique_oldprevioussum_body_terminal. fs_h_pfc_step_unique_oldprevioussum_body_terminal + S (pfc_natural_sum_step_unique_oldprevious) = S ((S (S (i))) * fs_v_pfc_step_unique_oldprevioussum)) /\ exists fs_q_pfc_step_unique_oldprevioussum_body_terminal. fs_u_pfc_step_unique_oldprevioussum = fs_q_pfc_step_unique_oldprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_step_unique_oldprevioussum) + (pfc_natural_sum_step_unique_oldprevious))) /\ forall fs_i_pfc_step_unique_oldprevioussum_body_steps. (exists fs_lt_pfc_step_unique_oldprevioussum_body_steps_bound. fs_lt_pfc_step_unique_oldprevioussum_body_steps_bound + S fs_i_pfc_step_unique_oldprevioussum_body_steps = S (i)) -> exists fs_a_pfc_step_unique_oldprevioussum_body_steps fs_r_pfc_step_unique_oldprevioussum_body_steps fs_s_pfc_step_unique_oldprevioussum_body_steps. ((((exists fs_h_pfc_step_unique_oldprevioussum_body_steps_summand. fs_h_pfc_step_unique_oldprevioussum_body_steps_summand + S (fs_a_pfc_step_unique_oldprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_oldprevioussum_body_steps)) * pfc_terms_scale_step_unique_oldprevious)) /\ exists fs_q_pfc_step_unique_oldprevioussum_body_steps_summand. pfc_terms_code_step_unique_oldprevious = fs_q_pfc_step_unique_oldprevioussum_body_steps_summand * S ((S (fs_i_pfc_step_unique_oldprevioussum_body_steps)) * pfc_terms_scale_step_unique_oldprevious) + (fs_a_pfc_step_unique_oldprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_oldprevioussum_body_steps_partial. fs_h_pfc_step_unique_oldprevioussum_body_steps_partial + S (fs_r_pfc_step_unique_oldprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_oldprevioussum_body_steps)) * fs_v_pfc_step_unique_oldprevioussum)) /\ exists fs_q_pfc_step_unique_oldprevioussum_body_steps_partial. fs_u_pfc_step_unique_oldprevioussum = fs_q_pfc_step_unique_oldprevioussum_body_steps_partial * S ((S (fs_i_pfc_step_unique_oldprevioussum_body_steps)) * fs_v_pfc_step_unique_oldprevioussum) + (fs_r_pfc_step_unique_oldprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_oldprevioussum_body_steps_successor. fs_h_pfc_step_unique_oldprevioussum_body_steps_successor + S (fs_s_pfc_step_unique_oldprevioussum_body_steps) = S ((S (S fs_i_pfc_step_unique_oldprevioussum_body_steps)) * fs_v_pfc_step_unique_oldprevioussum)) /\ exists fs_q_pfc_step_unique_oldprevioussum_body_steps_successor. fs_u_pfc_step_unique_oldprevioussum = fs_q_pfc_step_unique_oldprevioussum_body_steps_successor * S ((S (S fs_i_pfc_step_unique_oldprevioussum_body_steps)) * fs_v_pfc_step_unique_oldprevioussum) + (fs_s_pfc_step_unique_oldprevioussum_body_steps))) /\ fs_s_pfc_step_unique_oldprevioussum_body_steps = fs_r_pfc_step_unique_oldprevioussum_body_steps + fs_a_pfc_step_unique_oldprevioussum_body_steps)))))) /\ ((((exists pfa_gap_step_unique_oldpreviousresiduebound. pfa_gap_step_unique_oldpreviousresiduebound + S (pfd_previous_step_unique_old) = (p)) /\ ((exists pfa_offset_left_step_unique_oldpreviousresiduecongruence pfa_offset_right_step_unique_oldpreviousresiduecongruence. (pfc_natural_sum_step_unique_oldprevious) + (p) * pfa_offset_left_step_unique_oldpreviousresiduecongruence = (pfd_previous_step_unique_old) + (p) * pfa_offset_right_step_unique_oldpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_step_unique_oldsubtractleft. pfa_gap_step_unique_oldsubtractleft + S (pfd_previous_step_unique_old) = (p)) /\ (((exists pfa_gap_step_unique_oldsubtractright. pfa_gap_step_unique_oldsubtractright + S (pfd_difference_step_unique_old) = (p)) /\ ((((exists pfa_gap_step_unique_oldsubtractresultbound. pfa_gap_step_unique_oldsubtractresultbound + S (pfd_input_step_unique_old) = (p)) /\ ((exists pfa_offset_left_step_unique_oldsubtractresultcongruence pfa_offset_right_step_unique_oldsubtractresultcongruence. ((pfd_previous_step_unique_old) + (pfd_difference_step_unique_old)) + (p) * pfa_offset_left_step_unique_oldsubtractresultcongruence = (pfd_input_step_unique_old) + (p) * pfa_offset_right_step_unique_oldsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_step_unique_oldmultiplyleft. pfa_gap_step_unique_oldmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_step_unique_oldmultiplyright. pfa_gap_step_unique_oldmultiplyright + S (pfd_difference_step_unique_old) = (p)) /\ ((((exists pfa_gap_step_unique_oldmultiplyresultbound. pfa_gap_step_unique_oldmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_step_unique_oldmultiplyresultcongruence pfa_offset_right_step_unique_oldmultiplyresultcongruence. ((k) * (pfd_difference_step_unique_old)) + (p) * pfa_offset_left_step_unique_oldmultiplyresultcongruence = (q) + (p) * pfa_offset_right_step_unique_oldmultiplyresultcongruence)))))))))))))))) -> (exists pfd_input_step_unique_new pfd_previous_step_unique_new pfd_difference_step_unique_new. ((((exists ff_h_pfp_step_unique_newinput. ff_h_pfp_step_unique_newinput + S (pfd_input_step_unique_new) = S ((S (i)) * ac)) /\ exists ff_q_pfp_step_unique_newinput. ab = ff_q_pfp_step_unique_newinput * S ((S (i)) * ac) + (pfd_input_step_unique_new))) /\ (((exists pfc_terms_code_step_unique_newprevious pfc_terms_scale_step_unique_newprevious pfc_natural_sum_step_unique_newprevious. ((forall pfc_index_step_unique_newpreviousdiagonal. (exists pfa_gap_step_unique_newpreviousdiagonalbound. pfa_gap_step_unique_newpreviousdiagonalbound + S (pfc_index_step_unique_newpreviousdiagonal) = (S (i))) -> exists pfc_value_step_unique_newpreviousdiagonal. ((((exists ff_h_pfp_step_unique_newpreviousdiagonalentry. ff_h_pfp_step_unique_newpreviousdiagonalentry + S (pfc_value_step_unique_newpreviousdiagonal) = S ((S (pfc_index_step_unique_newpreviousdiagonal)) * pfc_terms_scale_step_unique_newprevious)) /\ exists ff_q_pfp_step_unique_newpreviousdiagonalentry. pfc_terms_code_step_unique_newprevious = ff_q_pfp_step_unique_newpreviousdiagonalentry * S ((S (pfc_index_step_unique_newpreviousdiagonal)) * pfc_terms_scale_step_unique_newprevious) + (pfc_value_step_unique_newpreviousdiagonal))) /\ ((exists pfc_complement_step_unique_newpreviousdiagonalterm pfc_left_step_unique_newpreviousdiagonalterm pfc_right_step_unique_newpreviousdiagonalterm. (((pfc_index_step_unique_newpreviousdiagonal)+pfc_complement_step_unique_newpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_step_unique_newpreviousdiagonaltermleftinside. pfa_gap_step_unique_newpreviousdiagonaltermleftinside + S (pfc_index_step_unique_newpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_step_unique_newpreviousdiagonaltermleftentry. ff_h_pfp_step_unique_newpreviousdiagonaltermleftentry + S (pfc_left_step_unique_newpreviousdiagonalterm) = S ((S (pfc_index_step_unique_newpreviousdiagonal)) * QC)) /\ exists ff_q_pfp_step_unique_newpreviousdiagonaltermleftentry. QB = ff_q_pfp_step_unique_newpreviousdiagonaltermleftentry * S ((S (pfc_index_step_unique_newpreviousdiagonal)) * QC) + (pfc_left_step_unique_newpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_newpreviousdiagonaltermleftoutside. pfc_gap_step_unique_newpreviousdiagonaltermleftoutside+(i)=(pfc_index_step_unique_newpreviousdiagonal)) /\ (((pfc_left_step_unique_newpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_step_unique_newpreviousdiagonaltermrightinside. pfa_gap_step_unique_newpreviousdiagonaltermrightinside + S (pfc_complement_step_unique_newpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_step_unique_newpreviousdiagonaltermrightentry. ff_h_pfp_step_unique_newpreviousdiagonaltermrightentry + S (pfc_right_step_unique_newpreviousdiagonalterm) = S ((S (pfc_complement_step_unique_newpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_step_unique_newpreviousdiagonaltermrightentry. bb = ff_q_pfp_step_unique_newpreviousdiagonaltermrightentry * S ((S (pfc_complement_step_unique_newpreviousdiagonalterm)) * bc) + (pfc_right_step_unique_newpreviousdiagonalterm)))))) \/ (((exists pfc_gap_step_unique_newpreviousdiagonaltermrightoutside. pfc_gap_step_unique_newpreviousdiagonaltermrightoutside+(M)=(pfc_complement_step_unique_newpreviousdiagonalterm)) /\ (((pfc_right_step_unique_newpreviousdiagonalterm)=0))))) /\ (((pfc_value_step_unique_newpreviousdiagonal)=pfc_left_step_unique_newpreviousdiagonalterm*pfc_right_step_unique_newpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_step_unique_newprevioussum fs_v_pfc_step_unique_newprevioussum. ((((exists fs_h_pfc_step_unique_newprevioussum_body_start. fs_h_pfc_step_unique_newprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_step_unique_newprevioussum)) /\ exists fs_q_pfc_step_unique_newprevioussum_body_start. fs_u_pfc_step_unique_newprevioussum = fs_q_pfc_step_unique_newprevioussum_body_start * S ((S (0)) * fs_v_pfc_step_unique_newprevioussum) + (0))) /\ ((((exists fs_h_pfc_step_unique_newprevioussum_body_terminal. fs_h_pfc_step_unique_newprevioussum_body_terminal + S (pfc_natural_sum_step_unique_newprevious) = S ((S (S (i))) * fs_v_pfc_step_unique_newprevioussum)) /\ exists fs_q_pfc_step_unique_newprevioussum_body_terminal. fs_u_pfc_step_unique_newprevioussum = fs_q_pfc_step_unique_newprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_step_unique_newprevioussum) + (pfc_natural_sum_step_unique_newprevious))) /\ forall fs_i_pfc_step_unique_newprevioussum_body_steps. (exists fs_lt_pfc_step_unique_newprevioussum_body_steps_bound. fs_lt_pfc_step_unique_newprevioussum_body_steps_bound + S fs_i_pfc_step_unique_newprevioussum_body_steps = S (i)) -> exists fs_a_pfc_step_unique_newprevioussum_body_steps fs_r_pfc_step_unique_newprevioussum_body_steps fs_s_pfc_step_unique_newprevioussum_body_steps. ((((exists fs_h_pfc_step_unique_newprevioussum_body_steps_summand. fs_h_pfc_step_unique_newprevioussum_body_steps_summand + S (fs_a_pfc_step_unique_newprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_newprevioussum_body_steps)) * pfc_terms_scale_step_unique_newprevious)) /\ exists fs_q_pfc_step_unique_newprevioussum_body_steps_summand. pfc_terms_code_step_unique_newprevious = fs_q_pfc_step_unique_newprevioussum_body_steps_summand * S ((S (fs_i_pfc_step_unique_newprevioussum_body_steps)) * pfc_terms_scale_step_unique_newprevious) + (fs_a_pfc_step_unique_newprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_newprevioussum_body_steps_partial. fs_h_pfc_step_unique_newprevioussum_body_steps_partial + S (fs_r_pfc_step_unique_newprevioussum_body_steps) = S ((S (fs_i_pfc_step_unique_newprevioussum_body_steps)) * fs_v_pfc_step_unique_newprevioussum)) /\ exists fs_q_pfc_step_unique_newprevioussum_body_steps_partial. fs_u_pfc_step_unique_newprevioussum = fs_q_pfc_step_unique_newprevioussum_body_steps_partial * S ((S (fs_i_pfc_step_unique_newprevioussum_body_steps)) * fs_v_pfc_step_unique_newprevioussum) + (fs_r_pfc_step_unique_newprevioussum_body_steps))) /\ ((((exists fs_h_pfc_step_unique_newprevioussum_body_steps_successor. fs_h_pfc_step_unique_newprevioussum_body_steps_successor + S (fs_s_pfc_step_unique_newprevioussum_body_steps) = S ((S (S fs_i_pfc_step_unique_newprevioussum_body_steps)) * fs_v_pfc_step_unique_newprevioussum)) /\ exists fs_q_pfc_step_unique_newprevioussum_body_steps_successor. fs_u_pfc_step_unique_newprevioussum = fs_q_pfc_step_unique_newprevioussum_body_steps_successor * S ((S (S fs_i_pfc_step_unique_newprevioussum_body_steps)) * fs_v_pfc_step_unique_newprevioussum) + (fs_s_pfc_step_unique_newprevioussum_body_steps))) /\ fs_s_pfc_step_unique_newprevioussum_body_steps = fs_r_pfc_step_unique_newprevioussum_body_steps + fs_a_pfc_step_unique_newprevioussum_body_steps)))))) /\ ((((exists pfa_gap_step_unique_newpreviousresiduebound. pfa_gap_step_unique_newpreviousresiduebound + S (pfd_previous_step_unique_new) = (p)) /\ ((exists pfa_offset_left_step_unique_newpreviousresiduecongruence pfa_offset_right_step_unique_newpreviousresiduecongruence. (pfc_natural_sum_step_unique_newprevious) + (p) * pfa_offset_left_step_unique_newpreviousresiduecongruence = (pfd_previous_step_unique_new) + (p) * pfa_offset_right_step_unique_newpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_step_unique_newsubtractleft. pfa_gap_step_unique_newsubtractleft + S (pfd_previous_step_unique_new) = (p)) /\ (((exists pfa_gap_step_unique_newsubtractright. pfa_gap_step_unique_newsubtractright + S (pfd_difference_step_unique_new) = (p)) /\ ((((exists pfa_gap_step_unique_newsubtractresultbound. pfa_gap_step_unique_newsubtractresultbound + S (pfd_input_step_unique_new) = (p)) /\ ((exists pfa_offset_left_step_unique_newsubtractresultcongruence pfa_offset_right_step_unique_newsubtractresultcongruence. ((pfd_previous_step_unique_new) + (pfd_difference_step_unique_new)) + (p) * pfa_offset_left_step_unique_newsubtractresultcongruence = (pfd_input_step_unique_new) + (p) * pfa_offset_right_step_unique_newsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_step_unique_newmultiplyleft. pfa_gap_step_unique_newmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_step_unique_newmultiplyright. pfa_gap_step_unique_newmultiplyright + S (pfd_difference_step_unique_new) = (p)) /\ ((((exists pfa_gap_step_unique_newmultiplyresultbound. pfa_gap_step_unique_newmultiplyresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_step_unique_newmultiplyresultcongruence pfa_offset_right_step_unique_newmultiplyresultcongruence. ((k) * (pfd_difference_step_unique_new)) + (p) * pfa_offset_left_step_unique_newmultiplyresultcongruence = (r) + (p) * pfa_offset_right_step_unique_newmultiplyresultcongruence)))))))))))))))) -> q=r