An actual beta-prefix extension preserves all earlier steps and adds the independently computed next quotient value.
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 QB QC N q. (forall pfd_index_division_append_old. (exists pfa_gap_division_append_oldbound. pfa_gap_division_append_oldbound + S (pfd_index_division_append_old) = (N)) -> exists pfd_value_division_append_old. ((((exists ff_h_pfp_division_append_oldentry. ff_h_pfp_division_append_oldentry + S (pfd_value_division_append_old) = S ((S (pfd_index_division_append_old)) * qc)) /\ exists ff_q_pfp_division_append_oldentry. qb = ff_q_pfp_division_append_oldentry * S ((S (pfd_index_division_append_old)) * qc) + (pfd_value_division_append_old))) /\ ((exists pfd_input_division_append_oldstep pfd_previous_division_append_oldstep pfd_difference_division_append_oldstep. ((((exists ff_h_pfp_division_append_oldstepinput. ff_h_pfp_division_append_oldstepinput + S (pfd_input_division_append_oldstep) = S ((S (pfd_index_division_append_old)) * ac)) /\ exists ff_q_pfp_division_append_oldstepinput. ab = ff_q_pfp_division_append_oldstepinput * S ((S (pfd_index_division_append_old)) * ac) + (pfd_input_division_append_oldstep))) /\ (((exists pfc_terms_code_division_append_oldstepprevious pfc_terms_scale_division_append_oldstepprevious pfc_natural_sum_division_append_oldstepprevious. ((forall pfc_index_division_append_oldsteppreviousdiagonal. (exists pfa_gap_division_append_oldsteppreviousdiagonalbound. pfa_gap_division_append_oldsteppreviousdiagonalbound + S (pfc_index_division_append_oldsteppreviousdiagonal) = (S (pfd_index_division_append_old))) -> exists pfc_value_division_append_oldsteppreviousdiagonal. ((((exists ff_h_pfp_division_append_oldsteppreviousdiagonalentry. ff_h_pfp_division_append_oldsteppreviousdiagonalentry + S (pfc_value_division_append_oldsteppreviousdiagonal) = S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * pfc_terms_scale_division_append_oldstepprevious)) /\ exists ff_q_pfp_division_append_oldsteppreviousdiagonalentry. pfc_terms_code_division_append_oldstepprevious = ff_q_pfp_division_append_oldsteppreviousdiagonalentry * S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * pfc_terms_scale_division_append_oldstepprevious) + (pfc_value_division_append_oldsteppreviousdiagonal))) /\ ((exists pfc_complement_division_append_oldsteppreviousdiagonalterm pfc_left_division_append_oldsteppreviousdiagonalterm pfc_right_division_append_oldsteppreviousdiagonalterm. (((pfc_index_division_append_oldsteppreviousdiagonal)+pfc_complement_division_append_oldsteppreviousdiagonalterm=(pfd_index_division_append_old)) /\ ((((((exists pfa_gap_division_append_oldsteppreviousdiagonaltermleftinside. pfa_gap_division_append_oldsteppreviousdiagonaltermleftinside + S (pfc_index_division_append_oldsteppreviousdiagonal) = (pfd_index_division_append_old)) /\ ((((exists ff_h_pfp_division_append_oldsteppreviousdiagonaltermleftentry. ff_h_pfp_division_append_oldsteppreviousdiagonaltermleftentry + S (pfc_left_division_append_oldsteppreviousdiagonalterm) = S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_append_oldsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_append_oldsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_append_oldsteppreviousdiagonal)) * qc) + (pfc_left_division_append_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_oldsteppreviousdiagonaltermleftoutside. pfc_gap_division_append_oldsteppreviousdiagonaltermleftoutside+(pfd_index_division_append_old)=(pfc_index_division_append_oldsteppreviousdiagonal)) /\ (((pfc_left_division_append_oldsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_append_oldsteppreviousdiagonaltermrightinside. pfa_gap_division_append_oldsteppreviousdiagonaltermrightinside + S (pfc_complement_division_append_oldsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_append_oldsteppreviousdiagonaltermrightentry. ff_h_pfp_division_append_oldsteppreviousdiagonaltermrightentry + S (pfc_right_division_append_oldsteppreviousdiagonalterm) = S ((S (pfc_complement_division_append_oldsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_append_oldsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_append_oldsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_append_oldsteppreviousdiagonalterm)) * bc) + (pfc_right_division_append_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_oldsteppreviousdiagonaltermrightoutside. pfc_gap_division_append_oldsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_append_oldsteppreviousdiagonalterm)) /\ (((pfc_right_division_append_oldsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_append_oldsteppreviousdiagonal)=pfc_left_division_append_oldsteppreviousdiagonalterm*pfc_right_division_append_oldsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_append_oldstepprevioussum fs_v_pfc_division_append_oldstepprevioussum. ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_start. fs_h_pfc_division_append_oldstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_start. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_append_oldstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_terminal. fs_h_pfc_division_append_oldstepprevioussum_body_terminal + S (pfc_natural_sum_division_append_oldstepprevious) = S ((S (S (pfd_index_division_append_old))) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_terminal. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_terminal * S ((S (S (pfd_index_division_append_old))) * fs_v_pfc_division_append_oldstepprevioussum) + (pfc_natural_sum_division_append_oldstepprevious))) /\ forall fs_i_pfc_division_append_oldstepprevioussum_body_steps. (exists fs_lt_pfc_division_append_oldstepprevioussum_body_steps_bound. fs_lt_pfc_division_append_oldstepprevioussum_body_steps_bound + S fs_i_pfc_division_append_oldstepprevioussum_body_steps = S (pfd_index_division_append_old)) -> exists fs_a_pfc_division_append_oldstepprevioussum_body_steps fs_r_pfc_division_append_oldstepprevioussum_body_steps fs_s_pfc_division_append_oldstepprevioussum_body_steps. ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_steps_summand. fs_h_pfc_division_append_oldstepprevioussum_body_steps_summand + S (fs_a_pfc_division_append_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_append_oldstepprevious)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_steps_summand. pfc_terms_code_division_append_oldstepprevious = fs_q_pfc_division_append_oldstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_append_oldstepprevious) + (fs_a_pfc_division_append_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_steps_partial. fs_h_pfc_division_append_oldstepprevioussum_body_steps_partial + S (fs_r_pfc_division_append_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_steps_partial. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum) + (fs_r_pfc_division_append_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_oldstepprevioussum_body_steps_successor. fs_h_pfc_division_append_oldstepprevioussum_body_steps_successor + S (fs_s_pfc_division_append_oldstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum)) /\ exists fs_q_pfc_division_append_oldstepprevioussum_body_steps_successor. fs_u_pfc_division_append_oldstepprevioussum = fs_q_pfc_division_append_oldstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_append_oldstepprevioussum_body_steps)) * fs_v_pfc_division_append_oldstepprevioussum) + (fs_s_pfc_division_append_oldstepprevioussum_body_steps))) /\ fs_s_pfc_division_append_oldstepprevioussum_body_steps = fs_r_pfc_division_append_oldstepprevioussum_body_steps + fs_a_pfc_division_append_oldstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_append_oldsteppreviousresiduebound. pfa_gap_division_append_oldsteppreviousresiduebound + S (pfd_previous_division_append_oldstep) = (p)) /\ ((exists pfa_offset_left_division_append_oldsteppreviousresiduecongruence pfa_offset_right_division_append_oldsteppreviousresiduecongruence. (pfc_natural_sum_division_append_oldstepprevious) + (p) * pfa_offset_left_division_append_oldsteppreviousresiduecongruence = (pfd_previous_division_append_oldstep) + (p) * pfa_offset_right_division_append_oldsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_append_oldstepsubtractleft. pfa_gap_division_append_oldstepsubtractleft + S (pfd_previous_division_append_oldstep) = (p)) /\ (((exists pfa_gap_division_append_oldstepsubtractright. pfa_gap_division_append_oldstepsubtractright + S (pfd_difference_division_append_oldstep) = (p)) /\ ((((exists pfa_gap_division_append_oldstepsubtractresultbound. pfa_gap_division_append_oldstepsubtractresultbound + S (pfd_input_division_append_oldstep) = (p)) /\ ((exists pfa_offset_left_division_append_oldstepsubtractresultcongruence pfa_offset_right_division_append_oldstepsubtractresultcongruence. ((pfd_previous_division_append_oldstep) + (pfd_difference_division_append_oldstep)) + (p) * pfa_offset_left_division_append_oldstepsubtractresultcongruence = (pfd_input_division_append_oldstep) + (p) * pfa_offset_right_division_append_oldstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_append_oldstepmultiplyleft. pfa_gap_division_append_oldstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_append_oldstepmultiplyright. pfa_gap_division_append_oldstepmultiplyright + S (pfd_difference_division_append_oldstep) = (p)) /\ ((((exists pfa_gap_division_append_oldstepmultiplyresultbound. pfa_gap_division_append_oldstepmultiplyresultbound + S (pfd_value_division_append_old) = (p)) /\ ((exists pfa_offset_left_division_append_oldstepmultiplyresultcongruence pfa_offset_right_division_append_oldstepmultiplyresultcongruence. ((k) * (pfd_difference_division_append_oldstep)) + (p) * pfa_offset_left_division_append_oldstepmultiplyresultcongruence = (pfd_value_division_append_old) + (p) * pfa_offset_right_division_append_oldstepmultiplyresultcongruence))))))))))))))))))) -> (forall mdr_i_pfp_division_append_equal mdr_a_pfp_division_append_equal. (exists mdr_gap_pfp_division_append_equalb. mdr_gap_pfp_division_append_equalb + S (mdr_i_pfp_division_append_equal) = (N)) -> (((exists ff_h_mdr_pfp_division_append_equalo. ff_h_mdr_pfp_division_append_equalo + S (mdr_a_pfp_division_append_equal) = S ((S (mdr_i_pfp_division_append_equal)) * qc)) /\ exists ff_q_mdr_pfp_division_append_equalo. qb = ff_q_mdr_pfp_division_append_equalo * S ((S (mdr_i_pfp_division_append_equal)) * qc) + (mdr_a_pfp_division_append_equal))) -> (((exists ff_h_mdr_pfp_division_append_equaln. ff_h_mdr_pfp_division_append_equaln + S (mdr_a_pfp_division_append_equal) = S ((S (mdr_i_pfp_division_append_equal)) * QC)) /\ exists ff_q_mdr_pfp_division_append_equaln. QB = ff_q_mdr_pfp_division_append_equaln * S ((S (mdr_i_pfp_division_append_equal)) * QC) + (mdr_a_pfp_division_append_equal)))) -> (((exists ff_h_pfp_division_append_given_entry. ff_h_pfp_division_append_given_entry + S (q) = S ((S (N)) * QC)) /\ exists ff_q_pfp_division_append_given_entry. QB = ff_q_pfp_division_append_given_entry * S ((S (N)) * QC) + (q))) -> (exists pfd_input_division_append_given_step pfd_previous_division_append_given_step pfd_difference_division_append_given_step. ((((exists ff_h_pfp_division_append_given_stepinput. ff_h_pfp_division_append_given_stepinput + S (pfd_input_division_append_given_step) = S ((S (N)) * ac)) /\ exists ff_q_pfp_division_append_given_stepinput. ab = ff_q_pfp_division_append_given_stepinput * S ((S (N)) * ac) + (pfd_input_division_append_given_step))) /\ (((exists pfc_terms_code_division_append_given_stepprevious pfc_terms_scale_division_append_given_stepprevious pfc_natural_sum_division_append_given_stepprevious. ((forall pfc_index_division_append_given_steppreviousdiagonal. (exists pfa_gap_division_append_given_steppreviousdiagonalbound. pfa_gap_division_append_given_steppreviousdiagonalbound + S (pfc_index_division_append_given_steppreviousdiagonal) = (S (N))) -> exists pfc_value_division_append_given_steppreviousdiagonal. ((((exists ff_h_pfp_division_append_given_steppreviousdiagonalentry. ff_h_pfp_division_append_given_steppreviousdiagonalentry + S (pfc_value_division_append_given_steppreviousdiagonal) = S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * pfc_terms_scale_division_append_given_stepprevious)) /\ exists ff_q_pfp_division_append_given_steppreviousdiagonalentry. pfc_terms_code_division_append_given_stepprevious = ff_q_pfp_division_append_given_steppreviousdiagonalentry * S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * pfc_terms_scale_division_append_given_stepprevious) + (pfc_value_division_append_given_steppreviousdiagonal))) /\ ((exists pfc_complement_division_append_given_steppreviousdiagonalterm pfc_left_division_append_given_steppreviousdiagonalterm pfc_right_division_append_given_steppreviousdiagonalterm. (((pfc_index_division_append_given_steppreviousdiagonal)+pfc_complement_division_append_given_steppreviousdiagonalterm=(N)) /\ ((((((exists pfa_gap_division_append_given_steppreviousdiagonaltermleftinside. pfa_gap_division_append_given_steppreviousdiagonaltermleftinside + S (pfc_index_division_append_given_steppreviousdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_append_given_steppreviousdiagonaltermleftentry. ff_h_pfp_division_append_given_steppreviousdiagonaltermleftentry + S (pfc_left_division_append_given_steppreviousdiagonalterm) = S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_append_given_steppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_append_given_steppreviousdiagonaltermleftentry * S ((S (pfc_index_division_append_given_steppreviousdiagonal)) * qc) + (pfc_left_division_append_given_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_given_steppreviousdiagonaltermleftoutside. pfc_gap_division_append_given_steppreviousdiagonaltermleftoutside+(N)=(pfc_index_division_append_given_steppreviousdiagonal)) /\ (((pfc_left_division_append_given_steppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_append_given_steppreviousdiagonaltermrightinside. pfa_gap_division_append_given_steppreviousdiagonaltermrightinside + S (pfc_complement_division_append_given_steppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_append_given_steppreviousdiagonaltermrightentry. ff_h_pfp_division_append_given_steppreviousdiagonaltermrightentry + S (pfc_right_division_append_given_steppreviousdiagonalterm) = S ((S (pfc_complement_division_append_given_steppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_append_given_steppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_append_given_steppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_append_given_steppreviousdiagonalterm)) * bc) + (pfc_right_division_append_given_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_given_steppreviousdiagonaltermrightoutside. pfc_gap_division_append_given_steppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_append_given_steppreviousdiagonalterm)) /\ (((pfc_right_division_append_given_steppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_append_given_steppreviousdiagonal)=pfc_left_division_append_given_steppreviousdiagonalterm*pfc_right_division_append_given_steppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_append_given_stepprevioussum fs_v_pfc_division_append_given_stepprevioussum. ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_start. fs_h_pfc_division_append_given_stepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_start. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_append_given_stepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_terminal. fs_h_pfc_division_append_given_stepprevioussum_body_terminal + S (pfc_natural_sum_division_append_given_stepprevious) = S ((S (S (N))) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_terminal. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_terminal * S ((S (S (N))) * fs_v_pfc_division_append_given_stepprevioussum) + (pfc_natural_sum_division_append_given_stepprevious))) /\ forall fs_i_pfc_division_append_given_stepprevioussum_body_steps. (exists fs_lt_pfc_division_append_given_stepprevioussum_body_steps_bound. fs_lt_pfc_division_append_given_stepprevioussum_body_steps_bound + S fs_i_pfc_division_append_given_stepprevioussum_body_steps = S (N)) -> exists fs_a_pfc_division_append_given_stepprevioussum_body_steps fs_r_pfc_division_append_given_stepprevioussum_body_steps fs_s_pfc_division_append_given_stepprevioussum_body_steps. ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_steps_summand. fs_h_pfc_division_append_given_stepprevioussum_body_steps_summand + S (fs_a_pfc_division_append_given_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * pfc_terms_scale_division_append_given_stepprevious)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_steps_summand. pfc_terms_code_division_append_given_stepprevious = fs_q_pfc_division_append_given_stepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * pfc_terms_scale_division_append_given_stepprevious) + (fs_a_pfc_division_append_given_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_steps_partial. fs_h_pfc_division_append_given_stepprevioussum_body_steps_partial + S (fs_r_pfc_division_append_given_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_steps_partial. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum) + (fs_r_pfc_division_append_given_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_given_stepprevioussum_body_steps_successor. fs_h_pfc_division_append_given_stepprevioussum_body_steps_successor + S (fs_s_pfc_division_append_given_stepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum)) /\ exists fs_q_pfc_division_append_given_stepprevioussum_body_steps_successor. fs_u_pfc_division_append_given_stepprevioussum = fs_q_pfc_division_append_given_stepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_append_given_stepprevioussum_body_steps)) * fs_v_pfc_division_append_given_stepprevioussum) + (fs_s_pfc_division_append_given_stepprevioussum_body_steps))) /\ fs_s_pfc_division_append_given_stepprevioussum_body_steps = fs_r_pfc_division_append_given_stepprevioussum_body_steps + fs_a_pfc_division_append_given_stepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_append_given_steppreviousresiduebound. pfa_gap_division_append_given_steppreviousresiduebound + S (pfd_previous_division_append_given_step) = (p)) /\ ((exists pfa_offset_left_division_append_given_steppreviousresiduecongruence pfa_offset_right_division_append_given_steppreviousresiduecongruence. (pfc_natural_sum_division_append_given_stepprevious) + (p) * pfa_offset_left_division_append_given_steppreviousresiduecongruence = (pfd_previous_division_append_given_step) + (p) * pfa_offset_right_division_append_given_steppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_append_given_stepsubtractleft. pfa_gap_division_append_given_stepsubtractleft + S (pfd_previous_division_append_given_step) = (p)) /\ (((exists pfa_gap_division_append_given_stepsubtractright. pfa_gap_division_append_given_stepsubtractright + S (pfd_difference_division_append_given_step) = (p)) /\ ((((exists pfa_gap_division_append_given_stepsubtractresultbound. pfa_gap_division_append_given_stepsubtractresultbound + S (pfd_input_division_append_given_step) = (p)) /\ ((exists pfa_offset_left_division_append_given_stepsubtractresultcongruence pfa_offset_right_division_append_given_stepsubtractresultcongruence. ((pfd_previous_division_append_given_step) + (pfd_difference_division_append_given_step)) + (p) * pfa_offset_left_division_append_given_stepsubtractresultcongruence = (pfd_input_division_append_given_step) + (p) * pfa_offset_right_division_append_given_stepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_append_given_stepmultiplyleft. pfa_gap_division_append_given_stepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_append_given_stepmultiplyright. pfa_gap_division_append_given_stepmultiplyright + S (pfd_difference_division_append_given_step) = (p)) /\ ((((exists pfa_gap_division_append_given_stepmultiplyresultbound. pfa_gap_division_append_given_stepmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_append_given_stepmultiplyresultcongruence pfa_offset_right_division_append_given_stepmultiplyresultcongruence. ((k) * (pfd_difference_division_append_given_step)) + (p) * pfa_offset_left_division_append_given_stepmultiplyresultcongruence = (q) + (p) * pfa_offset_right_division_append_given_stepmultiplyresultcongruence)))))))))))))))) -> (forall pfd_index_division_append_new. (exists pfa_gap_division_append_newbound. pfa_gap_division_append_newbound + S (pfd_index_division_append_new) = (S N)) -> exists pfd_value_division_append_new. ((((exists ff_h_pfp_division_append_newentry. ff_h_pfp_division_append_newentry + S (pfd_value_division_append_new) = S ((S (pfd_index_division_append_new)) * QC)) /\ exists ff_q_pfp_division_append_newentry. QB = ff_q_pfp_division_append_newentry * S ((S (pfd_index_division_append_new)) * QC) + (pfd_value_division_append_new))) /\ ((exists pfd_input_division_append_newstep pfd_previous_division_append_newstep pfd_difference_division_append_newstep. ((((exists ff_h_pfp_division_append_newstepinput. ff_h_pfp_division_append_newstepinput + S (pfd_input_division_append_newstep) = S ((S (pfd_index_division_append_new)) * ac)) /\ exists ff_q_pfp_division_append_newstepinput. ab = ff_q_pfp_division_append_newstepinput * S ((S (pfd_index_division_append_new)) * ac) + (pfd_input_division_append_newstep))) /\ (((exists pfc_terms_code_division_append_newstepprevious pfc_terms_scale_division_append_newstepprevious pfc_natural_sum_division_append_newstepprevious. ((forall pfc_index_division_append_newsteppreviousdiagonal. (exists pfa_gap_division_append_newsteppreviousdiagonalbound. pfa_gap_division_append_newsteppreviousdiagonalbound + S (pfc_index_division_append_newsteppreviousdiagonal) = (S (pfd_index_division_append_new))) -> exists pfc_value_division_append_newsteppreviousdiagonal. ((((exists ff_h_pfp_division_append_newsteppreviousdiagonalentry. ff_h_pfp_division_append_newsteppreviousdiagonalentry + S (pfc_value_division_append_newsteppreviousdiagonal) = S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * pfc_terms_scale_division_append_newstepprevious)) /\ exists ff_q_pfp_division_append_newsteppreviousdiagonalentry. pfc_terms_code_division_append_newstepprevious = ff_q_pfp_division_append_newsteppreviousdiagonalentry * S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * pfc_terms_scale_division_append_newstepprevious) + (pfc_value_division_append_newsteppreviousdiagonal))) /\ ((exists pfc_complement_division_append_newsteppreviousdiagonalterm pfc_left_division_append_newsteppreviousdiagonalterm pfc_right_division_append_newsteppreviousdiagonalterm. (((pfc_index_division_append_newsteppreviousdiagonal)+pfc_complement_division_append_newsteppreviousdiagonalterm=(pfd_index_division_append_new)) /\ ((((((exists pfa_gap_division_append_newsteppreviousdiagonaltermleftinside. pfa_gap_division_append_newsteppreviousdiagonaltermleftinside + S (pfc_index_division_append_newsteppreviousdiagonal) = (pfd_index_division_append_new)) /\ ((((exists ff_h_pfp_division_append_newsteppreviousdiagonaltermleftentry. ff_h_pfp_division_append_newsteppreviousdiagonaltermleftentry + S (pfc_left_division_append_newsteppreviousdiagonalterm) = S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * QC)) /\ exists ff_q_pfp_division_append_newsteppreviousdiagonaltermleftentry. QB = ff_q_pfp_division_append_newsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_append_newsteppreviousdiagonal)) * QC) + (pfc_left_division_append_newsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_newsteppreviousdiagonaltermleftoutside. pfc_gap_division_append_newsteppreviousdiagonaltermleftoutside+(pfd_index_division_append_new)=(pfc_index_division_append_newsteppreviousdiagonal)) /\ (((pfc_left_division_append_newsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_append_newsteppreviousdiagonaltermrightinside. pfa_gap_division_append_newsteppreviousdiagonaltermrightinside + S (pfc_complement_division_append_newsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_append_newsteppreviousdiagonaltermrightentry. ff_h_pfp_division_append_newsteppreviousdiagonaltermrightentry + S (pfc_right_division_append_newsteppreviousdiagonalterm) = S ((S (pfc_complement_division_append_newsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_append_newsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_append_newsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_append_newsteppreviousdiagonalterm)) * bc) + (pfc_right_division_append_newsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_append_newsteppreviousdiagonaltermrightoutside. pfc_gap_division_append_newsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_append_newsteppreviousdiagonalterm)) /\ (((pfc_right_division_append_newsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_append_newsteppreviousdiagonal)=pfc_left_division_append_newsteppreviousdiagonalterm*pfc_right_division_append_newsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_append_newstepprevioussum fs_v_pfc_division_append_newstepprevioussum. ((((exists fs_h_pfc_division_append_newstepprevioussum_body_start. fs_h_pfc_division_append_newstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_start. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_append_newstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_append_newstepprevioussum_body_terminal. fs_h_pfc_division_append_newstepprevioussum_body_terminal + S (pfc_natural_sum_division_append_newstepprevious) = S ((S (S (pfd_index_division_append_new))) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_terminal. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_terminal * S ((S (S (pfd_index_division_append_new))) * fs_v_pfc_division_append_newstepprevioussum) + (pfc_natural_sum_division_append_newstepprevious))) /\ forall fs_i_pfc_division_append_newstepprevioussum_body_steps. (exists fs_lt_pfc_division_append_newstepprevioussum_body_steps_bound. fs_lt_pfc_division_append_newstepprevioussum_body_steps_bound + S fs_i_pfc_division_append_newstepprevioussum_body_steps = S (pfd_index_division_append_new)) -> exists fs_a_pfc_division_append_newstepprevioussum_body_steps fs_r_pfc_division_append_newstepprevioussum_body_steps fs_s_pfc_division_append_newstepprevioussum_body_steps. ((((exists fs_h_pfc_division_append_newstepprevioussum_body_steps_summand. fs_h_pfc_division_append_newstepprevioussum_body_steps_summand + S (fs_a_pfc_division_append_newstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * pfc_terms_scale_division_append_newstepprevious)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_steps_summand. pfc_terms_code_division_append_newstepprevious = fs_q_pfc_division_append_newstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * pfc_terms_scale_division_append_newstepprevious) + (fs_a_pfc_division_append_newstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_newstepprevioussum_body_steps_partial. fs_h_pfc_division_append_newstepprevioussum_body_steps_partial + S (fs_r_pfc_division_append_newstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_steps_partial. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum) + (fs_r_pfc_division_append_newstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_append_newstepprevioussum_body_steps_successor. fs_h_pfc_division_append_newstepprevioussum_body_steps_successor + S (fs_s_pfc_division_append_newstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum)) /\ exists fs_q_pfc_division_append_newstepprevioussum_body_steps_successor. fs_u_pfc_division_append_newstepprevioussum = fs_q_pfc_division_append_newstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_append_newstepprevioussum_body_steps)) * fs_v_pfc_division_append_newstepprevioussum) + (fs_s_pfc_division_append_newstepprevioussum_body_steps))) /\ fs_s_pfc_division_append_newstepprevioussum_body_steps = fs_r_pfc_division_append_newstepprevioussum_body_steps + fs_a_pfc_division_append_newstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_append_newsteppreviousresiduebound. pfa_gap_division_append_newsteppreviousresiduebound + S (pfd_previous_division_append_newstep) = (p)) /\ ((exists pfa_offset_left_division_append_newsteppreviousresiduecongruence pfa_offset_right_division_append_newsteppreviousresiduecongruence. (pfc_natural_sum_division_append_newstepprevious) + (p) * pfa_offset_left_division_append_newsteppreviousresiduecongruence = (pfd_previous_division_append_newstep) + (p) * pfa_offset_right_division_append_newsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_append_newstepsubtractleft. pfa_gap_division_append_newstepsubtractleft + S (pfd_previous_division_append_newstep) = (p)) /\ (((exists pfa_gap_division_append_newstepsubtractright. pfa_gap_division_append_newstepsubtractright + S (pfd_difference_division_append_newstep) = (p)) /\ ((((exists pfa_gap_division_append_newstepsubtractresultbound. pfa_gap_division_append_newstepsubtractresultbound + S (pfd_input_division_append_newstep) = (p)) /\ ((exists pfa_offset_left_division_append_newstepsubtractresultcongruence pfa_offset_right_division_append_newstepsubtractresultcongruence. ((pfd_previous_division_append_newstep) + (pfd_difference_division_append_newstep)) + (p) * pfa_offset_left_division_append_newstepsubtractresultcongruence = (pfd_input_division_append_newstep) + (p) * pfa_offset_right_division_append_newstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_append_newstepmultiplyleft. pfa_gap_division_append_newstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_append_newstepmultiplyright. pfa_gap_division_append_newstepmultiplyright + S (pfd_difference_division_append_newstep) = (p)) /\ ((((exists pfa_gap_division_append_newstepmultiplyresultbound. pfa_gap_division_append_newstepmultiplyresultbound + S (pfd_value_division_append_new) = (p)) /\ ((exists pfa_offset_left_division_append_newstepmultiplyresultcongruence pfa_offset_right_division_append_newstepmultiplyresultcongruence. ((k) * (pfd_difference_division_append_newstep)) + (p) * pfa_offset_left_division_append_newstepmultiplyresultcongruence = (pfd_value_division_append_new) + (p) * pfa_offset_right_division_append_newstepmultiplyresultcongruence)))))))))))))))))))
Complete tactic proof in conservative notation
All 100 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.