PX0075

prime_field_polynomial_add_equivalent_congruent

Pairwise formal-equivalent inputs give formal-equivalent actual add outputs at either ordering of the two aligned lengths, including empty prefixes; no output equivalence or raw-code equality is assumed.

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

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ cb. ∀ cc. ∀ L. ∀ AB. ∀ AC. ∀ BB. ∀ BC. ∀ CB. ∀ CC. ∀ K. Prime(p) → PolynomialEquivalent(ab,ac,L,AB,AC,K) → PolynomialEquivalent(bb,bc,L,BB,BC,K) → FpPolyAdd(p,ab,ac,bb,bc,cb,cc,L) → FpPolyAdd(p,AB,AC,BB,BC,CB,CC,K) → PolynomialEquivalent(cb,cc,L,CB,CC,K)

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

Definition DAG

FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 2PolynomialLeftPad(b,c,L,t,d,e) · 4PolynomialEquivalent(b,c,L,d,e,M) · 3Le(a,b) · 2Prime(p) · 1

Actual proof prerequisites

le_total · checked external prerequisiteprime_field_polynomial_equivalent_implies_left_padprime_field_polynomial_add_left_pad_outputprime_field_polynomial_left_pad_equivalentprime_field_polynomial_equivalent_symmetric
Original expanded first-order statement 
forall p ab ac bb bc cb cc L AB AC BB BC CB CC K. (~((p) = 1) /\ forall pfa_factor_left_add_congruent_prime pfa_factor_right_add_congruent_prime. (p) = pfa_factor_left_add_congruent_prime * pfa_factor_right_add_congruent_prime -> pfa_factor_left_add_congruent_prime = 1 \/ pfa_factor_right_add_congruent_prime = 1) -> (forall pfrep_power_add_congruent_first pfrep_left_add_congruent_first pfrep_right_add_congruent_first. ((exists pfrep_position_add_congruent_firstfirst. ((pfrep_position_add_congruent_firstfirst+S (pfrep_power_add_congruent_first)=(L)) /\ ((((exists ff_h_pfp_add_congruent_firstfirstentry. ff_h_pfp_add_congruent_firstfirstentry + S (pfrep_left_add_congruent_first) = S ((S (pfrep_position_add_congruent_firstfirst)) * ac)) /\ exists ff_q_pfp_add_congruent_firstfirstentry. ab = ff_q_pfp_add_congruent_firstfirstentry * S ((S (pfrep_position_add_congruent_firstfirst)) * ac) + (pfrep_left_add_congruent_first)))))) \/ (((exists pfrep_gap_add_congruent_firstfirstoutside. pfrep_gap_add_congruent_firstfirstoutside+(L)=(pfrep_power_add_congruent_first)) /\ (((pfrep_left_add_congruent_first)=0))))) -> ((exists pfrep_position_add_congruent_firstsecond. ((pfrep_position_add_congruent_firstsecond+S (pfrep_power_add_congruent_first)=(K)) /\ ((((exists ff_h_pfp_add_congruent_firstsecondentry. ff_h_pfp_add_congruent_firstsecondentry + S (pfrep_right_add_congruent_first) = S ((S (pfrep_position_add_congruent_firstsecond)) * AC)) /\ exists ff_q_pfp_add_congruent_firstsecondentry. AB = ff_q_pfp_add_congruent_firstsecondentry * S ((S (pfrep_position_add_congruent_firstsecond)) * AC) + (pfrep_right_add_congruent_first)))))) \/ (((exists pfrep_gap_add_congruent_firstsecondoutside. pfrep_gap_add_congruent_firstsecondoutside+(K)=(pfrep_power_add_congruent_first)) /\ (((pfrep_right_add_congruent_first)=0))))) -> pfrep_left_add_congruent_first=pfrep_right_add_congruent_first) -> (forall pfrep_power_add_congruent_second pfrep_left_add_congruent_second pfrep_right_add_congruent_second. ((exists pfrep_position_add_congruent_secondfirst. ((pfrep_position_add_congruent_secondfirst+S (pfrep_power_add_congruent_second)=(L)) /\ ((((exists ff_h_pfp_add_congruent_secondfirstentry. ff_h_pfp_add_congruent_secondfirstentry + S (pfrep_left_add_congruent_second) = S ((S (pfrep_position_add_congruent_secondfirst)) * bc)) /\ exists ff_q_pfp_add_congruent_secondfirstentry. bb = ff_q_pfp_add_congruent_secondfirstentry * S ((S (pfrep_position_add_congruent_secondfirst)) * bc) + (pfrep_left_add_congruent_second)))))) \/ (((exists pfrep_gap_add_congruent_secondfirstoutside. pfrep_gap_add_congruent_secondfirstoutside+(L)=(pfrep_power_add_congruent_second)) /\ (((pfrep_left_add_congruent_second)=0))))) -> ((exists pfrep_position_add_congruent_secondsecond. ((pfrep_position_add_congruent_secondsecond+S (pfrep_power_add_congruent_second)=(K)) /\ ((((exists ff_h_pfp_add_congruent_secondsecondentry. ff_h_pfp_add_congruent_secondsecondentry + S (pfrep_right_add_congruent_second) = S ((S (pfrep_position_add_congruent_secondsecond)) * BC)) /\ exists ff_q_pfp_add_congruent_secondsecondentry. BB = ff_q_pfp_add_congruent_secondsecondentry * S ((S (pfrep_position_add_congruent_secondsecond)) * BC) + (pfrep_right_add_congruent_second)))))) \/ (((exists pfrep_gap_add_congruent_secondsecondoutside. pfrep_gap_add_congruent_secondsecondoutside+(K)=(pfrep_power_add_congruent_second)) /\ (((pfrep_right_add_congruent_second)=0))))) -> pfrep_left_add_congruent_second=pfrep_right_add_congruent_second) -> (forall pfp_index_add_congruent_original. (exists pfa_gap_add_congruent_originalindex. pfa_gap_add_congruent_originalindex + S (pfp_index_add_congruent_original) = (L)) -> exists pfp_left_add_congruent_original pfp_right_add_congruent_original pfp_value_add_congruent_original. ((((exists ff_h_pfp_add_congruent_originalleft. ff_h_pfp_add_congruent_originalleft + S (pfp_left_add_congruent_original) = S ((S (pfp_index_add_congruent_original)) * ac)) /\ exists ff_q_pfp_add_congruent_originalleft. ab = ff_q_pfp_add_congruent_originalleft * S ((S (pfp_index_add_congruent_original)) * ac) + (pfp_left_add_congruent_original))) /\ (((((exists ff_h_pfp_add_congruent_originalright. ff_h_pfp_add_congruent_originalright + S (pfp_right_add_congruent_original) = S ((S (pfp_index_add_congruent_original)) * bc)) /\ exists ff_q_pfp_add_congruent_originalright. bb = ff_q_pfp_add_congruent_originalright * S ((S (pfp_index_add_congruent_original)) * bc) + (pfp_right_add_congruent_original))) /\ (((((exists ff_h_pfp_add_congruent_originaltarget. ff_h_pfp_add_congruent_originaltarget + S (pfp_value_add_congruent_original) = S ((S (pfp_index_add_congruent_original)) * cc)) /\ exists ff_q_pfp_add_congruent_originaltarget. cb = ff_q_pfp_add_congruent_originaltarget * S ((S (pfp_index_add_congruent_original)) * cc) + (pfp_value_add_congruent_original))) /\ ((((exists pfa_gap_add_congruent_originaloperationleft. pfa_gap_add_congruent_originaloperationleft + S (pfp_left_add_congruent_original) = (p)) /\ (((exists pfa_gap_add_congruent_originaloperationright. pfa_gap_add_congruent_originaloperationright + S (pfp_right_add_congruent_original) = (p)) /\ ((((exists pfa_gap_add_congruent_originaloperationresultbound. pfa_gap_add_congruent_originaloperationresultbound + S (pfp_value_add_congruent_original) = (p)) /\ ((exists pfa_offset_left_add_congruent_originaloperationresultcongruence pfa_offset_right_add_congruent_originaloperationresultcongruence. ((pfp_left_add_congruent_original) + (pfp_right_add_congruent_original)) + (p) * pfa_offset_left_add_congruent_originaloperationresultcongruence = (pfp_value_add_congruent_original) + (p) * pfa_offset_right_add_congruent_originaloperationresultcongruence)))))))))))))))) -> (forall pfp_index_add_congruent_other. (exists pfa_gap_add_congruent_otherindex. pfa_gap_add_congruent_otherindex + S (pfp_index_add_congruent_other) = (K)) -> exists pfp_left_add_congruent_other pfp_right_add_congruent_other pfp_value_add_congruent_other. ((((exists ff_h_pfp_add_congruent_otherleft. ff_h_pfp_add_congruent_otherleft + S (pfp_left_add_congruent_other) = S ((S (pfp_index_add_congruent_other)) * AC)) /\ exists ff_q_pfp_add_congruent_otherleft. AB = ff_q_pfp_add_congruent_otherleft * S ((S (pfp_index_add_congruent_other)) * AC) + (pfp_left_add_congruent_other))) /\ (((((exists ff_h_pfp_add_congruent_otherright. ff_h_pfp_add_congruent_otherright + S (pfp_right_add_congruent_other) = S ((S (pfp_index_add_congruent_other)) * BC)) /\ exists ff_q_pfp_add_congruent_otherright. BB = ff_q_pfp_add_congruent_otherright * S ((S (pfp_index_add_congruent_other)) * BC) + (pfp_right_add_congruent_other))) /\ (((((exists ff_h_pfp_add_congruent_othertarget. ff_h_pfp_add_congruent_othertarget + S (pfp_value_add_congruent_other) = S ((S (pfp_index_add_congruent_other)) * CC)) /\ exists ff_q_pfp_add_congruent_othertarget. CB = ff_q_pfp_add_congruent_othertarget * S ((S (pfp_index_add_congruent_other)) * CC) + (pfp_value_add_congruent_other))) /\ ((((exists pfa_gap_add_congruent_otheroperationleft. pfa_gap_add_congruent_otheroperationleft + S (pfp_left_add_congruent_other) = (p)) /\ (((exists pfa_gap_add_congruent_otheroperationright. pfa_gap_add_congruent_otheroperationright + S (pfp_right_add_congruent_other) = (p)) /\ ((((exists pfa_gap_add_congruent_otheroperationresultbound. pfa_gap_add_congruent_otheroperationresultbound + S (pfp_value_add_congruent_other) = (p)) /\ ((exists pfa_offset_left_add_congruent_otheroperationresultcongruence pfa_offset_right_add_congruent_otheroperationresultcongruence. ((pfp_left_add_congruent_other) + (pfp_right_add_congruent_other)) + (p) * pfa_offset_left_add_congruent_otheroperationresultcongruence = (pfp_value_add_congruent_other) + (p) * pfa_offset_right_add_congruent_otheroperationresultcongruence)))))))))))))))) -> (forall pfrep_power_add_congruent_result pfrep_left_add_congruent_result pfrep_right_add_congruent_result. ((exists pfrep_position_add_congruent_resultfirst. ((pfrep_position_add_congruent_resultfirst+S (pfrep_power_add_congruent_result)=(L)) /\ ((((exists ff_h_pfp_add_congruent_resultfirstentry. ff_h_pfp_add_congruent_resultfirstentry + S (pfrep_left_add_congruent_result) = S ((S (pfrep_position_add_congruent_resultfirst)) * cc)) /\ exists ff_q_pfp_add_congruent_resultfirstentry. cb = ff_q_pfp_add_congruent_resultfirstentry * S ((S (pfrep_position_add_congruent_resultfirst)) * cc) + (pfrep_left_add_congruent_result)))))) \/ (((exists pfrep_gap_add_congruent_resultfirstoutside. pfrep_gap_add_congruent_resultfirstoutside+(L)=(pfrep_power_add_congruent_result)) /\ (((pfrep_left_add_congruent_result)=0))))) -> ((exists pfrep_position_add_congruent_resultsecond. ((pfrep_position_add_congruent_resultsecond+S (pfrep_power_add_congruent_result)=(K)) /\ ((((exists ff_h_pfp_add_congruent_resultsecondentry. ff_h_pfp_add_congruent_resultsecondentry + S (pfrep_right_add_congruent_result) = S ((S (pfrep_position_add_congruent_resultsecond)) * CC)) /\ exists ff_q_pfp_add_congruent_resultsecondentry. CB = ff_q_pfp_add_congruent_resultsecondentry * S ((S (pfrep_position_add_congruent_resultsecond)) * CC) + (pfrep_right_add_congruent_result)))))) \/ (((exists pfrep_gap_add_congruent_resultsecondoutside. pfrep_gap_add_congruent_resultsecondoutside+(K)=(pfrep_power_add_congruent_result)) /\ (((pfrep_right_add_congruent_result)=0))))) -> pfrep_left_add_congruent_result=pfrep_right_add_congruent_result)

