PG000C

prime_field_polynomial_convolution_shift_right_equivalent

At every nonzero modulus, the actual product with a shifted right factor is formally coefficient-equivalent to every actual shift of the original product, including both empty-factor cases.

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. ∀ N. ∀ BB. ∀ BC. ∀ db. ∀ dc. ∀ K. ∀ eb. ∀ ec. ¬p = 0 → PolynomialShift(bb,bc,M,BB,BC) → FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) → FpPolyProduct(p,ab,ac,L,BB,BC,S M,db,dc,K) → PolynomialShift(cb,cc,N,eb,ec) → PolynomialEquivalent(db,dc,K,eb,ec,S N)

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

Definition DAG

FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2PolynomialEquivalent(b,c,L,d,e,M) · 1PolynomialShift(b,c,L,d,e) · 3Repeat(b,c,a,l) · 6

Actual proof prerequisites

eq_decidable · checked external prerequisiteprime_field_polynomial_convolution_shift_right_emptyprime_field_polynomial_shift_zero_prefixprime_field_polynomial_equivalent_transitive · checked external prerequisiteprime_field_polynomial_zero_prefix_equivalent_empty · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_convolution_shift_right_nonemptyprime_field_polynomial_equal_implies_equivalent · checked external prerequisiteprime_field_polynomial_shift_functional
Original expanded first-order statement 
forall p ab ac L bb bc M cb cc N BB BC db dc K eb ec. (~(p=0)) -> (((forall mdr_i_pfp_shift_equivalent_factorprefix mdr_a_pfp_shift_equivalent_factorprefix. (exists mdr_gap_pfp_shift_equivalent_factorprefixb. mdr_gap_pfp_shift_equivalent_factorprefixb + S (mdr_i_pfp_shift_equivalent_factorprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_equivalent_factorprefixo. ff_h_mdr_pfp_shift_equivalent_factorprefixo + S (mdr_a_pfp_shift_equivalent_factorprefix) = S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_equivalent_factorprefixo. bb = ff_q_mdr_pfp_shift_equivalent_factorprefixo * S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * bc) + (mdr_a_pfp_shift_equivalent_factorprefix))) -> (((exists ff_h_mdr_pfp_shift_equivalent_factorprefixn. ff_h_mdr_pfp_shift_equivalent_factorprefixn + S (mdr_a_pfp_shift_equivalent_factorprefix) = S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_equivalent_factorprefixn. BB = ff_q_mdr_pfp_shift_equivalent_factorprefixn * S ((S (mdr_i_pfp_shift_equivalent_factorprefix)) * BC) + (mdr_a_pfp_shift_equivalent_factorprefix)))) /\ ((((exists ff_h_pfp_shift_equivalent_factorlast. ff_h_pfp_shift_equivalent_factorlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_equivalent_factorlast. BB = ff_q_pfp_shift_equivalent_factorlast * S ((S (M)) * BC) + (0)))))) -> (((forall fom_index_pfp_shift_equivalent_oldleft. (exists fom_gap_pfp_shift_equivalent_oldleft_index_bound. fom_gap_pfp_shift_equivalent_oldleft_index_bound + S (fom_index_pfp_shift_equivalent_oldleft) = L) -> exists fom_value_pfp_shift_equivalent_oldleft. ((((exists fom_beta_height_pfp_shift_equivalent_oldleft_entry. fom_beta_height_pfp_shift_equivalent_oldleft_entry + S (fom_value_pfp_shift_equivalent_oldleft) = S ((S (fom_index_pfp_shift_equivalent_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_equivalent_oldleft_entry. ab = fom_beta_quotient_pfp_shift_equivalent_oldleft_entry * S ((S (fom_index_pfp_shift_equivalent_oldleft)) * ac) + (fom_value_pfp_shift_equivalent_oldleft))) /\ (exists fom_gap_pfp_shift_equivalent_oldleft_value_bound. fom_gap_pfp_shift_equivalent_oldleft_value_bound + S (fom_value_pfp_shift_equivalent_oldleft) = p))) /\ (((forall fom_index_pfp_shift_equivalent_oldright. (exists fom_gap_pfp_shift_equivalent_oldright_index_bound. fom_gap_pfp_shift_equivalent_oldright_index_bound + S (fom_index_pfp_shift_equivalent_oldright) = M) -> exists fom_value_pfp_shift_equivalent_oldright. ((((exists fom_beta_height_pfp_shift_equivalent_oldright_entry. fom_beta_height_pfp_shift_equivalent_oldright_entry + S (fom_value_pfp_shift_equivalent_oldright) = S ((S (fom_index_pfp_shift_equivalent_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_shift_equivalent_oldright_entry. bb = fom_beta_quotient_pfp_shift_equivalent_oldright_entry * S ((S (fom_index_pfp_shift_equivalent_oldright)) * bc) + (fom_value_pfp_shift_equivalent_oldright))) /\ (exists fom_gap_pfp_shift_equivalent_oldright_value_bound. fom_gap_pfp_shift_equivalent_oldright_value_bound + S (fom_value_pfp_shift_equivalent_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_shift_equivalent_oldcoefficients. (exists pfa_gap_shift_equivalent_oldcoefficientsbound. pfa_gap_shift_equivalent_oldcoefficientsbound + S (pfc_index_shift_equivalent_oldcoefficients) = (N)) -> exists pfc_value_shift_equivalent_oldcoefficients. ((((exists ff_h_pfp_shift_equivalent_oldcoefficientsentry. ff_h_pfp_shift_equivalent_oldcoefficientsentry + S (pfc_value_shift_equivalent_oldcoefficients) = S ((S (pfc_index_shift_equivalent_oldcoefficients)) * cc)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientsentry. cb = ff_q_pfp_shift_equivalent_oldcoefficientsentry * S ((S (pfc_index_shift_equivalent_oldcoefficients)) * cc) + (pfc_value_shift_equivalent_oldcoefficients))) /\ ((exists pfc_terms_code_shift_equivalent_oldcoefficientscoefficient pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient. ((forall pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal. (exists pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonalbound. pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonalbound + S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal) = (S (pfc_index_shift_equivalent_oldcoefficients))) -> exists pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry + S (pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_equivalent_oldcoefficientscoefficient = ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient) + (pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm. (((pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)+pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm=(pfc_index_shift_equivalent_oldcoefficients)) /\ ((((((exists pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_equivalent_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_equivalent_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_shift_equivalent_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_equivalent_oldcoefficientscoefficientdiagonal)=pfc_left_shift_equivalent_oldcoefficientscoefficientdiagonalterm*pfc_right_shift_equivalent_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient) = S ((S (S (pfc_index_shift_equivalent_oldcoefficients))) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_equivalent_oldcoefficients))) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient))) /\ forall fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps = S (pfc_index_shift_equivalent_oldcoefficients)) -> exists fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_equivalent_oldcoefficientscoefficient = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_oldcoefficientscoefficient) + (fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_equivalent_oldcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_oldcoefficientscoefficientsum) + (fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_equivalent_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_equivalent_oldcoefficientscoefficientresiduebound. pfa_gap_shift_equivalent_oldcoefficientscoefficientresiduebound + S (pfc_value_shift_equivalent_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_equivalent_oldcoefficientscoefficientresiduecongruence pfa_offset_right_shift_equivalent_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_equivalent_oldcoefficientscoefficient) + (p) * pfa_offset_left_shift_equivalent_oldcoefficientscoefficientresiduecongruence = (pfc_value_shift_equivalent_oldcoefficients) + (p) * pfa_offset_right_shift_equivalent_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_shift_equivalent_newleft. (exists fom_gap_pfp_shift_equivalent_newleft_index_bound. fom_gap_pfp_shift_equivalent_newleft_index_bound + S (fom_index_pfp_shift_equivalent_newleft) = L) -> exists fom_value_pfp_shift_equivalent_newleft. ((((exists fom_beta_height_pfp_shift_equivalent_newleft_entry. fom_beta_height_pfp_shift_equivalent_newleft_entry + S (fom_value_pfp_shift_equivalent_newleft) = S ((S (fom_index_pfp_shift_equivalent_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_equivalent_newleft_entry. ab = fom_beta_quotient_pfp_shift_equivalent_newleft_entry * S ((S (fom_index_pfp_shift_equivalent_newleft)) * ac) + (fom_value_pfp_shift_equivalent_newleft))) /\ (exists fom_gap_pfp_shift_equivalent_newleft_value_bound. fom_gap_pfp_shift_equivalent_newleft_value_bound + S (fom_value_pfp_shift_equivalent_newleft) = p))) /\ (((forall fom_index_pfp_shift_equivalent_newright. (exists fom_gap_pfp_shift_equivalent_newright_index_bound. fom_gap_pfp_shift_equivalent_newright_index_bound + S (fom_index_pfp_shift_equivalent_newright) = S M) -> exists fom_value_pfp_shift_equivalent_newright. ((((exists fom_beta_height_pfp_shift_equivalent_newright_entry. fom_beta_height_pfp_shift_equivalent_newright_entry + S (fom_value_pfp_shift_equivalent_newright) = S ((S (fom_index_pfp_shift_equivalent_newright)) * BC)) /\ exists fom_beta_quotient_pfp_shift_equivalent_newright_entry. BB = fom_beta_quotient_pfp_shift_equivalent_newright_entry * S ((S (fom_index_pfp_shift_equivalent_newright)) * BC) + (fom_value_pfp_shift_equivalent_newright))) /\ (exists fom_gap_pfp_shift_equivalent_newright_value_bound. fom_gap_pfp_shift_equivalent_newright_value_bound + S (fom_value_pfp_shift_equivalent_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_shift_equivalent_newcoefficients. (exists pfa_gap_shift_equivalent_newcoefficientsbound. pfa_gap_shift_equivalent_newcoefficientsbound + S (pfc_index_shift_equivalent_newcoefficients) = (K)) -> exists pfc_value_shift_equivalent_newcoefficients. ((((exists ff_h_pfp_shift_equivalent_newcoefficientsentry. ff_h_pfp_shift_equivalent_newcoefficientsentry + S (pfc_value_shift_equivalent_newcoefficients) = S ((S (pfc_index_shift_equivalent_newcoefficients)) * dc)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientsentry. db = ff_q_pfp_shift_equivalent_newcoefficientsentry * S ((S (pfc_index_shift_equivalent_newcoefficients)) * dc) + (pfc_value_shift_equivalent_newcoefficients))) /\ ((exists pfc_terms_code_shift_equivalent_newcoefficientscoefficient pfc_terms_scale_shift_equivalent_newcoefficientscoefficient pfc_natural_sum_shift_equivalent_newcoefficientscoefficient. ((forall pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal. (exists pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonalbound. pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonalbound + S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal) = (S (pfc_index_shift_equivalent_newcoefficients))) -> exists pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry + S (pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_equivalent_newcoefficientscoefficient = ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient) + (pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm. (((pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)+pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm=(pfc_index_shift_equivalent_newcoefficients)) /\ ((((((exists pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_equivalent_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_equivalent_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_equivalent_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_equivalent_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_equivalent_newcoefficientscoefficientdiagonal)=pfc_left_shift_equivalent_newcoefficientscoefficientdiagonalterm*pfc_right_shift_equivalent_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_equivalent_newcoefficientscoefficient) = S ((S (S (pfc_index_shift_equivalent_newcoefficients))) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_equivalent_newcoefficients))) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (pfc_natural_sum_shift_equivalent_newcoefficientscoefficient))) /\ forall fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps = S (pfc_index_shift_equivalent_newcoefficients)) -> exists fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_equivalent_newcoefficientscoefficient = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_equivalent_newcoefficientscoefficient) + (fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_equivalent_newcoefficientscoefficientsum = fs_q_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_equivalent_newcoefficientscoefficientsum) + (fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_equivalent_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_equivalent_newcoefficientscoefficientresiduebound. pfa_gap_shift_equivalent_newcoefficientscoefficientresiduebound + S (pfc_value_shift_equivalent_newcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_equivalent_newcoefficientscoefficientresiduecongruence pfa_offset_right_shift_equivalent_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_equivalent_newcoefficientscoefficient) + (p) * pfa_offset_left_shift_equivalent_newcoefficientscoefficientresiduecongruence = (pfc_value_shift_equivalent_newcoefficients) + (p) * pfa_offset_right_shift_equivalent_newcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall mdr_i_pfp_shift_equivalent_comparisonprefix mdr_a_pfp_shift_equivalent_comparisonprefix. (exists mdr_gap_pfp_shift_equivalent_comparisonprefixb. mdr_gap_pfp_shift_equivalent_comparisonprefixb + S (mdr_i_pfp_shift_equivalent_comparisonprefix) = (N)) -> (((exists ff_h_mdr_pfp_shift_equivalent_comparisonprefixo. ff_h_mdr_pfp_shift_equivalent_comparisonprefixo + S (mdr_a_pfp_shift_equivalent_comparisonprefix) = S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * cc)) /\ exists ff_q_mdr_pfp_shift_equivalent_comparisonprefixo. cb = ff_q_mdr_pfp_shift_equivalent_comparisonprefixo * S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * cc) + (mdr_a_pfp_shift_equivalent_comparisonprefix))) -> (((exists ff_h_mdr_pfp_shift_equivalent_comparisonprefixn. ff_h_mdr_pfp_shift_equivalent_comparisonprefixn + S (mdr_a_pfp_shift_equivalent_comparisonprefix) = S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * ec)) /\ exists ff_q_mdr_pfp_shift_equivalent_comparisonprefixn. eb = ff_q_mdr_pfp_shift_equivalent_comparisonprefixn * S ((S (mdr_i_pfp_shift_equivalent_comparisonprefix)) * ec) + (mdr_a_pfp_shift_equivalent_comparisonprefix)))) /\ ((((exists ff_h_pfp_shift_equivalent_comparisonlast. ff_h_pfp_shift_equivalent_comparisonlast + S (0) = S ((S (N)) * ec)) /\ exists ff_q_pfp_shift_equivalent_comparisonlast. eb = ff_q_pfp_shift_equivalent_comparisonlast * S ((S (N)) * ec) + (0)))))) -> (forall pfrep_power_shift_equivalent_result pfrep_left_shift_equivalent_result pfrep_right_shift_equivalent_result. ((exists pfrep_position_shift_equivalent_resultfirst. ((pfrep_position_shift_equivalent_resultfirst+S (pfrep_power_shift_equivalent_result)=(K)) /\ ((((exists ff_h_pfp_shift_equivalent_resultfirstentry. ff_h_pfp_shift_equivalent_resultfirstentry + S (pfrep_left_shift_equivalent_result) = S ((S (pfrep_position_shift_equivalent_resultfirst)) * dc)) /\ exists ff_q_pfp_shift_equivalent_resultfirstentry. db = ff_q_pfp_shift_equivalent_resultfirstentry * S ((S (pfrep_position_shift_equivalent_resultfirst)) * dc) + (pfrep_left_shift_equivalent_result)))))) \/ (((exists pfrep_gap_shift_equivalent_resultfirstoutside. pfrep_gap_shift_equivalent_resultfirstoutside+(K)=(pfrep_power_shift_equivalent_result)) /\ (((pfrep_left_shift_equivalent_result)=0))))) -> ((exists pfrep_position_shift_equivalent_resultsecond. ((pfrep_position_shift_equivalent_resultsecond+S (pfrep_power_shift_equivalent_result)=(S N)) /\ ((((exists ff_h_pfp_shift_equivalent_resultsecondentry. ff_h_pfp_shift_equivalent_resultsecondentry + S (pfrep_right_shift_equivalent_result) = S ((S (pfrep_position_shift_equivalent_resultsecond)) * ec)) /\ exists ff_q_pfp_shift_equivalent_resultsecondentry. eb = ff_q_pfp_shift_equivalent_resultsecondentry * S ((S (pfrep_position_shift_equivalent_resultsecond)) * ec) + (pfrep_right_shift_equivalent_result)))))) \/ (((exists pfrep_gap_shift_equivalent_resultsecondoutside. pfrep_gap_shift_equivalent_resultsecondoutside+(S N)=(pfrep_power_shift_equivalent_result)) /\ (((pfrep_right_shift_equivalent_result)=0))))) -> pfrep_left_shift_equivalent_result=pfrep_right_shift_equivalent_result)

Complete tactic proof in conservative notation

All 194 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

194 script commands · 34 reading checkpoints · 7 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 (4)
prime field polynomial convolution shift right emptyprime field polynomial shift zero prefixprime field polynomial convolution shift right nonemptyprime field polynomial shift functional
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 N
02Fix variables and assumptionsL11–20

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

  1. L11
    intro BB
  2. L12
    intro BC
  3. L13
    intro db
  4. L14
    intro dc
  5. L15
    intro K
  6. L16
    intro eb
  7. L17
    intro ec
  8. L18
    intro hp
  9. L19
    intro hs
  10. L20
    intro hc
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hd
  2. L22
    intro he
04Establish hLL23–26

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

  1. L23
    have hL : L=0 \/ ~(L=0)
  2. L24
    specialize eq_decidable (L)
  3. L25
    specialize eq_decidable (0)
  4. L26
    apply eq_decidable
05Separate the logical casesL27–27

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

  1. L27
    cases hL
06Establish hzL28–37

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

  1. L28
    have hz : Repeat(cb,cc,0,N) ∧ Repeat(db,dc,0,K)Definitions: Repeat(cb,cc,0,N)Repeat(db,dc,0,K)Original native command in the exact edition
  2. L29
    specialize prime_field_polynomial_convolution_shift_right_empty (p)
  3. L30
    specialize prime_field_polynomial_convolution_shift_right_empty (ab)
  4. L31
    specialize prime_field_polynomial_convolution_shift_right_empty (ac)
  5. L32
    specialize prime_field_polynomial_convolution_shift_right_empty (L)
  6. L33
    specialize prime_field_polynomial_convolution_shift_right_empty (bb)
  7. L34
    specialize prime_field_polynomial_convolution_shift_right_empty (bc)
  8. L35
    specialize prime_field_polynomial_convolution_shift_right_empty (M)
  9. L36
    specialize prime_field_polynomial_convolution_shift_right_empty (cb)
  10. L37
    specialize prime_field_polynomial_convolution_shift_right_empty (cc)
07Use earlier factsL38–47

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

  1. L38
    specialize prime_field_polynomial_convolution_shift_right_empty (N)
  2. L39
    specialize prime_field_polynomial_convolution_shift_right_empty (BB)
  3. L40
    specialize prime_field_polynomial_convolution_shift_right_empty (BC)
  4. L41
    specialize prime_field_polynomial_convolution_shift_right_empty (db)
  5. L42
    specialize prime_field_polynomial_convolution_shift_right_empty (dc)
  6. L43
    specialize prime_field_polynomial_convolution_shift_right_empty (K)
  7. L44
    apply prime_field_polynomial_convolution_shift_right_empty
  8. L45
    exact hp
  9. L46
    exact hs
  10. L47
    exact hc
08Use earlier factsL48–48

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

  1. L48
    exact hd
09Separate the logical casesL49–49

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

  1. L49
    left
10Use earlier factsL50–50

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

  1. L50
    exact hL_left
11Separate the logical casesL51–51

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

  1. L51
    cases hz
12Establish hezeroL52–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial shift zero prefix.

  1. L52
    have hezero : Repeat(eb,ec,0,S N)Definitions: Repeat(eb,ec,0,S N)Original native command in the exact edition
  2. L53
    specialize prime_field_polynomial_shift_zero_prefix (cb)
  3. L54
    specialize prime_field_polynomial_shift_zero_prefix (cc)
  4. L55
    specialize prime_field_polynomial_shift_zero_prefix (N)
  5. L56
    specialize prime_field_polynomial_shift_zero_prefix (eb)
  6. L57
    specialize prime_field_polynomial_shift_zero_prefix (ec)
  7. L58
    apply prime_field_polynomial_shift_zero_prefix
  8. L59
    exact hz_left
  9. L60
    exact he
  10. L61
    specialize prime_field_polynomial_equivalent_transitive (db)
13Use earlier factsL62–71

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

  1. L62
    specialize prime_field_polynomial_equivalent_transitive (dc)
  2. L63
    specialize prime_field_polynomial_equivalent_transitive (K)
  3. L64
    specialize prime_field_polynomial_equivalent_transitive (0)
  4. L65
    specialize prime_field_polynomial_equivalent_transitive (0)
  5. L66
    specialize prime_field_polynomial_equivalent_transitive (0)
  6. L67
    specialize prime_field_polynomial_equivalent_transitive (eb)
  7. L68
    specialize prime_field_polynomial_equivalent_transitive (ec)
  8. L69
    specialize prime_field_polynomial_equivalent_transitive (S N)
  9. L70
    apply prime_field_polynomial_equivalent_transitive
  10. L71
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (db)
14Use earlier factsL72–81

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

  1. L72
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (dc)
  2. L73
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  3. L74
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  4. L75
    exact hz_right
  5. L76
    specialize prime_field_polynomial_equivalent_symmetric (eb)
  6. L77
    specialize prime_field_polynomial_equivalent_symmetric (ec)
  7. L78
    specialize prime_field_polynomial_equivalent_symmetric (S N)
  8. L79
    specialize prime_field_polynomial_equivalent_symmetric (0)
  9. L80
    specialize prime_field_polynomial_equivalent_symmetric (0)
  10. L81
    specialize prime_field_polynomial_equivalent_symmetric (0)
15Use earlier factsL82–87

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

  1. L82
    apply prime_field_polynomial_equivalent_symmetric
  2. L83
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (eb)
  3. L84
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (ec)
  4. L85
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (S N)
  5. L86
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L87
    exact hezero
16Establish hML88–91

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

  1. L88
    have hM : M=0 \/ ~(M=0)
  2. L89
    specialize eq_decidable (M)
  3. L90
    specialize eq_decidable (0)
  4. L91
    apply eq_decidable
17Separate the logical casesL92–92

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

  1. L92
    cases hM
18Establish hzL93–102

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

  1. L93
    have hz : Repeat(cb,cc,0,N) ∧ Repeat(db,dc,0,K)Definitions: Repeat(cb,cc,0,N)Repeat(db,dc,0,K)Original native command in the exact edition
  2. L94
    specialize prime_field_polynomial_convolution_shift_right_empty (p)
  3. L95
    specialize prime_field_polynomial_convolution_shift_right_empty (ab)
  4. L96
    specialize prime_field_polynomial_convolution_shift_right_empty (ac)
  5. L97
    specialize prime_field_polynomial_convolution_shift_right_empty (L)
  6. L98
    specialize prime_field_polynomial_convolution_shift_right_empty (bb)
  7. L99
    specialize prime_field_polynomial_convolution_shift_right_empty (bc)
  8. L100
    specialize prime_field_polynomial_convolution_shift_right_empty (M)
  9. L101
    specialize prime_field_polynomial_convolution_shift_right_empty (cb)
  10. L102
    specialize prime_field_polynomial_convolution_shift_right_empty (cc)
19Use earlier factsL103–112

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

  1. L103
    specialize prime_field_polynomial_convolution_shift_right_empty (N)
  2. L104
    specialize prime_field_polynomial_convolution_shift_right_empty (BB)
  3. L105
    specialize prime_field_polynomial_convolution_shift_right_empty (BC)
  4. L106
    specialize prime_field_polynomial_convolution_shift_right_empty (db)
  5. L107
    specialize prime_field_polynomial_convolution_shift_right_empty (dc)
  6. L108
    specialize prime_field_polynomial_convolution_shift_right_empty (K)
  7. L109
    apply prime_field_polynomial_convolution_shift_right_empty
  8. L110
    exact hp
  9. L111
    exact hs
  10. L112
    exact hc
20Use earlier factsL113–113

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

  1. L113
    exact hd
21Separate the logical casesL114–114

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

  1. L114
    right
22Use earlier factsL115–115

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

  1. L115
    exact hM_left
23Separate the logical casesL116–116

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

  1. L116
    cases hz
24Establish hezeroL117–126

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial shift zero prefix.

  1. L117
    have hezero : Repeat(eb,ec,0,S N)Definitions: Repeat(eb,ec,0,S N)Original native command in the exact edition
  2. L118
    specialize prime_field_polynomial_shift_zero_prefix (cb)
  3. L119
    specialize prime_field_polynomial_shift_zero_prefix (cc)
  4. L120
    specialize prime_field_polynomial_shift_zero_prefix (N)
  5. L121
    specialize prime_field_polynomial_shift_zero_prefix (eb)
  6. L122
    specialize prime_field_polynomial_shift_zero_prefix (ec)
  7. L123
    apply prime_field_polynomial_shift_zero_prefix
  8. L124
    exact hz_left
  9. L125
    exact he
  10. L126
    specialize prime_field_polynomial_equivalent_transitive (db)
25Use earlier factsL127–136

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

  1. L127
    specialize prime_field_polynomial_equivalent_transitive (dc)
  2. L128
    specialize prime_field_polynomial_equivalent_transitive (K)
  3. L129
    specialize prime_field_polynomial_equivalent_transitive (0)
  4. L130
    specialize prime_field_polynomial_equivalent_transitive (0)
  5. L131
    specialize prime_field_polynomial_equivalent_transitive (0)
  6. L132
    specialize prime_field_polynomial_equivalent_transitive (eb)
  7. L133
    specialize prime_field_polynomial_equivalent_transitive (ec)
  8. L134
    specialize prime_field_polynomial_equivalent_transitive (S N)
  9. L135
    apply prime_field_polynomial_equivalent_transitive
  10. L136
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (db)
26Use earlier factsL137–146

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

  1. L137
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (dc)
  2. L138
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  3. L139
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  4. L140
    exact hz_right
  5. L141
    specialize prime_field_polynomial_equivalent_symmetric (eb)
  6. L142
    specialize prime_field_polynomial_equivalent_symmetric (ec)
  7. L143
    specialize prime_field_polynomial_equivalent_symmetric (S N)
  8. L144
    specialize prime_field_polynomial_equivalent_symmetric (0)
  9. L145
    specialize prime_field_polynomial_equivalent_symmetric (0)
  10. L146
    specialize prime_field_polynomial_equivalent_symmetric (0)
27Use earlier factsL147–152

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

  1. L147
    apply prime_field_polynomial_equivalent_symmetric
  2. L148
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (eb)
  3. L149
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (ec)
  4. L150
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (S N)
  5. L151
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L152
    exact hezero
28Establish hdataL153–162

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

  1. L153
    have hdata : K = S N ∧ PolynomialShift(cb,cc,N,db,dc)Definitions: PolynomialShift(cb,cc,N,db,dc)Original native command in the exact edition
  2. L154
    specialize prime_field_polynomial_convolution_shift_right_nonempty (p)
  3. L155
    specialize prime_field_polynomial_convolution_shift_right_nonempty (ab)
  4. L156
    specialize prime_field_polynomial_convolution_shift_right_nonempty (ac)
  5. L157
    specialize prime_field_polynomial_convolution_shift_right_nonempty (L)
  6. L158
    specialize prime_field_polynomial_convolution_shift_right_nonempty (bb)
  7. L159
    specialize prime_field_polynomial_convolution_shift_right_nonempty (bc)
  8. L160
    specialize prime_field_polynomial_convolution_shift_right_nonempty (M)
  9. L161
    specialize prime_field_polynomial_convolution_shift_right_nonempty (cb)
  10. L162
    specialize prime_field_polynomial_convolution_shift_right_nonempty (cc)
29Use earlier factsL163–172

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

  1. L163
    specialize prime_field_polynomial_convolution_shift_right_nonempty (N)
  2. L164
    specialize prime_field_polynomial_convolution_shift_right_nonempty (BB)
  3. L165
    specialize prime_field_polynomial_convolution_shift_right_nonempty (BC)
  4. L166
    specialize prime_field_polynomial_convolution_shift_right_nonempty (db)
  5. L167
    specialize prime_field_polynomial_convolution_shift_right_nonempty (dc)
  6. L168
    specialize prime_field_polynomial_convolution_shift_right_nonempty (K)
  7. L169
    apply prime_field_polynomial_convolution_shift_right_nonempty
  8. L170
    exact hp
  9. L171
    exact hL_right
  10. L172
    exact hM_right
30Use earlier factsL173–175

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

  1. L173
    exact hs
  2. L174
    exact hc
  3. L175
    exact hd
31Separate the logical casesL176–176

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

  1. L176
    cases hdata
32Calculate and transport equalitiesL177–178

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

  1. L177
    rewrite hdata_left
  2. L178
    rewrite hdata_left
33Use earlier factsL179–188

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

  1. L179
    specialize prime_field_polynomial_equal_implies_equivalent (db)
  2. L180
    specialize prime_field_polynomial_equal_implies_equivalent (dc)
  3. L181
    specialize prime_field_polynomial_equal_implies_equivalent (eb)
  4. L182
    specialize prime_field_polynomial_equal_implies_equivalent (ec)
  5. L183
    specialize prime_field_polynomial_equal_implies_equivalent (S N)
  6. L184
    apply prime_field_polynomial_equal_implies_equivalent
  7. L185
    specialize prime_field_polynomial_shift_functional (cb)
  8. L186
    specialize prime_field_polynomial_shift_functional (cc)
  9. L187
    specialize prime_field_polynomial_shift_functional (N)
  10. L188
    specialize prime_field_polynomial_shift_functional (db)
34Use earlier factsL189–194

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

  1. L189
    specialize prime_field_polynomial_shift_functional (dc)
  2. L190
    specialize prime_field_polynomial_shift_functional (eb)
  3. L191
    specialize prime_field_polynomial_shift_functional (ec)
  4. L192
    apply prime_field_polynomial_shift_functional
  5. L193
    exact hdata_right
  6. L194
    exact he

Library-wide reading audit

Original defined command ledger · 194 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 N
  11. 0011intro BB
  12. 0012intro BC
  13. 0013intro db
  14. 0014intro dc
  15. 0015intro K
  16. 0016intro eb
  17. 0017intro ec
  18. 0018intro hp
  19. 0019intro hs
  20. 0020intro hc
  21. 0021intro hd
  22. 0022intro he
  23. 0023have hL : L=0 \/ ~(L=0)
  24. 0024specialize eq_decidable (L)
  25. 0025specialize eq_decidable (0)
  26. 0026apply eq_decidable
  27. 0027cases hL
  28. 0028have hz : Repeat(cb,cc,0,N) ∧ Repeat(db,dc,0,K)
  29. 0029specialize prime_field_polynomial_convolution_shift_right_empty (p)
  30. 0030specialize prime_field_polynomial_convolution_shift_right_empty (ab)
  31. 0031specialize prime_field_polynomial_convolution_shift_right_empty (ac)
  32. 0032specialize prime_field_polynomial_convolution_shift_right_empty (L)
  33. 0033specialize prime_field_polynomial_convolution_shift_right_empty (bb)
  34. 0034specialize prime_field_polynomial_convolution_shift_right_empty (bc)
  35. 0035specialize prime_field_polynomial_convolution_shift_right_empty (M)
  36. 0036specialize prime_field_polynomial_convolution_shift_right_empty (cb)
  37. 0037specialize prime_field_polynomial_convolution_shift_right_empty (cc)
  38. 0038specialize prime_field_polynomial_convolution_shift_right_empty (N)
  39. 0039specialize prime_field_polynomial_convolution_shift_right_empty (BB)
  40. 0040specialize prime_field_polynomial_convolution_shift_right_empty (BC)
  41. 0041specialize prime_field_polynomial_convolution_shift_right_empty (db)
  42. 0042specialize prime_field_polynomial_convolution_shift_right_empty (dc)
  43. 0043specialize prime_field_polynomial_convolution_shift_right_empty (K)
  44. 0044apply prime_field_polynomial_convolution_shift_right_empty
  45. 0045exact hp
  46. 0046exact hs
  47. 0047exact hc
  48. 0048exact hd
  49. 0049left
  50. 0050exact hL_left
  51. 0051cases hz
  52. 0052have hezero : Repeat(eb,ec,0,S N)
  53. 0053specialize prime_field_polynomial_shift_zero_prefix (cb)
  54. 0054specialize prime_field_polynomial_shift_zero_prefix (cc)
  55. 0055specialize prime_field_polynomial_shift_zero_prefix (N)
  56. 0056specialize prime_field_polynomial_shift_zero_prefix (eb)
  57. 0057specialize prime_field_polynomial_shift_zero_prefix (ec)
  58. 0058apply prime_field_polynomial_shift_zero_prefix
  59. 0059exact hz_left
  60. 0060exact he
  61. 0061specialize prime_field_polynomial_equivalent_transitive (db)
  62. 0062specialize prime_field_polynomial_equivalent_transitive (dc)
  63. 0063specialize prime_field_polynomial_equivalent_transitive (K)
  64. 0064specialize prime_field_polynomial_equivalent_transitive (0)
  65. 0065specialize prime_field_polynomial_equivalent_transitive (0)
  66. 0066specialize prime_field_polynomial_equivalent_transitive (0)
  67. 0067specialize prime_field_polynomial_equivalent_transitive (eb)
  68. 0068specialize prime_field_polynomial_equivalent_transitive (ec)
  69. 0069specialize prime_field_polynomial_equivalent_transitive (S N)
  70. 0070apply prime_field_polynomial_equivalent_transitive
  71. 0071specialize prime_field_polynomial_zero_prefix_equivalent_empty (db)
  72. 0072specialize prime_field_polynomial_zero_prefix_equivalent_empty (dc)
  73. 0073specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  74. 0074apply prime_field_polynomial_zero_prefix_equivalent_empty
  75. 0075exact hz_right
  76. 0076specialize prime_field_polynomial_equivalent_symmetric (eb)
  77. 0077specialize prime_field_polynomial_equivalent_symmetric (ec)
  78. 0078specialize prime_field_polynomial_equivalent_symmetric (S N)
  79. 0079specialize prime_field_polynomial_equivalent_symmetric (0)
  80. 0080specialize prime_field_polynomial_equivalent_symmetric (0)
  81. 0081specialize prime_field_polynomial_equivalent_symmetric (0)
  82. 0082apply prime_field_polynomial_equivalent_symmetric
  83. 0083specialize prime_field_polynomial_zero_prefix_equivalent_empty (eb)
  84. 0084specialize prime_field_polynomial_zero_prefix_equivalent_empty (ec)
  85. 0085specialize prime_field_polynomial_zero_prefix_equivalent_empty (S N)
  86. 0086apply prime_field_polynomial_zero_prefix_equivalent_empty
  87. 0087exact hezero
  88. 0088have hM : M=0 \/ ~(M=0)
  89. 0089specialize eq_decidable (M)
  90. 0090specialize eq_decidable (0)
  91. 0091apply eq_decidable
  92. 0092cases hM
  93. 0093have hz : Repeat(cb,cc,0,N) ∧ Repeat(db,dc,0,K)
  94. 0094specialize prime_field_polynomial_convolution_shift_right_empty (p)
  95. 0095specialize prime_field_polynomial_convolution_shift_right_empty (ab)
  96. 0096specialize prime_field_polynomial_convolution_shift_right_empty (ac)
  97. 0097specialize prime_field_polynomial_convolution_shift_right_empty (L)
  98. 0098specialize prime_field_polynomial_convolution_shift_right_empty (bb)
  99. 0099specialize prime_field_polynomial_convolution_shift_right_empty (bc)
  100. 0100specialize prime_field_polynomial_convolution_shift_right_empty (M)
  101. 0101specialize prime_field_polynomial_convolution_shift_right_empty (cb)
  102. 0102specialize prime_field_polynomial_convolution_shift_right_empty (cc)
  103. 0103specialize prime_field_polynomial_convolution_shift_right_empty (N)
  104. 0104specialize prime_field_polynomial_convolution_shift_right_empty (BB)
  105. 0105specialize prime_field_polynomial_convolution_shift_right_empty (BC)
  106. 0106specialize prime_field_polynomial_convolution_shift_right_empty (db)
  107. 0107specialize prime_field_polynomial_convolution_shift_right_empty (dc)
  108. 0108specialize prime_field_polynomial_convolution_shift_right_empty (K)
  109. 0109apply prime_field_polynomial_convolution_shift_right_empty
  110. 0110exact hp
  111. 0111exact hs
  112. 0112exact hc
  113. 0113exact hd
  114. 0114right
  115. 0115exact hM_left
  116. 0116cases hz
  117. 0117have hezero : Repeat(eb,ec,0,S N)
  118. 0118specialize prime_field_polynomial_shift_zero_prefix (cb)
  119. 0119specialize prime_field_polynomial_shift_zero_prefix (cc)
  120. 0120specialize prime_field_polynomial_shift_zero_prefix (N)
  121. 0121specialize prime_field_polynomial_shift_zero_prefix (eb)
  122. 0122specialize prime_field_polynomial_shift_zero_prefix (ec)
  123. 0123apply prime_field_polynomial_shift_zero_prefix
  124. 0124exact hz_left
  125. 0125exact he
  126. 0126specialize prime_field_polynomial_equivalent_transitive (db)
  127. 0127specialize prime_field_polynomial_equivalent_transitive (dc)
  128. 0128specialize prime_field_polynomial_equivalent_transitive (K)
  129. 0129specialize prime_field_polynomial_equivalent_transitive (0)
  130. 0130specialize prime_field_polynomial_equivalent_transitive (0)
  131. 0131specialize prime_field_polynomial_equivalent_transitive (0)
  132. 0132specialize prime_field_polynomial_equivalent_transitive (eb)
  133. 0133specialize prime_field_polynomial_equivalent_transitive (ec)
  134. 0134specialize prime_field_polynomial_equivalent_transitive (S N)
  135. 0135apply prime_field_polynomial_equivalent_transitive
  136. 0136specialize prime_field_polynomial_zero_prefix_equivalent_empty (db)
  137. 0137specialize prime_field_polynomial_zero_prefix_equivalent_empty (dc)
  138. 0138specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  139. 0139apply prime_field_polynomial_zero_prefix_equivalent_empty
  140. 0140exact hz_right
  141. 0141specialize prime_field_polynomial_equivalent_symmetric (eb)
  142. 0142specialize prime_field_polynomial_equivalent_symmetric (ec)
  143. 0143specialize prime_field_polynomial_equivalent_symmetric (S N)
  144. 0144specialize prime_field_polynomial_equivalent_symmetric (0)
  145. 0145specialize prime_field_polynomial_equivalent_symmetric (0)
  146. 0146specialize prime_field_polynomial_equivalent_symmetric (0)
  147. 0147apply prime_field_polynomial_equivalent_symmetric
  148. 0148specialize prime_field_polynomial_zero_prefix_equivalent_empty (eb)
  149. 0149specialize prime_field_polynomial_zero_prefix_equivalent_empty (ec)
  150. 0150specialize prime_field_polynomial_zero_prefix_equivalent_empty (S N)
  151. 0151apply prime_field_polynomial_zero_prefix_equivalent_empty
  152. 0152exact hezero
  153. 0153have hdata : K = S N ∧ PolynomialShift(cb,cc,N,db,dc)
  154. 0154specialize prime_field_polynomial_convolution_shift_right_nonempty (p)
  155. 0155specialize prime_field_polynomial_convolution_shift_right_nonempty (ab)
  156. 0156specialize prime_field_polynomial_convolution_shift_right_nonempty (ac)
  157. 0157specialize prime_field_polynomial_convolution_shift_right_nonempty (L)
  158. 0158specialize prime_field_polynomial_convolution_shift_right_nonempty (bb)
  159. 0159specialize prime_field_polynomial_convolution_shift_right_nonempty (bc)
  160. 0160specialize prime_field_polynomial_convolution_shift_right_nonempty (M)
  161. 0161specialize prime_field_polynomial_convolution_shift_right_nonempty (cb)
  162. 0162specialize prime_field_polynomial_convolution_shift_right_nonempty (cc)
  163. 0163specialize prime_field_polynomial_convolution_shift_right_nonempty (N)
  164. 0164specialize prime_field_polynomial_convolution_shift_right_nonempty (BB)
  165. 0165specialize prime_field_polynomial_convolution_shift_right_nonempty (BC)
  166. 0166specialize prime_field_polynomial_convolution_shift_right_nonempty (db)
  167. 0167specialize prime_field_polynomial_convolution_shift_right_nonempty (dc)
  168. 0168specialize prime_field_polynomial_convolution_shift_right_nonempty (K)
  169. 0169apply prime_field_polynomial_convolution_shift_right_nonempty
  170. 0170exact hp
  171. 0171exact hL_right
  172. 0172exact hM_right
  173. 0173exact hs
  174. 0174exact hc
  175. 0175exact hd
  176. 0176cases hdata
  177. 0177rewrite hdata_left
  178. 0178rewrite hdata_left
  179. 0179specialize prime_field_polynomial_equal_implies_equivalent (db)
  180. 0180specialize prime_field_polynomial_equal_implies_equivalent (dc)
  181. 0181specialize prime_field_polynomial_equal_implies_equivalent (eb)
  182. 0182specialize prime_field_polynomial_equal_implies_equivalent (ec)
  183. 0183specialize prime_field_polynomial_equal_implies_equivalent (S N)
  184. 0184apply prime_field_polynomial_equal_implies_equivalent
  185. 0185specialize prime_field_polynomial_shift_functional (cb)
  186. 0186specialize prime_field_polynomial_shift_functional (cc)
  187. 0187specialize prime_field_polynomial_shift_functional (N)
  188. 0188specialize prime_field_polynomial_shift_functional (db)
  189. 0189specialize prime_field_polynomial_shift_functional (dc)
  190. 0190specialize prime_field_polynomial_shift_functional (eb)
  191. 0191specialize prime_field_polynomial_shift_functional (ec)
  192. 0192apply prime_field_polynomial_shift_functional
  193. 0193exact hdata_right
  194. 0194exact he