PP001C

prime_field_polynomial_add_associative

Both actual bracketings of three finite coefficient additions yield extensionally equal prefixes.

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

Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ cb. ∀ cc. ∀ xb. ∀ xc. ∀ yb. ∀ yc. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ l. FpPolyAdd(p,ab,ac,bb,bc,xb,xc,l) → FpPolyAdd(p,xb,xc,cb,cc,ub,uc,l) → FpPolyAdd(p,bb,bc,cb,cc,yb,yc,l) → FpPolyAdd(p,ab,ac,yb,yc,vb,vc,l) → BetaPrefixEqual(ub,uc,vb,vc,l)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 4BetaAt(b,c,i,x) · 6

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_add_associative · checked external prerequisiteprime_field_polynomial_add_entry
Original expanded first-order statement 
forall p ab ac bb bc cb cc xb xc yb yc ub uc vb vc l. (forall pfp_index_assoc_ab. (exists pfa_gap_assoc_abindex. pfa_gap_assoc_abindex + S (pfp_index_assoc_ab) = (l)) -> exists pfp_left_assoc_ab pfp_right_assoc_ab pfp_value_assoc_ab. ((((exists ff_h_pfp_assoc_ableft. ff_h_pfp_assoc_ableft + S (pfp_left_assoc_ab) = S ((S (pfp_index_assoc_ab)) * ac)) /\ exists ff_q_pfp_assoc_ableft. ab = ff_q_pfp_assoc_ableft * S ((S (pfp_index_assoc_ab)) * ac) + (pfp_left_assoc_ab))) /\ (((((exists ff_h_pfp_assoc_abright. ff_h_pfp_assoc_abright + S (pfp_right_assoc_ab) = S ((S (pfp_index_assoc_ab)) * bc)) /\ exists ff_q_pfp_assoc_abright. bb = ff_q_pfp_assoc_abright * S ((S (pfp_index_assoc_ab)) * bc) + (pfp_right_assoc_ab))) /\ (((((exists ff_h_pfp_assoc_abtarget. ff_h_pfp_assoc_abtarget + S (pfp_value_assoc_ab) = S ((S (pfp_index_assoc_ab)) * xc)) /\ exists ff_q_pfp_assoc_abtarget. xb = ff_q_pfp_assoc_abtarget * S ((S (pfp_index_assoc_ab)) * xc) + (pfp_value_assoc_ab))) /\ ((((exists pfa_gap_assoc_aboperationleft. pfa_gap_assoc_aboperationleft + S (pfp_left_assoc_ab) = (p)) /\ (((exists pfa_gap_assoc_aboperationright. pfa_gap_assoc_aboperationright + S (pfp_right_assoc_ab) = (p)) /\ ((((exists pfa_gap_assoc_aboperationresultbound. pfa_gap_assoc_aboperationresultbound + S (pfp_value_assoc_ab) = (p)) /\ ((exists pfa_offset_left_assoc_aboperationresultcongruence pfa_offset_right_assoc_aboperationresultcongruence. ((pfp_left_assoc_ab) + (pfp_right_assoc_ab)) + (p) * pfa_offset_left_assoc_aboperationresultcongruence = (pfp_value_assoc_ab) + (p) * pfa_offset_right_assoc_aboperationresultcongruence)))))))))))))))) -> (forall pfp_index_assoc_left. (exists pfa_gap_assoc_leftindex. pfa_gap_assoc_leftindex + S (pfp_index_assoc_left) = (l)) -> exists pfp_left_assoc_left pfp_right_assoc_left pfp_value_assoc_left. ((((exists ff_h_pfp_assoc_leftleft. ff_h_pfp_assoc_leftleft + S (pfp_left_assoc_left) = S ((S (pfp_index_assoc_left)) * xc)) /\ exists ff_q_pfp_assoc_leftleft. xb = ff_q_pfp_assoc_leftleft * S ((S (pfp_index_assoc_left)) * xc) + (pfp_left_assoc_left))) /\ (((((exists ff_h_pfp_assoc_leftright. ff_h_pfp_assoc_leftright + S (pfp_right_assoc_left) = S ((S (pfp_index_assoc_left)) * cc)) /\ exists ff_q_pfp_assoc_leftright. cb = ff_q_pfp_assoc_leftright * S ((S (pfp_index_assoc_left)) * cc) + (pfp_right_assoc_left))) /\ (((((exists ff_h_pfp_assoc_lefttarget. ff_h_pfp_assoc_lefttarget + S (pfp_value_assoc_left) = S ((S (pfp_index_assoc_left)) * uc)) /\ exists ff_q_pfp_assoc_lefttarget. ub = ff_q_pfp_assoc_lefttarget * S ((S (pfp_index_assoc_left)) * uc) + (pfp_value_assoc_left))) /\ ((((exists pfa_gap_assoc_leftoperationleft. pfa_gap_assoc_leftoperationleft + S (pfp_left_assoc_left) = (p)) /\ (((exists pfa_gap_assoc_leftoperationright. pfa_gap_assoc_leftoperationright + S (pfp_right_assoc_left) = (p)) /\ ((((exists pfa_gap_assoc_leftoperationresultbound. pfa_gap_assoc_leftoperationresultbound + S (pfp_value_assoc_left) = (p)) /\ ((exists pfa_offset_left_assoc_leftoperationresultcongruence pfa_offset_right_assoc_leftoperationresultcongruence. ((pfp_left_assoc_left) + (pfp_right_assoc_left)) + (p) * pfa_offset_left_assoc_leftoperationresultcongruence = (pfp_value_assoc_left) + (p) * pfa_offset_right_assoc_leftoperationresultcongruence)))))))))))))))) -> (forall pfp_index_assoc_bc. (exists pfa_gap_assoc_bcindex. pfa_gap_assoc_bcindex + S (pfp_index_assoc_bc) = (l)) -> exists pfp_left_assoc_bc pfp_right_assoc_bc pfp_value_assoc_bc. ((((exists ff_h_pfp_assoc_bcleft. ff_h_pfp_assoc_bcleft + S (pfp_left_assoc_bc) = S ((S (pfp_index_assoc_bc)) * bc)) /\ exists ff_q_pfp_assoc_bcleft. bb = ff_q_pfp_assoc_bcleft * S ((S (pfp_index_assoc_bc)) * bc) + (pfp_left_assoc_bc))) /\ (((((exists ff_h_pfp_assoc_bcright. ff_h_pfp_assoc_bcright + S (pfp_right_assoc_bc) = S ((S (pfp_index_assoc_bc)) * cc)) /\ exists ff_q_pfp_assoc_bcright. cb = ff_q_pfp_assoc_bcright * S ((S (pfp_index_assoc_bc)) * cc) + (pfp_right_assoc_bc))) /\ (((((exists ff_h_pfp_assoc_bctarget. ff_h_pfp_assoc_bctarget + S (pfp_value_assoc_bc) = S ((S (pfp_index_assoc_bc)) * yc)) /\ exists ff_q_pfp_assoc_bctarget. yb = ff_q_pfp_assoc_bctarget * S ((S (pfp_index_assoc_bc)) * yc) + (pfp_value_assoc_bc))) /\ ((((exists pfa_gap_assoc_bcoperationleft. pfa_gap_assoc_bcoperationleft + S (pfp_left_assoc_bc) = (p)) /\ (((exists pfa_gap_assoc_bcoperationright. pfa_gap_assoc_bcoperationright + S (pfp_right_assoc_bc) = (p)) /\ ((((exists pfa_gap_assoc_bcoperationresultbound. pfa_gap_assoc_bcoperationresultbound + S (pfp_value_assoc_bc) = (p)) /\ ((exists pfa_offset_left_assoc_bcoperationresultcongruence pfa_offset_right_assoc_bcoperationresultcongruence. ((pfp_left_assoc_bc) + (pfp_right_assoc_bc)) + (p) * pfa_offset_left_assoc_bcoperationresultcongruence = (pfp_value_assoc_bc) + (p) * pfa_offset_right_assoc_bcoperationresultcongruence)))))))))))))))) -> (forall pfp_index_assoc_right. (exists pfa_gap_assoc_rightindex. pfa_gap_assoc_rightindex + S (pfp_index_assoc_right) = (l)) -> exists pfp_left_assoc_right pfp_right_assoc_right pfp_value_assoc_right. ((((exists ff_h_pfp_assoc_rightleft. ff_h_pfp_assoc_rightleft + S (pfp_left_assoc_right) = S ((S (pfp_index_assoc_right)) * ac)) /\ exists ff_q_pfp_assoc_rightleft. ab = ff_q_pfp_assoc_rightleft * S ((S (pfp_index_assoc_right)) * ac) + (pfp_left_assoc_right))) /\ (((((exists ff_h_pfp_assoc_rightright. ff_h_pfp_assoc_rightright + S (pfp_right_assoc_right) = S ((S (pfp_index_assoc_right)) * yc)) /\ exists ff_q_pfp_assoc_rightright. yb = ff_q_pfp_assoc_rightright * S ((S (pfp_index_assoc_right)) * yc) + (pfp_right_assoc_right))) /\ (((((exists ff_h_pfp_assoc_righttarget. ff_h_pfp_assoc_righttarget + S (pfp_value_assoc_right) = S ((S (pfp_index_assoc_right)) * vc)) /\ exists ff_q_pfp_assoc_righttarget. vb = ff_q_pfp_assoc_righttarget * S ((S (pfp_index_assoc_right)) * vc) + (pfp_value_assoc_right))) /\ ((((exists pfa_gap_assoc_rightoperationleft. pfa_gap_assoc_rightoperationleft + S (pfp_left_assoc_right) = (p)) /\ (((exists pfa_gap_assoc_rightoperationright. pfa_gap_assoc_rightoperationright + S (pfp_right_assoc_right) = (p)) /\ ((((exists pfa_gap_assoc_rightoperationresultbound. pfa_gap_assoc_rightoperationresultbound + S (pfp_value_assoc_right) = (p)) /\ ((exists pfa_offset_left_assoc_rightoperationresultcongruence pfa_offset_right_assoc_rightoperationresultcongruence. ((pfp_left_assoc_right) + (pfp_right_assoc_right)) + (p) * pfa_offset_left_assoc_rightoperationresultcongruence = (pfp_value_assoc_right) + (p) * pfa_offset_right_assoc_rightoperationresultcongruence)))))))))))))))) -> (forall mdr_i_pfp_assoc_result mdr_a_pfp_assoc_result. (exists mdr_gap_pfp_assoc_resultb. mdr_gap_pfp_assoc_resultb + S (mdr_i_pfp_assoc_result) = (l)) -> (((exists ff_h_mdr_pfp_assoc_resulto. ff_h_mdr_pfp_assoc_resulto + S (mdr_a_pfp_assoc_result) = S ((S (mdr_i_pfp_assoc_result)) * uc)) /\ exists ff_q_mdr_pfp_assoc_resulto. ub = ff_q_mdr_pfp_assoc_resulto * S ((S (mdr_i_pfp_assoc_result)) * uc) + (mdr_a_pfp_assoc_result))) -> (((exists ff_h_mdr_pfp_assoc_resultn. ff_h_mdr_pfp_assoc_resultn + S (mdr_a_pfp_assoc_result) = S ((S (mdr_i_pfp_assoc_result)) * vc)) /\ exists ff_q_mdr_pfp_assoc_resultn. vb = ff_q_mdr_pfp_assoc_resultn * S ((S (mdr_i_pfp_assoc_result)) * vc) + (mdr_a_pfp_assoc_result))))