Complete tactic proof in conservative notation

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

154 script commands · 20 reading checkpoints · 5 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 equivalent implies left padprime field polynomial left pad equivalentprime field polynomial add left pad outputprime field polynomial equivalent symmetric
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 bb
  5. L5
    intro bc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro L
  9. L9
    intro AB
  10. L10
    intro AC
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 CB
  4. L14
    intro CC
  5. L15
    intro K
  6. L16
    intro hp
  7. L17
    intro hA
  8. L18
    intro hB
  9. L19
    intro ho
  10. L20
    intro hn
03Establish horderL21–24

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

  1. L21
    have horder : Le(L,K) ∨ Le(K,L)Definitions: Le(L,K)Le(K,L)Original native command in the exact edition
  2. L22
    specialize le_total (L)
  3. L23
    specialize le_total (K)
  4. L24
    apply le_total
04Separate the logical casesL25–26

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

  1. L25
    cases horder
  2. L26
    cases horder_left
05Calculate and transport equalitiesL27–33

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

  1. L27
    rewrite <- horder_left_witness at hA
  2. L28
    rewrite <- horder_left_witness at hA
  3. L29
    rewrite <- horder_left_witness at hB
  4. L30
    rewrite <- horder_left_witness at hB
  5. L31
    rewrite <- horder_left_witness at hn
  6. L32
    rewrite <- horder_left_witness
  7. L33
    rewrite <- horder_left_witness
