PG003A

prime_field_polynomial_common_representatives_functional

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Any two choices of common representatives are pairwise formally equivalent, even at different common lengths; no raw-code or length uniqueness is asserted.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall ab ac L bb bc M ub uc vb vc K db dc eb ec J. (((forall pfrep_power_common_function_first_left pfrep_left_common_function_first_left pfrep_right_common_function_first_left. ((exists pfrep_position_common_function_first_leftfirst. ((pfrep_position_common_function_first_leftfirst+S (pfrep_power_common_function_first_left)=(L)) /\ ((((exists ff_h_pfp_common_function_first_leftfirstentry. ff_h_pfp_common_function_first_leftfirstentry + S (pfrep_left_common_function_first_left) = S ((S (pfrep_position_common_function_first_leftfirst)) * ac)) /\ exists ff_q_pfp_common_function_first_leftfirstentry. ab = ff_q_pfp_common_function_first_leftfirstentry * S ((S (pfrep_position_common_function_first_leftfirst)) * ac) + (pfrep_left_common_function_first_left)))))) \/ (((exists pfrep_gap_common_function_first_leftfirstoutside. pfrep_gap_common_function_first_leftfirstoutside+(L)=(pfrep_power_common_function_first_left)) /\ (((pfrep_left_common_function_first_left)=0))))) -> ((exists pfrep_position_common_function_first_leftsecond. ((pfrep_position_common_function_first_leftsecond+S (pfrep_power_common_function_first_left)=(K)) /\ ((((exists ff_h_pfp_common_function_first_leftsecondentry. ff_h_pfp_common_function_first_leftsecondentry + S (pfrep_right_common_function_first_left) = S ((S (pfrep_position_common_function_first_leftsecond)) * uc)) /\ exists ff_q_pfp_common_function_first_leftsecondentry. ub = ff_q_pfp_common_function_first_leftsecondentry * S ((S (pfrep_position_common_function_first_leftsecond)) * uc) + (pfrep_right_common_function_first_left)))))) \/ (((exists pfrep_gap_common_function_first_leftsecondoutside. pfrep_gap_common_function_first_leftsecondoutside+(K)=(pfrep_power_common_function_first_left)) /\ (((pfrep_right_common_function_first_left)=0))))) -> pfrep_left_common_function_first_left=pfrep_right_common_function_first_left) /\ ((forall pfrep_power_common_function_first_right pfrep_left_common_function_first_right pfrep_right_common_function_first_right. ((exists pfrep_position_common_function_first_rightfirst. ((pfrep_position_common_function_first_rightfirst+S (pfrep_power_common_function_first_right)=(M)) /\ ((((exists ff_h_pfp_common_function_first_rightfirstentry. ff_h_pfp_common_function_first_rightfirstentry + S (pfrep_left_common_function_first_right) = S ((S (pfrep_position_common_function_first_rightfirst)) * bc)) /\ exists ff_q_pfp_common_function_first_rightfirstentry. bb = ff_q_pfp_common_function_first_rightfirstentry * S ((S (pfrep_position_common_function_first_rightfirst)) * bc) + (pfrep_left_common_function_first_right)))))) \/ (((exists pfrep_gap_common_function_first_rightfirstoutside. pfrep_gap_common_function_first_rightfirstoutside+(M)=(pfrep_power_common_function_first_right)) /\ (((pfrep_left_common_function_first_right)=0))))) -> ((exists pfrep_position_common_function_first_rightsecond. ((pfrep_position_common_function_first_rightsecond+S (pfrep_power_common_function_first_right)=(K)) /\ ((((exists ff_h_pfp_common_function_first_rightsecondentry. ff_h_pfp_common_function_first_rightsecondentry + S (pfrep_right_common_function_first_right) = S ((S (pfrep_position_common_function_first_rightsecond)) * vc)) /\ exists ff_q_pfp_common_function_first_rightsecondentry. vb = ff_q_pfp_common_function_first_rightsecondentry * S ((S (pfrep_position_common_function_first_rightsecond)) * vc) + (pfrep_right_common_function_first_right)))))) \/ (((exists pfrep_gap_common_function_first_rightsecondoutside. pfrep_gap_common_function_first_rightsecondoutside+(K)=(pfrep_power_common_function_first_right)) /\ (((pfrep_right_common_function_first_right)=0))))) -> pfrep_left_common_function_first_right=pfrep_right_common_function_first_right)))) -> (((forall pfrep_power_common_function_second_left pfrep_left_common_function_second_left pfrep_right_common_function_second_left. ((exists pfrep_position_common_function_second_leftfirst. ((pfrep_position_common_function_second_leftfirst+S (pfrep_power_common_function_second_left)=(L)) /\ ((((exists ff_h_pfp_common_function_second_leftfirstentry. ff_h_pfp_common_function_second_leftfirstentry + S (pfrep_left_common_function_second_left) = S ((S (pfrep_position_common_function_second_leftfirst)) * ac)) /\ exists ff_q_pfp_common_function_second_leftfirstentry. ab = ff_q_pfp_common_function_second_leftfirstentry * S ((S (pfrep_position_common_function_second_leftfirst)) * ac) + (pfrep_left_common_function_second_left)))))) \/ (((exists pfrep_gap_common_function_second_leftfirstoutside. pfrep_gap_common_function_second_leftfirstoutside+(L)=(pfrep_power_common_function_second_left)) /\ (((pfrep_left_common_function_second_left)=0))))) -> ((exists pfrep_position_common_function_second_leftsecond. ((pfrep_position_common_function_second_leftsecond+S (pfrep_power_common_function_second_left)=(J)) /\ ((((exists ff_h_pfp_common_function_second_leftsecondentry. ff_h_pfp_common_function_second_leftsecondentry + S (pfrep_right_common_function_second_left) = S ((S (pfrep_position_common_function_second_leftsecond)) * dc)) /\ exists ff_q_pfp_common_function_second_leftsecondentry. db = ff_q_pfp_common_function_second_leftsecondentry * S ((S (pfrep_position_common_function_second_leftsecond)) * dc) + (pfrep_right_common_function_second_left)))))) \/ (((exists pfrep_gap_common_function_second_leftsecondoutside. pfrep_gap_common_function_second_leftsecondoutside+(J)=(pfrep_power_common_function_second_left)) /\ (((pfrep_right_common_function_second_left)=0))))) -> pfrep_left_common_function_second_left=pfrep_right_common_function_second_left) /\ ((forall pfrep_power_common_function_second_right pfrep_left_common_function_second_right pfrep_right_common_function_second_right. ((exists pfrep_position_common_function_second_rightfirst. ((pfrep_position_common_function_second_rightfirst+S (pfrep_power_common_function_second_right)=(M)) /\ ((((exists ff_h_pfp_common_function_second_rightfirstentry. ff_h_pfp_common_function_second_rightfirstentry + S (pfrep_left_common_function_second_right) = S ((S (pfrep_position_common_function_second_rightfirst)) * bc)) /\ exists ff_q_pfp_common_function_second_rightfirstentry. bb = ff_q_pfp_common_function_second_rightfirstentry * S ((S (pfrep_position_common_function_second_rightfirst)) * bc) + (pfrep_left_common_function_second_right)))))) \/ (((exists pfrep_gap_common_function_second_rightfirstoutside. pfrep_gap_common_function_second_rightfirstoutside+(M)=(pfrep_power_common_function_second_right)) /\ (((pfrep_left_common_function_second_right)=0))))) -> ((exists pfrep_position_common_function_second_rightsecond. ((pfrep_position_common_function_second_rightsecond+S (pfrep_power_common_function_second_right)=(J)) /\ ((((exists ff_h_pfp_common_function_second_rightsecondentry. ff_h_pfp_common_function_second_rightsecondentry + S (pfrep_right_common_function_second_right) = S ((S (pfrep_position_common_function_second_rightsecond)) * ec)) /\ exists ff_q_pfp_common_function_second_rightsecondentry. eb = ff_q_pfp_common_function_second_rightsecondentry * S ((S (pfrep_position_common_function_second_rightsecond)) * ec) + (pfrep_right_common_function_second_right)))))) \/ (((exists pfrep_gap_common_function_second_rightsecondoutside. pfrep_gap_common_function_second_rightsecondoutside+(J)=(pfrep_power_common_function_second_right)) /\ (((pfrep_right_common_function_second_right)=0))))) -> pfrep_left_common_function_second_right=pfrep_right_common_function_second_right)))) -> (((forall pfrep_power_common_function_result_left pfrep_left_common_function_result_left pfrep_right_common_function_result_left. ((exists pfrep_position_common_function_result_leftfirst. ((pfrep_position_common_function_result_leftfirst+S (pfrep_power_common_function_result_left)=(K)) /\ ((((exists ff_h_pfp_common_function_result_leftfirstentry. ff_h_pfp_common_function_result_leftfirstentry + S (pfrep_left_common_function_result_left) = S ((S (pfrep_position_common_function_result_leftfirst)) * uc)) /\ exists ff_q_pfp_common_function_result_leftfirstentry. ub = ff_q_pfp_common_function_result_leftfirstentry * S ((S (pfrep_position_common_function_result_leftfirst)) * uc) + (pfrep_left_common_function_result_left)))))) \/ (((exists pfrep_gap_common_function_result_leftfirstoutside. pfrep_gap_common_function_result_leftfirstoutside+(K)=(pfrep_power_common_function_result_left)) /\ (((pfrep_left_common_function_result_left)=0))))) -> ((exists pfrep_position_common_function_result_leftsecond. ((pfrep_position_common_function_result_leftsecond+S (pfrep_power_common_function_result_left)=(J)) /\ ((((exists ff_h_pfp_common_function_result_leftsecondentry. ff_h_pfp_common_function_result_leftsecondentry + S (pfrep_right_common_function_result_left) = S ((S (pfrep_position_common_function_result_leftsecond)) * dc)) /\ exists ff_q_pfp_common_function_result_leftsecondentry. db = ff_q_pfp_common_function_result_leftsecondentry * S ((S (pfrep_position_common_function_result_leftsecond)) * dc) + (pfrep_right_common_function_result_left)))))) \/ (((exists pfrep_gap_common_function_result_leftsecondoutside. pfrep_gap_common_function_result_leftsecondoutside+(J)=(pfrep_power_common_function_result_left)) /\ (((pfrep_right_common_function_result_left)=0))))) -> pfrep_left_common_function_result_left=pfrep_right_common_function_result_left) /\ ((forall pfrep_power_common_function_result_right pfrep_left_common_function_result_right pfrep_right_common_function_result_right. ((exists pfrep_position_common_function_result_rightfirst. ((pfrep_position_common_function_result_rightfirst+S (pfrep_power_common_function_result_right)=(K)) /\ ((((exists ff_h_pfp_common_function_result_rightfirstentry. ff_h_pfp_common_function_result_rightfirstentry + S (pfrep_left_common_function_result_right) = S ((S (pfrep_position_common_function_result_rightfirst)) * vc)) /\ exists ff_q_pfp_common_function_result_rightfirstentry. vb = ff_q_pfp_common_function_result_rightfirstentry * S ((S (pfrep_position_common_function_result_rightfirst)) * vc) + (pfrep_left_common_function_result_right)))))) \/ (((exists pfrep_gap_common_function_result_rightfirstoutside. pfrep_gap_common_function_result_rightfirstoutside+(K)=(pfrep_power_common_function_result_right)) /\ (((pfrep_left_common_function_result_right)=0))))) -> ((exists pfrep_position_common_function_result_rightsecond. ((pfrep_position_common_function_result_rightsecond+S (pfrep_power_common_function_result_right)=(J)) /\ ((((exists ff_h_pfp_common_function_result_rightsecondentry. ff_h_pfp_common_function_result_rightsecondentry + S (pfrep_right_common_function_result_right) = S ((S (pfrep_position_common_function_result_rightsecond)) * ec)) /\ exists ff_q_pfp_common_function_result_rightsecondentry. eb = ff_q_pfp_common_function_result_rightsecondentry * S ((S (pfrep_position_common_function_result_rightsecond)) * ec) + (pfrep_right_common_function_result_right)))))) \/ (((exists pfrep_gap_common_function_result_rightsecondoutside. pfrep_gap_common_function_result_rightsecondoutside+(J)=(pfrep_power_common_function_result_right)) /\ (((pfrep_right_common_function_result_right)=0))))) -> pfrep_left_common_function_result_right=pfrep_right_common_function_result_right))))

