PG0046

prime_field_polynomial_aligned_add_cancel_left

Cancel a common addend from actual aligned sums: construct four real common-length prefixes, realize both additions and apply checked coefficient subtraction functionality.

Alpha v34 checked-use · first admitted v34 · 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.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ cb. ∀ cc. ∀ J. ∀ rb. ∀ rc. ∀ N. Prime(p) → FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) → FpPolynomialAlignedAdd(p,ab,ac,L,cb,cc,J,rb,rc,N) → PolynomialEquivalent(bb,bc,M,cb,cc,J)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaPrefixInto(b,c,l,B) · 10BetaPrefixEqual(b,c,d,e,l) · 1FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 2PolynomialEquivalent(b,c,L,d,e,M) · 6FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 2Le(a,b) · 6Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_aligned_add_boundedprime_field_polynomial_bounded_representative_at_length_existsle_add_right · checked external prerequisitele_refl · checked external prerequisitele_trans · checked external prerequisiteprime_field_polynomial_aligned_add_realizeprime_field_polynomial_equivalent_transitive · checked external prerequisiteprime_field_polynomial_equal_implies_equivalent · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_subtract_functional · checked external prerequisiteprime_field_polynomial_subtract_from_add · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L bb bc M cb cc J rb rc N. (~((p) = 1) /\ forall pfa_factor_left_cancel_prime pfa_factor_right_cancel_prime. (p) = pfa_factor_left_cancel_prime * pfa_factor_right_cancel_prime -> pfa_factor_left_cancel_prime = 1 \/ pfa_factor_right_cancel_prime = 1) -> (((forall fom_index_pfp_cancel_first_left_bounded. (exists fom_gap_pfp_cancel_first_left_bounded_index_bound. fom_gap_pfp_cancel_first_left_bounded_index_bound + S (fom_index_pfp_cancel_first_left_bounded) = L) -> exists fom_value_pfp_cancel_first_left_bounded. ((((exists fom_beta_height_pfp_cancel_first_left_bounded_entry. fom_beta_height_pfp_cancel_first_left_bounded_entry + S (fom_value_pfp_cancel_first_left_bounded) = S ((S (fom_index_pfp_cancel_first_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_cancel_first_left_bounded_entry. ab = fom_beta_quotient_pfp_cancel_first_left_bounded_entry * S ((S (fom_index_pfp_cancel_first_left_bounded)) * ac) + (fom_value_pfp_cancel_first_left_bounded))) /\ (exists fom_gap_pfp_cancel_first_left_bounded_value_bound. fom_gap_pfp_cancel_first_left_bounded_value_bound + S (fom_value_pfp_cancel_first_left_bounded) = p))) /\ (((forall fom_index_pfp_cancel_first_right_bounded. (exists fom_gap_pfp_cancel_first_right_bounded_index_bound. fom_gap_pfp_cancel_first_right_bounded_index_bound + S (fom_index_pfp_cancel_first_right_bounded) = M) -> exists fom_value_pfp_cancel_first_right_bounded. ((((exists fom_beta_height_pfp_cancel_first_right_bounded_entry. fom_beta_height_pfp_cancel_first_right_bounded_entry + S (fom_value_pfp_cancel_first_right_bounded) = S ((S (fom_index_pfp_cancel_first_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_cancel_first_right_bounded_entry. bb = fom_beta_quotient_pfp_cancel_first_right_bounded_entry * S ((S (fom_index_pfp_cancel_first_right_bounded)) * bc) + (fom_value_pfp_cancel_first_right_bounded))) /\ (exists fom_gap_pfp_cancel_first_right_bounded_value_bound. fom_gap_pfp_cancel_first_right_bounded_value_bound + S (fom_value_pfp_cancel_first_right_bounded) = p))) /\ (((forall fom_index_pfp_cancel_first_result_bounded. (exists fom_gap_pfp_cancel_first_result_bounded_index_bound. fom_gap_pfp_cancel_first_result_bounded_index_bound + S (fom_index_pfp_cancel_first_result_bounded) = N) -> exists fom_value_pfp_cancel_first_result_bounded. ((((exists fom_beta_height_pfp_cancel_first_result_bounded_entry. fom_beta_height_pfp_cancel_first_result_bounded_entry + S (fom_value_pfp_cancel_first_result_bounded) = S ((S (fom_index_pfp_cancel_first_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_cancel_first_result_bounded_entry. rb = fom_beta_quotient_pfp_cancel_first_result_bounded_entry * S ((S (fom_index_pfp_cancel_first_result_bounded)) * rc) + (fom_value_pfp_cancel_first_result_bounded))) /\ (exists fom_gap_pfp_cancel_first_result_bounded_value_bound. fom_gap_pfp_cancel_first_result_bounded_value_bound + S (fom_value_pfp_cancel_first_result_bounded) = p))) /\ ((exists pfaa_left_b_cancel_first pfaa_left_c_cancel_first pfaa_right_b_cancel_first pfaa_right_c_cancel_first pfaa_sum_b_cancel_first pfaa_sum_c_cancel_first pfaa_length_cancel_first. ((((forall pfrep_power_cancel_first_witness_common_left pfrep_left_cancel_first_witness_common_left pfrep_right_cancel_first_witness_common_left. ((exists pfrep_position_cancel_first_witness_common_leftfirst. ((pfrep_position_cancel_first_witness_common_leftfirst+S (pfrep_power_cancel_first_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_cancel_first_witness_common_leftfirstentry. ff_h_pfp_cancel_first_witness_common_leftfirstentry + S (pfrep_left_cancel_first_witness_common_left) = S ((S (pfrep_position_cancel_first_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_cancel_first_witness_common_leftfirstentry. ab = ff_q_pfp_cancel_first_witness_common_leftfirstentry * S ((S (pfrep_position_cancel_first_witness_common_leftfirst)) * ac) + (pfrep_left_cancel_first_witness_common_left)))))) \/ (((exists pfrep_gap_cancel_first_witness_common_leftfirstoutside. pfrep_gap_cancel_first_witness_common_leftfirstoutside+(L)=(pfrep_power_cancel_first_witness_common_left)) /\ (((pfrep_left_cancel_first_witness_common_left)=0))))) -> ((exists pfrep_position_cancel_first_witness_common_leftsecond. ((pfrep_position_cancel_first_witness_common_leftsecond+S (pfrep_power_cancel_first_witness_common_left)=(pfaa_length_cancel_first)) /\ ((((exists ff_h_pfp_cancel_first_witness_common_leftsecondentry. ff_h_pfp_cancel_first_witness_common_leftsecondentry + S (pfrep_right_cancel_first_witness_common_left) = S ((S (pfrep_position_cancel_first_witness_common_leftsecond)) * pfaa_left_c_cancel_first)) /\ exists ff_q_pfp_cancel_first_witness_common_leftsecondentry. pfaa_left_b_cancel_first = ff_q_pfp_cancel_first_witness_common_leftsecondentry * S ((S (pfrep_position_cancel_first_witness_common_leftsecond)) * pfaa_left_c_cancel_first) + (pfrep_right_cancel_first_witness_common_left)))))) \/ (((exists pfrep_gap_cancel_first_witness_common_leftsecondoutside. pfrep_gap_cancel_first_witness_common_leftsecondoutside+(pfaa_length_cancel_first)=(pfrep_power_cancel_first_witness_common_left)) /\ (((pfrep_right_cancel_first_witness_common_left)=0))))) -> pfrep_left_cancel_first_witness_common_left=pfrep_right_cancel_first_witness_common_left) /\ ((forall pfrep_power_cancel_first_witness_common_right pfrep_left_cancel_first_witness_common_right pfrep_right_cancel_first_witness_common_right. ((exists pfrep_position_cancel_first_witness_common_rightfirst. ((pfrep_position_cancel_first_witness_common_rightfirst+S (pfrep_power_cancel_first_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_cancel_first_witness_common_rightfirstentry. ff_h_pfp_cancel_first_witness_common_rightfirstentry + S (pfrep_left_cancel_first_witness_common_right) = S ((S (pfrep_position_cancel_first_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_cancel_first_witness_common_rightfirstentry. bb = ff_q_pfp_cancel_first_witness_common_rightfirstentry * S ((S (pfrep_position_cancel_first_witness_common_rightfirst)) * bc) + (pfrep_left_cancel_first_witness_common_right)))))) \/ (((exists pfrep_gap_cancel_first_witness_common_rightfirstoutside. pfrep_gap_cancel_first_witness_common_rightfirstoutside+(M)=(pfrep_power_cancel_first_witness_common_right)) /\ (((pfrep_left_cancel_first_witness_common_right)=0))))) -> ((exists pfrep_position_cancel_first_witness_common_rightsecond. ((pfrep_position_cancel_first_witness_common_rightsecond+S (pfrep_power_cancel_first_witness_common_right)=(pfaa_length_cancel_first)) /\ ((((exists ff_h_pfp_cancel_first_witness_common_rightsecondentry. ff_h_pfp_cancel_first_witness_common_rightsecondentry + S (pfrep_right_cancel_first_witness_common_right) = S ((S (pfrep_position_cancel_first_witness_common_rightsecond)) * pfaa_right_c_cancel_first)) /\ exists ff_q_pfp_cancel_first_witness_common_rightsecondentry. pfaa_right_b_cancel_first = ff_q_pfp_cancel_first_witness_common_rightsecondentry * S ((S (pfrep_position_cancel_first_witness_common_rightsecond)) * pfaa_right_c_cancel_first) + (pfrep_right_cancel_first_witness_common_right)))))) \/ (((exists pfrep_gap_cancel_first_witness_common_rightsecondoutside. pfrep_gap_cancel_first_witness_common_rightsecondoutside+(pfaa_length_cancel_first)=(pfrep_power_cancel_first_witness_common_right)) /\ (((pfrep_right_cancel_first_witness_common_right)=0))))) -> pfrep_left_cancel_first_witness_common_right=pfrep_right_cancel_first_witness_common_right)))) /\ (((forall pfp_index_cancel_first_witness_operation. (exists pfa_gap_cancel_first_witness_operationindex. pfa_gap_cancel_first_witness_operationindex + S (pfp_index_cancel_first_witness_operation) = (pfaa_length_cancel_first)) -> exists pfp_left_cancel_first_witness_operation pfp_right_cancel_first_witness_operation pfp_value_cancel_first_witness_operation. ((((exists ff_h_pfp_cancel_first_witness_operationleft. ff_h_pfp_cancel_first_witness_operationleft + S (pfp_left_cancel_first_witness_operation) = S ((S (pfp_index_cancel_first_witness_operation)) * pfaa_left_c_cancel_first)) /\ exists ff_q_pfp_cancel_first_witness_operationleft. pfaa_left_b_cancel_first = ff_q_pfp_cancel_first_witness_operationleft * S ((S (pfp_index_cancel_first_witness_operation)) * pfaa_left_c_cancel_first) + (pfp_left_cancel_first_witness_operation))) /\ (((((exists ff_h_pfp_cancel_first_witness_operationright. ff_h_pfp_cancel_first_witness_operationright + S (pfp_right_cancel_first_witness_operation) = S ((S (pfp_index_cancel_first_witness_operation)) * pfaa_right_c_cancel_first)) /\ exists ff_q_pfp_cancel_first_witness_operationright. pfaa_right_b_cancel_first = ff_q_pfp_cancel_first_witness_operationright * S ((S (pfp_index_cancel_first_witness_operation)) * pfaa_right_c_cancel_first) + (pfp_right_cancel_first_witness_operation))) /\ (((((exists ff_h_pfp_cancel_first_witness_operationtarget. ff_h_pfp_cancel_first_witness_operationtarget + S (pfp_value_cancel_first_witness_operation) = S ((S (pfp_index_cancel_first_witness_operation)) * pfaa_sum_c_cancel_first)) /\ exists ff_q_pfp_cancel_first_witness_operationtarget. pfaa_sum_b_cancel_first = ff_q_pfp_cancel_first_witness_operationtarget * S ((S (pfp_index_cancel_first_witness_operation)) * pfaa_sum_c_cancel_first) + (pfp_value_cancel_first_witness_operation))) /\ ((((exists pfa_gap_cancel_first_witness_operationoperationleft. pfa_gap_cancel_first_witness_operationoperationleft + S (pfp_left_cancel_first_witness_operation) = (p)) /\ (((exists pfa_gap_cancel_first_witness_operationoperationright. pfa_gap_cancel_first_witness_operationoperationright + S (pfp_right_cancel_first_witness_operation) = (p)) /\ ((((exists pfa_gap_cancel_first_witness_operationoperationresultbound. pfa_gap_cancel_first_witness_operationoperationresultbound + S (pfp_value_cancel_first_witness_operation) = (p)) /\ ((exists pfa_offset_left_cancel_first_witness_operationoperationresultcongruence pfa_offset_right_cancel_first_witness_operationoperationresultcongruence. ((pfp_left_cancel_first_witness_operation) + (pfp_right_cancel_first_witness_operation)) + (p) * pfa_offset_left_cancel_first_witness_operationoperationresultcongruence = (pfp_value_cancel_first_witness_operation) + (p) * pfa_offset_right_cancel_first_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_cancel_first_witness_output pfrep_left_cancel_first_witness_output pfrep_right_cancel_first_witness_output. ((exists pfrep_position_cancel_first_witness_outputfirst. ((pfrep_position_cancel_first_witness_outputfirst+S (pfrep_power_cancel_first_witness_output)=(pfaa_length_cancel_first)) /\ ((((exists ff_h_pfp_cancel_first_witness_outputfirstentry. ff_h_pfp_cancel_first_witness_outputfirstentry + S (pfrep_left_cancel_first_witness_output) = S ((S (pfrep_position_cancel_first_witness_outputfirst)) * pfaa_sum_c_cancel_first)) /\ exists ff_q_pfp_cancel_first_witness_outputfirstentry. pfaa_sum_b_cancel_first = ff_q_pfp_cancel_first_witness_outputfirstentry * S ((S (pfrep_position_cancel_first_witness_outputfirst)) * pfaa_sum_c_cancel_first) + (pfrep_left_cancel_first_witness_output)))))) \/ (((exists pfrep_gap_cancel_first_witness_outputfirstoutside. pfrep_gap_cancel_first_witness_outputfirstoutside+(pfaa_length_cancel_first)=(pfrep_power_cancel_first_witness_output)) /\ (((pfrep_left_cancel_first_witness_output)=0))))) -> ((exists pfrep_position_cancel_first_witness_outputsecond. ((pfrep_position_cancel_first_witness_outputsecond+S (pfrep_power_cancel_first_witness_output)=(N)) /\ ((((exists ff_h_pfp_cancel_first_witness_outputsecondentry. ff_h_pfp_cancel_first_witness_outputsecondentry + S (pfrep_right_cancel_first_witness_output) = S ((S (pfrep_position_cancel_first_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_cancel_first_witness_outputsecondentry. rb = ff_q_pfp_cancel_first_witness_outputsecondentry * S ((S (pfrep_position_cancel_first_witness_outputsecond)) * rc) + (pfrep_right_cancel_first_witness_output)))))) \/ (((exists pfrep_gap_cancel_first_witness_outputsecondoutside. pfrep_gap_cancel_first_witness_outputsecondoutside+(N)=(pfrep_power_cancel_first_witness_output)) /\ (((pfrep_right_cancel_first_witness_output)=0))))) -> pfrep_left_cancel_first_witness_output=pfrep_right_cancel_first_witness_output))))))))))))) -> (((forall fom_index_pfp_cancel_second_left_bounded. (exists fom_gap_pfp_cancel_second_left_bounded_index_bound. fom_gap_pfp_cancel_second_left_bounded_index_bound + S (fom_index_pfp_cancel_second_left_bounded) = L) -> exists fom_value_pfp_cancel_second_left_bounded. ((((exists fom_beta_height_pfp_cancel_second_left_bounded_entry. fom_beta_height_pfp_cancel_second_left_bounded_entry + S (fom_value_pfp_cancel_second_left_bounded) = S ((S (fom_index_pfp_cancel_second_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_cancel_second_left_bounded_entry. ab = fom_beta_quotient_pfp_cancel_second_left_bounded_entry * S ((S (fom_index_pfp_cancel_second_left_bounded)) * ac) + (fom_value_pfp_cancel_second_left_bounded))) /\ (exists fom_gap_pfp_cancel_second_left_bounded_value_bound. fom_gap_pfp_cancel_second_left_bounded_value_bound + S (fom_value_pfp_cancel_second_left_bounded) = p))) /\ (((forall fom_index_pfp_cancel_second_right_bounded. (exists fom_gap_pfp_cancel_second_right_bounded_index_bound. fom_gap_pfp_cancel_second_right_bounded_index_bound + S (fom_index_pfp_cancel_second_right_bounded) = J) -> exists fom_value_pfp_cancel_second_right_bounded. ((((exists fom_beta_height_pfp_cancel_second_right_bounded_entry. fom_beta_height_pfp_cancel_second_right_bounded_entry + S (fom_value_pfp_cancel_second_right_bounded) = S ((S (fom_index_pfp_cancel_second_right_bounded)) * cc)) /\ exists fom_beta_quotient_pfp_cancel_second_right_bounded_entry. cb = fom_beta_quotient_pfp_cancel_second_right_bounded_entry * S ((S (fom_index_pfp_cancel_second_right_bounded)) * cc) + (fom_value_pfp_cancel_second_right_bounded))) /\ (exists fom_gap_pfp_cancel_second_right_bounded_value_bound. fom_gap_pfp_cancel_second_right_bounded_value_bound + S (fom_value_pfp_cancel_second_right_bounded) = p))) /\ (((forall fom_index_pfp_cancel_second_result_bounded. (exists fom_gap_pfp_cancel_second_result_bounded_index_bound. fom_gap_pfp_cancel_second_result_bounded_index_bound + S (fom_index_pfp_cancel_second_result_bounded) = N) -> exists fom_value_pfp_cancel_second_result_bounded. ((((exists fom_beta_height_pfp_cancel_second_result_bounded_entry. fom_beta_height_pfp_cancel_second_result_bounded_entry + S (fom_value_pfp_cancel_second_result_bounded) = S ((S (fom_index_pfp_cancel_second_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_cancel_second_result_bounded_entry. rb = fom_beta_quotient_pfp_cancel_second_result_bounded_entry * S ((S (fom_index_pfp_cancel_second_result_bounded)) * rc) + (fom_value_pfp_cancel_second_result_bounded))) /\ (exists fom_gap_pfp_cancel_second_result_bounded_value_bound. fom_gap_pfp_cancel_second_result_bounded_value_bound + S (fom_value_pfp_cancel_second_result_bounded) = p))) /\ ((exists pfaa_left_b_cancel_second pfaa_left_c_cancel_second pfaa_right_b_cancel_second pfaa_right_c_cancel_second pfaa_sum_b_cancel_second pfaa_sum_c_cancel_second pfaa_length_cancel_second. ((((forall pfrep_power_cancel_second_witness_common_left pfrep_left_cancel_second_witness_common_left pfrep_right_cancel_second_witness_common_left. ((exists pfrep_position_cancel_second_witness_common_leftfirst. ((pfrep_position_cancel_second_witness_common_leftfirst+S (pfrep_power_cancel_second_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_cancel_second_witness_common_leftfirstentry. ff_h_pfp_cancel_second_witness_common_leftfirstentry + S (pfrep_left_cancel_second_witness_common_left) = S ((S (pfrep_position_cancel_second_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_cancel_second_witness_common_leftfirstentry. ab = ff_q_pfp_cancel_second_witness_common_leftfirstentry * S ((S (pfrep_position_cancel_second_witness_common_leftfirst)) * ac) + (pfrep_left_cancel_second_witness_common_left)))))) \/ (((exists pfrep_gap_cancel_second_witness_common_leftfirstoutside. pfrep_gap_cancel_second_witness_common_leftfirstoutside+(L)=(pfrep_power_cancel_second_witness_common_left)) /\ (((pfrep_left_cancel_second_witness_common_left)=0))))) -> ((exists pfrep_position_cancel_second_witness_common_leftsecond. ((pfrep_position_cancel_second_witness_common_leftsecond+S (pfrep_power_cancel_second_witness_common_left)=(pfaa_length_cancel_second)) /\ ((((exists ff_h_pfp_cancel_second_witness_common_leftsecondentry. ff_h_pfp_cancel_second_witness_common_leftsecondentry + S (pfrep_right_cancel_second_witness_common_left) = S ((S (pfrep_position_cancel_second_witness_common_leftsecond)) * pfaa_left_c_cancel_second)) /\ exists ff_q_pfp_cancel_second_witness_common_leftsecondentry. pfaa_left_b_cancel_second = ff_q_pfp_cancel_second_witness_common_leftsecondentry * S ((S (pfrep_position_cancel_second_witness_common_leftsecond)) * pfaa_left_c_cancel_second) + (pfrep_right_cancel_second_witness_common_left)))))) \/ (((exists pfrep_gap_cancel_second_witness_common_leftsecondoutside. pfrep_gap_cancel_second_witness_common_leftsecondoutside+(pfaa_length_cancel_second)=(pfrep_power_cancel_second_witness_common_left)) /\ (((pfrep_right_cancel_second_witness_common_left)=0))))) -> pfrep_left_cancel_second_witness_common_left=pfrep_right_cancel_second_witness_common_left) /\ ((forall pfrep_power_cancel_second_witness_common_right pfrep_left_cancel_second_witness_common_right pfrep_right_cancel_second_witness_common_right. ((exists pfrep_position_cancel_second_witness_common_rightfirst. ((pfrep_position_cancel_second_witness_common_rightfirst+S (pfrep_power_cancel_second_witness_common_right)=(J)) /\ ((((exists ff_h_pfp_cancel_second_witness_common_rightfirstentry. ff_h_pfp_cancel_second_witness_common_rightfirstentry + S (pfrep_left_cancel_second_witness_common_right) = S ((S (pfrep_position_cancel_second_witness_common_rightfirst)) * cc)) /\ exists ff_q_pfp_cancel_second_witness_common_rightfirstentry. cb = ff_q_pfp_cancel_second_witness_common_rightfirstentry * S ((S (pfrep_position_cancel_second_witness_common_rightfirst)) * cc) + (pfrep_left_cancel_second_witness_common_right)))))) \/ (((exists pfrep_gap_cancel_second_witness_common_rightfirstoutside. pfrep_gap_cancel_second_witness_common_rightfirstoutside+(J)=(pfrep_power_cancel_second_witness_common_right)) /\ (((pfrep_left_cancel_second_witness_common_right)=0))))) -> ((exists pfrep_position_cancel_second_witness_common_rightsecond. ((pfrep_position_cancel_second_witness_common_rightsecond+S (pfrep_power_cancel_second_witness_common_right)=(pfaa_length_cancel_second)) /\ ((((exists ff_h_pfp_cancel_second_witness_common_rightsecondentry. ff_h_pfp_cancel_second_witness_common_rightsecondentry + S (pfrep_right_cancel_second_witness_common_right) = S ((S (pfrep_position_cancel_second_witness_common_rightsecond)) * pfaa_right_c_cancel_second)) /\ exists ff_q_pfp_cancel_second_witness_common_rightsecondentry. pfaa_right_b_cancel_second = ff_q_pfp_cancel_second_witness_common_rightsecondentry * S ((S (pfrep_position_cancel_second_witness_common_rightsecond)) * pfaa_right_c_cancel_second) + (pfrep_right_cancel_second_witness_common_right)))))) \/ (((exists pfrep_gap_cancel_second_witness_common_rightsecondoutside. pfrep_gap_cancel_second_witness_common_rightsecondoutside+(pfaa_length_cancel_second)=(pfrep_power_cancel_second_witness_common_right)) /\ (((pfrep_right_cancel_second_witness_common_right)=0))))) -> pfrep_left_cancel_second_witness_common_right=pfrep_right_cancel_second_witness_common_right)))) /\ (((forall pfp_index_cancel_second_witness_operation. (exists pfa_gap_cancel_second_witness_operationindex. pfa_gap_cancel_second_witness_operationindex + S (pfp_index_cancel_second_witness_operation) = (pfaa_length_cancel_second)) -> exists pfp_left_cancel_second_witness_operation pfp_right_cancel_second_witness_operation pfp_value_cancel_second_witness_operation. ((((exists ff_h_pfp_cancel_second_witness_operationleft. ff_h_pfp_cancel_second_witness_operationleft + S (pfp_left_cancel_second_witness_operation) = S ((S (pfp_index_cancel_second_witness_operation)) * pfaa_left_c_cancel_second)) /\ exists ff_q_pfp_cancel_second_witness_operationleft. pfaa_left_b_cancel_second = ff_q_pfp_cancel_second_witness_operationleft * S ((S (pfp_index_cancel_second_witness_operation)) * pfaa_left_c_cancel_second) + (pfp_left_cancel_second_witness_operation))) /\ (((((exists ff_h_pfp_cancel_second_witness_operationright. ff_h_pfp_cancel_second_witness_operationright + S (pfp_right_cancel_second_witness_operation) = S ((S (pfp_index_cancel_second_witness_operation)) * pfaa_right_c_cancel_second)) /\ exists ff_q_pfp_cancel_second_witness_operationright. pfaa_right_b_cancel_second = ff_q_pfp_cancel_second_witness_operationright * S ((S (pfp_index_cancel_second_witness_operation)) * pfaa_right_c_cancel_second) + (pfp_right_cancel_second_witness_operation))) /\ (((((exists ff_h_pfp_cancel_second_witness_operationtarget. ff_h_pfp_cancel_second_witness_operationtarget + S (pfp_value_cancel_second_witness_operation) = S ((S (pfp_index_cancel_second_witness_operation)) * pfaa_sum_c_cancel_second)) /\ exists ff_q_pfp_cancel_second_witness_operationtarget. pfaa_sum_b_cancel_second = ff_q_pfp_cancel_second_witness_operationtarget * S ((S (pfp_index_cancel_second_witness_operation)) * pfaa_sum_c_cancel_second) + (pfp_value_cancel_second_witness_operation))) /\ ((((exists pfa_gap_cancel_second_witness_operationoperationleft. pfa_gap_cancel_second_witness_operationoperationleft + S (pfp_left_cancel_second_witness_operation) = (p)) /\ (((exists pfa_gap_cancel_second_witness_operationoperationright. pfa_gap_cancel_second_witness_operationoperationright + S (pfp_right_cancel_second_witness_operation) = (p)) /\ ((((exists pfa_gap_cancel_second_witness_operationoperationresultbound. pfa_gap_cancel_second_witness_operationoperationresultbound + S (pfp_value_cancel_second_witness_operation) = (p)) /\ ((exists pfa_offset_left_cancel_second_witness_operationoperationresultcongruence pfa_offset_right_cancel_second_witness_operationoperationresultcongruence. ((pfp_left_cancel_second_witness_operation) + (pfp_right_cancel_second_witness_operation)) + (p) * pfa_offset_left_cancel_second_witness_operationoperationresultcongruence = (pfp_value_cancel_second_witness_operation) + (p) * pfa_offset_right_cancel_second_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_cancel_second_witness_output pfrep_left_cancel_second_witness_output pfrep_right_cancel_second_witness_output. ((exists pfrep_position_cancel_second_witness_outputfirst. ((pfrep_position_cancel_second_witness_outputfirst+S (pfrep_power_cancel_second_witness_output)=(pfaa_length_cancel_second)) /\ ((((exists ff_h_pfp_cancel_second_witness_outputfirstentry. ff_h_pfp_cancel_second_witness_outputfirstentry + S (pfrep_left_cancel_second_witness_output) = S ((S (pfrep_position_cancel_second_witness_outputfirst)) * pfaa_sum_c_cancel_second)) /\ exists ff_q_pfp_cancel_second_witness_outputfirstentry. pfaa_sum_b_cancel_second = ff_q_pfp_cancel_second_witness_outputfirstentry * S ((S (pfrep_position_cancel_second_witness_outputfirst)) * pfaa_sum_c_cancel_second) + (pfrep_left_cancel_second_witness_output)))))) \/ (((exists pfrep_gap_cancel_second_witness_outputfirstoutside. pfrep_gap_cancel_second_witness_outputfirstoutside+(pfaa_length_cancel_second)=(pfrep_power_cancel_second_witness_output)) /\ (((pfrep_left_cancel_second_witness_output)=0))))) -> ((exists pfrep_position_cancel_second_witness_outputsecond. ((pfrep_position_cancel_second_witness_outputsecond+S (pfrep_power_cancel_second_witness_output)=(N)) /\ ((((exists ff_h_pfp_cancel_second_witness_outputsecondentry. ff_h_pfp_cancel_second_witness_outputsecondentry + S (pfrep_right_cancel_second_witness_output) = S ((S (pfrep_position_cancel_second_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_cancel_second_witness_outputsecondentry. rb = ff_q_pfp_cancel_second_witness_outputsecondentry * S ((S (pfrep_position_cancel_second_witness_outputsecond)) * rc) + (pfrep_right_cancel_second_witness_output)))))) \/ (((exists pfrep_gap_cancel_second_witness_outputsecondoutside. pfrep_gap_cancel_second_witness_outputsecondoutside+(N)=(pfrep_power_cancel_second_witness_output)) /\ (((pfrep_right_cancel_second_witness_output)=0))))) -> pfrep_left_cancel_second_witness_output=pfrep_right_cancel_second_witness_output))))))))))))) -> (forall pfrep_power_cancel_result pfrep_left_cancel_result pfrep_right_cancel_result. ((exists pfrep_position_cancel_resultfirst. ((pfrep_position_cancel_resultfirst+S (pfrep_power_cancel_result)=(M)) /\ ((((exists ff_h_pfp_cancel_resultfirstentry. ff_h_pfp_cancel_resultfirstentry + S (pfrep_left_cancel_result) = S ((S (pfrep_position_cancel_resultfirst)) * bc)) /\ exists ff_q_pfp_cancel_resultfirstentry. bb = ff_q_pfp_cancel_resultfirstentry * S ((S (pfrep_position_cancel_resultfirst)) * bc) + (pfrep_left_cancel_result)))))) \/ (((exists pfrep_gap_cancel_resultfirstoutside. pfrep_gap_cancel_resultfirstoutside+(M)=(pfrep_power_cancel_result)) /\ (((pfrep_left_cancel_result)=0))))) -> ((exists pfrep_position_cancel_resultsecond. ((pfrep_position_cancel_resultsecond+S (pfrep_power_cancel_result)=(J)) /\ ((((exists ff_h_pfp_cancel_resultsecondentry. ff_h_pfp_cancel_resultsecondentry + S (pfrep_right_cancel_result) = S ((S (pfrep_position_cancel_resultsecond)) * cc)) /\ exists ff_q_pfp_cancel_resultsecondentry. cb = ff_q_pfp_cancel_resultsecondentry * S ((S (pfrep_position_cancel_resultsecond)) * cc) + (pfrep_right_cancel_result)))))) \/ (((exists pfrep_gap_cancel_resultsecondoutside. pfrep_gap_cancel_resultsecondoutside+(J)=(pfrep_power_cancel_result)) /\ (((pfrep_right_cancel_result)=0))))) -> pfrep_left_cancel_result=pfrep_right_cancel_result)

Complete tactic proof in conservative notation

All 279 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

279 script commands · 56 reading checkpoints · 16 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
prime field polynomial aligned add boundedprime field polynomial bounded representative at length existsprime field polynomial aligned add realize
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro cb
  9. L9
    intro cc
  10. L10
    intro J
02Fix variables and assumptionsL11–16

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro rb
  2. L12
    intro rc
  3. L13
    intro N
  4. L14
    intro hp
  5. L15
    intro hb
  6. L16
    intro hc
03Establish hbboundL17–26

Establish this local claim before using it. It is not an additional assumption.

  1. L17
    have hbbound : BetaPrefixInto(ab,ac,L,p) ∧ (BetaPrefixInto(bb,bc,M,p) ∧ BetaPrefixInto(rb,rc,N,p))Definitions: BetaPrefixInto(ab,ac,L,p)BetaPrefixInto(bb,bc,M,p)BetaPrefixInto(rb,rc,N,p)Original native command in the exact edition
  2. L18
    specialize prime_field_polynomial_aligned_add_bounded (p)
  3. L19
    specialize prime_field_polynomial_aligned_add_bounded (ab)
  4. L20
    specialize prime_field_polynomial_aligned_add_bounded (ac)
  5. L21
    specialize prime_field_polynomial_aligned_add_bounded (L)
  6. L22
    specialize prime_field_polynomial_aligned_add_bounded (bb)
  7. L23
    specialize prime_field_polynomial_aligned_add_bounded (bc)
  8. L24
    specialize prime_field_polynomial_aligned_add_bounded (M)
  9. L25
    specialize prime_field_polynomial_aligned_add_bounded (rb)
  10. L26
    specialize prime_field_polynomial_aligned_add_bounded (rc)
04Use earlier factsL27–29

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L27
    specialize prime_field_polynomial_aligned_add_bounded (N)
  2. L28
    apply prime_field_polynomial_aligned_add_bounded
  3. L29
    exact hb
05Separate the logical casesL30–31

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L30
    cases hbbound
  2. L31
    cases hbbound_right
06Establish hcboundL32–41

Establish this local claim before using it. It is not an additional assumption.

  1. L32
    have hcbound : BetaPrefixInto(ab,ac,L,p) ∧ (BetaPrefixInto(cb,cc,J,p) ∧ BetaPrefixInto(rb,rc,N,p))Definitions: BetaPrefixInto(ab,ac,L,p)BetaPrefixInto(cb,cc,J,p)BetaPrefixInto(rb,rc,N,p)Original native command in the exact edition
  2. L33
    specialize prime_field_polynomial_aligned_add_bounded (p)
  3. L34
    specialize prime_field_polynomial_aligned_add_bounded (ab)
  4. L35
    specialize prime_field_polynomial_aligned_add_bounded (ac)
  5. L36
    specialize prime_field_polynomial_aligned_add_bounded (L)
  6. L37
    specialize prime_field_polynomial_aligned_add_bounded (cb)
  7. L38
    specialize prime_field_polynomial_aligned_add_bounded (cc)
  8. L39
    specialize prime_field_polynomial_aligned_add_bounded (J)
  9. L40
    specialize prime_field_polynomial_aligned_add_bounded (rb)
  10. L41
    specialize prime_field_polynomial_aligned_add_bounded (rc)
07Use earlier factsL42–44

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L42
    specialize prime_field_polynomial_aligned_add_bounded (N)
  2. L43
    apply prime_field_polynomial_aligned_add_bounded
  3. L44
    exact hc
08Separate the logical casesL45–46

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L45
    cases hcbound
  2. L46
    cases hcbound_right
09Establish cancel_representative_0L47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial bounded representative at length exists.

  1. L47
    have cancel_representative_0 : ∃ cancel_representative_0_code. ∃ cancel_representative_0_scale. BetaPrefixInto(cancel_representative_0_code,cancel_representative_0_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(ab,ac,L,cancel_representative_0_code,cancel_representative_0_scale,L + (M + (J + N)))Definitions: BetaPrefixInto(cancel_representative_0_code,cancel_representative_0_scale,L + (M + (J + N)),p)PolynomialEquivalent(ab,ac,L,cancel_representative_0_code,cancel_representative_0_scale,L + (M + (J + N)))Original native command in the exact edition
  2. L48
    specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  3. L49
    specialize prime_field_polynomial_bounded_representative_at_length_exists (ab)
  4. L50
    specialize prime_field_polynomial_bounded_representative_at_length_exists (ac)
  5. L51
    specialize prime_field_polynomial_bounded_representative_at_length_exists (L)
  6. L52
    specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  7. L53
    apply prime_field_polynomial_bounded_representative_at_length_exists
  8. L54
    exact hp
  9. L55
    exact hbbound_left
  10. L56
    specialize le_add_right (L)
10Use earlier factsL57–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L57
    specialize le_add_right ((M)+((J)+(N)))
  2. L58
    apply le_add_right
11Separate the logical casesL59–61

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L59
    cases cancel_representative_0
  2. L60
    cases cancel_representative_0_witness
  3. L61
    cases cancel_representative_0_witness_witness
12Establish cancel_representative_1L62–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial bounded representative at length exists.

  1. L62
    have cancel_representative_1 : ∃ cancel_representative_1_code. ∃ cancel_representative_1_scale. BetaPrefixInto(cancel_representative_1_code,cancel_representative_1_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(bb,bc,M,cancel_representative_1_code,cancel_representative_1_scale,L + (M + (J + N)))Definitions: BetaPrefixInto(cancel_representative_1_code,cancel_representative_1_scale,L + (M + (J + N)),p)PolynomialEquivalent(bb,bc,M,cancel_representative_1_code,cancel_representative_1_scale,L + (M + (J + N)))Original native command in the exact edition
  2. L63
    specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  3. L64
    specialize prime_field_polynomial_bounded_representative_at_length_exists (bb)
  4. L65
    specialize prime_field_polynomial_bounded_representative_at_length_exists (bc)
  5. L66
    specialize prime_field_polynomial_bounded_representative_at_length_exists (M)
  6. L67
    specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  7. L68
    apply prime_field_polynomial_bounded_representative_at_length_exists
  8. L69
    exact hp
  9. L70
    exact hbbound_right_left
13Establish length_bound_cancel_representative_1L71–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le add right.

  1. L71
    have length_bound_cancel_representative_1 : Le(M,M + (J + N))Definitions: Le(M,M + (J + N))Original native command in the exact edition
  2. L72
    specialize le_add_right (M)
  3. L73
    specialize le_add_right ((J)+(N))
  4. L74
    apply le_add_right
  5. L75
    specialize le_trans (M)
  6. L76
    specialize le_trans ((M)+((J)+(N)))
  7. L77
    specialize le_trans ((L)+((M)+((J)+(N))))
  8. L78
    apply le_trans
  9. L79
    exact length_bound_cancel_representative_1
14Construct an explicit witnessL80–80

Supply the displayed value, then prove that it has the required property.

  1. L80
    exists L
15Calculate and transport equalitiesL81–81

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L81
    refl
16Separate the logical casesL82–84

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L82
    cases cancel_representative_1
  2. L83
    cases cancel_representative_1_witness
  3. L84
    cases cancel_representative_1_witness_witness
17Establish cancel_representative_2L85–93

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial bounded representative at length exists.

  1. L85
    have cancel_representative_2 : ∃ cancel_representative_2_code. ∃ cancel_representative_2_scale. BetaPrefixInto(cancel_representative_2_code,cancel_representative_2_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(cb,cc,J,cancel_representative_2_code,cancel_representative_2_scale,L + (M + (J + N)))Definitions: BetaPrefixInto(cancel_representative_2_code,cancel_representative_2_scale,L + (M + (J + N)),p)PolynomialEquivalent(cb,cc,J,cancel_representative_2_code,cancel_representative_2_scale,L + (M + (J + N)))Original native command in the exact edition
  2. L86
    specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  3. L87
    specialize prime_field_polynomial_bounded_representative_at_length_exists (cb)
  4. L88
    specialize prime_field_polynomial_bounded_representative_at_length_exists (cc)
  5. L89
    specialize prime_field_polynomial_bounded_representative_at_length_exists (J)
  6. L90
    specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  7. L91
    apply prime_field_polynomial_bounded_representative_at_length_exists
  8. L92
    exact hp
  9. L93
    exact hcbound_right_left
18Establish length_bound_cancel_representative_2L94–94

Establish this local claim before using it. It is not an additional assumption.

  1. L94
    have length_bound_cancel_representative_2 : Le(J,M + (J + N))Definitions: Le(J,M + (J + N))Original native command in the exact edition
19Establish length_bound_cancel_representative_2_innerL95–103

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le add right.

  1. L95
    have length_bound_cancel_representative_2_inner : Le(J,J + N)Definitions: Le(J,J + N)Original native command in the exact edition
  2. L96
    specialize le_add_right (J)
  3. L97
    specialize le_add_right (N)
  4. L98
    apply le_add_right
  5. L99
    specialize le_trans (J)
  6. L100
    specialize le_trans ((J)+(N))
  7. L101
    specialize le_trans ((M)+((J)+(N)))
  8. L102
    apply le_trans
  9. L103
    exact length_bound_cancel_representative_2_inner
20Construct an explicit witnessL104–104

Supply the displayed value, then prove that it has the required property.

  1. L104
    exists M
21Calculate and transport equalitiesL105–105

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L105
    refl
22Use earlier factsL106–110

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L106
    specialize le_trans (J)
  2. L107
    specialize le_trans ((M)+((J)+(N)))
  3. L108
    specialize le_trans ((L)+((M)+((J)+(N))))
  4. L109
    apply le_trans
  5. L110
    exact length_bound_cancel_representative_2
23Construct an explicit witnessL111–111

Supply the displayed value, then prove that it has the required property.

  1. L111
    exists L
24Calculate and transport equalitiesL112–112

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L112
    refl
25Separate the logical casesL113–115

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L113
    cases cancel_representative_2
  2. L114
    cases cancel_representative_2_witness
  3. L115
    cases cancel_representative_2_witness_witness
26Establish cancel_representative_3L116–124

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial bounded representative at length exists.

  1. L116
    have cancel_representative_3 : ∃ cancel_representative_3_code. ∃ cancel_representative_3_scale. BetaPrefixInto(cancel_representative_3_code,cancel_representative_3_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(rb,rc,N,cancel_representative_3_code,cancel_representative_3_scale,L + (M + (J + N)))Definitions: BetaPrefixInto(cancel_representative_3_code,cancel_representative_3_scale,L + (M + (J + N)),p)PolynomialEquivalent(rb,rc,N,cancel_representative_3_code,cancel_representative_3_scale,L + (M + (J + N)))Original native command in the exact edition
  2. L117
    specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  3. L118
    specialize prime_field_polynomial_bounded_representative_at_length_exists (rb)
  4. L119
    specialize prime_field_polynomial_bounded_representative_at_length_exists (rc)
  5. L120
    specialize prime_field_polynomial_bounded_representative_at_length_exists (N)
  6. L121
    specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  7. L122
    apply prime_field_polynomial_bounded_representative_at_length_exists
  8. L123
    exact hp
  9. L124
    exact hbbound_right_right
27Establish length_bound_cancel_representative_3L125–125

Establish this local claim before using it. It is not an additional assumption.

  1. L125
    have length_bound_cancel_representative_3 : Le(N,M + (J + N))Definitions: Le(N,M + (J + N))Original native command in the exact edition
28Establish length_bound_cancel_representative_3_innerL126–126

Establish this local claim before using it. It is not an additional assumption.

  1. L126
    have length_bound_cancel_representative_3_inner : Le(N,J + N)Definitions: Le(N,J + N)Original native command in the exact edition
29Establish length_bound_cancel_representative_3_inner_innerL127–134

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le refl.

  1. L127
    have length_bound_cancel_representative_3_inner_inner : Le(N,N)Definitions: Le(N,N)Original native command in the exact edition
  2. L128
    specialize le_refl (N)
  3. L129
    apply le_refl
  4. L130
    specialize le_trans (N)
  5. L131
    specialize le_trans (N)
  6. L132
    specialize le_trans ((J)+(N))
  7. L133
    apply le_trans
  8. L134
    exact length_bound_cancel_representative_3_inner_inner
30Construct an explicit witnessL135–135

Supply the displayed value, then prove that it has the required property.

  1. L135
    exists J
31Calculate and transport equalitiesL136–136

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L136
    refl
32Use earlier factsL137–141

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L137
    specialize le_trans (N)
  2. L138
    specialize le_trans ((J)+(N))
  3. L139
    specialize le_trans ((M)+((J)+(N)))
  4. L140
    apply le_trans
  5. L141
    exact length_bound_cancel_representative_3_inner
33Construct an explicit witnessL142–142

Supply the displayed value, then prove that it has the required property.

  1. L142
    exists M
34Calculate and transport equalitiesL143–143

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L143
    refl
35Use earlier factsL144–148

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L144
    specialize le_trans (N)
  2. L145
    specialize le_trans ((M)+((J)+(N)))
  3. L146
    specialize le_trans ((L)+((M)+((J)+(N))))
  4. L147
    apply le_trans
  5. L148
    exact length_bound_cancel_representative_3
36Construct an explicit witnessL149–149

Supply the displayed value, then prove that it has the required property.

  1. L149
    exists L
37Calculate and transport equalitiesL150–150

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L150
    refl
38Separate the logical casesL151–153

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L151
    cases cancel_representative_3
  2. L152
    cases cancel_representative_3_witness
  3. L153
    cases cancel_representative_3_witness_witness
39Establish hfirstL154–163

Establish this local claim before using it. It is not an additional assumption.

  1. L154
    have hfirst : FpPolyAdd(p,x,x1,x2,x3,x6,x7,L + (M + (J + N)))Definitions: FpPolyAdd(p,x,x1,x2,x3,x6,x7,L + (M + (J + N)))Original native command in the exact edition
  2. L155
    specialize prime_field_polynomial_aligned_add_realize (p)
  3. L156
    specialize prime_field_polynomial_aligned_add_realize (ab)
  4. L157
    specialize prime_field_polynomial_aligned_add_realize (ac)
  5. L158
    specialize prime_field_polynomial_aligned_add_realize (L)
  6. L159
    specialize prime_field_polynomial_aligned_add_realize (bb)
  7. L160
    specialize prime_field_polynomial_aligned_add_realize (bc)
  8. L161
    specialize prime_field_polynomial_aligned_add_realize (M)
  9. L162
    specialize prime_field_polynomial_aligned_add_realize (rb)
  10. L163
    specialize prime_field_polynomial_aligned_add_realize (rc)
40Use earlier factsL164–173

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L164
    specialize prime_field_polynomial_aligned_add_realize (N)
  2. L165
    specialize prime_field_polynomial_aligned_add_realize (x)
  3. L166
    specialize prime_field_polynomial_aligned_add_realize (x1)
  4. L167
    specialize prime_field_polynomial_aligned_add_realize (x2)
  5. L168
    specialize prime_field_polynomial_aligned_add_realize (x3)
  6. L169
    specialize prime_field_polynomial_aligned_add_realize (x6)
  7. L170
    specialize prime_field_polynomial_aligned_add_realize (x7)
  8. L171
    specialize prime_field_polynomial_aligned_add_realize ((L)+((M)+((J)+(N))))
  9. L172
    apply prime_field_polynomial_aligned_add_realize
  10. L173
    exact hp
41Use earlier factsL174–177

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L174
    exact hb
  2. L175
    exact cancel_representative_0_witness_witness_left
  3. L176
    exact cancel_representative_1_witness_witness_left
  4. L177
    exact cancel_representative_3_witness_witness_left
42Separate the logical casesL178–178

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L178
    split
43Use earlier factsL179–181

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L179
    exact cancel_representative_0_witness_witness_right
  2. L180
    exact cancel_representative_1_witness_witness_right
  3. L181
    exact cancel_representative_3_witness_witness_right
44Establish hsecondL182–191

Establish this local claim before using it. It is not an additional assumption.

  1. L182
    have hsecond : FpPolyAdd(p,x,x1,x4,x5,x6,x7,L + (M + (J + N)))Definitions: FpPolyAdd(p,x,x1,x4,x5,x6,x7,L + (M + (J + N)))Original native command in the exact edition
  2. L183
    specialize prime_field_polynomial_aligned_add_realize (p)
  3. L184
    specialize prime_field_polynomial_aligned_add_realize (ab)
  4. L185
    specialize prime_field_polynomial_aligned_add_realize (ac)
  5. L186
    specialize prime_field_polynomial_aligned_add_realize (L)
  6. L187
    specialize prime_field_polynomial_aligned_add_realize (cb)
  7. L188
    specialize prime_field_polynomial_aligned_add_realize (cc)
  8. L189
    specialize prime_field_polynomial_aligned_add_realize (J)
  9. L190
    specialize prime_field_polynomial_aligned_add_realize (rb)
  10. L191
    specialize prime_field_polynomial_aligned_add_realize (rc)
45Use earlier factsL192–201

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L192
    specialize prime_field_polynomial_aligned_add_realize (N)
  2. L193
    specialize prime_field_polynomial_aligned_add_realize (x)
  3. L194
    specialize prime_field_polynomial_aligned_add_realize (x1)
  4. L195
    specialize prime_field_polynomial_aligned_add_realize (x4)
  5. L196
    specialize prime_field_polynomial_aligned_add_realize (x5)
  6. L197
    specialize prime_field_polynomial_aligned_add_realize (x6)
  7. L198
    specialize prime_field_polynomial_aligned_add_realize (x7)
  8. L199
    specialize prime_field_polynomial_aligned_add_realize ((L)+((M)+((J)+(N))))
  9. L200
    apply prime_field_polynomial_aligned_add_realize
  10. L201
    exact hp
46Use earlier factsL202–205

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L202
    exact hc
  2. L203
    exact cancel_representative_0_witness_witness_left
  3. L204
    exact cancel_representative_2_witness_witness_left
  4. L205
    exact cancel_representative_3_witness_witness_left
47Separate the logical casesL206–206

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L206
    split
48Use earlier factsL207–209

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L207
    exact cancel_representative_0_witness_witness_right
  2. L208
    exact cancel_representative_2_witness_witness_right
  3. L209
    exact cancel_representative_3_witness_witness_right
49Establish heqL210–219

Establish this local claim before using it. It is not an additional assumption.

  1. L210
    have heq : BetaPrefixEqual(x2,x3,x4,x5,L + (M + (J + N)))Definitions: BetaPrefixEqual(x2,x3,x4,x5,L + (M + (J + N)))Original native command in the exact edition
  2. L211
    specialize prime_field_polynomial_subtract_functional (p)
  3. L212
    specialize prime_field_polynomial_subtract_functional (x6)
  4. L213
    specialize prime_field_polynomial_subtract_functional (x7)
  5. L214
    specialize prime_field_polynomial_subtract_functional (x)
  6. L215
    specialize prime_field_polynomial_subtract_functional (x1)
  7. L216
    specialize prime_field_polynomial_subtract_functional (x2)
  8. L217
    specialize prime_field_polynomial_subtract_functional (x3)
  9. L218
    specialize prime_field_polynomial_subtract_functional (x4)
  10. L219
    specialize prime_field_polynomial_subtract_functional (x5)
50Use earlier factsL220–229

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L220
    specialize prime_field_polynomial_subtract_functional ((L)+((M)+((J)+(N))))
  2. L221
    apply prime_field_polynomial_subtract_functional
  3. L222
    specialize prime_field_polynomial_subtract_from_add (p)
  4. L223
    specialize prime_field_polynomial_subtract_from_add (x6)
  5. L224
    specialize prime_field_polynomial_subtract_from_add (x7)
  6. L225
    specialize prime_field_polynomial_subtract_from_add (x)
  7. L226
    specialize prime_field_polynomial_subtract_from_add (x1)
  8. L227
    specialize prime_field_polynomial_subtract_from_add (x2)
  9. L228
    specialize prime_field_polynomial_subtract_from_add (x3)
  10. L229
    specialize prime_field_polynomial_subtract_from_add ((L)+((M)+((J)+(N))))
51Use earlier factsL230–239

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L230
    apply prime_field_polynomial_subtract_from_add
  2. L231
    exact hfirst
  3. L232
    specialize prime_field_polynomial_subtract_from_add (p)
  4. L233
    specialize prime_field_polynomial_subtract_from_add (x6)
  5. L234
    specialize prime_field_polynomial_subtract_from_add (x7)
  6. L235
    specialize prime_field_polynomial_subtract_from_add (x)
  7. L236
    specialize prime_field_polynomial_subtract_from_add (x1)
  8. L237
    specialize prime_field_polynomial_subtract_from_add (x4)
  9. L238
    specialize prime_field_polynomial_subtract_from_add (x5)
  10. L239
    specialize prime_field_polynomial_subtract_from_add ((L)+((M)+((J)+(N))))
52Use earlier factsL240–241

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L240
    apply prime_field_polynomial_subtract_from_add
  2. L241
    exact hsecond
53Establish cancel_middleL242–251

Establish this local claim before using it. It is not an additional assumption.

  1. L242
    have cancel_middle : PolynomialEquivalent(bb,bc,M,x4,x5,L + (M + (J + N)))Definitions: PolynomialEquivalent(bb,bc,M,x4,x5,L + (M + (J + N)))Original native command in the exact edition
  2. L243
    specialize prime_field_polynomial_equivalent_transitive (bb)
  3. L244
    specialize prime_field_polynomial_equivalent_transitive (bc)
  4. L245
    specialize prime_field_polynomial_equivalent_transitive (M)
  5. L246
    specialize prime_field_polynomial_equivalent_transitive (x2)
  6. L247
    specialize prime_field_polynomial_equivalent_transitive (x3)
  7. L248
    specialize prime_field_polynomial_equivalent_transitive ((L)+((M)+((J)+(N))))
  8. L249
    specialize prime_field_polynomial_equivalent_transitive (x4)
  9. L250
    specialize prime_field_polynomial_equivalent_transitive (x5)
  10. L251
    specialize prime_field_polynomial_equivalent_transitive ((L)+((M)+((J)+(N))))
54Use earlier factsL252–261

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L252
    apply prime_field_polynomial_equivalent_transitive
  2. L253
    exact cancel_representative_1_witness_witness_right
  3. L254
    specialize prime_field_polynomial_equal_implies_equivalent (x2)
  4. L255
    specialize prime_field_polynomial_equal_implies_equivalent (x3)
  5. L256
    specialize prime_field_polynomial_equal_implies_equivalent (x4)
  6. L257
    specialize prime_field_polynomial_equal_implies_equivalent (x5)
  7. L258
    specialize prime_field_polynomial_equal_implies_equivalent ((L)+((M)+((J)+(N))))
  8. L259
    apply prime_field_polynomial_equal_implies_equivalent
  9. L260
    exact heq
  10. L261
    specialize prime_field_polynomial_equivalent_transitive (bb)
55Use earlier factsL262–271

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L262
    specialize prime_field_polynomial_equivalent_transitive (bc)
  2. L263
    specialize prime_field_polynomial_equivalent_transitive (M)
  3. L264
    specialize prime_field_polynomial_equivalent_transitive (x4)
  4. L265
    specialize prime_field_polynomial_equivalent_transitive (x5)
  5. L266
    specialize prime_field_polynomial_equivalent_transitive ((L)+((M)+((J)+(N))))
  6. L267
    specialize prime_field_polynomial_equivalent_transitive (cb)
  7. L268
    specialize prime_field_polynomial_equivalent_transitive (cc)
  8. L269
    specialize prime_field_polynomial_equivalent_transitive (J)
  9. L270
    apply prime_field_polynomial_equivalent_transitive
  10. L271
    exact cancel_middle
56Use earlier factsL272–279

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L272
    specialize prime_field_polynomial_equivalent_symmetric (cb)
  2. L273
    specialize prime_field_polynomial_equivalent_symmetric (cc)
  3. L274
    specialize prime_field_polynomial_equivalent_symmetric (J)
  4. L275
    specialize prime_field_polynomial_equivalent_symmetric (x4)
  5. L276
    specialize prime_field_polynomial_equivalent_symmetric (x5)
  6. L277
    specialize prime_field_polynomial_equivalent_symmetric ((L)+((M)+((J)+(N))))
  7. L278
    apply prime_field_polynomial_equivalent_symmetric
  8. L279
    exact cancel_representative_2_witness_witness_right

Library-wide reading audit

Original defined command ledger · 279 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro cb
  9. 0009intro cc
  10. 0010intro J
  11. 0011intro rb
  12. 0012intro rc
  13. 0013intro N
  14. 0014intro hp
  15. 0015intro hb
  16. 0016intro hc
  17. 0017have hbbound : BetaPrefixInto(ab,ac,L,p) ∧ (BetaPrefixInto(bb,bc,M,p) ∧ BetaPrefixInto(rb,rc,N,p))
  18. 0018specialize prime_field_polynomial_aligned_add_bounded (p)
  19. 0019specialize prime_field_polynomial_aligned_add_bounded (ab)
  20. 0020specialize prime_field_polynomial_aligned_add_bounded (ac)
  21. 0021specialize prime_field_polynomial_aligned_add_bounded (L)
  22. 0022specialize prime_field_polynomial_aligned_add_bounded (bb)
  23. 0023specialize prime_field_polynomial_aligned_add_bounded (bc)
  24. 0024specialize prime_field_polynomial_aligned_add_bounded (M)
  25. 0025specialize prime_field_polynomial_aligned_add_bounded (rb)
  26. 0026specialize prime_field_polynomial_aligned_add_bounded (rc)
  27. 0027specialize prime_field_polynomial_aligned_add_bounded (N)
  28. 0028apply prime_field_polynomial_aligned_add_bounded
  29. 0029exact hb
  30. 0030cases hbbound
  31. 0031cases hbbound_right
  32. 0032have hcbound : BetaPrefixInto(ab,ac,L,p) ∧ (BetaPrefixInto(cb,cc,J,p) ∧ BetaPrefixInto(rb,rc,N,p))
  33. 0033specialize prime_field_polynomial_aligned_add_bounded (p)
  34. 0034specialize prime_field_polynomial_aligned_add_bounded (ab)
  35. 0035specialize prime_field_polynomial_aligned_add_bounded (ac)
  36. 0036specialize prime_field_polynomial_aligned_add_bounded (L)
  37. 0037specialize prime_field_polynomial_aligned_add_bounded (cb)
  38. 0038specialize prime_field_polynomial_aligned_add_bounded (cc)
  39. 0039specialize prime_field_polynomial_aligned_add_bounded (J)
  40. 0040specialize prime_field_polynomial_aligned_add_bounded (rb)
  41. 0041specialize prime_field_polynomial_aligned_add_bounded (rc)
  42. 0042specialize prime_field_polynomial_aligned_add_bounded (N)
  43. 0043apply prime_field_polynomial_aligned_add_bounded
  44. 0044exact hc
  45. 0045cases hcbound
  46. 0046cases hcbound_right
  47. 0047have cancel_representative_0 : ∃ cancel_representative_0_code. ∃ cancel_representative_0_scale. BetaPrefixInto(cancel_representative_0_code,cancel_representative_0_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(ab,ac,L,cancel_representative_0_code,cancel_representative_0_scale,L + (M + (J + N)))
  48. 0048specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  49. 0049specialize prime_field_polynomial_bounded_representative_at_length_exists (ab)
  50. 0050specialize prime_field_polynomial_bounded_representative_at_length_exists (ac)
  51. 0051specialize prime_field_polynomial_bounded_representative_at_length_exists (L)
  52. 0052specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  53. 0053apply prime_field_polynomial_bounded_representative_at_length_exists
  54. 0054exact hp
  55. 0055exact hbbound_left
  56. 0056specialize le_add_right (L)
  57. 0057specialize le_add_right ((M)+((J)+(N)))
  58. 0058apply le_add_right
  59. 0059cases cancel_representative_0
  60. 0060cases cancel_representative_0_witness
  61. 0061cases cancel_representative_0_witness_witness
  62. 0062have cancel_representative_1 : ∃ cancel_representative_1_code. ∃ cancel_representative_1_scale. BetaPrefixInto(cancel_representative_1_code,cancel_representative_1_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(bb,bc,M,cancel_representative_1_code,cancel_representative_1_scale,L + (M + (J + N)))
  63. 0063specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  64. 0064specialize prime_field_polynomial_bounded_representative_at_length_exists (bb)
  65. 0065specialize prime_field_polynomial_bounded_representative_at_length_exists (bc)
  66. 0066specialize prime_field_polynomial_bounded_representative_at_length_exists (M)
  67. 0067specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  68. 0068apply prime_field_polynomial_bounded_representative_at_length_exists
  69. 0069exact hp
  70. 0070exact hbbound_right_left
  71. 0071have length_bound_cancel_representative_1 : Le(M,M + (J + N))
  72. 0072specialize le_add_right (M)
  73. 0073specialize le_add_right ((J)+(N))
  74. 0074apply le_add_right
  75. 0075specialize le_trans (M)
  76. 0076specialize le_trans ((M)+((J)+(N)))
  77. 0077specialize le_trans ((L)+((M)+((J)+(N))))
  78. 0078apply le_trans
  79. 0079exact length_bound_cancel_representative_1
  80. 0080exists L
  81. 0081refl
  82. 0082cases cancel_representative_1
  83. 0083cases cancel_representative_1_witness
  84. 0084cases cancel_representative_1_witness_witness
  85. 0085have cancel_representative_2 : ∃ cancel_representative_2_code. ∃ cancel_representative_2_scale. BetaPrefixInto(cancel_representative_2_code,cancel_representative_2_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(cb,cc,J,cancel_representative_2_code,cancel_representative_2_scale,L + (M + (J + N)))
  86. 0086specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  87. 0087specialize prime_field_polynomial_bounded_representative_at_length_exists (cb)
  88. 0088specialize prime_field_polynomial_bounded_representative_at_length_exists (cc)
  89. 0089specialize prime_field_polynomial_bounded_representative_at_length_exists (J)
  90. 0090specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  91. 0091apply prime_field_polynomial_bounded_representative_at_length_exists
  92. 0092exact hp
  93. 0093exact hcbound_right_left
  94. 0094have length_bound_cancel_representative_2 : Le(J,M + (J + N))
  95. 0095have length_bound_cancel_representative_2_inner : Le(J,J + N)
  96. 0096specialize le_add_right (J)
  97. 0097specialize le_add_right (N)
  98. 0098apply le_add_right
  99. 0099specialize le_trans (J)
  100. 0100specialize le_trans ((J)+(N))
  101. 0101specialize le_trans ((M)+((J)+(N)))
  102. 0102apply le_trans
  103. 0103exact length_bound_cancel_representative_2_inner
  104. 0104exists M
  105. 0105refl
  106. 0106specialize le_trans (J)
  107. 0107specialize le_trans ((M)+((J)+(N)))
  108. 0108specialize le_trans ((L)+((M)+((J)+(N))))
  109. 0109apply le_trans
  110. 0110exact length_bound_cancel_representative_2
  111. 0111exists L
  112. 0112refl
  113. 0113cases cancel_representative_2
  114. 0114cases cancel_representative_2_witness
  115. 0115cases cancel_representative_2_witness_witness
  116. 0116have cancel_representative_3 : ∃ cancel_representative_3_code. ∃ cancel_representative_3_scale. BetaPrefixInto(cancel_representative_3_code,cancel_representative_3_scale,L + (M + (J + N)),p) ∧ PolynomialEquivalent(rb,rc,N,cancel_representative_3_code,cancel_representative_3_scale,L + (M + (J + N)))
  117. 0117specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  118. 0118specialize prime_field_polynomial_bounded_representative_at_length_exists (rb)
  119. 0119specialize prime_field_polynomial_bounded_representative_at_length_exists (rc)
  120. 0120specialize prime_field_polynomial_bounded_representative_at_length_exists (N)
  121. 0121specialize prime_field_polynomial_bounded_representative_at_length_exists ((L)+((M)+((J)+(N))))
  122. 0122apply prime_field_polynomial_bounded_representative_at_length_exists
  123. 0123exact hp
  124. 0124exact hbbound_right_right
  125. 0125have length_bound_cancel_representative_3 : Le(N,M + (J + N))
  126. 0126have length_bound_cancel_representative_3_inner : Le(N,J + N)
  127. 0127have length_bound_cancel_representative_3_inner_inner : Le(N,N)
  128. 0128specialize le_refl (N)
  129. 0129apply le_refl
  130. 0130specialize le_trans (N)
  131. 0131specialize le_trans (N)
  132. 0132specialize le_trans ((J)+(N))
  133. 0133apply le_trans
  134. 0134exact length_bound_cancel_representative_3_inner_inner
  135. 0135exists J
  136. 0136refl
  137. 0137specialize le_trans (N)
  138. 0138specialize le_trans ((J)+(N))
  139. 0139specialize le_trans ((M)+((J)+(N)))
  140. 0140apply le_trans
  141. 0141exact length_bound_cancel_representative_3_inner
  142. 0142exists M
  143. 0143refl
  144. 0144specialize le_trans (N)
  145. 0145specialize le_trans ((M)+((J)+(N)))
  146. 0146specialize le_trans ((L)+((M)+((J)+(N))))
  147. 0147apply le_trans
  148. 0148exact length_bound_cancel_representative_3
  149. 0149exists L
  150. 0150refl
  151. 0151cases cancel_representative_3
  152. 0152cases cancel_representative_3_witness
  153. 0153cases cancel_representative_3_witness_witness
  154. 0154have hfirst : FpPolyAdd(p,x,x1,x2,x3,x6,x7,L + (M + (J + N)))
  155. 0155specialize prime_field_polynomial_aligned_add_realize (p)
  156. 0156specialize prime_field_polynomial_aligned_add_realize (ab)
  157. 0157specialize prime_field_polynomial_aligned_add_realize (ac)
  158. 0158specialize prime_field_polynomial_aligned_add_realize (L)
  159. 0159specialize prime_field_polynomial_aligned_add_realize (bb)
  160. 0160specialize prime_field_polynomial_aligned_add_realize (bc)
  161. 0161specialize prime_field_polynomial_aligned_add_realize (M)
  162. 0162specialize prime_field_polynomial_aligned_add_realize (rb)
  163. 0163specialize prime_field_polynomial_aligned_add_realize (rc)
  164. 0164specialize prime_field_polynomial_aligned_add_realize (N)
  165. 0165specialize prime_field_polynomial_aligned_add_realize (x)
  166. 0166specialize prime_field_polynomial_aligned_add_realize (x1)
  167. 0167specialize prime_field_polynomial_aligned_add_realize (x2)
  168. 0168specialize prime_field_polynomial_aligned_add_realize (x3)
  169. 0169specialize prime_field_polynomial_aligned_add_realize (x6)
  170. 0170specialize prime_field_polynomial_aligned_add_realize (x7)
  171. 0171specialize prime_field_polynomial_aligned_add_realize ((L)+((M)+((J)+(N))))
  172. 0172apply prime_field_polynomial_aligned_add_realize
  173. 0173exact hp
  174. 0174exact hb
  175. 0175exact cancel_representative_0_witness_witness_left
  176. 0176exact cancel_representative_1_witness_witness_left
  177. 0177exact cancel_representative_3_witness_witness_left
  178. 0178split
  179. 0179exact cancel_representative_0_witness_witness_right
  180. 0180exact cancel_representative_1_witness_witness_right
  181. 0181exact cancel_representative_3_witness_witness_right
  182. 0182have hsecond : FpPolyAdd(p,x,x1,x4,x5,x6,x7,L + (M + (J + N)))
  183. 0183specialize prime_field_polynomial_aligned_add_realize (p)
  184. 0184specialize prime_field_polynomial_aligned_add_realize (ab)
  185. 0185specialize prime_field_polynomial_aligned_add_realize (ac)
  186. 0186specialize prime_field_polynomial_aligned_add_realize (L)
  187. 0187specialize prime_field_polynomial_aligned_add_realize (cb)
  188. 0188specialize prime_field_polynomial_aligned_add_realize (cc)
  189. 0189specialize prime_field_polynomial_aligned_add_realize (J)
  190. 0190specialize prime_field_polynomial_aligned_add_realize (rb)
  191. 0191specialize prime_field_polynomial_aligned_add_realize (rc)
  192. 0192specialize prime_field_polynomial_aligned_add_realize (N)
  193. 0193specialize prime_field_polynomial_aligned_add_realize (x)
  194. 0194specialize prime_field_polynomial_aligned_add_realize (x1)
  195. 0195specialize prime_field_polynomial_aligned_add_realize (x4)
  196. 0196specialize prime_field_polynomial_aligned_add_realize (x5)
  197. 0197specialize prime_field_polynomial_aligned_add_realize (x6)
  198. 0198specialize prime_field_polynomial_aligned_add_realize (x7)
  199. 0199specialize prime_field_polynomial_aligned_add_realize ((L)+((M)+((J)+(N))))
  200. 0200apply prime_field_polynomial_aligned_add_realize
  201. 0201exact hp
  202. 0202exact hc
  203. 0203exact cancel_representative_0_witness_witness_left
  204. 0204exact cancel_representative_2_witness_witness_left
  205. 0205exact cancel_representative_3_witness_witness_left
  206. 0206split
  207. 0207exact cancel_representative_0_witness_witness_right
  208. 0208exact cancel_representative_2_witness_witness_right
  209. 0209exact cancel_representative_3_witness_witness_right
  210. 0210have heq : BetaPrefixEqual(x2,x3,x4,x5,L + (M + (J + N)))
  211. 0211specialize prime_field_polynomial_subtract_functional (p)
  212. 0212specialize prime_field_polynomial_subtract_functional (x6)
  213. 0213specialize prime_field_polynomial_subtract_functional (x7)
  214. 0214specialize prime_field_polynomial_subtract_functional (x)
  215. 0215specialize prime_field_polynomial_subtract_functional (x1)
  216. 0216specialize prime_field_polynomial_subtract_functional (x2)
  217. 0217specialize prime_field_polynomial_subtract_functional (x3)
  218. 0218specialize prime_field_polynomial_subtract_functional (x4)
  219. 0219specialize prime_field_polynomial_subtract_functional (x5)
  220. 0220specialize prime_field_polynomial_subtract_functional ((L)+((M)+((J)+(N))))
  221. 0221apply prime_field_polynomial_subtract_functional
  222. 0222specialize prime_field_polynomial_subtract_from_add (p)
  223. 0223specialize prime_field_polynomial_subtract_from_add (x6)
  224. 0224specialize prime_field_polynomial_subtract_from_add (x7)
  225. 0225specialize prime_field_polynomial_subtract_from_add (x)
  226. 0226specialize prime_field_polynomial_subtract_from_add (x1)
  227. 0227specialize prime_field_polynomial_subtract_from_add (x2)
  228. 0228specialize prime_field_polynomial_subtract_from_add (x3)
  229. 0229specialize prime_field_polynomial_subtract_from_add ((L)+((M)+((J)+(N))))
  230. 0230apply prime_field_polynomial_subtract_from_add
  231. 0231exact hfirst
  232. 0232specialize prime_field_polynomial_subtract_from_add (p)
  233. 0233specialize prime_field_polynomial_subtract_from_add (x6)
  234. 0234specialize prime_field_polynomial_subtract_from_add (x7)
  235. 0235specialize prime_field_polynomial_subtract_from_add (x)
  236. 0236specialize prime_field_polynomial_subtract_from_add (x1)
  237. 0237specialize prime_field_polynomial_subtract_from_add (x4)
  238. 0238specialize prime_field_polynomial_subtract_from_add (x5)
  239. 0239specialize prime_field_polynomial_subtract_from_add ((L)+((M)+((J)+(N))))
  240. 0240apply prime_field_polynomial_subtract_from_add
  241. 0241exact hsecond
  242. 0242have cancel_middle : PolynomialEquivalent(bb,bc,M,x4,x5,L + (M + (J + N)))
  243. 0243specialize prime_field_polynomial_equivalent_transitive (bb)
  244. 0244specialize prime_field_polynomial_equivalent_transitive (bc)
  245. 0245specialize prime_field_polynomial_equivalent_transitive (M)
  246. 0246specialize prime_field_polynomial_equivalent_transitive (x2)
  247. 0247specialize prime_field_polynomial_equivalent_transitive (x3)
  248. 0248specialize prime_field_polynomial_equivalent_transitive ((L)+((M)+((J)+(N))))
  249. 0249specialize prime_field_polynomial_equivalent_transitive (x4)
  250. 0250specialize prime_field_polynomial_equivalent_transitive (x5)
  251. 0251specialize prime_field_polynomial_equivalent_transitive ((L)+((M)+((J)+(N))))
  252. 0252apply prime_field_polynomial_equivalent_transitive
  253. 0253exact cancel_representative_1_witness_witness_right
  254. 0254specialize prime_field_polynomial_equal_implies_equivalent (x2)
  255. 0255specialize prime_field_polynomial_equal_implies_equivalent (x3)
  256. 0256specialize prime_field_polynomial_equal_implies_equivalent (x4)
  257. 0257specialize prime_field_polynomial_equal_implies_equivalent (x5)
  258. 0258specialize prime_field_polynomial_equal_implies_equivalent ((L)+((M)+((J)+(N))))
  259. 0259apply prime_field_polynomial_equal_implies_equivalent
  260. 0260exact heq
  261. 0261specialize prime_field_polynomial_equivalent_transitive (bb)
  262. 0262specialize prime_field_polynomial_equivalent_transitive (bc)
  263. 0263specialize prime_field_polynomial_equivalent_transitive (M)
  264. 0264specialize prime_field_polynomial_equivalent_transitive (x4)
  265. 0265specialize prime_field_polynomial_equivalent_transitive (x5)
  266. 0266specialize prime_field_polynomial_equivalent_transitive ((L)+((M)+((J)+(N))))
  267. 0267specialize prime_field_polynomial_equivalent_transitive (cb)
  268. 0268specialize prime_field_polynomial_equivalent_transitive (cc)
  269. 0269specialize prime_field_polynomial_equivalent_transitive (J)
  270. 0270apply prime_field_polynomial_equivalent_transitive
  271. 0271exact cancel_middle
  272. 0272specialize prime_field_polynomial_equivalent_symmetric (cb)
  273. 0273specialize prime_field_polynomial_equivalent_symmetric (cc)
  274. 0274specialize prime_field_polynomial_equivalent_symmetric (J)
  275. 0275specialize prime_field_polynomial_equivalent_symmetric (x4)
  276. 0276specialize prime_field_polynomial_equivalent_symmetric (x5)
  277. 0277specialize prime_field_polynomial_equivalent_symmetric ((L)+((M)+((J)+(N))))
  278. 0278apply prime_field_polynomial_equivalent_symmetric
  279. 0279exact cancel_representative_2_witness_witness_right