06Establish hpadAL34–42

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

  1. L34
    have hpadA : PolynomialLeftPad(ab,ac,L,x,AB,AC)Definitions: PolynomialLeftPad(ab,ac,L,x,AB,AC)Original native command in the exact edition
  2. L35
    specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  3. L36
    specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  4. L37
    specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  5. L38
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L39
    specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  7. L40
    specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  8. L41
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L42
    exact hA
07Establish hpadBL43–52

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

  1. L43
    have hpadB : PolynomialLeftPad(bb,bc,L,x,BB,BC)Definitions: PolynomialLeftPad(bb,bc,L,x,BB,BC)Original native command in the exact edition
  2. L44
    specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  3. L45
    specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  4. L46
    specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  5. L47
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L48
    specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  7. L49
    specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  8. L50
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L51
    exact hB
  10. L52
    specialize prime_field_polynomial_left_pad_equivalent (cb)
08Use earlier factsL53–62

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

  1. L53
    specialize prime_field_polynomial_left_pad_equivalent (cc)
  2. L54
    specialize prime_field_polynomial_left_pad_equivalent (L)
  3. L55
    specialize prime_field_polynomial_left_pad_equivalent (x)
  4. L56
    specialize prime_field_polynomial_left_pad_equivalent (CB)
  5. L57
    specialize prime_field_polynomial_left_pad_equivalent (CC)
  6. L58
    apply prime_field_polynomial_left_pad_equivalent
  7. L59
    specialize prime_field_polynomial_add_left_pad_output (p)
  8. L60
    specialize prime_field_polynomial_add_left_pad_output (ab)
  9. L61
    specialize prime_field_polynomial_add_left_pad_output (ac)
  10. L62
    specialize prime_field_polynomial_add_left_pad_output (bb)