Constructive proof overview

Generated structural guide

Any two choices of common representatives are pairwise formally equivalent, even at different common lengths; no raw-code or length uniqueness is asserted.

The unchanged tactic script uses 2 declared prerequisites and contains 63 exact native proof lines.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_transitive Alpha theorem; checked-use authorized

Direct dependents

PG0041 prime_field_polynomial_aligned_add_functional

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

63 script commands · 9 reading checkpoints · 2 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro L
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro M
  7. L7
    intro ub
  8. L8
    intro uc
  9. L9
    intro vb
  10. L10
    intro vc
02Fix variables and assumptionsL11–18

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

  1. L11
    intro K
  2. L12
    intro db
  3. L13
    intro dc
  4. L14
    intro eb
  5. L15
    intro ec
  6. L16
    intro J
  7. L17
    intro h
  8. L18
    intro hnew
03Separate the logical casesL19–21

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

  1. L19
    cases h
  2. L20
    cases hnew
  3. L21
    split
04Establish hrL22–31

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

  1. L22
    have hr : PolynomialEquivalent(ub,uc,K,ab,ac,L)Definitions: PolynomialEquivalent
  2. L23
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  3. L24
    specialize prime_field_polynomial_equivalent_symmetric (ac)
  4. L25
    specialize prime_field_polynomial_equivalent_symmetric (L)
  5. L26
    specialize prime_field_polynomial_equivalent_symmetric (ub)
  6. L27
    specialize prime_field_polynomial_equivalent_symmetric (uc)
  7. L28
    specialize prime_field_polynomial_equivalent_symmetric (K)
  8. L29
    apply prime_field_polynomial_equivalent_symmetric
  9. L30
    exact h_left
  10. L31
    specialize prime_field_polynomial_equivalent_transitive (ub)