Complete tactic proof in conservative notation

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

145 script commands · 26 reading checkpoints · 7 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
prime field polynomial add entry
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 xb
  9. L9
    intro xc
  10. L10
    intro yb
02Fix variables and assumptionsL11–20

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

  1. L11
    intro yc
  2. L12
    intro ub
  3. L13
    intro uc
  4. L14
    intro vb
  5. L15
    intro vc
  6. L16
    intro l
  7. L17
    intro hab
  8. L18
    intro hleft
  9. L19
    intro hbc
  10. L20
    intro hright
03Fix variables and assumptionsL21–24

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

  1. L21
    intro i
  2. L22
    intro r
  3. L23
    intro hi
  4. L24
    intro hr
04Establish entry_aL25–29

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

  1. L25
    have entry_a : ∃ z. BetaAt(ab,ac,i,z)Definitions: BetaAt(ab,ac,i,z)Original native command in the exact edition
  2. L26
    specialize beta_at_exists (ab)
  3. L27
    specialize beta_at_exists (ac)
  4. L28
    specialize beta_at_exists (i)
  5. L29
    apply beta_at_exists
05Separate the logical casesL30–30

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

  1. L30
    cases entry_a
06Establish entry_bL31–35

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

  1. L31
    have entry_b : ∃ z. BetaAt(bb,bc,i,z)Definitions: BetaAt(bb,bc,i,z)Original native command in the exact edition
  2. L32
    specialize beta_at_exists (bb)
  3. L33
    specialize beta_at_exists (bc)
  4. L34
    specialize beta_at_exists (i)
  5. L35
    apply beta_at_exists