09Use earlier factsL63–72

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

  1. L63
    specialize prime_field_polynomial_add_left_pad_output (bc)
  2. L64
    specialize prime_field_polynomial_add_left_pad_output (cb)
  3. L65
    specialize prime_field_polynomial_add_left_pad_output (cc)
  4. L66
    specialize prime_field_polynomial_add_left_pad_output (L)
  5. L67
    specialize prime_field_polynomial_add_left_pad_output (x)
  6. L68
    specialize prime_field_polynomial_add_left_pad_output (AB)
  7. L69
    specialize prime_field_polynomial_add_left_pad_output (AC)
  8. L70
    specialize prime_field_polynomial_add_left_pad_output (BB)
  9. L71
    specialize prime_field_polynomial_add_left_pad_output (BC)
  10. L72
    specialize prime_field_polynomial_add_left_pad_output (CB)
10Use earlier factsL73–79

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

  1. L73
    specialize prime_field_polynomial_add_left_pad_output (CC)
  2. L74
    apply prime_field_polynomial_add_left_pad_output
  3. L75
    exact hp
  4. L76
    exact ho
  5. L77
    exact hpadA
  6. L78
    exact hpadB
  7. L79
    exact hn
11Separate the logical casesL80–80

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

  1. L80
    cases horder_right
