Every actual bounded decoded quotient value has the exact subtraction-and-inverse-product execution witnesses.
Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable
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.
forall p k ab ac bb bc M qb qc N i q. (forall pfd_index_division_entry_source. (exists pfa_gap_division_entry_sourcebound. pfa_gap_division_entry_sourcebound + S (pfd_index_division_entry_source) = (N)) -> exists pfd_value_division_entry_source. ((((exists ff_h_pfp_division_entry_sourceentry. ff_h_pfp_division_entry_sourceentry + S (pfd_value_division_entry_source) = S ((S (pfd_index_division_entry_source)) * qc)) /\ exists ff_q_pfp_division_entry_sourceentry. qb = ff_q_pfp_division_entry_sourceentry * S ((S (pfd_index_division_entry_source)) * qc) + (pfd_value_division_entry_source))) /\ ((exists pfd_input_division_entry_sourcestep pfd_previous_division_entry_sourcestep pfd_difference_division_entry_sourcestep. ((((exists ff_h_pfp_division_entry_sourcestepinput. ff_h_pfp_division_entry_sourcestepinput + S (pfd_input_division_entry_sourcestep) = S ((S (pfd_index_division_entry_source)) * ac)) /\ exists ff_q_pfp_division_entry_sourcestepinput. ab = ff_q_pfp_division_entry_sourcestepinput * S ((S (pfd_index_division_entry_source)) * ac) + (pfd_input_division_entry_sourcestep))) /\ (((exists pfc_terms_code_division_entry_sourcestepprevious pfc_terms_scale_division_entry_sourcestepprevious pfc_natural_sum_division_entry_sourcestepprevious. ((forall pfc_index_division_entry_sourcesteppreviousdiagonal. (exists pfa_gap_division_entry_sourcesteppreviousdiagonalbound. pfa_gap_division_entry_sourcesteppreviousdiagonalbound + S (pfc_index_division_entry_sourcesteppreviousdiagonal) = (S (pfd_index_division_entry_source))) -> exists pfc_value_division_entry_sourcesteppreviousdiagonal. ((((exists ff_h_pfp_division_entry_sourcesteppreviousdiagonalentry. ff_h_pfp_division_entry_sourcesteppreviousdiagonalentry + S (pfc_value_division_entry_sourcesteppreviousdiagonal) = S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * pfc_terms_scale_division_entry_sourcestepprevious)) /\ exists ff_q_pfp_division_entry_sourcesteppreviousdiagonalentry. pfc_terms_code_division_entry_sourcestepprevious = ff_q_pfp_division_entry_sourcesteppreviousdiagonalentry * S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * pfc_terms_scale_division_entry_sourcestepprevious) + (pfc_value_division_entry_sourcesteppreviousdiagonal))) /\ ((exists pfc_complement_division_entry_sourcesteppreviousdiagonalterm pfc_left_division_entry_sourcesteppreviousdiagonalterm pfc_right_division_entry_sourcesteppreviousdiagonalterm. (((pfc_index_division_entry_sourcesteppreviousdiagonal)+pfc_complement_division_entry_sourcesteppreviousdiagonalterm=(pfd_index_division_entry_source)) /\ ((((((exists pfa_gap_division_entry_sourcesteppreviousdiagonaltermleftinside. pfa_gap_division_entry_sourcesteppreviousdiagonaltermleftinside + S (pfc_index_division_entry_sourcesteppreviousdiagonal) = (pfd_index_division_entry_source)) /\ ((((exists ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry. ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry + S (pfc_left_division_entry_sourcesteppreviousdiagonalterm) = S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_entry_sourcesteppreviousdiagonal)) * qc) + (pfc_left_division_entry_sourcesteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_sourcesteppreviousdiagonaltermleftoutside. pfc_gap_division_entry_sourcesteppreviousdiagonaltermleftoutside+(pfd_index_division_entry_source)=(pfc_index_division_entry_sourcesteppreviousdiagonal)) /\ (((pfc_left_division_entry_sourcesteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_entry_sourcesteppreviousdiagonaltermrightinside. pfa_gap_division_entry_sourcesteppreviousdiagonaltermrightinside + S (pfc_complement_division_entry_sourcesteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry. ff_h_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry + S (pfc_right_division_entry_sourcesteppreviousdiagonalterm) = S ((S (pfc_complement_division_entry_sourcesteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_entry_sourcesteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_entry_sourcesteppreviousdiagonalterm)) * bc) + (pfc_right_division_entry_sourcesteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_sourcesteppreviousdiagonaltermrightoutside. pfc_gap_division_entry_sourcesteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_entry_sourcesteppreviousdiagonalterm)) /\ (((pfc_right_division_entry_sourcesteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_entry_sourcesteppreviousdiagonal)=pfc_left_division_entry_sourcesteppreviousdiagonalterm*pfc_right_division_entry_sourcesteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_entry_sourcestepprevioussum fs_v_pfc_division_entry_sourcestepprevioussum. ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_start. fs_h_pfc_division_entry_sourcestepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_start. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_entry_sourcestepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_terminal. fs_h_pfc_division_entry_sourcestepprevioussum_body_terminal + S (pfc_natural_sum_division_entry_sourcestepprevious) = S ((S (S (pfd_index_division_entry_source))) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_terminal. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_terminal * S ((S (S (pfd_index_division_entry_source))) * fs_v_pfc_division_entry_sourcestepprevioussum) + (pfc_natural_sum_division_entry_sourcestepprevious))) /\ forall fs_i_pfc_division_entry_sourcestepprevioussum_body_steps. (exists fs_lt_pfc_division_entry_sourcestepprevioussum_body_steps_bound. fs_lt_pfc_division_entry_sourcestepprevioussum_body_steps_bound + S fs_i_pfc_division_entry_sourcestepprevioussum_body_steps = S (pfd_index_division_entry_source)) -> exists fs_a_pfc_division_entry_sourcestepprevioussum_body_steps fs_r_pfc_division_entry_sourcestepprevioussum_body_steps fs_s_pfc_division_entry_sourcestepprevioussum_body_steps. ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_summand. fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_summand + S (fs_a_pfc_division_entry_sourcestepprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * pfc_terms_scale_division_entry_sourcestepprevious)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_summand. pfc_terms_code_division_entry_sourcestepprevious = fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * pfc_terms_scale_division_entry_sourcestepprevious) + (fs_a_pfc_division_entry_sourcestepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_partial. fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_partial + S (fs_r_pfc_division_entry_sourcestepprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_partial. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum) + (fs_r_pfc_division_entry_sourcestepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_successor. fs_h_pfc_division_entry_sourcestepprevioussum_body_steps_successor + S (fs_s_pfc_division_entry_sourcestepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum)) /\ exists fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_successor. fs_u_pfc_division_entry_sourcestepprevioussum = fs_q_pfc_division_entry_sourcestepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_entry_sourcestepprevioussum_body_steps)) * fs_v_pfc_division_entry_sourcestepprevioussum) + (fs_s_pfc_division_entry_sourcestepprevioussum_body_steps))) /\ fs_s_pfc_division_entry_sourcestepprevioussum_body_steps = fs_r_pfc_division_entry_sourcestepprevioussum_body_steps + fs_a_pfc_division_entry_sourcestepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_entry_sourcesteppreviousresiduebound. pfa_gap_division_entry_sourcesteppreviousresiduebound + S (pfd_previous_division_entry_sourcestep) = (p)) /\ ((exists pfa_offset_left_division_entry_sourcesteppreviousresiduecongruence pfa_offset_right_division_entry_sourcesteppreviousresiduecongruence. (pfc_natural_sum_division_entry_sourcestepprevious) + (p) * pfa_offset_left_division_entry_sourcesteppreviousresiduecongruence = (pfd_previous_division_entry_sourcestep) + (p) * pfa_offset_right_division_entry_sourcesteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_entry_sourcestepsubtractleft. pfa_gap_division_entry_sourcestepsubtractleft + S (pfd_previous_division_entry_sourcestep) = (p)) /\ (((exists pfa_gap_division_entry_sourcestepsubtractright. pfa_gap_division_entry_sourcestepsubtractright + S (pfd_difference_division_entry_sourcestep) = (p)) /\ ((((exists pfa_gap_division_entry_sourcestepsubtractresultbound. pfa_gap_division_entry_sourcestepsubtractresultbound + S (pfd_input_division_entry_sourcestep) = (p)) /\ ((exists pfa_offset_left_division_entry_sourcestepsubtractresultcongruence pfa_offset_right_division_entry_sourcestepsubtractresultcongruence. ((pfd_previous_division_entry_sourcestep) + (pfd_difference_division_entry_sourcestep)) + (p) * pfa_offset_left_division_entry_sourcestepsubtractresultcongruence = (pfd_input_division_entry_sourcestep) + (p) * pfa_offset_right_division_entry_sourcestepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_entry_sourcestepmultiplyleft. pfa_gap_division_entry_sourcestepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_entry_sourcestepmultiplyright. pfa_gap_division_entry_sourcestepmultiplyright + S (pfd_difference_division_entry_sourcestep) = (p)) /\ ((((exists pfa_gap_division_entry_sourcestepmultiplyresultbound. pfa_gap_division_entry_sourcestepmultiplyresultbound + S (pfd_value_division_entry_source) = (p)) /\ ((exists pfa_offset_left_division_entry_sourcestepmultiplyresultcongruence pfa_offset_right_division_entry_sourcestepmultiplyresultcongruence. ((k) * (pfd_difference_division_entry_sourcestep)) + (p) * pfa_offset_left_division_entry_sourcestepmultiplyresultcongruence = (pfd_value_division_entry_source) + (p) * pfa_offset_right_division_entry_sourcestepmultiplyresultcongruence))))))))))))))))))) -> (exists pfa_gap_division_entry_bound. pfa_gap_division_entry_bound + S (i) = (N)) -> (((exists ff_h_pfp_division_entry_given. ff_h_pfp_division_entry_given + S (q) = S ((S (i)) * qc)) /\ exists ff_q_pfp_division_entry_given. qb = ff_q_pfp_division_entry_given * S ((S (i)) * qc) + (q))) -> (exists pfd_input_division_entry_result pfd_previous_division_entry_result pfd_difference_division_entry_result. ((((exists ff_h_pfp_division_entry_resultinput. ff_h_pfp_division_entry_resultinput + S (pfd_input_division_entry_result) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_entry_resultinput. ab = ff_q_pfp_division_entry_resultinput * S ((S (i)) * ac) + (pfd_input_division_entry_result))) /\ (((exists pfc_terms_code_division_entry_resultprevious pfc_terms_scale_division_entry_resultprevious pfc_natural_sum_division_entry_resultprevious. ((forall pfc_index_division_entry_resultpreviousdiagonal. (exists pfa_gap_division_entry_resultpreviousdiagonalbound. pfa_gap_division_entry_resultpreviousdiagonalbound + S (pfc_index_division_entry_resultpreviousdiagonal) = (S (i))) -> exists pfc_value_division_entry_resultpreviousdiagonal. ((((exists ff_h_pfp_division_entry_resultpreviousdiagonalentry. ff_h_pfp_division_entry_resultpreviousdiagonalentry + S (pfc_value_division_entry_resultpreviousdiagonal) = S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * pfc_terms_scale_division_entry_resultprevious)) /\ exists ff_q_pfp_division_entry_resultpreviousdiagonalentry. pfc_terms_code_division_entry_resultprevious = ff_q_pfp_division_entry_resultpreviousdiagonalentry * S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * pfc_terms_scale_division_entry_resultprevious) + (pfc_value_division_entry_resultpreviousdiagonal))) /\ ((exists pfc_complement_division_entry_resultpreviousdiagonalterm pfc_left_division_entry_resultpreviousdiagonalterm pfc_right_division_entry_resultpreviousdiagonalterm. (((pfc_index_division_entry_resultpreviousdiagonal)+pfc_complement_division_entry_resultpreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_entry_resultpreviousdiagonaltermleftinside. pfa_gap_division_entry_resultpreviousdiagonaltermleftinside + S (pfc_index_division_entry_resultpreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_division_entry_resultpreviousdiagonaltermleftentry. ff_h_pfp_division_entry_resultpreviousdiagonaltermleftentry + S (pfc_left_division_entry_resultpreviousdiagonalterm) = S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_entry_resultpreviousdiagonaltermleftentry. qb = ff_q_pfp_division_entry_resultpreviousdiagonaltermleftentry * S ((S (pfc_index_division_entry_resultpreviousdiagonal)) * qc) + (pfc_left_division_entry_resultpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_resultpreviousdiagonaltermleftoutside. pfc_gap_division_entry_resultpreviousdiagonaltermleftoutside+(i)=(pfc_index_division_entry_resultpreviousdiagonal)) /\ (((pfc_left_division_entry_resultpreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_entry_resultpreviousdiagonaltermrightinside. pfa_gap_division_entry_resultpreviousdiagonaltermrightinside + S (pfc_complement_division_entry_resultpreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_entry_resultpreviousdiagonaltermrightentry. ff_h_pfp_division_entry_resultpreviousdiagonaltermrightentry + S (pfc_right_division_entry_resultpreviousdiagonalterm) = S ((S (pfc_complement_division_entry_resultpreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_entry_resultpreviousdiagonaltermrightentry. bb = ff_q_pfp_division_entry_resultpreviousdiagonaltermrightentry * S ((S (pfc_complement_division_entry_resultpreviousdiagonalterm)) * bc) + (pfc_right_division_entry_resultpreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_entry_resultpreviousdiagonaltermrightoutside. pfc_gap_division_entry_resultpreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_entry_resultpreviousdiagonalterm)) /\ (((pfc_right_division_entry_resultpreviousdiagonalterm)=0))))) /\ (((pfc_value_division_entry_resultpreviousdiagonal)=pfc_left_division_entry_resultpreviousdiagonalterm*pfc_right_division_entry_resultpreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_entry_resultprevioussum fs_v_pfc_division_entry_resultprevioussum. ((((exists fs_h_pfc_division_entry_resultprevioussum_body_start. fs_h_pfc_division_entry_resultprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_start. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_entry_resultprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_entry_resultprevioussum_body_terminal. fs_h_pfc_division_entry_resultprevioussum_body_terminal + S (pfc_natural_sum_division_entry_resultprevious) = S ((S (S (i))) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_terminal. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_entry_resultprevioussum) + (pfc_natural_sum_division_entry_resultprevious))) /\ forall fs_i_pfc_division_entry_resultprevioussum_body_steps. (exists fs_lt_pfc_division_entry_resultprevioussum_body_steps_bound. fs_lt_pfc_division_entry_resultprevioussum_body_steps_bound + S fs_i_pfc_division_entry_resultprevioussum_body_steps = S (i)) -> exists fs_a_pfc_division_entry_resultprevioussum_body_steps fs_r_pfc_division_entry_resultprevioussum_body_steps fs_s_pfc_division_entry_resultprevioussum_body_steps. ((((exists fs_h_pfc_division_entry_resultprevioussum_body_steps_summand. fs_h_pfc_division_entry_resultprevioussum_body_steps_summand + S (fs_a_pfc_division_entry_resultprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * pfc_terms_scale_division_entry_resultprevious)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_steps_summand. pfc_terms_code_division_entry_resultprevious = fs_q_pfc_division_entry_resultprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * pfc_terms_scale_division_entry_resultprevious) + (fs_a_pfc_division_entry_resultprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_resultprevioussum_body_steps_partial. fs_h_pfc_division_entry_resultprevioussum_body_steps_partial + S (fs_r_pfc_division_entry_resultprevioussum_body_steps) = S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_steps_partial. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum) + (fs_r_pfc_division_entry_resultprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_entry_resultprevioussum_body_steps_successor. fs_h_pfc_division_entry_resultprevioussum_body_steps_successor + S (fs_s_pfc_division_entry_resultprevioussum_body_steps) = S ((S (S fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum)) /\ exists fs_q_pfc_division_entry_resultprevioussum_body_steps_successor. fs_u_pfc_division_entry_resultprevioussum = fs_q_pfc_division_entry_resultprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_entry_resultprevioussum_body_steps)) * fs_v_pfc_division_entry_resultprevioussum) + (fs_s_pfc_division_entry_resultprevioussum_body_steps))) /\ fs_s_pfc_division_entry_resultprevioussum_body_steps = fs_r_pfc_division_entry_resultprevioussum_body_steps + fs_a_pfc_division_entry_resultprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_entry_resultpreviousresiduebound. pfa_gap_division_entry_resultpreviousresiduebound + S (pfd_previous_division_entry_result) = (p)) /\ ((exists pfa_offset_left_division_entry_resultpreviousresiduecongruence pfa_offset_right_division_entry_resultpreviousresiduecongruence. (pfc_natural_sum_division_entry_resultprevious) + (p) * pfa_offset_left_division_entry_resultpreviousresiduecongruence = (pfd_previous_division_entry_result) + (p) * pfa_offset_right_division_entry_resultpreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_entry_resultsubtractleft. pfa_gap_division_entry_resultsubtractleft + S (pfd_previous_division_entry_result) = (p)) /\ (((exists pfa_gap_division_entry_resultsubtractright. pfa_gap_division_entry_resultsubtractright + S (pfd_difference_division_entry_result) = (p)) /\ ((((exists pfa_gap_division_entry_resultsubtractresultbound. pfa_gap_division_entry_resultsubtractresultbound + S (pfd_input_division_entry_result) = (p)) /\ ((exists pfa_offset_left_division_entry_resultsubtractresultcongruence pfa_offset_right_division_entry_resultsubtractresultcongruence. ((pfd_previous_division_entry_result) + (pfd_difference_division_entry_result)) + (p) * pfa_offset_left_division_entry_resultsubtractresultcongruence = (pfd_input_division_entry_result) + (p) * pfa_offset_right_division_entry_resultsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_entry_resultmultiplyleft. pfa_gap_division_entry_resultmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_entry_resultmultiplyright. pfa_gap_division_entry_resultmultiplyright + S (pfd_difference_division_entry_result) = (p)) /\ ((((exists pfa_gap_division_entry_resultmultiplyresultbound. pfa_gap_division_entry_resultmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_entry_resultmultiplyresultcongruence pfa_offset_right_division_entry_resultmultiplyresultcongruence. ((k) * (pfd_difference_division_entry_result)) + (p) * pfa_offset_left_division_entry_resultmultiplyresultcongruence = (q) + (p) * pfa_offset_right_division_entry_resultmultiplyresultcongruence))))))))))))))))
Complete tactic proof in conservative notation
All 33 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.
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.
01Fix variables and assumptionsL1–10
Work with arbitrary variables or the premises of the current implication.