PG003E

prime_field_polynomial_aligned_add_from_fixed

Every genuine fixed-length addition supplies its own actual common representatives and is an aligned addition, without an extra prime hypothesis.

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. ∀ bb. ∀ bc. ∀ rb. ∀ rc. ∀ K. FpPolyAdd(p,ab,ac,bb,bc,rb,rc,K) → FpPolynomialAlignedAdd(p,ab,ac,K,bb,bc,K,rb,rc,K)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 3FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 1FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 1

Actual proof prerequisites

prime_field_polynomial_add_bounded · checked external prerequisiteprime_field_polynomial_aligned_add_from_commonprime_field_polynomial_common_representatives_same_lengthprime_field_polynomial_power_coefficient_functional · checked external prerequisite
Original expanded first-order statement 
forall p ab ac bb bc rb rc K. (forall pfp_index_fixed_input. (exists pfa_gap_fixed_inputindex. pfa_gap_fixed_inputindex + S (pfp_index_fixed_input) = (K)) -> exists pfp_left_fixed_input pfp_right_fixed_input pfp_value_fixed_input. ((((exists ff_h_pfp_fixed_inputleft. ff_h_pfp_fixed_inputleft + S (pfp_left_fixed_input) = S ((S (pfp_index_fixed_input)) * ac)) /\ exists ff_q_pfp_fixed_inputleft. ab = ff_q_pfp_fixed_inputleft * S ((S (pfp_index_fixed_input)) * ac) + (pfp_left_fixed_input))) /\ (((((exists ff_h_pfp_fixed_inputright. ff_h_pfp_fixed_inputright + S (pfp_right_fixed_input) = S ((S (pfp_index_fixed_input)) * bc)) /\ exists ff_q_pfp_fixed_inputright. bb = ff_q_pfp_fixed_inputright * S ((S (pfp_index_fixed_input)) * bc) + (pfp_right_fixed_input))) /\ (((((exists ff_h_pfp_fixed_inputtarget. ff_h_pfp_fixed_inputtarget + S (pfp_value_fixed_input) = S ((S (pfp_index_fixed_input)) * rc)) /\ exists ff_q_pfp_fixed_inputtarget. rb = ff_q_pfp_fixed_inputtarget * S ((S (pfp_index_fixed_input)) * rc) + (pfp_value_fixed_input))) /\ ((((exists pfa_gap_fixed_inputoperationleft. pfa_gap_fixed_inputoperationleft + S (pfp_left_fixed_input) = (p)) /\ (((exists pfa_gap_fixed_inputoperationright. pfa_gap_fixed_inputoperationright + S (pfp_right_fixed_input) = (p)) /\ ((((exists pfa_gap_fixed_inputoperationresultbound. pfa_gap_fixed_inputoperationresultbound + S (pfp_value_fixed_input) = (p)) /\ ((exists pfa_offset_left_fixed_inputoperationresultcongruence pfa_offset_right_fixed_inputoperationresultcongruence. ((pfp_left_fixed_input) + (pfp_right_fixed_input)) + (p) * pfa_offset_left_fixed_inputoperationresultcongruence = (pfp_value_fixed_input) + (p) * pfa_offset_right_fixed_inputoperationresultcongruence)))))))))))))))) -> (((forall fom_index_pfp_fixed_result_left_bounded. (exists fom_gap_pfp_fixed_result_left_bounded_index_bound. fom_gap_pfp_fixed_result_left_bounded_index_bound + S (fom_index_pfp_fixed_result_left_bounded) = K) -> exists fom_value_pfp_fixed_result_left_bounded. ((((exists fom_beta_height_pfp_fixed_result_left_bounded_entry. fom_beta_height_pfp_fixed_result_left_bounded_entry + S (fom_value_pfp_fixed_result_left_bounded) = S ((S (fom_index_pfp_fixed_result_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_fixed_result_left_bounded_entry. ab = fom_beta_quotient_pfp_fixed_result_left_bounded_entry * S ((S (fom_index_pfp_fixed_result_left_bounded)) * ac) + (fom_value_pfp_fixed_result_left_bounded))) /\ (exists fom_gap_pfp_fixed_result_left_bounded_value_bound. fom_gap_pfp_fixed_result_left_bounded_value_bound + S (fom_value_pfp_fixed_result_left_bounded) = p))) /\ (((forall fom_index_pfp_fixed_result_right_bounded. (exists fom_gap_pfp_fixed_result_right_bounded_index_bound. fom_gap_pfp_fixed_result_right_bounded_index_bound + S (fom_index_pfp_fixed_result_right_bounded) = K) -> exists fom_value_pfp_fixed_result_right_bounded. ((((exists fom_beta_height_pfp_fixed_result_right_bounded_entry. fom_beta_height_pfp_fixed_result_right_bounded_entry + S (fom_value_pfp_fixed_result_right_bounded) = S ((S (fom_index_pfp_fixed_result_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_fixed_result_right_bounded_entry. bb = fom_beta_quotient_pfp_fixed_result_right_bounded_entry * S ((S (fom_index_pfp_fixed_result_right_bounded)) * bc) + (fom_value_pfp_fixed_result_right_bounded))) /\ (exists fom_gap_pfp_fixed_result_right_bounded_value_bound. fom_gap_pfp_fixed_result_right_bounded_value_bound + S (fom_value_pfp_fixed_result_right_bounded) = p))) /\ (((forall fom_index_pfp_fixed_result_result_bounded. (exists fom_gap_pfp_fixed_result_result_bounded_index_bound. fom_gap_pfp_fixed_result_result_bounded_index_bound + S (fom_index_pfp_fixed_result_result_bounded) = K) -> exists fom_value_pfp_fixed_result_result_bounded. ((((exists fom_beta_height_pfp_fixed_result_result_bounded_entry. fom_beta_height_pfp_fixed_result_result_bounded_entry + S (fom_value_pfp_fixed_result_result_bounded) = S ((S (fom_index_pfp_fixed_result_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_fixed_result_result_bounded_entry. rb = fom_beta_quotient_pfp_fixed_result_result_bounded_entry * S ((S (fom_index_pfp_fixed_result_result_bounded)) * rc) + (fom_value_pfp_fixed_result_result_bounded))) /\ (exists fom_gap_pfp_fixed_result_result_bounded_value_bound. fom_gap_pfp_fixed_result_result_bounded_value_bound + S (fom_value_pfp_fixed_result_result_bounded) = p))) /\ ((exists pfaa_left_b_fixed_result pfaa_left_c_fixed_result pfaa_right_b_fixed_result pfaa_right_c_fixed_result pfaa_sum_b_fixed_result pfaa_sum_c_fixed_result pfaa_length_fixed_result. ((((forall pfrep_power_fixed_result_witness_common_left pfrep_left_fixed_result_witness_common_left pfrep_right_fixed_result_witness_common_left. ((exists pfrep_position_fixed_result_witness_common_leftfirst. ((pfrep_position_fixed_result_witness_common_leftfirst+S (pfrep_power_fixed_result_witness_common_left)=(K)) /\ ((((exists ff_h_pfp_fixed_result_witness_common_leftfirstentry. ff_h_pfp_fixed_result_witness_common_leftfirstentry + S (pfrep_left_fixed_result_witness_common_left) = S ((S (pfrep_position_fixed_result_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_fixed_result_witness_common_leftfirstentry. ab = ff_q_pfp_fixed_result_witness_common_leftfirstentry * S ((S (pfrep_position_fixed_result_witness_common_leftfirst)) * ac) + (pfrep_left_fixed_result_witness_common_left)))))) \/ (((exists pfrep_gap_fixed_result_witness_common_leftfirstoutside. pfrep_gap_fixed_result_witness_common_leftfirstoutside+(K)=(pfrep_power_fixed_result_witness_common_left)) /\ (((pfrep_left_fixed_result_witness_common_left)=0))))) -> ((exists pfrep_position_fixed_result_witness_common_leftsecond. ((pfrep_position_fixed_result_witness_common_leftsecond+S (pfrep_power_fixed_result_witness_common_left)=(pfaa_length_fixed_result)) /\ ((((exists ff_h_pfp_fixed_result_witness_common_leftsecondentry. ff_h_pfp_fixed_result_witness_common_leftsecondentry + S (pfrep_right_fixed_result_witness_common_left) = S ((S (pfrep_position_fixed_result_witness_common_leftsecond)) * pfaa_left_c_fixed_result)) /\ exists ff_q_pfp_fixed_result_witness_common_leftsecondentry. pfaa_left_b_fixed_result = ff_q_pfp_fixed_result_witness_common_leftsecondentry * S ((S (pfrep_position_fixed_result_witness_common_leftsecond)) * pfaa_left_c_fixed_result) + (pfrep_right_fixed_result_witness_common_left)))))) \/ (((exists pfrep_gap_fixed_result_witness_common_leftsecondoutside. pfrep_gap_fixed_result_witness_common_leftsecondoutside+(pfaa_length_fixed_result)=(pfrep_power_fixed_result_witness_common_left)) /\ (((pfrep_right_fixed_result_witness_common_left)=0))))) -> pfrep_left_fixed_result_witness_common_left=pfrep_right_fixed_result_witness_common_left) /\ ((forall pfrep_power_fixed_result_witness_common_right pfrep_left_fixed_result_witness_common_right pfrep_right_fixed_result_witness_common_right. ((exists pfrep_position_fixed_result_witness_common_rightfirst. ((pfrep_position_fixed_result_witness_common_rightfirst+S (pfrep_power_fixed_result_witness_common_right)=(K)) /\ ((((exists ff_h_pfp_fixed_result_witness_common_rightfirstentry. ff_h_pfp_fixed_result_witness_common_rightfirstentry + S (pfrep_left_fixed_result_witness_common_right) = S ((S (pfrep_position_fixed_result_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_fixed_result_witness_common_rightfirstentry. bb = ff_q_pfp_fixed_result_witness_common_rightfirstentry * S ((S (pfrep_position_fixed_result_witness_common_rightfirst)) * bc) + (pfrep_left_fixed_result_witness_common_right)))))) \/ (((exists pfrep_gap_fixed_result_witness_common_rightfirstoutside. pfrep_gap_fixed_result_witness_common_rightfirstoutside+(K)=(pfrep_power_fixed_result_witness_common_right)) /\ (((pfrep_left_fixed_result_witness_common_right)=0))))) -> ((exists pfrep_position_fixed_result_witness_common_rightsecond. ((pfrep_position_fixed_result_witness_common_rightsecond+S (pfrep_power_fixed_result_witness_common_right)=(pfaa_length_fixed_result)) /\ ((((exists ff_h_pfp_fixed_result_witness_common_rightsecondentry. ff_h_pfp_fixed_result_witness_common_rightsecondentry + S (pfrep_right_fixed_result_witness_common_right) = S ((S (pfrep_position_fixed_result_witness_common_rightsecond)) * pfaa_right_c_fixed_result)) /\ exists ff_q_pfp_fixed_result_witness_common_rightsecondentry. pfaa_right_b_fixed_result = ff_q_pfp_fixed_result_witness_common_rightsecondentry * S ((S (pfrep_position_fixed_result_witness_common_rightsecond)) * pfaa_right_c_fixed_result) + (pfrep_right_fixed_result_witness_common_right)))))) \/ (((exists pfrep_gap_fixed_result_witness_common_rightsecondoutside. pfrep_gap_fixed_result_witness_common_rightsecondoutside+(pfaa_length_fixed_result)=(pfrep_power_fixed_result_witness_common_right)) /\ (((pfrep_right_fixed_result_witness_common_right)=0))))) -> pfrep_left_fixed_result_witness_common_right=pfrep_right_fixed_result_witness_common_right)))) /\ (((forall pfp_index_fixed_result_witness_operation. (exists pfa_gap_fixed_result_witness_operationindex. pfa_gap_fixed_result_witness_operationindex + S (pfp_index_fixed_result_witness_operation) = (pfaa_length_fixed_result)) -> exists pfp_left_fixed_result_witness_operation pfp_right_fixed_result_witness_operation pfp_value_fixed_result_witness_operation. ((((exists ff_h_pfp_fixed_result_witness_operationleft. ff_h_pfp_fixed_result_witness_operationleft + S (pfp_left_fixed_result_witness_operation) = S ((S (pfp_index_fixed_result_witness_operation)) * pfaa_left_c_fixed_result)) /\ exists ff_q_pfp_fixed_result_witness_operationleft. pfaa_left_b_fixed_result = ff_q_pfp_fixed_result_witness_operationleft * S ((S (pfp_index_fixed_result_witness_operation)) * pfaa_left_c_fixed_result) + (pfp_left_fixed_result_witness_operation))) /\ (((((exists ff_h_pfp_fixed_result_witness_operationright. ff_h_pfp_fixed_result_witness_operationright + S (pfp_right_fixed_result_witness_operation) = S ((S (pfp_index_fixed_result_witness_operation)) * pfaa_right_c_fixed_result)) /\ exists ff_q_pfp_fixed_result_witness_operationright. pfaa_right_b_fixed_result = ff_q_pfp_fixed_result_witness_operationright * S ((S (pfp_index_fixed_result_witness_operation)) * pfaa_right_c_fixed_result) + (pfp_right_fixed_result_witness_operation))) /\ (((((exists ff_h_pfp_fixed_result_witness_operationtarget. ff_h_pfp_fixed_result_witness_operationtarget + S (pfp_value_fixed_result_witness_operation) = S ((S (pfp_index_fixed_result_witness_operation)) * pfaa_sum_c_fixed_result)) /\ exists ff_q_pfp_fixed_result_witness_operationtarget. pfaa_sum_b_fixed_result = ff_q_pfp_fixed_result_witness_operationtarget * S ((S (pfp_index_fixed_result_witness_operation)) * pfaa_sum_c_fixed_result) + (pfp_value_fixed_result_witness_operation))) /\ ((((exists pfa_gap_fixed_result_witness_operationoperationleft. pfa_gap_fixed_result_witness_operationoperationleft + S (pfp_left_fixed_result_witness_operation) = (p)) /\ (((exists pfa_gap_fixed_result_witness_operationoperationright. pfa_gap_fixed_result_witness_operationoperationright + S (pfp_right_fixed_result_witness_operation) = (p)) /\ ((((exists pfa_gap_fixed_result_witness_operationoperationresultbound. pfa_gap_fixed_result_witness_operationoperationresultbound + S (pfp_value_fixed_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_fixed_result_witness_operationoperationresultcongruence pfa_offset_right_fixed_result_witness_operationoperationresultcongruence. ((pfp_left_fixed_result_witness_operation) + (pfp_right_fixed_result_witness_operation)) + (p) * pfa_offset_left_fixed_result_witness_operationoperationresultcongruence = (pfp_value_fixed_result_witness_operation) + (p) * pfa_offset_right_fixed_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_fixed_result_witness_output pfrep_left_fixed_result_witness_output pfrep_right_fixed_result_witness_output. ((exists pfrep_position_fixed_result_witness_outputfirst. ((pfrep_position_fixed_result_witness_outputfirst+S (pfrep_power_fixed_result_witness_output)=(pfaa_length_fixed_result)) /\ ((((exists ff_h_pfp_fixed_result_witness_outputfirstentry. ff_h_pfp_fixed_result_witness_outputfirstentry + S (pfrep_left_fixed_result_witness_output) = S ((S (pfrep_position_fixed_result_witness_outputfirst)) * pfaa_sum_c_fixed_result)) /\ exists ff_q_pfp_fixed_result_witness_outputfirstentry. pfaa_sum_b_fixed_result = ff_q_pfp_fixed_result_witness_outputfirstentry * S ((S (pfrep_position_fixed_result_witness_outputfirst)) * pfaa_sum_c_fixed_result) + (pfrep_left_fixed_result_witness_output)))))) \/ (((exists pfrep_gap_fixed_result_witness_outputfirstoutside. pfrep_gap_fixed_result_witness_outputfirstoutside+(pfaa_length_fixed_result)=(pfrep_power_fixed_result_witness_output)) /\ (((pfrep_left_fixed_result_witness_output)=0))))) -> ((exists pfrep_position_fixed_result_witness_outputsecond. ((pfrep_position_fixed_result_witness_outputsecond+S (pfrep_power_fixed_result_witness_output)=(K)) /\ ((((exists ff_h_pfp_fixed_result_witness_outputsecondentry. ff_h_pfp_fixed_result_witness_outputsecondentry + S (pfrep_right_fixed_result_witness_output) = S ((S (pfrep_position_fixed_result_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_fixed_result_witness_outputsecondentry. rb = ff_q_pfp_fixed_result_witness_outputsecondentry * S ((S (pfrep_position_fixed_result_witness_outputsecond)) * rc) + (pfrep_right_fixed_result_witness_output)))))) \/ (((exists pfrep_gap_fixed_result_witness_outputsecondoutside. pfrep_gap_fixed_result_witness_outputsecondoutside+(K)=(pfrep_power_fixed_result_witness_output)) /\ (((pfrep_right_fixed_result_witness_output)=0))))) -> pfrep_left_fixed_result_witness_output=pfrep_right_fixed_result_witness_output)))))))))))))

Complete tactic proof in conservative notation

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

54 script commands · 8 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 (2)
prime field polynomial aligned add from commonprime field polynomial common representatives same length
01Fix variables and assumptionsL1–9

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 bb
  5. L5
    intro bc
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro K
  9. L9
    intro h
02Establish hbL10–19

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

  1. L10
    have hb : BetaPrefixInto(ab,ac,K,p) ∧ (BetaPrefixInto(bb,bc,K,p) ∧ BetaPrefixInto(rb,rc,K,p))Definitions: BetaPrefixInto(ab,ac,K,p)BetaPrefixInto(bb,bc,K,p)BetaPrefixInto(rb,rc,K,p)Original native command in the exact edition
  2. L11
    specialize prime_field_polynomial_add_bounded (p)
  3. L12
    specialize prime_field_polynomial_add_bounded (ab)
  4. L13
    specialize prime_field_polynomial_add_bounded (ac)
  5. L14
    specialize prime_field_polynomial_add_bounded (bb)
  6. L15
    specialize prime_field_polynomial_add_bounded (bc)
  7. L16
    specialize prime_field_polynomial_add_bounded (rb)
  8. L17
    specialize prime_field_polynomial_add_bounded (rc)
  9. L18
    specialize prime_field_polynomial_add_bounded (K)
  10. L19
    apply prime_field_polynomial_add_bounded
03Use earlier factsL20–20

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

  1. L20
    exact h
04Separate the logical casesL21–22

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

  1. L21
    cases hb
  2. L22
    cases hb_right
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 (p)
  2. L24
    specialize prime_field_polynomial_aligned_add_from_common (ab)
  3. L25
    specialize prime_field_polynomial_aligned_add_from_common (ac)
  4. L26
    specialize prime_field_polynomial_aligned_add_from_common (K)
  5. L27
    specialize prime_field_polynomial_aligned_add_from_common (bb)
  6. L28
    specialize prime_field_polynomial_aligned_add_from_common (bc)
  7. L29
    specialize prime_field_polynomial_aligned_add_from_common (K)
  8. L30
    specialize prime_field_polynomial_aligned_add_from_common (rb)
  9. L31
    specialize prime_field_polynomial_aligned_add_from_common (rc)
  10. L32
    specialize prime_field_polynomial_aligned_add_from_common (K)
06Use earlier factsL33–42

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

  1. L33
    specialize prime_field_polynomial_aligned_add_from_common (ab)
  2. L34
    specialize prime_field_polynomial_aligned_add_from_common (ac)
  3. L35
    specialize prime_field_polynomial_aligned_add_from_common (bb)
  4. L36
    specialize prime_field_polynomial_aligned_add_from_common (bc)
  5. L37
    specialize prime_field_polynomial_aligned_add_from_common (rb)
  6. L38
    specialize prime_field_polynomial_aligned_add_from_common (rc)
  7. L39
    specialize prime_field_polynomial_aligned_add_from_common (K)
  8. L40
    apply prime_field_polynomial_aligned_add_from_common
  9. L41
    exact hb_left
  10. L42
    exact hb_right_left
07Use earlier factsL43–52

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

  1. L43
    exact hb_right_right
  2. L44
    specialize prime_field_polynomial_common_representatives_same_length (ab)
  3. L45
    specialize prime_field_polynomial_common_representatives_same_length (ac)
  4. L46
    specialize prime_field_polynomial_common_representatives_same_length (bb)
  5. L47
    specialize prime_field_polynomial_common_representatives_same_length (bc)
  6. L48
    specialize prime_field_polynomial_common_representatives_same_length (K)
  7. L49
    apply prime_field_polynomial_common_representatives_same_length
  8. L50
    exact h
  9. L51
    specialize prime_field_polynomial_power_coefficient_functional (rb)
  10. L52
    specialize prime_field_polynomial_power_coefficient_functional (rc)
08Use earlier factsL53–54

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

  1. L53
    specialize prime_field_polynomial_power_coefficient_functional (K)
  2. L54
    apply prime_field_polynomial_power_coefficient_functional

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro K
  9. 0009intro h
  10. 0010have hb : BetaPrefixInto(ab,ac,K,p) ∧ (BetaPrefixInto(bb,bc,K,p) ∧ BetaPrefixInto(rb,rc,K,p))
  11. 0011specialize prime_field_polynomial_add_bounded (p)
  12. 0012specialize prime_field_polynomial_add_bounded (ab)
  13. 0013specialize prime_field_polynomial_add_bounded (ac)
  14. 0014specialize prime_field_polynomial_add_bounded (bb)
  15. 0015specialize prime_field_polynomial_add_bounded (bc)
  16. 0016specialize prime_field_polynomial_add_bounded (rb)
  17. 0017specialize prime_field_polynomial_add_bounded (rc)
  18. 0018specialize prime_field_polynomial_add_bounded (K)
  19. 0019apply prime_field_polynomial_add_bounded
  20. 0020exact h
  21. 0021cases hb
  22. 0022cases hb_right
  23. 0023specialize prime_field_polynomial_aligned_add_from_common (p)
  24. 0024specialize prime_field_polynomial_aligned_add_from_common (ab)
  25. 0025specialize prime_field_polynomial_aligned_add_from_common (ac)
  26. 0026specialize prime_field_polynomial_aligned_add_from_common (K)
  27. 0027specialize prime_field_polynomial_aligned_add_from_common (bb)
  28. 0028specialize prime_field_polynomial_aligned_add_from_common (bc)
  29. 0029specialize prime_field_polynomial_aligned_add_from_common (K)
  30. 0030specialize prime_field_polynomial_aligned_add_from_common (rb)
  31. 0031specialize prime_field_polynomial_aligned_add_from_common (rc)
  32. 0032specialize prime_field_polynomial_aligned_add_from_common (K)
  33. 0033specialize prime_field_polynomial_aligned_add_from_common (ab)
  34. 0034specialize prime_field_polynomial_aligned_add_from_common (ac)
  35. 0035specialize prime_field_polynomial_aligned_add_from_common (bb)
  36. 0036specialize prime_field_polynomial_aligned_add_from_common (bc)
  37. 0037specialize prime_field_polynomial_aligned_add_from_common (rb)
  38. 0038specialize prime_field_polynomial_aligned_add_from_common (rc)
  39. 0039specialize prime_field_polynomial_aligned_add_from_common (K)
  40. 0040apply prime_field_polynomial_aligned_add_from_common
  41. 0041exact hb_left
  42. 0042exact hb_right_left
  43. 0043exact hb_right_right
  44. 0044specialize prime_field_polynomial_common_representatives_same_length (ab)
  45. 0045specialize prime_field_polynomial_common_representatives_same_length (ac)
  46. 0046specialize prime_field_polynomial_common_representatives_same_length (bb)
  47. 0047specialize prime_field_polynomial_common_representatives_same_length (bc)
  48. 0048specialize prime_field_polynomial_common_representatives_same_length (K)
  49. 0049apply prime_field_polynomial_common_representatives_same_length
  50. 0050exact h
  51. 0051specialize prime_field_polynomial_power_coefficient_functional (rb)
  52. 0052specialize prime_field_polynomial_power_coefficient_functional (rc)
  53. 0053specialize prime_field_polynomial_power_coefficient_functional (K)
  54. 0054apply prime_field_polynomial_power_coefficient_functional