12Calculate and transport equalitiesL81–87

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

  1. L81
    rewrite <- horder_right_witness at hA
  2. L82
    rewrite <- horder_right_witness at hA
  3. L83
    rewrite <- horder_right_witness at hB
  4. L84
    rewrite <- horder_right_witness at hB
  5. L85
    rewrite <- horder_right_witness at ho
  6. L86
    rewrite <- horder_right_witness
  7. L87
    rewrite <- horder_right_witness
13Establish hpadAL88–97

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

  1. L88
    have hpadA : PolynomialLeftPad(AB,AC,K,x,ab,ac)Definitions: PolynomialLeftPad(AB,AC,K,x,ab,ac)Original native command in the exact edition
  2. L89
    specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  3. L90
    specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  4. L91
    specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  5. L92
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L93
    specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  7. L94
    specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  8. L95
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L96
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  10. L97
    specialize prime_field_polynomial_equivalent_symmetric (ac)
14Use earlier factsL98–103

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

  1. L98
    specialize prime_field_polynomial_equivalent_symmetric (x+K)
  2. L99
    specialize prime_field_polynomial_equivalent_symmetric (AB)
  3. L100
    specialize prime_field_polynomial_equivalent_symmetric (AC)
  4. L101
    specialize prime_field_polynomial_equivalent_symmetric (K)
  5. L102
    apply prime_field_polynomial_equivalent_symmetric
  6. L103
    exact hA
15Establish hpadBL104–113

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

  1. L104
    have hpadB : PolynomialLeftPad(BB,BC,K,x,bb,bc)Definitions: PolynomialLeftPad(BB,BC,K,x,bb,bc)Original native command in the exact edition
  2. L105
    specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  3. L106
    specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  4. L107
    specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  5. L108
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L109
    specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  7. L110
    specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  8. L111
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L112
    specialize prime_field_polynomial_equivalent_symmetric (bb)
  10. L113
    specialize prime_field_polynomial_equivalent_symmetric (bc)