05Use earlier factsL32–41

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

  1. L32
    specialize prime_field_polynomial_equivalent_transitive (uc)
  2. L33
    specialize prime_field_polynomial_equivalent_transitive (K)
  3. L34
    specialize prime_field_polynomial_equivalent_transitive (ab)
  4. L35
    specialize prime_field_polynomial_equivalent_transitive (ac)
  5. L36
    specialize prime_field_polynomial_equivalent_transitive (L)
  6. L37
    specialize prime_field_polynomial_equivalent_transitive (db)
  7. L38
    specialize prime_field_polynomial_equivalent_transitive (dc)
  8. L39
    specialize prime_field_polynomial_equivalent_transitive (J)
  9. L40
    apply prime_field_polynomial_equivalent_transitive
  10. L41
    exact hr
06Use earlier factsL42–42

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

  1. L42
    exact hnew_left
07Establish hrL43–52

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

  1. L43
    have hr : PolynomialEquivalent(vb,vc,K,bb,bc,M)Definitions: PolynomialEquivalent
  2. L44
    specialize prime_field_polynomial_equivalent_symmetric (bb)
  3. L45
    specialize prime_field_polynomial_equivalent_symmetric (bc)
  4. L46
    specialize prime_field_polynomial_equivalent_symmetric (M)
  5. L47
    specialize prime_field_polynomial_equivalent_symmetric (vb)
  6. L48
    specialize prime_field_polynomial_equivalent_symmetric (vc)
  7. L49
    specialize prime_field_polynomial_equivalent_symmetric (K)
  8. L50
    apply prime_field_polynomial_equivalent_symmetric
  9. L51
    exact h_right
  10. L52
    specialize prime_field_polynomial_equivalent_transitive (vb)
