PG0060

prime_field_polynomial_aligned_add_empty_right

Construct a real zero prefix at the input length and its formal equivalence to the empty polynomial, giving an actual aligned right-zero sum for every canonical input.

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. ∀ A. Prime(p) → BetaPrefixInto(ab,ac,A,p) → FpPolynomialAlignedAdd(p,ab,ac,A,0,0,0,ab,ac,A)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 1Prime(p) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

beta_repeat_exists · checked external prerequisiteprime_field_polynomial_aligned_add_from_commonmatrix_rank_bounded_prefix_empty · checked external prerequisiteprime_field_polynomial_power_coefficient_functional · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_zero_prefix_equivalent_empty · checked external prerequisiteprime_field_polynomial_add_zero_right · checked external prerequisite
Original expanded first-order statement 
forall p ab ac A. (~((p) = 1) /\ forall pfa_factor_left_empty_add_prime pfa_factor_right_empty_add_prime. (p) = pfa_factor_left_empty_add_prime * pfa_factor_right_empty_add_prime -> pfa_factor_left_empty_add_prime = 1 \/ pfa_factor_right_empty_add_prime = 1) -> (forall fom_index_pfp_empty_add_bound. (exists fom_gap_pfp_empty_add_bound_index_bound. fom_gap_pfp_empty_add_bound_index_bound + S (fom_index_pfp_empty_add_bound) = A) -> exists fom_value_pfp_empty_add_bound. ((((exists fom_beta_height_pfp_empty_add_bound_entry. fom_beta_height_pfp_empty_add_bound_entry + S (fom_value_pfp_empty_add_bound) = S ((S (fom_index_pfp_empty_add_bound)) * ac)) /\ exists fom_beta_quotient_pfp_empty_add_bound_entry. ab = fom_beta_quotient_pfp_empty_add_bound_entry * S ((S (fom_index_pfp_empty_add_bound)) * ac) + (fom_value_pfp_empty_add_bound))) /\ (exists fom_gap_pfp_empty_add_bound_value_bound. fom_gap_pfp_empty_add_bound_value_bound + S (fom_value_pfp_empty_add_bound) = p))) -> (((forall fom_index_pfp_empty_add_result_left_bounded. (exists fom_gap_pfp_empty_add_result_left_bounded_index_bound. fom_gap_pfp_empty_add_result_left_bounded_index_bound + S (fom_index_pfp_empty_add_result_left_bounded) = A) -> exists fom_value_pfp_empty_add_result_left_bounded. ((((exists fom_beta_height_pfp_empty_add_result_left_bounded_entry. fom_beta_height_pfp_empty_add_result_left_bounded_entry + S (fom_value_pfp_empty_add_result_left_bounded) = S ((S (fom_index_pfp_empty_add_result_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_empty_add_result_left_bounded_entry. ab = fom_beta_quotient_pfp_empty_add_result_left_bounded_entry * S ((S (fom_index_pfp_empty_add_result_left_bounded)) * ac) + (fom_value_pfp_empty_add_result_left_bounded))) /\ (exists fom_gap_pfp_empty_add_result_left_bounded_value_bound. fom_gap_pfp_empty_add_result_left_bounded_value_bound + S (fom_value_pfp_empty_add_result_left_bounded) = p))) /\ (((forall fom_index_pfp_empty_add_result_right_bounded. (exists fom_gap_pfp_empty_add_result_right_bounded_index_bound. fom_gap_pfp_empty_add_result_right_bounded_index_bound + S (fom_index_pfp_empty_add_result_right_bounded) = 0) -> exists fom_value_pfp_empty_add_result_right_bounded. ((((exists fom_beta_height_pfp_empty_add_result_right_bounded_entry. fom_beta_height_pfp_empty_add_result_right_bounded_entry + S (fom_value_pfp_empty_add_result_right_bounded) = S ((S (fom_index_pfp_empty_add_result_right_bounded)) * 0)) /\ exists fom_beta_quotient_pfp_empty_add_result_right_bounded_entry. 0 = fom_beta_quotient_pfp_empty_add_result_right_bounded_entry * S ((S (fom_index_pfp_empty_add_result_right_bounded)) * 0) + (fom_value_pfp_empty_add_result_right_bounded))) /\ (exists fom_gap_pfp_empty_add_result_right_bounded_value_bound. fom_gap_pfp_empty_add_result_right_bounded_value_bound + S (fom_value_pfp_empty_add_result_right_bounded) = p))) /\ (((forall fom_index_pfp_empty_add_result_result_bounded. (exists fom_gap_pfp_empty_add_result_result_bounded_index_bound. fom_gap_pfp_empty_add_result_result_bounded_index_bound + S (fom_index_pfp_empty_add_result_result_bounded) = A) -> exists fom_value_pfp_empty_add_result_result_bounded. ((((exists fom_beta_height_pfp_empty_add_result_result_bounded_entry. fom_beta_height_pfp_empty_add_result_result_bounded_entry + S (fom_value_pfp_empty_add_result_result_bounded) = S ((S (fom_index_pfp_empty_add_result_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_empty_add_result_result_bounded_entry. ab = fom_beta_quotient_pfp_empty_add_result_result_bounded_entry * S ((S (fom_index_pfp_empty_add_result_result_bounded)) * ac) + (fom_value_pfp_empty_add_result_result_bounded))) /\ (exists fom_gap_pfp_empty_add_result_result_bounded_value_bound. fom_gap_pfp_empty_add_result_result_bounded_value_bound + S (fom_value_pfp_empty_add_result_result_bounded) = p))) /\ ((exists pfaa_left_b_empty_add_result pfaa_left_c_empty_add_result pfaa_right_b_empty_add_result pfaa_right_c_empty_add_result pfaa_sum_b_empty_add_result pfaa_sum_c_empty_add_result pfaa_length_empty_add_result. ((((forall pfrep_power_empty_add_result_witness_common_left pfrep_left_empty_add_result_witness_common_left pfrep_right_empty_add_result_witness_common_left. ((exists pfrep_position_empty_add_result_witness_common_leftfirst. ((pfrep_position_empty_add_result_witness_common_leftfirst+S (pfrep_power_empty_add_result_witness_common_left)=(A)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_leftfirstentry. ff_h_pfp_empty_add_result_witness_common_leftfirstentry + S (pfrep_left_empty_add_result_witness_common_left) = S ((S (pfrep_position_empty_add_result_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_empty_add_result_witness_common_leftfirstentry. ab = ff_q_pfp_empty_add_result_witness_common_leftfirstentry * S ((S (pfrep_position_empty_add_result_witness_common_leftfirst)) * ac) + (pfrep_left_empty_add_result_witness_common_left)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_leftfirstoutside. pfrep_gap_empty_add_result_witness_common_leftfirstoutside+(A)=(pfrep_power_empty_add_result_witness_common_left)) /\ (((pfrep_left_empty_add_result_witness_common_left)=0))))) -> ((exists pfrep_position_empty_add_result_witness_common_leftsecond. ((pfrep_position_empty_add_result_witness_common_leftsecond+S (pfrep_power_empty_add_result_witness_common_left)=(pfaa_length_empty_add_result)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_leftsecondentry. ff_h_pfp_empty_add_result_witness_common_leftsecondentry + S (pfrep_right_empty_add_result_witness_common_left) = S ((S (pfrep_position_empty_add_result_witness_common_leftsecond)) * pfaa_left_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_common_leftsecondentry. pfaa_left_b_empty_add_result = ff_q_pfp_empty_add_result_witness_common_leftsecondentry * S ((S (pfrep_position_empty_add_result_witness_common_leftsecond)) * pfaa_left_c_empty_add_result) + (pfrep_right_empty_add_result_witness_common_left)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_leftsecondoutside. pfrep_gap_empty_add_result_witness_common_leftsecondoutside+(pfaa_length_empty_add_result)=(pfrep_power_empty_add_result_witness_common_left)) /\ (((pfrep_right_empty_add_result_witness_common_left)=0))))) -> pfrep_left_empty_add_result_witness_common_left=pfrep_right_empty_add_result_witness_common_left) /\ ((forall pfrep_power_empty_add_result_witness_common_right pfrep_left_empty_add_result_witness_common_right pfrep_right_empty_add_result_witness_common_right. ((exists pfrep_position_empty_add_result_witness_common_rightfirst. ((pfrep_position_empty_add_result_witness_common_rightfirst+S (pfrep_power_empty_add_result_witness_common_right)=(0)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_rightfirstentry. ff_h_pfp_empty_add_result_witness_common_rightfirstentry + S (pfrep_left_empty_add_result_witness_common_right) = S ((S (pfrep_position_empty_add_result_witness_common_rightfirst)) * 0)) /\ exists ff_q_pfp_empty_add_result_witness_common_rightfirstentry. 0 = ff_q_pfp_empty_add_result_witness_common_rightfirstentry * S ((S (pfrep_position_empty_add_result_witness_common_rightfirst)) * 0) + (pfrep_left_empty_add_result_witness_common_right)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_rightfirstoutside. pfrep_gap_empty_add_result_witness_common_rightfirstoutside+(0)=(pfrep_power_empty_add_result_witness_common_right)) /\ (((pfrep_left_empty_add_result_witness_common_right)=0))))) -> ((exists pfrep_position_empty_add_result_witness_common_rightsecond. ((pfrep_position_empty_add_result_witness_common_rightsecond+S (pfrep_power_empty_add_result_witness_common_right)=(pfaa_length_empty_add_result)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_rightsecondentry. ff_h_pfp_empty_add_result_witness_common_rightsecondentry + S (pfrep_right_empty_add_result_witness_common_right) = S ((S (pfrep_position_empty_add_result_witness_common_rightsecond)) * pfaa_right_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_common_rightsecondentry. pfaa_right_b_empty_add_result = ff_q_pfp_empty_add_result_witness_common_rightsecondentry * S ((S (pfrep_position_empty_add_result_witness_common_rightsecond)) * pfaa_right_c_empty_add_result) + (pfrep_right_empty_add_result_witness_common_right)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_rightsecondoutside. pfrep_gap_empty_add_result_witness_common_rightsecondoutside+(pfaa_length_empty_add_result)=(pfrep_power_empty_add_result_witness_common_right)) /\ (((pfrep_right_empty_add_result_witness_common_right)=0))))) -> pfrep_left_empty_add_result_witness_common_right=pfrep_right_empty_add_result_witness_common_right)))) /\ (((forall pfp_index_empty_add_result_witness_operation. (exists pfa_gap_empty_add_result_witness_operationindex. pfa_gap_empty_add_result_witness_operationindex + S (pfp_index_empty_add_result_witness_operation) = (pfaa_length_empty_add_result)) -> exists pfp_left_empty_add_result_witness_operation pfp_right_empty_add_result_witness_operation pfp_value_empty_add_result_witness_operation. ((((exists ff_h_pfp_empty_add_result_witness_operationleft. ff_h_pfp_empty_add_result_witness_operationleft + S (pfp_left_empty_add_result_witness_operation) = S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_left_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_operationleft. pfaa_left_b_empty_add_result = ff_q_pfp_empty_add_result_witness_operationleft * S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_left_c_empty_add_result) + (pfp_left_empty_add_result_witness_operation))) /\ (((((exists ff_h_pfp_empty_add_result_witness_operationright. ff_h_pfp_empty_add_result_witness_operationright + S (pfp_right_empty_add_result_witness_operation) = S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_right_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_operationright. pfaa_right_b_empty_add_result = ff_q_pfp_empty_add_result_witness_operationright * S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_right_c_empty_add_result) + (pfp_right_empty_add_result_witness_operation))) /\ (((((exists ff_h_pfp_empty_add_result_witness_operationtarget. ff_h_pfp_empty_add_result_witness_operationtarget + S (pfp_value_empty_add_result_witness_operation) = S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_sum_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_operationtarget. pfaa_sum_b_empty_add_result = ff_q_pfp_empty_add_result_witness_operationtarget * S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_sum_c_empty_add_result) + (pfp_value_empty_add_result_witness_operation))) /\ ((((exists pfa_gap_empty_add_result_witness_operationoperationleft. pfa_gap_empty_add_result_witness_operationoperationleft + S (pfp_left_empty_add_result_witness_operation) = (p)) /\ (((exists pfa_gap_empty_add_result_witness_operationoperationright. pfa_gap_empty_add_result_witness_operationoperationright + S (pfp_right_empty_add_result_witness_operation) = (p)) /\ ((((exists pfa_gap_empty_add_result_witness_operationoperationresultbound. pfa_gap_empty_add_result_witness_operationoperationresultbound + S (pfp_value_empty_add_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_empty_add_result_witness_operationoperationresultcongruence pfa_offset_right_empty_add_result_witness_operationoperationresultcongruence. ((pfp_left_empty_add_result_witness_operation) + (pfp_right_empty_add_result_witness_operation)) + (p) * pfa_offset_left_empty_add_result_witness_operationoperationresultcongruence = (pfp_value_empty_add_result_witness_operation) + (p) * pfa_offset_right_empty_add_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_empty_add_result_witness_output pfrep_left_empty_add_result_witness_output pfrep_right_empty_add_result_witness_output. ((exists pfrep_position_empty_add_result_witness_outputfirst. ((pfrep_position_empty_add_result_witness_outputfirst+S (pfrep_power_empty_add_result_witness_output)=(pfaa_length_empty_add_result)) /\ ((((exists ff_h_pfp_empty_add_result_witness_outputfirstentry. ff_h_pfp_empty_add_result_witness_outputfirstentry + S (pfrep_left_empty_add_result_witness_output) = S ((S (pfrep_position_empty_add_result_witness_outputfirst)) * pfaa_sum_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_outputfirstentry. pfaa_sum_b_empty_add_result = ff_q_pfp_empty_add_result_witness_outputfirstentry * S ((S (pfrep_position_empty_add_result_witness_outputfirst)) * pfaa_sum_c_empty_add_result) + (pfrep_left_empty_add_result_witness_output)))))) \/ (((exists pfrep_gap_empty_add_result_witness_outputfirstoutside. pfrep_gap_empty_add_result_witness_outputfirstoutside+(pfaa_length_empty_add_result)=(pfrep_power_empty_add_result_witness_output)) /\ (((pfrep_left_empty_add_result_witness_output)=0))))) -> ((exists pfrep_position_empty_add_result_witness_outputsecond. ((pfrep_position_empty_add_result_witness_outputsecond+S (pfrep_power_empty_add_result_witness_output)=(A)) /\ ((((exists ff_h_pfp_empty_add_result_witness_outputsecondentry. ff_h_pfp_empty_add_result_witness_outputsecondentry + S (pfrep_right_empty_add_result_witness_output) = S ((S (pfrep_position_empty_add_result_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_empty_add_result_witness_outputsecondentry. ab = ff_q_pfp_empty_add_result_witness_outputsecondentry * S ((S (pfrep_position_empty_add_result_witness_outputsecond)) * ac) + (pfrep_right_empty_add_result_witness_output)))))) \/ (((exists pfrep_gap_empty_add_result_witness_outputsecondoutside. pfrep_gap_empty_add_result_witness_outputsecondoutside+(A)=(pfrep_power_empty_add_result_witness_output)) /\ (((pfrep_right_empty_add_result_witness_output)=0))))) -> pfrep_left_empty_add_result_witness_output=pfrep_right_empty_add_result_witness_output)))))))))))))

Complete tactic proof in conservative notation

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

67 script commands · 10 reading checkpoints · 1 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 (1)
prime field polynomial aligned add from common
01Fix variables and assumptionsL1–6

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 A
  5. L5
    intro hp
  6. L6
    intro ha
02Establish hzL7–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta repeat exists.

  1. L7
    have hz : ∃ zb. ∃ zc. Repeat(zb,zc,0,A)Definitions: Repeat(zb,zc,0,A)Original native command in the exact edition
  2. L8
    specialize beta_repeat_exists (0)
  3. L9
    specialize beta_repeat_exists (A)
  4. L10
    apply beta_repeat_exists
03Separate the logical casesL11–12

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

  1. L11
    cases hz
  2. L12
    cases hz_witness
04Use earlier factsL13–22

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

  1. L13
    specialize prime_field_polynomial_aligned_add_from_common (p)
  2. L14
    specialize prime_field_polynomial_aligned_add_from_common (ab)
  3. L15
    specialize prime_field_polynomial_aligned_add_from_common (ac)
  4. L16
    specialize prime_field_polynomial_aligned_add_from_common (A)
  5. L17
    specialize prime_field_polynomial_aligned_add_from_common (0)
  6. L18
    specialize prime_field_polynomial_aligned_add_from_common (0)
  7. L19
    specialize prime_field_polynomial_aligned_add_from_common (0)
  8. L20
    specialize prime_field_polynomial_aligned_add_from_common (ab)
  9. L21
    specialize prime_field_polynomial_aligned_add_from_common (ac)
  10. L22
    specialize prime_field_polynomial_aligned_add_from_common (A)
05Use earlier factsL23–32

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

  1. L23
    specialize prime_field_polynomial_aligned_add_from_common (ab)
  2. L24
    specialize prime_field_polynomial_aligned_add_from_common (ac)
  3. L25
    specialize prime_field_polynomial_aligned_add_from_common (x)
  4. L26
    specialize prime_field_polynomial_aligned_add_from_common (x1)
  5. L27
    specialize prime_field_polynomial_aligned_add_from_common (ab)
  6. L28
    specialize prime_field_polynomial_aligned_add_from_common (ac)
  7. L29
    specialize prime_field_polynomial_aligned_add_from_common (A)
  8. L30
    apply prime_field_polynomial_aligned_add_from_common
  9. L31
    exact ha
  10. L32
    specialize matrix_rank_bounded_prefix_empty (0)
06Use earlier factsL33–36

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

  1. L33
    specialize matrix_rank_bounded_prefix_empty (0)
  2. L34
    specialize matrix_rank_bounded_prefix_empty (p)
  3. L35
    apply matrix_rank_bounded_prefix_empty
  4. L36
    exact ha
07Separate the logical casesL37–37

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

  1. L37
    split
08Use earlier factsL38–47

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

  1. L38
    specialize prime_field_polynomial_power_coefficient_functional (ab)
  2. L39
    specialize prime_field_polynomial_power_coefficient_functional (ac)
  3. L40
    specialize prime_field_polynomial_power_coefficient_functional (A)
  4. L41
    apply prime_field_polynomial_power_coefficient_functional
  5. L42
    specialize prime_field_polynomial_equivalent_symmetric (x)
  6. L43
    specialize prime_field_polynomial_equivalent_symmetric (x1)
  7. L44
    specialize prime_field_polynomial_equivalent_symmetric (A)
  8. L45
    specialize prime_field_polynomial_equivalent_symmetric (0)
  9. L46
    specialize prime_field_polynomial_equivalent_symmetric (0)
  10. L47
    specialize prime_field_polynomial_equivalent_symmetric (0)
09Use earlier factsL48–57

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

  1. L48
    apply prime_field_polynomial_equivalent_symmetric
  2. L49
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (x)
  3. L50
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (x1)
  4. L51
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (A)
  5. L52
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L53
    exact hz_witness_witness
  7. L54
    specialize prime_field_polynomial_add_zero_right (p)
  8. L55
    specialize prime_field_polynomial_add_zero_right (ab)
  9. L56
    specialize prime_field_polynomial_add_zero_right (ac)
  10. L57
    specialize prime_field_polynomial_add_zero_right (x)
10Use earlier factsL58–67

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

  1. L58
    specialize prime_field_polynomial_add_zero_right (x1)
  2. L59
    specialize prime_field_polynomial_add_zero_right (A)
  3. L60
    apply prime_field_polynomial_add_zero_right
  4. L61
    exact hp
  5. L62
    exact ha
  6. L63
    exact hz_witness_witness
  7. L64
    specialize prime_field_polynomial_power_coefficient_functional (ab)
  8. L65
    specialize prime_field_polynomial_power_coefficient_functional (ac)
  9. L66
    specialize prime_field_polynomial_power_coefficient_functional (A)
  10. L67
    apply prime_field_polynomial_power_coefficient_functional

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro A
  5. 0005intro hp
  6. 0006intro ha
  7. 0007have hz : ∃ zb. ∃ zc. Repeat(zb,zc,0,A)
  8. 0008specialize beta_repeat_exists (0)
  9. 0009specialize beta_repeat_exists (A)
  10. 0010apply beta_repeat_exists
  11. 0011cases hz
  12. 0012cases hz_witness
  13. 0013specialize prime_field_polynomial_aligned_add_from_common (p)
  14. 0014specialize prime_field_polynomial_aligned_add_from_common (ab)
  15. 0015specialize prime_field_polynomial_aligned_add_from_common (ac)
  16. 0016specialize prime_field_polynomial_aligned_add_from_common (A)
  17. 0017specialize prime_field_polynomial_aligned_add_from_common (0)
  18. 0018specialize prime_field_polynomial_aligned_add_from_common (0)
  19. 0019specialize prime_field_polynomial_aligned_add_from_common (0)
  20. 0020specialize prime_field_polynomial_aligned_add_from_common (ab)
  21. 0021specialize prime_field_polynomial_aligned_add_from_common (ac)
  22. 0022specialize prime_field_polynomial_aligned_add_from_common (A)
  23. 0023specialize prime_field_polynomial_aligned_add_from_common (ab)
  24. 0024specialize prime_field_polynomial_aligned_add_from_common (ac)
  25. 0025specialize prime_field_polynomial_aligned_add_from_common (x)
  26. 0026specialize prime_field_polynomial_aligned_add_from_common (x1)
  27. 0027specialize prime_field_polynomial_aligned_add_from_common (ab)
  28. 0028specialize prime_field_polynomial_aligned_add_from_common (ac)
  29. 0029specialize prime_field_polynomial_aligned_add_from_common (A)
  30. 0030apply prime_field_polynomial_aligned_add_from_common
  31. 0031exact ha
  32. 0032specialize matrix_rank_bounded_prefix_empty (0)
  33. 0033specialize matrix_rank_bounded_prefix_empty (0)
  34. 0034specialize matrix_rank_bounded_prefix_empty (p)
  35. 0035apply matrix_rank_bounded_prefix_empty
  36. 0036exact ha
  37. 0037split
  38. 0038specialize prime_field_polynomial_power_coefficient_functional (ab)
  39. 0039specialize prime_field_polynomial_power_coefficient_functional (ac)
  40. 0040specialize prime_field_polynomial_power_coefficient_functional (A)
  41. 0041apply prime_field_polynomial_power_coefficient_functional
  42. 0042specialize prime_field_polynomial_equivalent_symmetric (x)
  43. 0043specialize prime_field_polynomial_equivalent_symmetric (x1)
  44. 0044specialize prime_field_polynomial_equivalent_symmetric (A)
  45. 0045specialize prime_field_polynomial_equivalent_symmetric (0)
  46. 0046specialize prime_field_polynomial_equivalent_symmetric (0)
  47. 0047specialize prime_field_polynomial_equivalent_symmetric (0)
  48. 0048apply prime_field_polynomial_equivalent_symmetric
  49. 0049specialize prime_field_polynomial_zero_prefix_equivalent_empty (x)
  50. 0050specialize prime_field_polynomial_zero_prefix_equivalent_empty (x1)
  51. 0051specialize prime_field_polynomial_zero_prefix_equivalent_empty (A)
  52. 0052apply prime_field_polynomial_zero_prefix_equivalent_empty
  53. 0053exact hz_witness_witness
  54. 0054specialize prime_field_polynomial_add_zero_right (p)
  55. 0055specialize prime_field_polynomial_add_zero_right (ab)
  56. 0056specialize prime_field_polynomial_add_zero_right (ac)
  57. 0057specialize prime_field_polynomial_add_zero_right (x)
  58. 0058specialize prime_field_polynomial_add_zero_right (x1)
  59. 0059specialize prime_field_polynomial_add_zero_right (A)
  60. 0060apply prime_field_polynomial_add_zero_right
  61. 0061exact hp
  62. 0062exact ha
  63. 0063exact hz_witness_witness
  64. 0064specialize prime_field_polynomial_power_coefficient_functional (ab)
  65. 0065specialize prime_field_polynomial_power_coefficient_functional (ac)
  66. 0066specialize prime_field_polynomial_power_coefficient_functional (A)
  67. 0067apply prime_field_polynomial_power_coefficient_functional