16Use earlier factsL114–123

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

  1. L114
    specialize prime_field_polynomial_equivalent_symmetric (x+K)
  2. L115
    specialize prime_field_polynomial_equivalent_symmetric (BB)
  3. L116
    specialize prime_field_polynomial_equivalent_symmetric (BC)
  4. L117
    specialize prime_field_polynomial_equivalent_symmetric (K)
  5. L118
    apply prime_field_polynomial_equivalent_symmetric
  6. L119
    exact hB
  7. L120
    specialize prime_field_polynomial_equivalent_symmetric (CB)
  8. L121
    specialize prime_field_polynomial_equivalent_symmetric (CC)
  9. L122
    specialize prime_field_polynomial_equivalent_symmetric (K)
  10. L123
    specialize prime_field_polynomial_equivalent_symmetric (cb)
17Use earlier factsL124–133

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

  1. L124
    specialize prime_field_polynomial_equivalent_symmetric (cc)
  2. L125
    specialize prime_field_polynomial_equivalent_symmetric (x+K)
  3. L126
    apply prime_field_polynomial_equivalent_symmetric
  4. L127
    specialize prime_field_polynomial_left_pad_equivalent (CB)
  5. L128
    specialize prime_field_polynomial_left_pad_equivalent (CC)
  6. L129
    specialize prime_field_polynomial_left_pad_equivalent (K)
  7. L130
    specialize prime_field_polynomial_left_pad_equivalent (x)
  8. L131
    specialize prime_field_polynomial_left_pad_equivalent (cb)
  9. L132
    specialize prime_field_polynomial_left_pad_equivalent (cc)
  10. L133
    apply prime_field_polynomial_left_pad_equivalent
18Use earlier factsL134–143

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

  1. L134
    specialize prime_field_polynomial_add_left_pad_output (p)
  2. L135
    specialize prime_field_polynomial_add_left_pad_output (AB)
  3. L136
    specialize prime_field_polynomial_add_left_pad_output (AC)
  4. L137
    specialize prime_field_polynomial_add_left_pad_output (BB)
  5. L138
    specialize prime_field_polynomial_add_left_pad_output (BC)
  6. L139
    specialize prime_field_polynomial_add_left_pad_output (CB)
  7. L140
    specialize prime_field_polynomial_add_left_pad_output (CC)
  8. L141
    specialize prime_field_polynomial_add_left_pad_output (K)
  9. L142
    specialize prime_field_polynomial_add_left_pad_output (x)
  10. L143
    specialize prime_field_polynomial_add_left_pad_output (ab)
19Use earlier factsL144–153

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

  1. L144
    specialize prime_field_polynomial_add_left_pad_output (ac)
  2. L145
    specialize prime_field_polynomial_add_left_pad_output (bb)
  3. L146
    specialize prime_field_polynomial_add_left_pad_output (bc)
  4. L147
    specialize prime_field_polynomial_add_left_pad_output (cb)
  5. L148
    specialize prime_field_polynomial_add_left_pad_output (cc)
  6. L149
    apply prime_field_polynomial_add_left_pad_output
  7. L150
    exact hp
  8. L151
    exact hn
  9. L152
    exact hpadA
  10. L153
    exact hpadB
20Use earlier factsL154–154

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

  1. L154
    exact ho

Library-wide reading audit