07Separate the logical casesL36–36

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

  1. L36
    cases entry_b
08Establish entry_cL37–41

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

  1. L37
    have entry_c : ∃ z. BetaAt(cb,cc,i,z)Definitions: BetaAt(cb,cc,i,z)Original native command in the exact edition
  2. L38
    specialize beta_at_exists (cb)
  3. L39
    specialize beta_at_exists (cc)
  4. L40
    specialize beta_at_exists (i)
  5. L41
    apply beta_at_exists
09Separate the logical casesL42–42

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

  1. L42
    cases entry_c
10Establish entry_xL43–47

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

  1. L43
    have entry_x : ∃ z. BetaAt(xb,xc,i,z)Definitions: BetaAt(xb,xc,i,z)Original native command in the exact edition
  2. L44
    specialize beta_at_exists (xb)
  3. L45
    specialize beta_at_exists (xc)
  4. L46
    specialize beta_at_exists (i)
  5. L47
    apply beta_at_exists
11Separate the logical casesL48–48

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

  1. L48
    cases entry_x
12Establish entry_yL49–53

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

  1. L49
    have entry_y : ∃ z. BetaAt(yb,yc,i,z)Definitions: BetaAt(yb,yc,i,z)Original native command in the exact edition
  2. L50
    specialize beta_at_exists (yb)
  3. L51
    specialize beta_at_exists (yc)
  4. L52
    specialize beta_at_exists (i)
  5. L53
    apply beta_at_exists
