PQ0049

prime_field_polynomial_synthetic_quotient_entry

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

Each decoded quotient coefficient is precisely the actual Horner value of the corresponding nonempty input prefix.

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 a n qb qc r i h. (exists pfs_history_code_entry_division pfs_history_scale_entry_division. ((((exists pfa_gap_entry_divisiontracebase. pfa_gap_entry_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_entry_divisiontraceinitial. ff_h_pfp_entry_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontraceinitial. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontraceinitial * S ((S (0)) * pfs_history_scale_entry_division) + (0))) /\ (((((exists ff_h_pfp_entry_divisiontraceterminal. ff_h_pfp_entry_divisiontraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontraceterminal. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontraceterminal * S ((S (S (n))) * pfs_history_scale_entry_division) + (r))) /\ ((forall pfh_index_entry_divisiontracesteps. (exists pfa_gap_entry_divisiontracestepsindex. pfa_gap_entry_divisiontracestepsindex + S (pfh_index_entry_divisiontracesteps) = (S (n))) -> (exists pfh_coefficient_entry_divisiontracestepsstep pfh_before_entry_divisiontracestepsstep pfh_after_entry_divisiontracestepsstep pfh_product_entry_divisiontracestepsstep. ((((exists ff_h_pfp_entry_divisiontracestepsstepcoefficient. ff_h_pfp_entry_divisiontracestepsstepcoefficient + S (pfh_coefficient_entry_divisiontracestepsstep) = S ((S (pfh_index_entry_divisiontracesteps)) * c)) /\ exists ff_q_pfp_entry_divisiontracestepsstepcoefficient. b = ff_q_pfp_entry_divisiontracestepsstepcoefficient * S ((S (pfh_index_entry_divisiontracesteps)) * c) + (pfh_coefficient_entry_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_divisiontracestepsstepbefore. ff_h_pfp_entry_divisiontracestepsstepbefore + S (pfh_before_entry_divisiontracestepsstep) = S ((S (pfh_index_entry_divisiontracesteps)) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontracestepsstepbefore. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontracestepsstepbefore * S ((S (pfh_index_entry_divisiontracesteps)) * pfs_history_scale_entry_division) + (pfh_before_entry_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_divisiontracestepsstepafter. ff_h_pfp_entry_divisiontracestepsstepafter + S (pfh_after_entry_divisiontracestepsstep) = S ((S (S (pfh_index_entry_divisiontracesteps))) * pfs_history_scale_entry_division)) /\ exists ff_q_pfp_entry_divisiontracestepsstepafter. pfs_history_code_entry_division = ff_q_pfp_entry_divisiontracestepsstepafter * S ((S (S (pfh_index_entry_divisiontracesteps))) * pfs_history_scale_entry_division) + (pfh_after_entry_divisiontracestepsstep))) /\ (((((exists pfa_gap_entry_divisiontracestepsstepmultiplyleft. pfa_gap_entry_divisiontracestepsstepmultiplyleft + S (pfh_before_entry_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_divisiontracestepsstepmultiplyright. pfa_gap_entry_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_entry_divisiontracestepsstepmultiplyresultbound. pfa_gap_entry_divisiontracestepsstepmultiplyresultbound + S (pfh_product_entry_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_entry_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_entry_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_entry_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_entry_divisiontracestepsstep) + (p) * pfa_offset_right_entry_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_entry_divisiontracestepsstepaddleft. pfa_gap_entry_divisiontracestepsstepaddleft + S (pfh_product_entry_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_divisiontracestepsstepaddright. pfa_gap_entry_divisiontracestepsstepaddright + S (pfh_coefficient_entry_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_entry_divisiontracestepsstepaddresultbound. pfa_gap_entry_divisiontracestepsstepaddresultbound + S (pfh_after_entry_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_divisiontracestepsstepaddresultcongruence pfa_offset_right_entry_divisiontracestepsstepaddresultcongruence. ((pfh_product_entry_divisiontracestepsstep) + (pfh_coefficient_entry_divisiontracestepsstep)) + (p) * pfa_offset_left_entry_divisiontracestepsstepaddresultcongruence = (pfh_after_entry_divisiontracestepsstep) + (p) * pfa_offset_right_entry_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_entry_divisionquotient ff_source_mcp_pfs_entry_divisionquotient ff_target_mcp_pfs_entry_divisionquotient. (exists mcp_gap_pfs_entry_divisionquotient_bound. mcp_gap_pfs_entry_divisionquotient_bound + S (ff_index_mcp_pfs_entry_divisionquotient) = (n)) -> (((exists fs_h_mcp_pfs_entry_divisionquotient_source. fs_h_mcp_pfs_entry_divisionquotient_source + S (ff_source_mcp_pfs_entry_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_entry_divisionquotient)) * pfs_history_scale_entry_division)) /\ exists fs_q_mcp_pfs_entry_divisionquotient_source. pfs_history_code_entry_division = fs_q_mcp_pfs_entry_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_entry_divisionquotient)) * pfs_history_scale_entry_division) + (ff_source_mcp_pfs_entry_divisionquotient))) -> (((exists fs_h_mcp_pfs_entry_divisionquotient_target. fs_h_mcp_pfs_entry_divisionquotient_target + S (ff_target_mcp_pfs_entry_divisionquotient) = S ((S (ff_index_mcp_pfs_entry_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_entry_divisionquotient_target. qb = fs_q_mcp_pfs_entry_divisionquotient_target * S ((S (ff_index_mcp_pfs_entry_divisionquotient)) * qc) + (ff_target_mcp_pfs_entry_divisionquotient))) -> ff_target_mcp_pfs_entry_divisionquotient = ff_source_mcp_pfs_entry_divisionquotient)))) -> (exists pfa_gap_entry_index. pfa_gap_entry_index + S (i) = (n)) -> (((exists ff_h_pfp_entry_quotient. ff_h_pfp_entry_quotient + S (h) = S ((S (i)) * qc)) /\ exists ff_q_pfp_entry_quotient. qb = ff_q_pfp_entry_quotient * S ((S (i)) * qc) + (h))) -> (exists pfh_trace_code_entry_execution pfh_trace_scale_entry_execution. (((exists pfa_gap_entry_executiontracebase. pfa_gap_entry_executiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_entry_executiontraceinitial. ff_h_pfp_entry_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontraceinitial. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontraceinitial * S ((S (0)) * pfh_trace_scale_entry_execution) + (0))) /\ (((((exists ff_h_pfp_entry_executiontraceterminal. ff_h_pfp_entry_executiontraceterminal + S (h) = S ((S (S i)) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontraceterminal. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontraceterminal * S ((S (S i)) * pfh_trace_scale_entry_execution) + (h))) /\ ((forall pfh_index_entry_executiontracesteps. (exists pfa_gap_entry_executiontracestepsindex. pfa_gap_entry_executiontracestepsindex + S (pfh_index_entry_executiontracesteps) = (S i)) -> (exists pfh_coefficient_entry_executiontracestepsstep pfh_before_entry_executiontracestepsstep pfh_after_entry_executiontracestepsstep pfh_product_entry_executiontracestepsstep. ((((exists ff_h_pfp_entry_executiontracestepsstepcoefficient. ff_h_pfp_entry_executiontracestepsstepcoefficient + S (pfh_coefficient_entry_executiontracestepsstep) = S ((S (pfh_index_entry_executiontracesteps)) * c)) /\ exists ff_q_pfp_entry_executiontracestepsstepcoefficient. b = ff_q_pfp_entry_executiontracestepsstepcoefficient * S ((S (pfh_index_entry_executiontracesteps)) * c) + (pfh_coefficient_entry_executiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_executiontracestepsstepbefore. ff_h_pfp_entry_executiontracestepsstepbefore + S (pfh_before_entry_executiontracestepsstep) = S ((S (pfh_index_entry_executiontracesteps)) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontracestepsstepbefore. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontracestepsstepbefore * S ((S (pfh_index_entry_executiontracesteps)) * pfh_trace_scale_entry_execution) + (pfh_before_entry_executiontracestepsstep))) /\ (((((exists ff_h_pfp_entry_executiontracestepsstepafter. ff_h_pfp_entry_executiontracestepsstepafter + S (pfh_after_entry_executiontracestepsstep) = S ((S (S (pfh_index_entry_executiontracesteps))) * pfh_trace_scale_entry_execution)) /\ exists ff_q_pfp_entry_executiontracestepsstepafter. pfh_trace_code_entry_execution = ff_q_pfp_entry_executiontracestepsstepafter * S ((S (S (pfh_index_entry_executiontracesteps))) * pfh_trace_scale_entry_execution) + (pfh_after_entry_executiontracestepsstep))) /\ (((((exists pfa_gap_entry_executiontracestepsstepmultiplyleft. pfa_gap_entry_executiontracestepsstepmultiplyleft + S (pfh_before_entry_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_executiontracestepsstepmultiplyright. pfa_gap_entry_executiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_entry_executiontracestepsstepmultiplyresultbound. pfa_gap_entry_executiontracestepsstepmultiplyresultbound + S (pfh_product_entry_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_entry_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_entry_executiontracestepsstep) * (a)) + (p) * pfa_offset_left_entry_executiontracestepsstepmultiplyresultcongruence = (pfh_product_entry_executiontracestepsstep) + (p) * pfa_offset_right_entry_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_entry_executiontracestepsstepaddleft. pfa_gap_entry_executiontracestepsstepaddleft + S (pfh_product_entry_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_entry_executiontracestepsstepaddright. pfa_gap_entry_executiontracestepsstepaddright + S (pfh_coefficient_entry_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_entry_executiontracestepsstepaddresultbound. pfa_gap_entry_executiontracestepsstepaddresultbound + S (pfh_after_entry_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_executiontracestepsstepaddresultcongruence pfa_offset_right_entry_executiontracestepsstepaddresultcongruence. ((pfh_product_entry_executiontracestepsstep) + (pfh_coefficient_entry_executiontracestepsstep)) + (p) * pfa_offset_left_entry_executiontracestepsstepaddresultcongruence = (pfh_after_entry_executiontracestepsstep) + (p) * pfa_offset_right_entry_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))

Constructive proof overview

Generated structural guide

Each decoded quotient coefficient is precisely the actual Horner value of the corresponding nonempty input prefix.

The unchanged tactic script uses 6 declared prerequisites and contains 60 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized one_mul Stable theorem; checked-use authorized add_succ_left Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized PQ0045 prime_field_polynomial_horner_trace_prefix le_succ Stable theorem; checked-use authorized

Direct dependents

PQ004A prime_field_polynomial_synthetic_quotient_bounded PQ004C prime_field_polynomial_synthetic_functional PQ004F prime_field_polynomial_synthetic_leading_coefficient PQ0050 prime_field_polynomial_synthetic_middle_coefficients PQ0051 prime_field_polynomial_synthetic_final_coefficient

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

60 script commands · 11 reading checkpoints · 6 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 (1)
prime field polynomial horner trace prefix

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 b
  3. L3
    intro c
  4. L4
    intro a
  5. L5
    intro n
  6. L6
    intro qb
  7. L7
    intro qc
  8. L8
    intro r
  9. L9
    intro i
  10. L10
    intro h
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hs
  2. L12
    intro hi
  3. L13
    intro hh
03Separate the logical casesL14–16

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

  1. L14
    cases hs
  2. L15
    cases hs_witness
  3. L16
    cases hs_witness_witness
04Establish heL17–21

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

  1. L17
    have he : exists z. (((exists ff_h_pfp_entry_history_state. ff_h_pfp_entry_history_state + S (z) = S ((S (S i)) * x1)) /\ exists ff_q_pfp_entry_history_state. x = ff_q_pfp_entry_history_state * S ((S (S i)) * x1) + (z)))
  2. L18
    specialize beta_at_exists (x)
  3. L19
    specialize beta_at_exists (x1)
  4. L20
    specialize beta_at_exists (S i)
  5. L21
    apply beta_at_exists
05Separate the logical casesL22–22

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

  1. L22
    cases he
06Establish hindexL23–24

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

  1. L23
    have hindex : 1+1*i=S i
  2. L24
    simp [one_mul,add_succ_left,zero_add]
07Establish hshiftL25–28

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

  1. L25
    have hshift : ((exists ff_h_pfp_entry_shifted_state. ff_h_pfp_entry_shifted_state + S (x2) = S ((S (1+1*i)) * x1)) /\ exists ff_q_pfp_entry_shifted_state. x = ff_q_pfp_entry_shifted_state * S ((S (1+1*i)) * x1) + (x2))
  2. L26
    rewrite hindex
  3. L27
    rewrite hindex
  4. L28
    exact he_witness
08Establish heqL29–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hs witness witness right.

  1. L29
    have heq : h=x2
  2. L30
    specialize hs_witness_witness_right (i)
  3. L31
    specialize hs_witness_witness_right (x2)
  4. L32
    specialize hs_witness_witness_right (h)
  5. L33
    apply hs_witness_witness_right
  6. L34
    exact hi
  7. L35
    exact hshift
  8. L36
    exact hh
09Establish hexL37–46

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

  1. L37
    have hex : FpHorner(p,b,c,a,S i,x2)Definitions: FpHorner
  2. L38
    specialize prime_field_polynomial_horner_trace_prefix (p)
  3. L39
    specialize prime_field_polynomial_horner_trace_prefix (b)
  4. L40
    specialize prime_field_polynomial_horner_trace_prefix (c)
  5. L41
    specialize prime_field_polynomial_horner_trace_prefix (a)
  6. L42
    specialize prime_field_polynomial_horner_trace_prefix (S n)
  7. L43
    specialize prime_field_polynomial_horner_trace_prefix (r)
  8. L44
    specialize prime_field_polynomial_horner_trace_prefix (x)
  9. L45
    specialize prime_field_polynomial_horner_trace_prefix (x1)
  10. L46
    specialize prime_field_polynomial_horner_trace_prefix (S i)
10Use earlier factsL47–54

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

  1. L47
    specialize prime_field_polynomial_horner_trace_prefix (x2)
  2. L48
    apply prime_field_polynomial_horner_trace_prefix
  3. L49
    exact hs_witness_witness_left
  4. L50
    specialize le_succ (S i)
  5. L51
    specialize le_succ (n)
  6. L52
    apply le_succ
  7. L53
    exact hi
  8. L54
    exact he_witness
11Establish hbackL55–60

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

  1. L55
    have hback : x2=h
  2. L56
    symm
  3. L57
    exact heq
  4. L58
    rewrite hback at hex
  5. L59
    rewrite hback at hex
  6. L60
    exact hex

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro a
  5. 0005intro n
  6. 0006intro qb
  7. 0007intro qc
  8. 0008intro r
  9. 0009intro i
  10. 0010intro h
  11. 0011intro hs
  12. 0012intro hi
  13. 0013intro hh
  14. 0014cases hs
  15. 0015cases hs_witness
  16. 0016cases hs_witness_witness
  17. 0017have he : exists z. (((exists ff_h_pfp_entry_history_state. ff_h_pfp_entry_history_state + S (z) = S ((S (S i)) * x1)) /\ exists ff_q_pfp_entry_history_state. x = ff_q_pfp_entry_history_state * S ((S (S i)) * x1) + (z)))
  18. 0018specialize beta_at_exists (x)
  19. 0019specialize beta_at_exists (x1)
  20. 0020specialize beta_at_exists (S i)
  21. 0021apply beta_at_exists
  22. 0022cases he
  23. 0023have hindex : 1+1*i=S i
  24. 0024simp [one_mul,add_succ_left,zero_add]
  25. 0025have hshift : ((exists ff_h_pfp_entry_shifted_state. ff_h_pfp_entry_shifted_state + S (x2) = S ((S (1+1*i)) * x1)) /\ exists ff_q_pfp_entry_shifted_state. x = ff_q_pfp_entry_shifted_state * S ((S (1+1*i)) * x1) + (x2))
  26. 0026rewrite hindex
  27. 0027rewrite hindex
  28. 0028exact he_witness
  29. 0029have heq : h=x2
  30. 0030specialize hs_witness_witness_right (i)
  31. 0031specialize hs_witness_witness_right (x2)
  32. 0032specialize hs_witness_witness_right (h)
  33. 0033apply hs_witness_witness_right
  34. 0034exact hi
  35. 0035exact hshift
  36. 0036exact hh
  37. 0037have hex : exists pfh_trace_code_entry_execution_chosen pfh_trace_scale_entry_execution_chosen. (((exists pfa_gap_entry_execution_chosentracebase. pfa_gap_entry_execution_chosentracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_entry_execution_chosentraceinitial. ff_h_pfp_entry_execution_chosentraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_entry_execution_chosen)) /\ exists ff_q_pfp_entry_execution_chosentraceinitial. pfh_trace_code_entry_execution_chosen = ff_q_pfp_entry_execution_chosentraceinitial * S ((S (0)) * pfh_trace_scale_entry_execution_chosen) + (0))) /\ (((((exists ff_h_pfp_entry_execution_chosentraceterminal. ff_h_pfp_entry_execution_chosentraceterminal + S (x2) = S ((S (S i)) * pfh_trace_scale_entry_execution_chosen)) /\ exists ff_q_pfp_entry_execution_chosentraceterminal. pfh_trace_code_entry_execution_chosen = ff_q_pfp_entry_execution_chosentraceterminal * S ((S (S i)) * pfh_trace_scale_entry_execution_chosen) + (x2))) /\ ((forall pfh_index_entry_execution_chosentracesteps. (exists pfa_gap_entry_execution_chosentracestepsindex. pfa_gap_entry_execution_chosentracestepsindex + S (pfh_index_entry_execution_chosentracesteps) = (S i)) -> (exists pfh_coefficient_entry_execution_chosentracestepsstep pfh_before_entry_execution_chosentracestepsstep pfh_after_entry_execution_chosentracestepsstep pfh_product_entry_execution_chosentracestepsstep. ((((exists ff_h_pfp_entry_execution_chosentracestepsstepcoefficient. ff_h_pfp_entry_execution_chosentracestepsstepcoefficient + S (pfh_coefficient_entry_execution_chosentracestepsstep) = S ((S (pfh_index_entry_execution_chosentracesteps)) * c)) /\ exists ff_q_pfp_entry_execution_chosentracestepsstepcoefficient. b = ff_q_pfp_entry_execution_chosentracestepsstepcoefficient * S ((S (pfh_index_entry_execution_chosentracesteps)) * c) + (pfh_coefficient_entry_execution_chosentracestepsstep))) /\ (((((exists ff_h_pfp_entry_execution_chosentracestepsstepbefore. ff_h_pfp_entry_execution_chosentracestepsstepbefore + S (pfh_before_entry_execution_chosentracestepsstep) = S ((S (pfh_index_entry_execution_chosentracesteps)) * pfh_trace_scale_entry_execution_chosen)) /\ exists ff_q_pfp_entry_execution_chosentracestepsstepbefore. pfh_trace_code_entry_execution_chosen = ff_q_pfp_entry_execution_chosentracestepsstepbefore * S ((S (pfh_index_entry_execution_chosentracesteps)) * pfh_trace_scale_entry_execution_chosen) + (pfh_before_entry_execution_chosentracestepsstep))) /\ (((((exists ff_h_pfp_entry_execution_chosentracestepsstepafter. ff_h_pfp_entry_execution_chosentracestepsstepafter + S (pfh_after_entry_execution_chosentracestepsstep) = S ((S (S (pfh_index_entry_execution_chosentracesteps))) * pfh_trace_scale_entry_execution_chosen)) /\ exists ff_q_pfp_entry_execution_chosentracestepsstepafter. pfh_trace_code_entry_execution_chosen = ff_q_pfp_entry_execution_chosentracestepsstepafter * S ((S (S (pfh_index_entry_execution_chosentracesteps))) * pfh_trace_scale_entry_execution_chosen) + (pfh_after_entry_execution_chosentracestepsstep))) /\ (((((exists pfa_gap_entry_execution_chosentracestepsstepmultiplyleft. pfa_gap_entry_execution_chosentracestepsstepmultiplyleft + S (pfh_before_entry_execution_chosentracestepsstep) = (p)) /\ (((exists pfa_gap_entry_execution_chosentracestepsstepmultiplyright. pfa_gap_entry_execution_chosentracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_entry_execution_chosentracestepsstepmultiplyresultbound. pfa_gap_entry_execution_chosentracestepsstepmultiplyresultbound + S (pfh_product_entry_execution_chosentracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_execution_chosentracestepsstepmultiplyresultcongruence pfa_offset_right_entry_execution_chosentracestepsstepmultiplyresultcongruence. ((pfh_before_entry_execution_chosentracestepsstep) * (a)) + (p) * pfa_offset_left_entry_execution_chosentracestepsstepmultiplyresultcongruence = (pfh_product_entry_execution_chosentracestepsstep) + (p) * pfa_offset_right_entry_execution_chosentracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_entry_execution_chosentracestepsstepaddleft. pfa_gap_entry_execution_chosentracestepsstepaddleft + S (pfh_product_entry_execution_chosentracestepsstep) = (p)) /\ (((exists pfa_gap_entry_execution_chosentracestepsstepaddright. pfa_gap_entry_execution_chosentracestepsstepaddright + S (pfh_coefficient_entry_execution_chosentracestepsstep) = (p)) /\ ((((exists pfa_gap_entry_execution_chosentracestepsstepaddresultbound. pfa_gap_entry_execution_chosentracestepsstepaddresultbound + S (pfh_after_entry_execution_chosentracestepsstep) = (p)) /\ ((exists pfa_offset_left_entry_execution_chosentracestepsstepaddresultcongruence pfa_offset_right_entry_execution_chosentracestepsstepaddresultcongruence. ((pfh_product_entry_execution_chosentracestepsstep) + (pfh_coefficient_entry_execution_chosentracestepsstep)) + (p) * pfa_offset_left_entry_execution_chosentracestepsstepaddresultcongruence = (pfh_after_entry_execution_chosentracestepsstep) + (p) * pfa_offset_right_entry_execution_chosentracestepsstepaddresultcongruence))))))))))))))))))))))))))
  38. 0038specialize prime_field_polynomial_horner_trace_prefix (p)
  39. 0039specialize prime_field_polynomial_horner_trace_prefix (b)
  40. 0040specialize prime_field_polynomial_horner_trace_prefix (c)
  41. 0041specialize prime_field_polynomial_horner_trace_prefix (a)
  42. 0042specialize prime_field_polynomial_horner_trace_prefix (S n)
  43. 0043specialize prime_field_polynomial_horner_trace_prefix (r)
  44. 0044specialize prime_field_polynomial_horner_trace_prefix (x)
  45. 0045specialize prime_field_polynomial_horner_trace_prefix (x1)
  46. 0046specialize prime_field_polynomial_horner_trace_prefix (S i)
  47. 0047specialize prime_field_polynomial_horner_trace_prefix (x2)
  48. 0048apply prime_field_polynomial_horner_trace_prefix
  49. 0049exact hs_witness_witness_left
  50. 0050specialize le_succ (S i)
  51. 0051specialize le_succ (n)
  52. 0052apply le_succ
  53. 0053exact hi
  54. 0054exact he_witness
  55. 0055have hback : x2=h
  56. 0056symm
  57. 0057exact heq
  58. 0058rewrite hback at hex
  59. 0059rewrite hback at hex
  60. 0060exact hex