08Use earlier factsL53–62

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

  1. L53
    specialize prime_field_polynomial_equivalent_transitive (vc)
  2. L54
    specialize prime_field_polynomial_equivalent_transitive (K)
  3. L55
    specialize prime_field_polynomial_equivalent_transitive (bb)
  4. L56
    specialize prime_field_polynomial_equivalent_transitive (bc)
  5. L57
    specialize prime_field_polynomial_equivalent_transitive (M)
  6. L58
    specialize prime_field_polynomial_equivalent_transitive (eb)
  7. L59
    specialize prime_field_polynomial_equivalent_transitive (ec)
  8. L60
    specialize prime_field_polynomial_equivalent_transitive (J)
  9. L61
    apply prime_field_polynomial_equivalent_transitive
  10. L62
    exact hr
09Use earlier factsL63–63

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

  1. L63
    exact hnew_right

Library-wide reading audit

Original exact command ledger · 63 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro L
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro M
  7. 0007intro ub
  8. 0008intro uc
  9. 0009intro vb
  10. 0010intro vc
  11. 0011intro K
  12. 0012intro db
  13. 0013intro dc
  14. 0014intro eb
  15. 0015intro ec
  16. 0016intro J
  17. 0017intro h
  18. 0018intro hnew
  19. 0019cases h
  20. 0020cases hnew
  21. 0021split
  22. 0022have hr : forall pfrep_power_common_function_left_reverse pfrep_left_common_function_left_reverse pfrep_right_common_function_left_reverse. ((exists pfrep_position_common_function_left_reversefirst. ((pfrep_position_common_function_left_reversefirst+S (pfrep_power_common_function_left_reverse)=(K)) /\ ((((exists ff_h_pfp_common_function_left_reversefirstentry. ff_h_pfp_common_function_left_reversefirstentry + S (pfrep_left_common_function_left_reverse) = S ((S (pfrep_position_common_function_left_reversefirst)) * uc)) /\ exists ff_q_pfp_common_function_left_reversefirstentry. ub = ff_q_pfp_common_function_left_reversefirstentry * S ((S (pfrep_position_common_function_left_reversefirst)) * uc) + (pfrep_left_common_function_left_reverse)))))) \/ (((exists pfrep_gap_common_function_left_reversefirstoutside. pfrep_gap_common_function_left_reversefirstoutside+(K)=(pfrep_power_common_function_left_reverse)) /\ (((pfrep_left_common_function_left_reverse)=0))))) -> ((exists pfrep_position_common_function_left_reversesecond. ((pfrep_position_common_function_left_reversesecond+S (pfrep_power_common_function_left_reverse)=(L)) /\ ((((exists ff_h_pfp_common_function_left_reversesecondentry. ff_h_pfp_common_function_left_reversesecondentry + S (pfrep_right_common_function_left_reverse) = S ((S (pfrep_position_common_function_left_reversesecond)) * ac)) /\ exists ff_q_pfp_common_function_left_reversesecondentry. ab = ff_q_pfp_common_function_left_reversesecondentry * S ((S (pfrep_position_common_function_left_reversesecond)) * ac) + (pfrep_right_common_function_left_reverse)))))) \/ (((exists pfrep_gap_common_function_left_reversesecondoutside. pfrep_gap_common_function_left_reversesecondoutside+(L)=(pfrep_power_common_function_left_reverse)) /\ (((pfrep_right_common_function_left_reverse)=0))))) -> pfrep_left_common_function_left_reverse=pfrep_right_common_function_left_reverse
  23. 0023specialize prime_field_polynomial_equivalent_symmetric (ab)
  24. 0024specialize prime_field_polynomial_equivalent_symmetric (ac)
  25. 0025specialize prime_field_polynomial_equivalent_symmetric (L)
  26. 0026specialize prime_field_polynomial_equivalent_symmetric (ub)
  27. 0027specialize prime_field_polynomial_equivalent_symmetric (uc)
  28. 0028specialize prime_field_polynomial_equivalent_symmetric (K)
  29. 0029apply prime_field_polynomial_equivalent_symmetric
  30. 0030exact h_left
  31. 0031specialize prime_field_polynomial_equivalent_transitive (ub)
  32. 0032specialize prime_field_polynomial_equivalent_transitive (uc)
  33. 0033specialize prime_field_polynomial_equivalent_transitive (K)
  34. 0034specialize prime_field_polynomial_equivalent_transitive (ab)
  35. 0035specialize prime_field_polynomial_equivalent_transitive (ac)
  36. 0036specialize prime_field_polynomial_equivalent_transitive (L)
  37. 0037specialize prime_field_polynomial_equivalent_transitive (db)
  38. 0038specialize prime_field_polynomial_equivalent_transitive (dc)
  39. 0039specialize prime_field_polynomial_equivalent_transitive (J)
  40. 0040apply prime_field_polynomial_equivalent_transitive
  41. 0041exact hr
  42. 0042exact hnew_left
  43. 0043have hr : forall pfrep_power_common_function_right_reverse pfrep_left_common_function_right_reverse pfrep_right_common_function_right_reverse. ((exists pfrep_position_common_function_right_reversefirst. ((pfrep_position_common_function_right_reversefirst+S (pfrep_power_common_function_right_reverse)=(K)) /\ ((((exists ff_h_pfp_common_function_right_reversefirstentry. ff_h_pfp_common_function_right_reversefirstentry + S (pfrep_left_common_function_right_reverse) = S ((S (pfrep_position_common_function_right_reversefirst)) * vc)) /\ exists ff_q_pfp_common_function_right_reversefirstentry. vb = ff_q_pfp_common_function_right_reversefirstentry * S ((S (pfrep_position_common_function_right_reversefirst)) * vc) + (pfrep_left_common_function_right_reverse)))))) \/ (((exists pfrep_gap_common_function_right_reversefirstoutside. pfrep_gap_common_function_right_reversefirstoutside+(K)=(pfrep_power_common_function_right_reverse)) /\ (((pfrep_left_common_function_right_reverse)=0))))) -> ((exists pfrep_position_common_function_right_reversesecond. ((pfrep_position_common_function_right_reversesecond+S (pfrep_power_common_function_right_reverse)=(M)) /\ ((((exists ff_h_pfp_common_function_right_reversesecondentry. ff_h_pfp_common_function_right_reversesecondentry + S (pfrep_right_common_function_right_reverse) = S ((S (pfrep_position_common_function_right_reversesecond)) * bc)) /\ exists ff_q_pfp_common_function_right_reversesecondentry. bb = ff_q_pfp_common_function_right_reversesecondentry * S ((S (pfrep_position_common_function_right_reversesecond)) * bc) + (pfrep_right_common_function_right_reverse)))))) \/ (((exists pfrep_gap_common_function_right_reversesecondoutside. pfrep_gap_common_function_right_reversesecondoutside+(M)=(pfrep_power_common_function_right_reverse)) /\ (((pfrep_right_common_function_right_reverse)=0))))) -> pfrep_left_common_function_right_reverse=pfrep_right_common_function_right_reverse
  44. 0044specialize prime_field_polynomial_equivalent_symmetric (bb)
  45. 0045specialize prime_field_polynomial_equivalent_symmetric (bc)
  46. 0046specialize prime_field_polynomial_equivalent_symmetric (M)
  47. 0047specialize prime_field_polynomial_equivalent_symmetric (vb)
  48. 0048specialize prime_field_polynomial_equivalent_symmetric (vc)
  49. 0049specialize prime_field_polynomial_equivalent_symmetric (K)
  50. 0050apply prime_field_polynomial_equivalent_symmetric
  51. 0051exact h_right
  52. 0052specialize prime_field_polynomial_equivalent_transitive (vb)
  53. 0053specialize prime_field_polynomial_equivalent_transitive (vc)
  54. 0054specialize prime_field_polynomial_equivalent_transitive (K)
  55. 0055specialize prime_field_polynomial_equivalent_transitive (bb)
  56. 0056specialize prime_field_polynomial_equivalent_transitive (bc)
  57. 0057specialize prime_field_polynomial_equivalent_transitive (M)
  58. 0058specialize prime_field_polynomial_equivalent_transitive (eb)
  59. 0059specialize prime_field_polynomial_equivalent_transitive (ec)
  60. 0060specialize prime_field_polynomial_equivalent_transitive (J)
  61. 0061apply prime_field_polynomial_equivalent_transitive
  62. 0062exact hr
  63. 0063exact hnew_right