13Separate the logical casesL54–54

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

  1. L54
    cases entry_y
14Establish entry_vL55–59

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

  1. L55
    have entry_v : ∃ z. BetaAt(vb,vc,i,z)Definitions: BetaAt(vb,vc,i,z)Original native command in the exact edition
  2. L56
    specialize beta_at_exists (vb)
  3. L57
    specialize beta_at_exists (vc)
  4. L58
    specialize beta_at_exists (i)
  5. L59
    apply beta_at_exists
15Separate the logical casesL60–60

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

  1. L60
    cases entry_v
16Establish heqL61–70

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

  1. L61
    have heq : r=x5
  2. L62
    specialize prime_field_add_associative (p)
  3. L63
    specialize prime_field_add_associative (x)
  4. L64
    specialize prime_field_add_associative (x1)
  5. L65
    specialize prime_field_add_associative (x2)
  6. L66
    specialize prime_field_add_associative (x3)
  7. L67
    specialize prime_field_add_associative (x4)
  8. L68
    specialize prime_field_add_associative (r)
  9. L69
    specialize prime_field_add_associative (x5)
  10. L70
    apply prime_field_add_associative
17Use earlier factsL71–80

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

  1. L71
    specialize prime_field_polynomial_add_entry (p)
  2. L72
    specialize prime_field_polynomial_add_entry (ab)
  3. L73
    specialize prime_field_polynomial_add_entry (ac)
  4. L74
    specialize prime_field_polynomial_add_entry (bb)
  5. L75
    specialize prime_field_polynomial_add_entry (bc)
  6. L76
    specialize prime_field_polynomial_add_entry (xb)
  7. L77
    specialize prime_field_polynomial_add_entry (xc)
  8. L78
    specialize prime_field_polynomial_add_entry (l)
  9. L79
    specialize prime_field_polynomial_add_entry (i)
  10. L80
    specialize prime_field_polynomial_add_entry (x)
