PX0073

prime_field_polynomial_add_left_pad_output

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

Actual add outputs inherit the genuine common leading-zero padding of their inputs: construct a padded original output, prove its operation, then identify the supplied output by functionality.

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 p ab ac bb bc cb cc L t AB AC BB BC CB CC. (~((p) = 1) /\ forall pfa_factor_left_add_output_prime pfa_factor_right_add_output_prime. (p) = pfa_factor_left_add_output_prime * pfa_factor_right_add_output_prime -> pfa_factor_left_add_output_prime = 1 \/ pfa_factor_right_add_output_prime = 1) -> (forall pfp_index_add_output_original. (exists pfa_gap_add_output_originalindex. pfa_gap_add_output_originalindex + S (pfp_index_add_output_original) = (L)) -> exists pfp_left_add_output_original pfp_right_add_output_original pfp_value_add_output_original. ((((exists ff_h_pfp_add_output_originalleft. ff_h_pfp_add_output_originalleft + S (pfp_left_add_output_original) = S ((S (pfp_index_add_output_original)) * ac)) /\ exists ff_q_pfp_add_output_originalleft. ab = ff_q_pfp_add_output_originalleft * S ((S (pfp_index_add_output_original)) * ac) + (pfp_left_add_output_original))) /\ (((((exists ff_h_pfp_add_output_originalright. ff_h_pfp_add_output_originalright + S (pfp_right_add_output_original) = S ((S (pfp_index_add_output_original)) * bc)) /\ exists ff_q_pfp_add_output_originalright. bb = ff_q_pfp_add_output_originalright * S ((S (pfp_index_add_output_original)) * bc) + (pfp_right_add_output_original))) /\ (((((exists ff_h_pfp_add_output_originaltarget. ff_h_pfp_add_output_originaltarget + S (pfp_value_add_output_original) = S ((S (pfp_index_add_output_original)) * cc)) /\ exists ff_q_pfp_add_output_originaltarget. cb = ff_q_pfp_add_output_originaltarget * S ((S (pfp_index_add_output_original)) * cc) + (pfp_value_add_output_original))) /\ ((((exists pfa_gap_add_output_originaloperationleft. pfa_gap_add_output_originaloperationleft + S (pfp_left_add_output_original) = (p)) /\ (((exists pfa_gap_add_output_originaloperationright. pfa_gap_add_output_originaloperationright + S (pfp_right_add_output_original) = (p)) /\ ((((exists pfa_gap_add_output_originaloperationresultbound. pfa_gap_add_output_originaloperationresultbound + S (pfp_value_add_output_original) = (p)) /\ ((exists pfa_offset_left_add_output_originaloperationresultcongruence pfa_offset_right_add_output_originaloperationresultcongruence. ((pfp_left_add_output_original) + (pfp_right_add_output_original)) + (p) * pfa_offset_left_add_output_originaloperationresultcongruence = (pfp_value_add_output_original) + (p) * pfa_offset_right_add_output_originaloperationresultcongruence)))))))))))))))) -> (((forall pfp_repeat_index_add_output_leftzeros. (exists pfa_gap_add_output_leftzerosindex. pfa_gap_add_output_leftzerosindex + S (pfp_repeat_index_add_output_leftzeros) = (t)) -> (((exists ff_h_pfp_add_output_leftzerosentry. ff_h_pfp_add_output_leftzerosentry + S (0) = S ((S (pfp_repeat_index_add_output_leftzeros)) * AC)) /\ exists ff_q_pfp_add_output_leftzerosentry. AB = ff_q_pfp_add_output_leftzerosentry * S ((S (pfp_repeat_index_add_output_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_add_output_left pfrep_value_add_output_left. (exists pfa_gap_add_output_leftbound. pfa_gap_add_output_leftbound + S (pfrep_index_add_output_left) = (L)) -> (((exists ff_h_pfp_add_output_leftinput. ff_h_pfp_add_output_leftinput + S (pfrep_value_add_output_left) = S ((S (pfrep_index_add_output_left)) * ac)) /\ exists ff_q_pfp_add_output_leftinput. ab = ff_q_pfp_add_output_leftinput * S ((S (pfrep_index_add_output_left)) * ac) + (pfrep_value_add_output_left))) -> (((exists ff_h_pfp_add_output_leftoutput. ff_h_pfp_add_output_leftoutput + S (pfrep_value_add_output_left) = S ((S ((t)+pfrep_index_add_output_left)) * AC)) /\ exists ff_q_pfp_add_output_leftoutput. AB = ff_q_pfp_add_output_leftoutput * S ((S ((t)+pfrep_index_add_output_left)) * AC) + (pfrep_value_add_output_left))))))) -> (((forall pfp_repeat_index_add_output_rightzeros. (exists pfa_gap_add_output_rightzerosindex. pfa_gap_add_output_rightzerosindex + S (pfp_repeat_index_add_output_rightzeros) = (t)) -> (((exists ff_h_pfp_add_output_rightzerosentry. ff_h_pfp_add_output_rightzerosentry + S (0) = S ((S (pfp_repeat_index_add_output_rightzeros)) * BC)) /\ exists ff_q_pfp_add_output_rightzerosentry. BB = ff_q_pfp_add_output_rightzerosentry * S ((S (pfp_repeat_index_add_output_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_add_output_right pfrep_value_add_output_right. (exists pfa_gap_add_output_rightbound. pfa_gap_add_output_rightbound + S (pfrep_index_add_output_right) = (L)) -> (((exists ff_h_pfp_add_output_rightinput. ff_h_pfp_add_output_rightinput + S (pfrep_value_add_output_right) = S ((S (pfrep_index_add_output_right)) * bc)) /\ exists ff_q_pfp_add_output_rightinput. bb = ff_q_pfp_add_output_rightinput * S ((S (pfrep_index_add_output_right)) * bc) + (pfrep_value_add_output_right))) -> (((exists ff_h_pfp_add_output_rightoutput. ff_h_pfp_add_output_rightoutput + S (pfrep_value_add_output_right) = S ((S ((t)+pfrep_index_add_output_right)) * BC)) /\ exists ff_q_pfp_add_output_rightoutput. BB = ff_q_pfp_add_output_rightoutput * S ((S ((t)+pfrep_index_add_output_right)) * BC) + (pfrep_value_add_output_right))))))) -> (forall pfp_index_add_output_padded. (exists pfa_gap_add_output_paddedindex. pfa_gap_add_output_paddedindex + S (pfp_index_add_output_padded) = (t+L)) -> exists pfp_left_add_output_padded pfp_right_add_output_padded pfp_value_add_output_padded. ((((exists ff_h_pfp_add_output_paddedleft. ff_h_pfp_add_output_paddedleft + S (pfp_left_add_output_padded) = S ((S (pfp_index_add_output_padded)) * AC)) /\ exists ff_q_pfp_add_output_paddedleft. AB = ff_q_pfp_add_output_paddedleft * S ((S (pfp_index_add_output_padded)) * AC) + (pfp_left_add_output_padded))) /\ (((((exists ff_h_pfp_add_output_paddedright. ff_h_pfp_add_output_paddedright + S (pfp_right_add_output_padded) = S ((S (pfp_index_add_output_padded)) * BC)) /\ exists ff_q_pfp_add_output_paddedright. BB = ff_q_pfp_add_output_paddedright * S ((S (pfp_index_add_output_padded)) * BC) + (pfp_right_add_output_padded))) /\ (((((exists ff_h_pfp_add_output_paddedtarget. ff_h_pfp_add_output_paddedtarget + S (pfp_value_add_output_padded) = S ((S (pfp_index_add_output_padded)) * CC)) /\ exists ff_q_pfp_add_output_paddedtarget. CB = ff_q_pfp_add_output_paddedtarget * S ((S (pfp_index_add_output_padded)) * CC) + (pfp_value_add_output_padded))) /\ ((((exists pfa_gap_add_output_paddedoperationleft. pfa_gap_add_output_paddedoperationleft + S (pfp_left_add_output_padded) = (p)) /\ (((exists pfa_gap_add_output_paddedoperationright. pfa_gap_add_output_paddedoperationright + S (pfp_right_add_output_padded) = (p)) /\ ((((exists pfa_gap_add_output_paddedoperationresultbound. pfa_gap_add_output_paddedoperationresultbound + S (pfp_value_add_output_padded) = (p)) /\ ((exists pfa_offset_left_add_output_paddedoperationresultcongruence pfa_offset_right_add_output_paddedoperationresultcongruence. ((pfp_left_add_output_padded) + (pfp_right_add_output_padded)) + (p) * pfa_offset_left_add_output_paddedoperationresultcongruence = (pfp_value_add_output_padded) + (p) * pfa_offset_right_add_output_paddedoperationresultcongruence)))))))))))))))) -> (((forall pfp_repeat_index_add_output_resultzeros. (exists pfa_gap_add_output_resultzerosindex. pfa_gap_add_output_resultzerosindex + S (pfp_repeat_index_add_output_resultzeros) = (t)) -> (((exists ff_h_pfp_add_output_resultzerosentry. ff_h_pfp_add_output_resultzerosentry + S (0) = S ((S (pfp_repeat_index_add_output_resultzeros)) * CC)) /\ exists ff_q_pfp_add_output_resultzerosentry. CB = ff_q_pfp_add_output_resultzerosentry * S ((S (pfp_repeat_index_add_output_resultzeros)) * CC) + (0)))) /\ ((forall pfrep_index_add_output_result pfrep_value_add_output_result. (exists pfa_gap_add_output_resultbound. pfa_gap_add_output_resultbound + S (pfrep_index_add_output_result) = (L)) -> (((exists ff_h_pfp_add_output_resultinput. ff_h_pfp_add_output_resultinput + S (pfrep_value_add_output_result) = S ((S (pfrep_index_add_output_result)) * cc)) /\ exists ff_q_pfp_add_output_resultinput. cb = ff_q_pfp_add_output_resultinput * S ((S (pfrep_index_add_output_result)) * cc) + (pfrep_value_add_output_result))) -> (((exists ff_h_pfp_add_output_resultoutput. ff_h_pfp_add_output_resultoutput + S (pfrep_value_add_output_result) = S ((S ((t)+pfrep_index_add_output_result)) * CC)) /\ exists ff_q_pfp_add_output_resultoutput. CB = ff_q_pfp_add_output_resultoutput * S ((S ((t)+pfrep_index_add_output_result)) * CC) + (pfrep_value_add_output_result)))))))

Constructive proof overview

Generated structural guide

Actual add outputs inherit the genuine common leading-zero padding of their inputs: construct a padded original output, prove its operation, then identify the supplied output by functionality.

The unchanged tactic script uses 4 declared prerequisites and contains 82 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PX0014 prime_field_polynomial_left_pad_exists PX001E prime_field_polynomial_add_left_pad_transport prime_field_polynomial_add_functional Alpha theorem; checked-use authorized PX001D prime_field_polynomial_left_pad_transport

Direct dependents

PX0075 prime_field_polynomial_add_equivalent_congruent

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

82 script commands · 12 reading checkpoints · 3 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.

Named ingredients (3)
prime field polynomial left pad existsprime field polynomial add left pad transportprime field polynomial left pad transport

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 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 t
  10. L10
    intro AB
02Fix variables and assumptionsL11–20

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

  1. L11
    intro AC
  2. L12
    intro BB
  3. L13
    intro BC
  4. L14
    intro CB
  5. L15
    intro CC
  6. L16
    intro hp
  7. L17
    intro ho
  8. L18
    intro hA
  9. L19
    intro hB
  10. L20
    intro hn
03Establish hdL21–26

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

  1. L21
    have hd : ∃ db. ∃ dc. PolynomialLeftPad(cb,cc,L,t,db,dc)Definitions: PolynomialLeftPad
  2. L22
    specialize prime_field_polynomial_left_pad_exists (cb)
  3. L23
    specialize prime_field_polynomial_left_pad_exists (cc)
  4. L24
    specialize prime_field_polynomial_left_pad_exists (t)
  5. L25
    specialize prime_field_polynomial_left_pad_exists (L)
  6. L26
    apply prime_field_polynomial_left_pad_exists
04Separate the logical casesL27–28

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

  1. L27
    cases hd
  2. L28
    cases hd_witness
05Establish hmL29–38

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have hm : FpPolyAdd(p,AB,AC,BB,BC,x,x1,t + L)Definitions: FpPolyAdd
  2. L30
    specialize prime_field_polynomial_add_left_pad_transport (p)
  3. L31
    specialize prime_field_polynomial_add_left_pad_transport (ab)
  4. L32
    specialize prime_field_polynomial_add_left_pad_transport (ac)
  5. L33
    specialize prime_field_polynomial_add_left_pad_transport (bb)
  6. L34
    specialize prime_field_polynomial_add_left_pad_transport (bc)
  7. L35
    specialize prime_field_polynomial_add_left_pad_transport (cb)
  8. L36
    specialize prime_field_polynomial_add_left_pad_transport (cc)
  9. L37
    specialize prime_field_polynomial_add_left_pad_transport (L)
  10. L38
    specialize prime_field_polynomial_add_left_pad_transport (t)
06Use earlier factsL39–48

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

  1. L39
    specialize prime_field_polynomial_add_left_pad_transport (AB)
  2. L40
    specialize prime_field_polynomial_add_left_pad_transport (AC)
  3. L41
    specialize prime_field_polynomial_add_left_pad_transport (BB)
  4. L42
    specialize prime_field_polynomial_add_left_pad_transport (BC)
  5. L43
    specialize prime_field_polynomial_add_left_pad_transport (x)
  6. L44
    specialize prime_field_polynomial_add_left_pad_transport (x1)
  7. L45
    apply prime_field_polynomial_add_left_pad_transport
  8. L46
    exact hp
  9. L47
    exact ho
  10. L48
    exact hA
07Use earlier factsL49–50

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

  1. L49
    exact hB
  2. L50
    exact hd_witness_witness
08Establish heL51–60

Establish this local claim before using it. It is not an additional assumption.

  1. L51
    have he : BetaPrefixEqual(x,x1,CB,CC,t + L)Definitions: BetaPrefixEqual
  2. L52
    specialize prime_field_polynomial_add_functional (p)
  3. L53
    specialize prime_field_polynomial_add_functional (AB)
  4. L54
    specialize prime_field_polynomial_add_functional (AC)
  5. L55
    specialize prime_field_polynomial_add_functional (BB)
  6. L56
    specialize prime_field_polynomial_add_functional (BC)
  7. L57
    specialize prime_field_polynomial_add_functional (x)
  8. L58
    specialize prime_field_polynomial_add_functional (x1)
  9. L59
    specialize prime_field_polynomial_add_functional (CB)
  10. L60
    specialize prime_field_polynomial_add_functional (CC)
09Use earlier factsL61–70

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

  1. L61
    specialize prime_field_polynomial_add_functional (t+L)
  2. L62
    apply prime_field_polynomial_add_functional
  3. L63
    exact hm
  4. L64
    exact hn
  5. L65
    specialize prime_field_polynomial_left_pad_transport (cb)
  6. L66
    specialize prime_field_polynomial_left_pad_transport (cc)
  7. L67
    specialize prime_field_polynomial_left_pad_transport (cb)
  8. L68
    specialize prime_field_polynomial_left_pad_transport (cc)
  9. L69
    specialize prime_field_polynomial_left_pad_transport (L)
  10. L70
    specialize prime_field_polynomial_left_pad_transport (t)
10Use earlier factsL71–75

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

  1. L71
    specialize prime_field_polynomial_left_pad_transport (x)
  2. L72
    specialize prime_field_polynomial_left_pad_transport (x1)
  3. L73
    specialize prime_field_polynomial_left_pad_transport (CB)
  4. L74
    specialize prime_field_polynomial_left_pad_transport (CC)
  5. L75
    apply prime_field_polynomial_left_pad_transport
11Fix variables and assumptionsL76–79

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

  1. L76
    intro i
  2. L77
    intro a
  3. L78
    intro hi
  4. L79
    intro ha
12Use earlier factsL80–82

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

  1. L80
    exact ha
  2. L81
    exact he
  3. L82
    exact hd_witness_witness

Library-wide reading audit

Original exact command ledger · 82 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 t
  10. 0010intro AB
  11. 0011intro AC
  12. 0012intro BB
  13. 0013intro BC
  14. 0014intro CB
  15. 0015intro CC
  16. 0016intro hp
  17. 0017intro ho
  18. 0018intro hA
  19. 0019intro hB
  20. 0020intro hn
  21. 0021have hd : exists db dc. (((forall pfp_repeat_index_add_output_constructedzeros. (exists pfa_gap_add_output_constructedzerosindex. pfa_gap_add_output_constructedzerosindex + S (pfp_repeat_index_add_output_constructedzeros) = (t)) -> (((exists ff_h_pfp_add_output_constructedzerosentry. ff_h_pfp_add_output_constructedzerosentry + S (0) = S ((S (pfp_repeat_index_add_output_constructedzeros)) * dc)) /\ exists ff_q_pfp_add_output_constructedzerosentry. db = ff_q_pfp_add_output_constructedzerosentry * S ((S (pfp_repeat_index_add_output_constructedzeros)) * dc) + (0)))) /\ ((forall pfrep_index_add_output_constructed pfrep_value_add_output_constructed. (exists pfa_gap_add_output_constructedbound. pfa_gap_add_output_constructedbound + S (pfrep_index_add_output_constructed) = (L)) -> (((exists ff_h_pfp_add_output_constructedinput. ff_h_pfp_add_output_constructedinput + S (pfrep_value_add_output_constructed) = S ((S (pfrep_index_add_output_constructed)) * cc)) /\ exists ff_q_pfp_add_output_constructedinput. cb = ff_q_pfp_add_output_constructedinput * S ((S (pfrep_index_add_output_constructed)) * cc) + (pfrep_value_add_output_constructed))) -> (((exists ff_h_pfp_add_output_constructedoutput. ff_h_pfp_add_output_constructedoutput + S (pfrep_value_add_output_constructed) = S ((S ((t)+pfrep_index_add_output_constructed)) * dc)) /\ exists ff_q_pfp_add_output_constructedoutput. db = ff_q_pfp_add_output_constructedoutput * S ((S ((t)+pfrep_index_add_output_constructed)) * dc) + (pfrep_value_add_output_constructed)))))))
  22. 0022specialize prime_field_polynomial_left_pad_exists (cb)
  23. 0023specialize prime_field_polynomial_left_pad_exists (cc)
  24. 0024specialize prime_field_polynomial_left_pad_exists (t)
  25. 0025specialize prime_field_polynomial_left_pad_exists (L)
  26. 0026apply prime_field_polynomial_left_pad_exists
  27. 0027cases hd
  28. 0028cases hd_witness
  29. 0029have hm : forall pfp_index_add_output_middle. (exists pfa_gap_add_output_middleindex. pfa_gap_add_output_middleindex + S (pfp_index_add_output_middle) = (t+L)) -> exists pfp_left_add_output_middle pfp_right_add_output_middle pfp_value_add_output_middle. ((((exists ff_h_pfp_add_output_middleleft. ff_h_pfp_add_output_middleleft + S (pfp_left_add_output_middle) = S ((S (pfp_index_add_output_middle)) * AC)) /\ exists ff_q_pfp_add_output_middleleft. AB = ff_q_pfp_add_output_middleleft * S ((S (pfp_index_add_output_middle)) * AC) + (pfp_left_add_output_middle))) /\ (((((exists ff_h_pfp_add_output_middleright. ff_h_pfp_add_output_middleright + S (pfp_right_add_output_middle) = S ((S (pfp_index_add_output_middle)) * BC)) /\ exists ff_q_pfp_add_output_middleright. BB = ff_q_pfp_add_output_middleright * S ((S (pfp_index_add_output_middle)) * BC) + (pfp_right_add_output_middle))) /\ (((((exists ff_h_pfp_add_output_middletarget. ff_h_pfp_add_output_middletarget + S (pfp_value_add_output_middle) = S ((S (pfp_index_add_output_middle)) * x1)) /\ exists ff_q_pfp_add_output_middletarget. x = ff_q_pfp_add_output_middletarget * S ((S (pfp_index_add_output_middle)) * x1) + (pfp_value_add_output_middle))) /\ ((((exists pfa_gap_add_output_middleoperationleft. pfa_gap_add_output_middleoperationleft + S (pfp_left_add_output_middle) = (p)) /\ (((exists pfa_gap_add_output_middleoperationright. pfa_gap_add_output_middleoperationright + S (pfp_right_add_output_middle) = (p)) /\ ((((exists pfa_gap_add_output_middleoperationresultbound. pfa_gap_add_output_middleoperationresultbound + S (pfp_value_add_output_middle) = (p)) /\ ((exists pfa_offset_left_add_output_middleoperationresultcongruence pfa_offset_right_add_output_middleoperationresultcongruence. ((pfp_left_add_output_middle) + (pfp_right_add_output_middle)) + (p) * pfa_offset_left_add_output_middleoperationresultcongruence = (pfp_value_add_output_middle) + (p) * pfa_offset_right_add_output_middleoperationresultcongruence)))))))))))))))
  30. 0030specialize prime_field_polynomial_add_left_pad_transport (p)
  31. 0031specialize prime_field_polynomial_add_left_pad_transport (ab)
  32. 0032specialize prime_field_polynomial_add_left_pad_transport (ac)
  33. 0033specialize prime_field_polynomial_add_left_pad_transport (bb)
  34. 0034specialize prime_field_polynomial_add_left_pad_transport (bc)
  35. 0035specialize prime_field_polynomial_add_left_pad_transport (cb)
  36. 0036specialize prime_field_polynomial_add_left_pad_transport (cc)
  37. 0037specialize prime_field_polynomial_add_left_pad_transport (L)
  38. 0038specialize prime_field_polynomial_add_left_pad_transport (t)
  39. 0039specialize prime_field_polynomial_add_left_pad_transport (AB)
  40. 0040specialize prime_field_polynomial_add_left_pad_transport (AC)
  41. 0041specialize prime_field_polynomial_add_left_pad_transport (BB)
  42. 0042specialize prime_field_polynomial_add_left_pad_transport (BC)
  43. 0043specialize prime_field_polynomial_add_left_pad_transport (x)
  44. 0044specialize prime_field_polynomial_add_left_pad_transport (x1)
  45. 0045apply prime_field_polynomial_add_left_pad_transport
  46. 0046exact hp
  47. 0047exact ho
  48. 0048exact hA
  49. 0049exact hB
  50. 0050exact hd_witness_witness
  51. 0051have he : forall mdr_i_pfp_add_output_values mdr_a_pfp_add_output_values. (exists mdr_gap_pfp_add_output_valuesb. mdr_gap_pfp_add_output_valuesb + S (mdr_i_pfp_add_output_values) = (t+L)) -> (((exists ff_h_mdr_pfp_add_output_valueso. ff_h_mdr_pfp_add_output_valueso + S (mdr_a_pfp_add_output_values) = S ((S (mdr_i_pfp_add_output_values)) * x1)) /\ exists ff_q_mdr_pfp_add_output_valueso. x = ff_q_mdr_pfp_add_output_valueso * S ((S (mdr_i_pfp_add_output_values)) * x1) + (mdr_a_pfp_add_output_values))) -> (((exists ff_h_mdr_pfp_add_output_valuesn. ff_h_mdr_pfp_add_output_valuesn + S (mdr_a_pfp_add_output_values) = S ((S (mdr_i_pfp_add_output_values)) * CC)) /\ exists ff_q_mdr_pfp_add_output_valuesn. CB = ff_q_mdr_pfp_add_output_valuesn * S ((S (mdr_i_pfp_add_output_values)) * CC) + (mdr_a_pfp_add_output_values)))
  52. 0052specialize prime_field_polynomial_add_functional (p)
  53. 0053specialize prime_field_polynomial_add_functional (AB)
  54. 0054specialize prime_field_polynomial_add_functional (AC)
  55. 0055specialize prime_field_polynomial_add_functional (BB)
  56. 0056specialize prime_field_polynomial_add_functional (BC)
  57. 0057specialize prime_field_polynomial_add_functional (x)
  58. 0058specialize prime_field_polynomial_add_functional (x1)
  59. 0059specialize prime_field_polynomial_add_functional (CB)
  60. 0060specialize prime_field_polynomial_add_functional (CC)
  61. 0061specialize prime_field_polynomial_add_functional (t+L)
  62. 0062apply prime_field_polynomial_add_functional
  63. 0063exact hm
  64. 0064exact hn
  65. 0065specialize prime_field_polynomial_left_pad_transport (cb)
  66. 0066specialize prime_field_polynomial_left_pad_transport (cc)
  67. 0067specialize prime_field_polynomial_left_pad_transport (cb)
  68. 0068specialize prime_field_polynomial_left_pad_transport (cc)
  69. 0069specialize prime_field_polynomial_left_pad_transport (L)
  70. 0070specialize prime_field_polynomial_left_pad_transport (t)
  71. 0071specialize prime_field_polynomial_left_pad_transport (x)
  72. 0072specialize prime_field_polynomial_left_pad_transport (x1)
  73. 0073specialize prime_field_polynomial_left_pad_transport (CB)
  74. 0074specialize prime_field_polynomial_left_pad_transport (CC)
  75. 0075apply prime_field_polynomial_left_pad_transport
  76. 0076intro i
  77. 0077intro a
  78. 0078intro hi
  79. 0079intro ha
  80. 0080exact ha
  81. 0081exact he
  82. 0082exact hd_witness_witness