PP0031

prime_field_polynomial_reduce_and_evaluate_exists

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

For arbitrary finite natural coefficients construct their canonical prime-field table and an actual Horner execution, and prove agreement with every natural T12 evaluation.

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 b c t l. (~((p) = 1) /\ forall pfa_factor_left_complete_prime pfa_factor_right_complete_prime. (p) = pfa_factor_left_complete_prime * pfa_factor_right_complete_prime -> pfa_factor_left_complete_prime = 1 \/ pfa_factor_right_complete_prime = 1) -> (exists pfa_gap_complete_base. pfa_gap_complete_base + S (t) = (p)) -> exists d e r. ((forall pfp_index_complete_reduction_result. (exists pfa_gap_complete_reduction_resultindex. pfa_gap_complete_reduction_resultindex + S (pfp_index_complete_reduction_result) = (l)) -> exists pfp_source_complete_reduction_result pfp_residue_complete_reduction_result. ((((exists ff_h_pfp_complete_reduction_resultsource. ff_h_pfp_complete_reduction_resultsource + S (pfp_source_complete_reduction_result) = S ((S (pfp_index_complete_reduction_result)) * c)) /\ exists ff_q_pfp_complete_reduction_resultsource. b = ff_q_pfp_complete_reduction_resultsource * S ((S (pfp_index_complete_reduction_result)) * c) + (pfp_source_complete_reduction_result))) /\ (((((exists ff_h_pfp_complete_reduction_resulttarget. ff_h_pfp_complete_reduction_resulttarget + S (pfp_residue_complete_reduction_result) = S ((S (pfp_index_complete_reduction_result)) * e)) /\ exists ff_q_pfp_complete_reduction_resulttarget. d = ff_q_pfp_complete_reduction_resulttarget * S ((S (pfp_index_complete_reduction_result)) * e) + (pfp_residue_complete_reduction_result))) /\ ((((exists pfa_gap_complete_reduction_resultresiduebound. pfa_gap_complete_reduction_resultresiduebound + S (pfp_residue_complete_reduction_result) = (p)) /\ ((exists pfa_offset_left_complete_reduction_resultresiduecongruence pfa_offset_right_complete_reduction_resultresiduecongruence. (pfp_source_complete_reduction_result) + (p) * pfa_offset_left_complete_reduction_resultresiduecongruence = (pfp_residue_complete_reduction_result) + (p) * pfa_offset_right_complete_reduction_resultresiduecongruence))))))))) /\ (((exists pfh_trace_code_complete_execution_result pfh_trace_scale_complete_execution_result. (((exists pfa_gap_complete_execution_resulttracebase. pfa_gap_complete_execution_resulttracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_complete_execution_resulttraceinitial. ff_h_pfp_complete_execution_resulttraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttraceinitial. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttraceinitial * S ((S (0)) * pfh_trace_scale_complete_execution_result) + (0))) /\ (((((exists ff_h_pfp_complete_execution_resulttraceterminal. ff_h_pfp_complete_execution_resulttraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttraceterminal. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttraceterminal * S ((S (l)) * pfh_trace_scale_complete_execution_result) + (r))) /\ ((forall pfh_index_complete_execution_resulttracesteps. (exists pfa_gap_complete_execution_resulttracestepsindex. pfa_gap_complete_execution_resulttracestepsindex + S (pfh_index_complete_execution_resulttracesteps) = (l)) -> (exists pfh_coefficient_complete_execution_resulttracestepsstep pfh_before_complete_execution_resulttracestepsstep pfh_after_complete_execution_resulttracestepsstep pfh_product_complete_execution_resulttracestepsstep. ((((exists ff_h_pfp_complete_execution_resulttracestepsstepcoefficient. ff_h_pfp_complete_execution_resulttracestepsstepcoefficient + S (pfh_coefficient_complete_execution_resulttracestepsstep) = S ((S (pfh_index_complete_execution_resulttracesteps)) * e)) /\ exists ff_q_pfp_complete_execution_resulttracestepsstepcoefficient. d = ff_q_pfp_complete_execution_resulttracestepsstepcoefficient * S ((S (pfh_index_complete_execution_resulttracesteps)) * e) + (pfh_coefficient_complete_execution_resulttracestepsstep))) /\ (((((exists ff_h_pfp_complete_execution_resulttracestepsstepbefore. ff_h_pfp_complete_execution_resulttracestepsstepbefore + S (pfh_before_complete_execution_resulttracestepsstep) = S ((S (pfh_index_complete_execution_resulttracesteps)) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttracestepsstepbefore. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttracestepsstepbefore * S ((S (pfh_index_complete_execution_resulttracesteps)) * pfh_trace_scale_complete_execution_result) + (pfh_before_complete_execution_resulttracestepsstep))) /\ (((((exists ff_h_pfp_complete_execution_resulttracestepsstepafter. ff_h_pfp_complete_execution_resulttracestepsstepafter + S (pfh_after_complete_execution_resulttracestepsstep) = S ((S (S (pfh_index_complete_execution_resulttracesteps))) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttracestepsstepafter. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttracestepsstepafter * S ((S (S (pfh_index_complete_execution_resulttracesteps))) * pfh_trace_scale_complete_execution_result) + (pfh_after_complete_execution_resulttracestepsstep))) /\ (((((exists pfa_gap_complete_execution_resulttracestepsstepmultiplyleft. pfa_gap_complete_execution_resulttracestepsstepmultiplyleft + S (pfh_before_complete_execution_resulttracestepsstep) = (p)) /\ (((exists pfa_gap_complete_execution_resulttracestepsstepmultiplyright. pfa_gap_complete_execution_resulttracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_complete_execution_resulttracestepsstepmultiplyresultbound. pfa_gap_complete_execution_resulttracestepsstepmultiplyresultbound + S (pfh_product_complete_execution_resulttracestepsstep) = (p)) /\ ((exists pfa_offset_left_complete_execution_resulttracestepsstepmultiplyresultcongruence pfa_offset_right_complete_execution_resulttracestepsstepmultiplyresultcongruence. ((pfh_before_complete_execution_resulttracestepsstep) * (t)) + (p) * pfa_offset_left_complete_execution_resulttracestepsstepmultiplyresultcongruence = (pfh_product_complete_execution_resulttracestepsstep) + (p) * pfa_offset_right_complete_execution_resulttracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_complete_execution_resulttracestepsstepaddleft. pfa_gap_complete_execution_resulttracestepsstepaddleft + S (pfh_product_complete_execution_resulttracestepsstep) = (p)) /\ (((exists pfa_gap_complete_execution_resulttracestepsstepaddright. pfa_gap_complete_execution_resulttracestepsstepaddright + S (pfh_coefficient_complete_execution_resulttracestepsstep) = (p)) /\ ((((exists pfa_gap_complete_execution_resulttracestepsstepaddresultbound. pfa_gap_complete_execution_resulttracestepsstepaddresultbound + S (pfh_after_complete_execution_resulttracestepsstep) = (p)) /\ ((exists pfa_offset_left_complete_execution_resulttracestepsstepaddresultcongruence pfa_offset_right_complete_execution_resulttracestepsstepaddresultcongruence. ((pfh_product_complete_execution_resulttracestepsstep) + (pfh_coefficient_complete_execution_resulttracestepsstep)) + (p) * pfa_offset_left_complete_execution_resulttracestepsstepaddresultcongruence = (pfh_after_complete_execution_resulttracestepsstep) + (p) * pfa_offset_right_complete_execution_resulttracestepsstepaddresultcongruence))))))))))))))))))))))))))) /\ ((forall n. (exists ff_u_ph_pfh_complete_natural ff_v_ph_pfh_complete_natural. ((((exists fs_h_ph_pfh_complete_natural_body_start. fs_h_ph_pfh_complete_natural_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_start. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_start * S ((S (0)) * ff_v_ph_pfh_complete_natural) + (0))) /\ ((((exists fs_h_ph_pfh_complete_natural_body_terminal. fs_h_ph_pfh_complete_natural_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_terminal. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_terminal * S ((S (l)) * ff_v_ph_pfh_complete_natural) + (n))) /\ forall ff_i_ph_pfh_complete_natural_body_steps. (exists ph_bound_pfh_complete_natural_body_steps. ph_bound_pfh_complete_natural_body_steps + S ff_i_ph_pfh_complete_natural_body_steps = l) -> exists ff_coefficient_ph_pfh_complete_natural_body_steps ff_previous_ph_pfh_complete_natural_body_steps ff_current_ph_pfh_complete_natural_body_steps. ((((exists fs_h_ph_pfh_complete_natural_body_steps_coefficient. fs_h_ph_pfh_complete_natural_body_steps_coefficient + S (ff_coefficient_ph_pfh_complete_natural_body_steps) = S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * c)) /\ exists fs_q_ph_pfh_complete_natural_body_steps_coefficient. b = fs_q_ph_pfh_complete_natural_body_steps_coefficient * S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * c) + (ff_coefficient_ph_pfh_complete_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_complete_natural_body_steps_before. fs_h_ph_pfh_complete_natural_body_steps_before + S (ff_previous_ph_pfh_complete_natural_body_steps) = S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_steps_before. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_steps_before * S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural) + (ff_previous_ph_pfh_complete_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_complete_natural_body_steps_after. fs_h_ph_pfh_complete_natural_body_steps_after + S (ff_current_ph_pfh_complete_natural_body_steps) = S ((S (S ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_steps_after. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_steps_after * S ((S (S ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural) + (ff_current_ph_pfh_complete_natural_body_steps))) /\ ff_current_ph_pfh_complete_natural_body_steps = ff_previous_ph_pfh_complete_natural_body_steps * t + ff_coefficient_ph_pfh_complete_natural_body_steps)))))) -> (((exists pfa_gap_complete_residuebound. pfa_gap_complete_residuebound + S (r) = (p)) /\ ((exists pfa_offset_left_complete_residuecongruence pfa_offset_right_complete_residuecongruence. (n) + (p) * pfa_offset_left_complete_residuecongruence = (r) + (p) * pfa_offset_right_complete_residuecongruence)))))))))

Constructive proof overview

Generated structural guide

For arbitrary finite natural coefficients construct their canonical prime-field table and an actual Horner execution, and prove agreement with every natural T12 evaluation.

The unchanged tactic script uses 5 declared prerequisites and contains 61 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PP0002 prime_field_polynomial_normalization_exists prime_nonzero Stable theorem; checked-use authorized PP0022 prime_field_polynomial_horner_exists PP0004 prime_field_polynomial_normalization_bounded PP0027 prime_field_polynomial_horner_normalization_residue

Direct dependents

none

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

61 script commands · 15 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.

Named ingredients (4)
prime field polynomial normalization existsprime field polynomial horner existsprime field polynomial normalization boundedprime field polynomial horner normalization residue

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–7

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro t
  5. L5
    intro l
  6. L6
    intro hp
  7. L7
    intro ht
02Establish hredL8–17

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

  1. L8
    have hred : ∃ d. ∃ e. FpCoefficientReduction(p,b,c,d,e,l)Definitions: FpCoefficientReduction
  2. L9
    specialize prime_field_polynomial_normalization_exists (p)
  3. L10
    specialize prime_field_polynomial_normalization_exists (b)
  4. L11
    specialize prime_field_polynomial_normalization_exists (c)
  5. L12
    specialize prime_field_polynomial_normalization_exists (l)
  6. L13
    apply prime_field_polynomial_normalization_exists
  7. L14
    intro hz
  8. L15
    specialize prime_nonzero (p)
  9. L16
    apply prime_nonzero
  10. L17
    exact hp
03Use earlier factsL18–18

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

  1. L18
    exact hz
04Separate the logical casesL19–20

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

  1. L19
    cases hred
  2. L20
    cases hred_witness
05Establish heL21–30

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

  1. L21
    have he : ∃ r. FpHorner(p,x,x1,t,l,r)Definitions: FpHorner
  2. L22
    specialize prime_field_polynomial_horner_exists (p)
  3. L23
    specialize prime_field_polynomial_horner_exists (x)
  4. L24
    specialize prime_field_polynomial_horner_exists (x1)
  5. L25
    specialize prime_field_polynomial_horner_exists (t)
  6. L26
    specialize prime_field_polynomial_horner_exists (l)
  7. L27
    apply prime_field_polynomial_horner_exists
  8. L28
    exact hp
  9. L29
    specialize prime_field_polynomial_normalization_bounded (p)
  10. L30
    specialize prime_field_polynomial_normalization_bounded (b)
06Use earlier factsL31–37

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

  1. L31
    specialize prime_field_polynomial_normalization_bounded (c)
  2. L32
    specialize prime_field_polynomial_normalization_bounded (x)
  3. L33
    specialize prime_field_polynomial_normalization_bounded (x1)
  4. L34
    specialize prime_field_polynomial_normalization_bounded (l)
  5. L35
    apply prime_field_polynomial_normalization_bounded
  6. L36
    exact hred_witness_witness
  7. L37
    exact ht
07Separate the logical casesL38–38

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

  1. L38
    cases he
08Construct an explicit witnessL39–41

Supply the displayed value, then prove that it has the required property.

  1. L39
    exists x
  2. L40
    exists x1
  3. L41
    exists x2
09Separate the logical casesL42–42

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

  1. L42
    split
10Use earlier factsL43–43

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

  1. L43
    exact hred_witness_witness
11Separate the logical casesL44–44

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

  1. L44
    split
12Use earlier factsL45–45

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

  1. L45
    exact he_witness
13Fix variables and assumptionsL46–47

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

  1. L46
    intro n
  2. L47
    intro hn
14Use earlier factsL48–57

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

  1. L48
    specialize prime_field_polynomial_horner_normalization_residue (p)
  2. L49
    specialize prime_field_polynomial_horner_normalization_residue (b)
  3. L50
    specialize prime_field_polynomial_horner_normalization_residue (c)
  4. L51
    specialize prime_field_polynomial_horner_normalization_residue (x)
  5. L52
    specialize prime_field_polynomial_horner_normalization_residue (x1)
  6. L53
    specialize prime_field_polynomial_horner_normalization_residue (t)
  7. L54
    specialize prime_field_polynomial_horner_normalization_residue (l)
  8. L55
    specialize prime_field_polynomial_horner_normalization_residue (n)
  9. L56
    specialize prime_field_polynomial_horner_normalization_residue (x2)
  10. L57
    apply prime_field_polynomial_horner_normalization_residue
15Use earlier factsL58–61

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

  1. L58
    exact hp
  2. L59
    exact hred_witness_witness
  3. L60
    exact hn
  4. L61
    exact he_witness

Library-wide reading audit

Original exact command ledger · 61 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro hp
  7. 0007intro ht
  8. 0008have hred : exists d e. (forall pfp_index_complete_reduction. (exists pfa_gap_complete_reductionindex. pfa_gap_complete_reductionindex + S (pfp_index_complete_reduction) = (l)) -> exists pfp_source_complete_reduction pfp_residue_complete_reduction. ((((exists ff_h_pfp_complete_reductionsource. ff_h_pfp_complete_reductionsource + S (pfp_source_complete_reduction) = S ((S (pfp_index_complete_reduction)) * c)) /\ exists ff_q_pfp_complete_reductionsource. b = ff_q_pfp_complete_reductionsource * S ((S (pfp_index_complete_reduction)) * c) + (pfp_source_complete_reduction))) /\ (((((exists ff_h_pfp_complete_reductiontarget. ff_h_pfp_complete_reductiontarget + S (pfp_residue_complete_reduction) = S ((S (pfp_index_complete_reduction)) * e)) /\ exists ff_q_pfp_complete_reductiontarget. d = ff_q_pfp_complete_reductiontarget * S ((S (pfp_index_complete_reduction)) * e) + (pfp_residue_complete_reduction))) /\ ((((exists pfa_gap_complete_reductionresiduebound. pfa_gap_complete_reductionresiduebound + S (pfp_residue_complete_reduction) = (p)) /\ ((exists pfa_offset_left_complete_reductionresiduecongruence pfa_offset_right_complete_reductionresiduecongruence. (pfp_source_complete_reduction) + (p) * pfa_offset_left_complete_reductionresiduecongruence = (pfp_residue_complete_reduction) + (p) * pfa_offset_right_complete_reductionresiduecongruence)))))))))
  9. 0009specialize prime_field_polynomial_normalization_exists (p)
  10. 0010specialize prime_field_polynomial_normalization_exists (b)
  11. 0011specialize prime_field_polynomial_normalization_exists (c)
  12. 0012specialize prime_field_polynomial_normalization_exists (l)
  13. 0013apply prime_field_polynomial_normalization_exists
  14. 0014intro hz
  15. 0015specialize prime_nonzero (p)
  16. 0016apply prime_nonzero
  17. 0017exact hp
  18. 0018exact hz
  19. 0019cases hred
  20. 0020cases hred_witness
  21. 0021have he : exists r. (exists pfh_trace_code_complete_execution pfh_trace_scale_complete_execution. (((exists pfa_gap_complete_executiontracebase. pfa_gap_complete_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_complete_executiontraceinitial. ff_h_pfp_complete_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_complete_execution)) /\ exists ff_q_pfp_complete_executiontraceinitial. pfh_trace_code_complete_execution = ff_q_pfp_complete_executiontraceinitial * S ((S (0)) * pfh_trace_scale_complete_execution) + (0))) /\ (((((exists ff_h_pfp_complete_executiontraceterminal. ff_h_pfp_complete_executiontraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_complete_execution)) /\ exists ff_q_pfp_complete_executiontraceterminal. pfh_trace_code_complete_execution = ff_q_pfp_complete_executiontraceterminal * S ((S (l)) * pfh_trace_scale_complete_execution) + (r))) /\ ((forall pfh_index_complete_executiontracesteps. (exists pfa_gap_complete_executiontracestepsindex. pfa_gap_complete_executiontracestepsindex + S (pfh_index_complete_executiontracesteps) = (l)) -> (exists pfh_coefficient_complete_executiontracestepsstep pfh_before_complete_executiontracestepsstep pfh_after_complete_executiontracestepsstep pfh_product_complete_executiontracestepsstep. ((((exists ff_h_pfp_complete_executiontracestepsstepcoefficient. ff_h_pfp_complete_executiontracestepsstepcoefficient + S (pfh_coefficient_complete_executiontracestepsstep) = S ((S (pfh_index_complete_executiontracesteps)) * x1)) /\ exists ff_q_pfp_complete_executiontracestepsstepcoefficient. x = ff_q_pfp_complete_executiontracestepsstepcoefficient * S ((S (pfh_index_complete_executiontracesteps)) * x1) + (pfh_coefficient_complete_executiontracestepsstep))) /\ (((((exists ff_h_pfp_complete_executiontracestepsstepbefore. ff_h_pfp_complete_executiontracestepsstepbefore + S (pfh_before_complete_executiontracestepsstep) = S ((S (pfh_index_complete_executiontracesteps)) * pfh_trace_scale_complete_execution)) /\ exists ff_q_pfp_complete_executiontracestepsstepbefore. pfh_trace_code_complete_execution = ff_q_pfp_complete_executiontracestepsstepbefore * S ((S (pfh_index_complete_executiontracesteps)) * pfh_trace_scale_complete_execution) + (pfh_before_complete_executiontracestepsstep))) /\ (((((exists ff_h_pfp_complete_executiontracestepsstepafter. ff_h_pfp_complete_executiontracestepsstepafter + S (pfh_after_complete_executiontracestepsstep) = S ((S (S (pfh_index_complete_executiontracesteps))) * pfh_trace_scale_complete_execution)) /\ exists ff_q_pfp_complete_executiontracestepsstepafter. pfh_trace_code_complete_execution = ff_q_pfp_complete_executiontracestepsstepafter * S ((S (S (pfh_index_complete_executiontracesteps))) * pfh_trace_scale_complete_execution) + (pfh_after_complete_executiontracestepsstep))) /\ (((((exists pfa_gap_complete_executiontracestepsstepmultiplyleft. pfa_gap_complete_executiontracestepsstepmultiplyleft + S (pfh_before_complete_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_complete_executiontracestepsstepmultiplyright. pfa_gap_complete_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_complete_executiontracestepsstepmultiplyresultbound. pfa_gap_complete_executiontracestepsstepmultiplyresultbound + S (pfh_product_complete_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_complete_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_complete_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_complete_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_complete_executiontracestepsstepmultiplyresultcongruence = (pfh_product_complete_executiontracestepsstep) + (p) * pfa_offset_right_complete_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_complete_executiontracestepsstepaddleft. pfa_gap_complete_executiontracestepsstepaddleft + S (pfh_product_complete_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_complete_executiontracestepsstepaddright. pfa_gap_complete_executiontracestepsstepaddright + S (pfh_coefficient_complete_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_complete_executiontracestepsstepaddresultbound. pfa_gap_complete_executiontracestepsstepaddresultbound + S (pfh_after_complete_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_complete_executiontracestepsstepaddresultcongruence pfa_offset_right_complete_executiontracestepsstepaddresultcongruence. ((pfh_product_complete_executiontracestepsstep) + (pfh_coefficient_complete_executiontracestepsstep)) + (p) * pfa_offset_left_complete_executiontracestepsstepaddresultcongruence = (pfh_after_complete_executiontracestepsstep) + (p) * pfa_offset_right_complete_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))
  22. 0022specialize prime_field_polynomial_horner_exists (p)
  23. 0023specialize prime_field_polynomial_horner_exists (x)
  24. 0024specialize prime_field_polynomial_horner_exists (x1)
  25. 0025specialize prime_field_polynomial_horner_exists (t)
  26. 0026specialize prime_field_polynomial_horner_exists (l)
  27. 0027apply prime_field_polynomial_horner_exists
  28. 0028exact hp
  29. 0029specialize prime_field_polynomial_normalization_bounded (p)
  30. 0030specialize prime_field_polynomial_normalization_bounded (b)
  31. 0031specialize prime_field_polynomial_normalization_bounded (c)
  32. 0032specialize prime_field_polynomial_normalization_bounded (x)
  33. 0033specialize prime_field_polynomial_normalization_bounded (x1)
  34. 0034specialize prime_field_polynomial_normalization_bounded (l)
  35. 0035apply prime_field_polynomial_normalization_bounded
  36. 0036exact hred_witness_witness
  37. 0037exact ht
  38. 0038cases he
  39. 0039exists x
  40. 0040exists x1
  41. 0041exists x2
  42. 0042split
  43. 0043exact hred_witness_witness
  44. 0044split
  45. 0045exact he_witness
  46. 0046intro n
  47. 0047intro hn
  48. 0048specialize prime_field_polynomial_horner_normalization_residue (p)
  49. 0049specialize prime_field_polynomial_horner_normalization_residue (b)
  50. 0050specialize prime_field_polynomial_horner_normalization_residue (c)
  51. 0051specialize prime_field_polynomial_horner_normalization_residue (x)
  52. 0052specialize prime_field_polynomial_horner_normalization_residue (x1)
  53. 0053specialize prime_field_polynomial_horner_normalization_residue (t)
  54. 0054specialize prime_field_polynomial_horner_normalization_residue (l)
  55. 0055specialize prime_field_polynomial_horner_normalization_residue (n)
  56. 0056specialize prime_field_polynomial_horner_normalization_residue (x2)
  57. 0057apply prime_field_polynomial_horner_normalization_residue
  58. 0058exact hp
  59. 0059exact hred_witness_witness
  60. 0060exact hn
  61. 0061exact he_witness