18Use earlier factsL81–90

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

  1. L81
    specialize prime_field_polynomial_add_entry (x1)
  2. L82
    specialize prime_field_polynomial_add_entry (x3)
  3. L83
    apply prime_field_polynomial_add_entry
  4. L84
    exact hab
  5. L85
    exact hi
  6. L86
    exact entry_a_witness
  7. L87
    exact entry_b_witness
  8. L88
    exact entry_x_witness
  9. L89
    specialize prime_field_polynomial_add_entry (p)
  10. L90
    specialize prime_field_polynomial_add_entry (xb)
19Use earlier factsL91–100

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

  1. L91
    specialize prime_field_polynomial_add_entry (xc)
  2. L92
    specialize prime_field_polynomial_add_entry (cb)
  3. L93
    specialize prime_field_polynomial_add_entry (cc)
  4. L94
    specialize prime_field_polynomial_add_entry (ub)
  5. L95
    specialize prime_field_polynomial_add_entry (uc)
  6. L96
    specialize prime_field_polynomial_add_entry (l)
  7. L97
    specialize prime_field_polynomial_add_entry (i)
  8. L98
    specialize prime_field_polynomial_add_entry (x3)
  9. L99
    specialize prime_field_polynomial_add_entry (x2)
  10. L100
    specialize prime_field_polynomial_add_entry (r)
20Use earlier factsL101–110

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

  1. L101
    apply prime_field_polynomial_add_entry
  2. L102
    exact hleft
  3. L103
    exact hi
  4. L104
    exact entry_x_witness
  5. L105
    exact entry_c_witness
  6. L106
    exact hr
  7. L107
    specialize prime_field_polynomial_add_entry (p)
  8. L108
    specialize prime_field_polynomial_add_entry (bb)
  9. L109
    specialize prime_field_polynomial_add_entry (bc)
  10. L110
    specialize prime_field_polynomial_add_entry (cb)
21Use earlier factsL111–120

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

  1. L111
    specialize prime_field_polynomial_add_entry (cc)
  2. L112
    specialize prime_field_polynomial_add_entry (yb)
  3. L113
    specialize prime_field_polynomial_add_entry (yc)
  4. L114
    specialize prime_field_polynomial_add_entry (l)
  5. L115
    specialize prime_field_polynomial_add_entry (i)
  6. L116
    specialize prime_field_polynomial_add_entry (x1)
  7. L117
    specialize prime_field_polynomial_add_entry (x2)
  8. L118
    specialize prime_field_polynomial_add_entry (x4)
  9. L119
    apply prime_field_polynomial_add_entry
  10. L120
    exact hbc
22Use earlier factsL121–130

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

  1. L121
    exact hi
  2. L122
    exact entry_b_witness
  3. L123
    exact entry_c_witness
  4. L124
    exact entry_y_witness
  5. L125
    specialize prime_field_polynomial_add_entry (p)
  6. L126
    specialize prime_field_polynomial_add_entry (ab)
  7. L127
    specialize prime_field_polynomial_add_entry (ac)
  8. L128
    specialize prime_field_polynomial_add_entry (yb)
  9. L129
    specialize prime_field_polynomial_add_entry (yc)
  10. L130
    specialize prime_field_polynomial_add_entry (vb)