Original defined command ledger · 154 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro L
  9. 0009intro AB
  10. 0010intro AC
  11. 0011intro BB
  12. 0012intro BC
  13. 0013intro CB
  14. 0014intro CC
  15. 0015intro K
  16. 0016intro hp
  17. 0017intro hA
  18. 0018intro hB
  19. 0019intro ho
  20. 0020intro hn
  21. 0021have horder : Le(L,K) ∨ Le(K,L)
  22. 0022specialize le_total (L)
  23. 0023specialize le_total (K)
  24. 0024apply le_total
  25. 0025cases horder
  26. 0026cases horder_left
  27. 0027rewrite <- horder_left_witness at hA
  28. 0028rewrite <- horder_left_witness at hA
  29. 0029rewrite <- horder_left_witness at hB
  30. 0030rewrite <- horder_left_witness at hB
  31. 0031rewrite <- horder_left_witness at hn
  32. 0032rewrite <- horder_left_witness
  33. 0033rewrite <- horder_left_witness
  34. 0034have hpadA : PolynomialLeftPad(ab,ac,L,x,AB,AC)
  35. 0035specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  36. 0036specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  37. 0037specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  38. 0038specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  39. 0039specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  40. 0040specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  41. 0041apply prime_field_polynomial_equivalent_implies_left_pad
  42. 0042exact hA
  43. 0043have hpadB : PolynomialLeftPad(bb,bc,L,x,BB,BC)
  44. 0044specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  45. 0045specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  46. 0046specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  47. 0047specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  48. 0048specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  49. 0049specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  50. 0050apply prime_field_polynomial_equivalent_implies_left_pad
  51. 0051exact hB
  52. 0052specialize prime_field_polynomial_left_pad_equivalent (cb)
  53. 0053specialize prime_field_polynomial_left_pad_equivalent (cc)
  54. 0054specialize prime_field_polynomial_left_pad_equivalent (L)
  55. 0055specialize prime_field_polynomial_left_pad_equivalent (x)
  56. 0056specialize prime_field_polynomial_left_pad_equivalent (CB)
  57. 0057specialize prime_field_polynomial_left_pad_equivalent (CC)
  58. 0058apply prime_field_polynomial_left_pad_equivalent
  59. 0059specialize prime_field_polynomial_add_left_pad_output (p)
  60. 0060specialize prime_field_polynomial_add_left_pad_output (ab)
  61. 0061specialize prime_field_polynomial_add_left_pad_output (ac)
  62. 0062specialize prime_field_polynomial_add_left_pad_output (bb)
  63. 0063specialize prime_field_polynomial_add_left_pad_output (bc)
  64. 0064specialize prime_field_polynomial_add_left_pad_output (cb)
  65. 0065specialize prime_field_polynomial_add_left_pad_output (cc)
  66. 0066specialize prime_field_polynomial_add_left_pad_output (L)
  67. 0067specialize prime_field_polynomial_add_left_pad_output (x)
  68. 0068specialize prime_field_polynomial_add_left_pad_output (AB)
  69. 0069specialize prime_field_polynomial_add_left_pad_output (AC)
  70. 0070specialize prime_field_polynomial_add_left_pad_output (BB)
  71. 0071specialize prime_field_polynomial_add_left_pad_output (BC)
  72. 0072specialize prime_field_polynomial_add_left_pad_output (CB)
  73. 0073specialize prime_field_polynomial_add_left_pad_output (CC)
  74. 0074apply prime_field_polynomial_add_left_pad_output
  75. 0075exact hp
  76. 0076exact ho
  77. 0077exact hpadA
  78. 0078exact hpadB
  79. 0079exact hn
  80. 0080cases horder_right
  81. 0081rewrite <- horder_right_witness at hA
  82. 0082rewrite <- horder_right_witness at hA
  83. 0083rewrite <- horder_right_witness at hB
  84. 0084rewrite <- horder_right_witness at hB
  85. 0085rewrite <- horder_right_witness at ho
  86. 0086rewrite <- horder_right_witness
  87. 0087rewrite <- horder_right_witness
  88. 0088have hpadA : PolynomialLeftPad(AB,AC,K,x,ab,ac)
  89. 0089specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  90. 0090specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  91. 0091specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  92. 0092specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  93. 0093specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  94. 0094specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  95. 0095apply prime_field_polynomial_equivalent_implies_left_pad
  96. 0096specialize prime_field_polynomial_equivalent_symmetric (ab)
  97. 0097specialize prime_field_polynomial_equivalent_symmetric (ac)
  98. 0098specialize prime_field_polynomial_equivalent_symmetric (x+K)
  99. 0099specialize prime_field_polynomial_equivalent_symmetric (AB)
  100. 0100specialize prime_field_polynomial_equivalent_symmetric (AC)
  101. 0101specialize prime_field_polynomial_equivalent_symmetric (K)
  102. 0102apply prime_field_polynomial_equivalent_symmetric
  103. 0103exact hA
  104. 0104have hpadB : PolynomialLeftPad(BB,BC,K,x,bb,bc)
  105. 0105specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  106. 0106specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  107. 0107specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  108. 0108specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  109. 0109specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  110. 0110specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  111. 0111apply prime_field_polynomial_equivalent_implies_left_pad
  112. 0112specialize prime_field_polynomial_equivalent_symmetric (bb)
  113. 0113specialize prime_field_polynomial_equivalent_symmetric (bc)
  114. 0114specialize prime_field_polynomial_equivalent_symmetric (x+K)
  115. 0115specialize prime_field_polynomial_equivalent_symmetric (BB)
  116. 0116specialize prime_field_polynomial_equivalent_symmetric (BC)
  117. 0117specialize prime_field_polynomial_equivalent_symmetric (K)
  118. 0118apply prime_field_polynomial_equivalent_symmetric
  119. 0119exact hB
  120. 0120specialize prime_field_polynomial_equivalent_symmetric (CB)
  121. 0121specialize prime_field_polynomial_equivalent_symmetric (CC)
  122. 0122specialize prime_field_polynomial_equivalent_symmetric (K)
  123. 0123specialize prime_field_polynomial_equivalent_symmetric (cb)
  124. 0124specialize prime_field_polynomial_equivalent_symmetric (cc)
  125. 0125specialize prime_field_polynomial_equivalent_symmetric (x+K)
  126. 0126apply prime_field_polynomial_equivalent_symmetric
  127. 0127specialize prime_field_polynomial_left_pad_equivalent (CB)
  128. 0128specialize prime_field_polynomial_left_pad_equivalent (CC)
  129. 0129specialize prime_field_polynomial_left_pad_equivalent (K)
  130. 0130specialize prime_field_polynomial_left_pad_equivalent (x)
  131. 0131specialize prime_field_polynomial_left_pad_equivalent (cb)
  132. 0132specialize prime_field_polynomial_left_pad_equivalent (cc)
  133. 0133apply prime_field_polynomial_left_pad_equivalent
  134. 0134specialize prime_field_polynomial_add_left_pad_output (p)
  135. 0135specialize prime_field_polynomial_add_left_pad_output (AB)
  136. 0136specialize prime_field_polynomial_add_left_pad_output (AC)
  137. 0137specialize prime_field_polynomial_add_left_pad_output (BB)
  138. 0138specialize prime_field_polynomial_add_left_pad_output (BC)
  139. 0139specialize prime_field_polynomial_add_left_pad_output (CB)
  140. 0140specialize prime_field_polynomial_add_left_pad_output (CC)
  141. 0141specialize prime_field_polynomial_add_left_pad_output (K)
  142. 0142specialize prime_field_polynomial_add_left_pad_output (x)
  143. 0143specialize prime_field_polynomial_add_left_pad_output (ab)
  144. 0144specialize prime_field_polynomial_add_left_pad_output (ac)
  145. 0145specialize prime_field_polynomial_add_left_pad_output (bb)
  146. 0146specialize prime_field_polynomial_add_left_pad_output (bc)
  147. 0147specialize prime_field_polynomial_add_left_pad_output (cb)
  148. 0148specialize prime_field_polynomial_add_left_pad_output (cc)
  149. 0149apply prime_field_polynomial_add_left_pad_output
  150. 0150exact hp
  151. 0151exact hn
  152. 0152exact hpadA
  153. 0153exact hpadB
  154. 0154exact ho