23Use earlier factsL131–140

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

  1. L131
    specialize prime_field_polynomial_add_entry (vc)
  2. L132
    specialize prime_field_polynomial_add_entry (l)
  3. L133
    specialize prime_field_polynomial_add_entry (i)
  4. L134
    specialize prime_field_polynomial_add_entry (x)
  5. L135
    specialize prime_field_polynomial_add_entry (x4)
  6. L136
    specialize prime_field_polynomial_add_entry (x5)
  7. L137
    apply prime_field_polynomial_add_entry
  8. L138
    exact hright
  9. L139
    exact hi
  10. L140
    exact entry_a_witness
24Use earlier factsL141–142

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

  1. L141
    exact entry_y_witness
  2. L142
    exact entry_v_witness
25Calculate and transport equalitiesL143–144

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

  1. L143
    rewrite heq
  2. L144
    rewrite heq
26Use earlier factsL145–145

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

  1. L145
    exact entry_v_witness

Library-wide reading audit

Original defined command ledger · 145 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro xb
  9. 0009intro xc
  10. 0010intro yb
  11. 0011intro yc
  12. 0012intro ub
  13. 0013intro uc
  14. 0014intro vb
  15. 0015intro vc
  16. 0016intro l
  17. 0017intro hab
  18. 0018intro hleft
  19. 0019intro hbc
  20. 0020intro hright
  21. 0021intro i
  22. 0022intro r
  23. 0023intro hi
  24. 0024intro hr
  25. 0025have entry_a : ∃ z. BetaAt(ab,ac,i,z)
  26. 0026specialize beta_at_exists (ab)
  27. 0027specialize beta_at_exists (ac)
  28. 0028specialize beta_at_exists (i)
  29. 0029apply beta_at_exists
  30. 0030cases entry_a
  31. 0031have entry_b : ∃ z. BetaAt(bb,bc,i,z)
  32. 0032specialize beta_at_exists (bb)
  33. 0033specialize beta_at_exists (bc)
  34. 0034specialize beta_at_exists (i)
  35. 0035apply beta_at_exists
  36. 0036cases entry_b
  37. 0037have entry_c : ∃ z. BetaAt(cb,cc,i,z)
  38. 0038specialize beta_at_exists (cb)
  39. 0039specialize beta_at_exists (cc)
  40. 0040specialize beta_at_exists (i)
  41. 0041apply beta_at_exists
  42. 0042cases entry_c
  43. 0043have entry_x : ∃ z. BetaAt(xb,xc,i,z)
  44. 0044specialize beta_at_exists (xb)
  45. 0045specialize beta_at_exists (xc)
  46. 0046specialize beta_at_exists (i)
  47. 0047apply beta_at_exists
  48. 0048cases entry_x
  49. 0049have entry_y : ∃ z. BetaAt(yb,yc,i,z)
  50. 0050specialize beta_at_exists (yb)
  51. 0051specialize beta_at_exists (yc)
  52. 0052specialize beta_at_exists (i)
  53. 0053apply beta_at_exists
  54. 0054cases entry_y
  55. 0055have entry_v : ∃ z. BetaAt(vb,vc,i,z)
  56. 0056specialize beta_at_exists (vb)
  57. 0057specialize beta_at_exists (vc)
  58. 0058specialize beta_at_exists (i)
  59. 0059apply beta_at_exists
  60. 0060cases entry_v
  61. 0061have heq : r=x5
  62. 0062specialize prime_field_add_associative (p)
  63. 0063specialize prime_field_add_associative (x)
  64. 0064specialize prime_field_add_associative (x1)
  65. 0065specialize prime_field_add_associative (x2)
  66. 0066specialize prime_field_add_associative (x3)
  67. 0067specialize prime_field_add_associative (x4)
  68. 0068specialize prime_field_add_associative (r)
  69. 0069specialize prime_field_add_associative (x5)
  70. 0070apply prime_field_add_associative
  71. 0071specialize prime_field_polynomial_add_entry (p)
  72. 0072specialize prime_field_polynomial_add_entry (ab)
  73. 0073specialize prime_field_polynomial_add_entry (ac)
  74. 0074specialize prime_field_polynomial_add_entry (bb)
  75. 0075specialize prime_field_polynomial_add_entry (bc)
  76. 0076specialize prime_field_polynomial_add_entry (xb)
  77. 0077specialize prime_field_polynomial_add_entry (xc)
  78. 0078specialize prime_field_polynomial_add_entry (l)
  79. 0079specialize prime_field_polynomial_add_entry (i)
  80. 0080specialize prime_field_polynomial_add_entry (x)
  81. 0081specialize prime_field_polynomial_add_entry (x1)
  82. 0082specialize prime_field_polynomial_add_entry (x3)
  83. 0083apply prime_field_polynomial_add_entry
  84. 0084exact hab
  85. 0085exact hi
  86. 0086exact entry_a_witness
  87. 0087exact entry_b_witness
  88. 0088exact entry_x_witness
  89. 0089specialize prime_field_polynomial_add_entry (p)
  90. 0090specialize prime_field_polynomial_add_entry (xb)
  91. 0091specialize prime_field_polynomial_add_entry (xc)
  92. 0092specialize prime_field_polynomial_add_entry (cb)
  93. 0093specialize prime_field_polynomial_add_entry (cc)
  94. 0094specialize prime_field_polynomial_add_entry (ub)
  95. 0095specialize prime_field_polynomial_add_entry (uc)
  96. 0096specialize prime_field_polynomial_add_entry (l)
  97. 0097specialize prime_field_polynomial_add_entry (i)
  98. 0098specialize prime_field_polynomial_add_entry (x3)
  99. 0099specialize prime_field_polynomial_add_entry (x2)
  100. 0100specialize prime_field_polynomial_add_entry (r)
  101. 0101apply prime_field_polynomial_add_entry
  102. 0102exact hleft
  103. 0103exact hi
  104. 0104exact entry_x_witness
  105. 0105exact entry_c_witness
  106. 0106exact hr
  107. 0107specialize prime_field_polynomial_add_entry (p)
  108. 0108specialize prime_field_polynomial_add_entry (bb)
  109. 0109specialize prime_field_polynomial_add_entry (bc)
  110. 0110specialize prime_field_polynomial_add_entry (cb)
  111. 0111specialize prime_field_polynomial_add_entry (cc)
  112. 0112specialize prime_field_polynomial_add_entry (yb)
  113. 0113specialize prime_field_polynomial_add_entry (yc)
  114. 0114specialize prime_field_polynomial_add_entry (l)
  115. 0115specialize prime_field_polynomial_add_entry (i)
  116. 0116specialize prime_field_polynomial_add_entry (x1)
  117. 0117specialize prime_field_polynomial_add_entry (x2)
  118. 0118specialize prime_field_polynomial_add_entry (x4)
  119. 0119apply prime_field_polynomial_add_entry
  120. 0120exact hbc
  121. 0121exact hi
  122. 0122exact entry_b_witness
  123. 0123exact entry_c_witness
  124. 0124exact entry_y_witness
  125. 0125specialize prime_field_polynomial_add_entry (p)
  126. 0126specialize prime_field_polynomial_add_entry (ab)
  127. 0127specialize prime_field_polynomial_add_entry (ac)
  128. 0128specialize prime_field_polynomial_add_entry (yb)
  129. 0129specialize prime_field_polynomial_add_entry (yc)
  130. 0130specialize prime_field_polynomial_add_entry (vb)
  131. 0131specialize prime_field_polynomial_add_entry (vc)
  132. 0132specialize prime_field_polynomial_add_entry (l)
  133. 0133specialize prime_field_polynomial_add_entry (i)
  134. 0134specialize prime_field_polynomial_add_entry (x)
  135. 0135specialize prime_field_polynomial_add_entry (x4)
  136. 0136specialize prime_field_polynomial_add_entry (x5)
  137. 0137apply prime_field_polynomial_add_entry
  138. 0138exact hright
  139. 0139exact hi
  140. 0140exact entry_a_witness
  141. 0141exact entry_y_witness
  142. 0142exact entry_v_witness
  143. 0143rewrite heq
  144. 0144rewrite heq
  145. 0145exact entry_v_witness