HD0009

beta_horner_derivative_functional

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

Both the value and exact formal derivative of every beta-coded polynomial are simultaneously unique.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall b c t l n z m w. (exists ff_u_hd_pair ff_v_hd_pair ff_d_hd_pair ff_e_hd_pair. ((((((exists fs_h_ph_hd_pair_body_value_start. fs_h_ph_hd_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_start. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_start * S ((S (0)) * ff_v_hd_pair) + (0))) /\ ((((exists fs_h_ph_hd_pair_body_value_terminal. fs_h_ph_hd_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_terminal. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pair) + (n))) /\ forall ff_i_ph_hd_pair_body_value_steps. (exists ph_bound_hd_pair_body_value_steps. ph_bound_hd_pair_body_value_steps + S ff_i_ph_hd_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pair_body_value_steps ff_previous_ph_hd_pair_body_value_steps ff_current_ph_hd_pair_body_value_steps. ((((exists fs_h_ph_hd_pair_body_value_steps_coefficient. fs_h_ph_hd_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pair_body_value_steps) = S ((S (ff_i_ph_hd_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pair_body_value_steps_before. fs_h_ph_hd_pair_body_value_steps_before + S (ff_previous_ph_hd_pair_body_value_steps) = S ((S (ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_steps_before. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair) + (ff_previous_ph_hd_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pair_body_value_steps_after. fs_h_ph_hd_pair_body_value_steps_after + S (ff_current_ph_hd_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_steps_after. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair) + (ff_current_ph_hd_pair_body_value_steps))) /\ ff_current_ph_hd_pair_body_value_steps = ff_previous_ph_hd_pair_body_value_steps * t + ff_coefficient_ph_hd_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pair_body_derivative_start. fs_h_ph_hd_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_start. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pair) + (0))) /\ ((((exists fs_h_ph_hd_pair_body_derivative_terminal. fs_h_ph_hd_pair_body_derivative_terminal + S (z) = S ((S (l)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_terminal. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pair) + (z))) /\ forall ff_i_ph_hd_pair_body_derivative_steps. (exists ph_bound_hd_pair_body_derivative_steps. ph_bound_hd_pair_body_derivative_steps + S ff_i_ph_hd_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pair_body_derivative_steps ff_previous_ph_hd_pair_body_derivative_steps ff_current_ph_hd_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_steps_coefficient. ff_u_hd_pair = fs_q_ph_hd_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_v_hd_pair) + (ff_coefficient_ph_hd_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pair_body_derivative_steps_before. fs_h_ph_hd_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_steps_before. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair) + (ff_previous_ph_hd_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pair_body_derivative_steps_after. fs_h_ph_hd_pair_body_derivative_steps_after + S (ff_current_ph_hd_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_steps_after. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair) + (ff_current_ph_hd_pair_body_derivative_steps))) /\ ff_current_ph_hd_pair_body_derivative_steps = ff_previous_ph_hd_pair_body_derivative_steps * t + ff_coefficient_ph_hd_pair_body_derivative_steps)))))))) -> (exists ff_u_hd_other ff_v_hd_other ff_d_hd_other ff_e_hd_other. ((((((exists fs_h_ph_hd_other_body_value_start. fs_h_ph_hd_other_body_value_start + S (0) = S ((S (0)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_start. ff_u_hd_other = fs_q_ph_hd_other_body_value_start * S ((S (0)) * ff_v_hd_other) + (0))) /\ ((((exists fs_h_ph_hd_other_body_value_terminal. fs_h_ph_hd_other_body_value_terminal + S (m) = S ((S (l)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_terminal. ff_u_hd_other = fs_q_ph_hd_other_body_value_terminal * S ((S (l)) * ff_v_hd_other) + (m))) /\ forall ff_i_ph_hd_other_body_value_steps. (exists ph_bound_hd_other_body_value_steps. ph_bound_hd_other_body_value_steps + S ff_i_ph_hd_other_body_value_steps = l) -> exists ff_coefficient_ph_hd_other_body_value_steps ff_previous_ph_hd_other_body_value_steps ff_current_ph_hd_other_body_value_steps. ((((exists fs_h_ph_hd_other_body_value_steps_coefficient. fs_h_ph_hd_other_body_value_steps_coefficient + S (ff_coefficient_ph_hd_other_body_value_steps) = S ((S (ff_i_ph_hd_other_body_value_steps)) * c)) /\ exists fs_q_ph_hd_other_body_value_steps_coefficient. b = fs_q_ph_hd_other_body_value_steps_coefficient * S ((S (ff_i_ph_hd_other_body_value_steps)) * c) + (ff_coefficient_ph_hd_other_body_value_steps))) /\ ((((exists fs_h_ph_hd_other_body_value_steps_before. fs_h_ph_hd_other_body_value_steps_before + S (ff_previous_ph_hd_other_body_value_steps) = S ((S (ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_steps_before. ff_u_hd_other = fs_q_ph_hd_other_body_value_steps_before * S ((S (ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other) + (ff_previous_ph_hd_other_body_value_steps))) /\ ((((exists fs_h_ph_hd_other_body_value_steps_after. fs_h_ph_hd_other_body_value_steps_after + S (ff_current_ph_hd_other_body_value_steps) = S ((S (S ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_steps_after. ff_u_hd_other = fs_q_ph_hd_other_body_value_steps_after * S ((S (S ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other) + (ff_current_ph_hd_other_body_value_steps))) /\ ff_current_ph_hd_other_body_value_steps = ff_previous_ph_hd_other_body_value_steps * t + ff_coefficient_ph_hd_other_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_other_body_derivative_start. fs_h_ph_hd_other_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_start. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_start * S ((S (0)) * ff_e_hd_other) + (0))) /\ ((((exists fs_h_ph_hd_other_body_derivative_terminal. fs_h_ph_hd_other_body_derivative_terminal + S (w) = S ((S (l)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_terminal. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_terminal * S ((S (l)) * ff_e_hd_other) + (w))) /\ forall ff_i_ph_hd_other_body_derivative_steps. (exists ph_bound_hd_other_body_derivative_steps. ph_bound_hd_other_body_derivative_steps + S ff_i_ph_hd_other_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_other_body_derivative_steps ff_previous_ph_hd_other_body_derivative_steps ff_current_ph_hd_other_body_derivative_steps. ((((exists fs_h_ph_hd_other_body_derivative_steps_coefficient. fs_h_ph_hd_other_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_other_body_derivative_steps) = S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_steps_coefficient. ff_u_hd_other = fs_q_ph_hd_other_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_v_hd_other) + (ff_coefficient_ph_hd_other_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_other_body_derivative_steps_before. fs_h_ph_hd_other_body_derivative_steps_before + S (ff_previous_ph_hd_other_body_derivative_steps) = S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_steps_before. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_steps_before * S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other) + (ff_previous_ph_hd_other_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_other_body_derivative_steps_after. fs_h_ph_hd_other_body_derivative_steps_after + S (ff_current_ph_hd_other_body_derivative_steps) = S ((S (S ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_steps_after. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_steps_after * S ((S (S ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other) + (ff_current_ph_hd_other_body_derivative_steps))) /\ ff_current_ph_hd_other_body_derivative_steps = ff_previous_ph_hd_other_body_derivative_steps * t + ff_coefficient_ph_hd_other_body_derivative_steps)))))))) -> (n = m /\ z = w)

Constructive proof overview

Generated structural guide

Both the value and exact formal derivative of every beta-coded polynomial are simultaneously unique.

The unchanged tactic script uses 3 declared prerequisites and contains 112 exact native proof lines.

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

Proof neighborhood

Direct dependencies

HD0007 beta_horner_derivative_empty HD0008 beta_horner_derivative_successor_decompose beta_at_unique Stable theorem; checked-use authorized

Direct dependents

HD000A beta_horner_derivative_second_component_functional HD000B beta_horner_derivative_exists_unique

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

112 script commands · 38 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 (2)
beta horner derivative emptybeta horner derivative successor decompose

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

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro t
02Induction on lL4–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro n
  3. L6
    intro z
  4. L7
    intro m
  5. L8
    intro w
  6. L9
    intro hleft
  7. L10
    intro hright
03Establish hleft_zeroL11–18

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

  1. L11
    have hleft_zero : (n = 0 /\ z = 0)
  2. L12
    specialize beta_horner_derivative_empty b
  3. L13
    specialize beta_horner_derivative_empty c
  4. L14
    specialize beta_horner_derivative_empty t
  5. L15
    specialize beta_horner_derivative_empty n
  6. L16
    specialize beta_horner_derivative_empty z
  7. L17
    apply beta_horner_derivative_empty
  8. L18
    exact hleft
04Establish hright_zeroL19–26

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

  1. L19
    have hright_zero : (m = 0 /\ w = 0)
  2. L20
    specialize beta_horner_derivative_empty b
  3. L21
    specialize beta_horner_derivative_empty c
  4. L22
    specialize beta_horner_derivative_empty t
  5. L23
    specialize beta_horner_derivative_empty m
  6. L24
    specialize beta_horner_derivative_empty w
  7. L25
    apply beta_horner_derivative_empty
  8. L26
    exact hright
05Separate the logical casesL27–29

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

  1. L27
    cases hleft_zero
  2. L28
    cases hright_zero
  3. L29
    split
06Calculate and transport equalitiesL30–30

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

  1. L30
    trans 0
07Use earlier factsL31–31

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

  1. L31
    exact hleft_zero_left
08Calculate and transport equalitiesL32–32

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

  1. L32
    symm
09Use earlier factsL33–33

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

  1. L33
    exact hright_zero_left
10Calculate and transport equalitiesL34–34

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

  1. L34
    trans 0
11Use earlier factsL35–35

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

  1. L35
    exact hleft_zero_right
12Calculate and transport equalitiesL36–36

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

  1. L36
    symm
13Use earlier factsL37–37

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

  1. L37
    exact hright_zero_right
14Fix variables and assumptionsL38–43

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

  1. L38
    intro n
  2. L39
    intro z
  3. L40
    intro m
  4. L41
    intro w
  5. L42
    intro hleft
  6. L43
    intro hright
15Establish hfirstL44–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L44
    have hfirst : ∃ a. ∃ r. ∃ q. Beta(b,c,l,a) ∧ (HornerDerivative(b,c,t,l,r,q) ∧ (n = r · t + a ∧ z = q · t + r))Definitions: BetaHornerDerivative
  2. L45
    specialize beta_horner_derivative_successor_decompose b
  3. L46
    specialize beta_horner_derivative_successor_decompose c
  4. L47
    specialize beta_horner_derivative_successor_decompose t
  5. L48
    specialize beta_horner_derivative_successor_decompose l
  6. L49
    specialize beta_horner_derivative_successor_decompose n
  7. L50
    specialize beta_horner_derivative_successor_decompose z
  8. L51
    apply beta_horner_derivative_successor_decompose
  9. L52
    exact hleft
16Separate the logical casesL53–58

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

  1. L53
    cases hfirst
  2. L54
    cases hfirst_witness
  3. L55
    cases hfirst_witness_witness
  4. L56
    cases hfirst_witness_witness_witness
  5. L57
    cases hfirst_witness_witness_witness_right
  6. L58
    cases hfirst_witness_witness_witness_right_right
17Establish hsecondL59–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L59
    have hsecond : ∃ a. ∃ r. ∃ q. Beta(b,c,l,a) ∧ (HornerDerivative(b,c,t,l,r,q) ∧ (m = r · t + a ∧ w = q · t + r))Definitions: BetaHornerDerivative
  2. L60
    specialize beta_horner_derivative_successor_decompose b
  3. L61
    specialize beta_horner_derivative_successor_decompose c
  4. L62
    specialize beta_horner_derivative_successor_decompose t
  5. L63
    specialize beta_horner_derivative_successor_decompose l
  6. L64
    specialize beta_horner_derivative_successor_decompose m
  7. L65
    specialize beta_horner_derivative_successor_decompose w
  8. L66
    apply beta_horner_derivative_successor_decompose
  9. L67
    exact hright
18Separate the logical casesL68–73

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

  1. L68
    cases hsecond
  2. L69
    cases hsecond_witness
  3. L70
    cases hsecond_witness_witness
  4. L71
    cases hsecond_witness_witness_witness
  5. L72
    cases hsecond_witness_witness_witness_right
  6. L73
    cases hsecond_witness_witness_witness_right_right
19Establish hprefix_equalL74–81

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

  1. L74
    have hprefix_equal : (x1 = x4 /\ x2 = x5)
  2. L75
    specialize IH x1
  3. L76
    specialize IH x2
  4. L77
    specialize IH x4
  5. L78
    specialize IH x5
  6. L79
    apply IH
  7. L80
    exact hfirst_witness_witness_witness_right_left
  8. L81
    exact hsecond_witness_witness_witness_right_left
20Separate the logical casesL82–82

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

  1. L82
    cases hprefix_equal
21Establish hcoefficient_equalL83–91

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

  1. L83
    have hcoefficient_equal : x = x3
  2. L84
    specialize beta_at_unique b
  3. L85
    specialize beta_at_unique c
  4. L86
    specialize beta_at_unique l
  5. L87
    specialize beta_at_unique x
  6. L88
    specialize beta_at_unique x3
  7. L89
    apply beta_at_unique
  8. L90
    exact hfirst_witness_witness_witness_left
  9. L91
    exact hsecond_witness_witness_witness_left
22Separate the logical casesL92–92

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

  1. L92
    split
23Calculate and transport equalitiesL93–93

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

  1. L93
    trans x1 * t + x
24Use earlier factsL94–94

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

  1. L94
    exact hfirst_witness_witness_witness_right_right_left
25Calculate and transport equalitiesL95–97

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

  1. L95
    trans x4 * t + x3
  2. L96
    congr
  3. L97
    congr
26Use earlier factsL98–98

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

  1. L98
    exact hprefix_equal_left
27Calculate and transport equalitiesL99–99

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

  1. L99
    refl
28Use earlier factsL100–100

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

  1. L100
    exact hcoefficient_equal
29Calculate and transport equalitiesL101–101

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

  1. L101
    symm
30Use earlier factsL102–102

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

  1. L102
    exact hsecond_witness_witness_witness_right_right_left
31Calculate and transport equalitiesL103–103

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

  1. L103
    trans x2 * t + x1
32Use earlier factsL104–104

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

  1. L104
    exact hfirst_witness_witness_witness_right_right_right
33Calculate and transport equalitiesL105–107

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

  1. L105
    trans x5 * t + x4
  2. L106
    congr
  3. L107
    congr
34Use earlier factsL108–108

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

  1. L108
    exact hprefix_equal_right
35Calculate and transport equalitiesL109–109

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

  1. L109
    refl
36Use earlier factsL110–110

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

  1. L110
    exact hprefix_equal_left
37Calculate and transport equalitiesL111–111

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

  1. L111
    symm
38Use earlier factsL112–112

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

  1. L112
    exact hsecond_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 112 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004induction l
  5. 0005intro n
  6. 0006intro z
  7. 0007intro m
  8. 0008intro w
  9. 0009intro hleft
  10. 0010intro hright
  11. 0011have hleft_zero : (n = 0 /\ z = 0)
  12. 0012specialize beta_horner_derivative_empty b
  13. 0013specialize beta_horner_derivative_empty c
  14. 0014specialize beta_horner_derivative_empty t
  15. 0015specialize beta_horner_derivative_empty n
  16. 0016specialize beta_horner_derivative_empty z
  17. 0017apply beta_horner_derivative_empty
  18. 0018exact hleft
  19. 0019have hright_zero : (m = 0 /\ w = 0)
  20. 0020specialize beta_horner_derivative_empty b
  21. 0021specialize beta_horner_derivative_empty c
  22. 0022specialize beta_horner_derivative_empty t
  23. 0023specialize beta_horner_derivative_empty m
  24. 0024specialize beta_horner_derivative_empty w
  25. 0025apply beta_horner_derivative_empty
  26. 0026exact hright
  27. 0027cases hleft_zero
  28. 0028cases hright_zero
  29. 0029split
  30. 0030trans 0
  31. 0031exact hleft_zero_left
  32. 0032symm
  33. 0033exact hright_zero_left
  34. 0034trans 0
  35. 0035exact hleft_zero_right
  36. 0036symm
  37. 0037exact hright_zero_right
  38. 0038intro n
  39. 0039intro z
  40. 0040intro m
  41. 0041intro w
  42. 0042intro hleft
  43. 0043intro hright
  44. 0044have hfirst : exists a r q. ((((exists fs_h_hd_functional_left_coefficient. fs_h_hd_functional_left_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_hd_functional_left_coefficient. b = fs_q_hd_functional_left_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_hd_functional_left_prefix ff_v_hd_functional_left_prefix ff_d_hd_functional_left_prefix ff_e_hd_functional_left_prefix. ((((((exists fs_h_ph_hd_functional_left_prefix_body_value_start. fs_h_ph_hd_functional_left_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_value_start. ff_u_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_value_start * S ((S (0)) * ff_v_hd_functional_left_prefix) + (0))) /\ ((((exists fs_h_ph_hd_functional_left_prefix_body_value_terminal. fs_h_ph_hd_functional_left_prefix_body_value_terminal + S (r) = S ((S (l)) * ff_v_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_value_terminal. ff_u_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_value_terminal * S ((S (l)) * ff_v_hd_functional_left_prefix) + (r))) /\ forall ff_i_ph_hd_functional_left_prefix_body_value_steps. (exists ph_bound_hd_functional_left_prefix_body_value_steps. ph_bound_hd_functional_left_prefix_body_value_steps + S ff_i_ph_hd_functional_left_prefix_body_value_steps = l) -> exists ff_coefficient_ph_hd_functional_left_prefix_body_value_steps ff_previous_ph_hd_functional_left_prefix_body_value_steps ff_current_ph_hd_functional_left_prefix_body_value_steps. ((((exists fs_h_ph_hd_functional_left_prefix_body_value_steps_coefficient. fs_h_ph_hd_functional_left_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_functional_left_prefix_body_value_steps) = S ((S (ff_i_ph_hd_functional_left_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_functional_left_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_functional_left_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_functional_left_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_functional_left_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_functional_left_prefix_body_value_steps_before. fs_h_ph_hd_functional_left_prefix_body_value_steps_before + S (ff_previous_ph_hd_functional_left_prefix_body_value_steps) = S ((S (ff_i_ph_hd_functional_left_prefix_body_value_steps)) * ff_v_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_value_steps_before. ff_u_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_functional_left_prefix_body_value_steps)) * ff_v_hd_functional_left_prefix) + (ff_previous_ph_hd_functional_left_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_functional_left_prefix_body_value_steps_after. fs_h_ph_hd_functional_left_prefix_body_value_steps_after + S (ff_current_ph_hd_functional_left_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_functional_left_prefix_body_value_steps)) * ff_v_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_value_steps_after. ff_u_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_functional_left_prefix_body_value_steps)) * ff_v_hd_functional_left_prefix) + (ff_current_ph_hd_functional_left_prefix_body_value_steps))) /\ ff_current_ph_hd_functional_left_prefix_body_value_steps = ff_previous_ph_hd_functional_left_prefix_body_value_steps * t + ff_coefficient_ph_hd_functional_left_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_functional_left_prefix_body_derivative_start. fs_h_ph_hd_functional_left_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_derivative_start. ff_d_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_functional_left_prefix) + (0))) /\ ((((exists fs_h_ph_hd_functional_left_prefix_body_derivative_terminal. fs_h_ph_hd_functional_left_prefix_body_derivative_terminal + S (q) = S ((S (l)) * ff_e_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_derivative_terminal. ff_d_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_derivative_terminal * S ((S (l)) * ff_e_hd_functional_left_prefix) + (q))) /\ forall ff_i_ph_hd_functional_left_prefix_body_derivative_steps. (exists ph_bound_hd_functional_left_prefix_body_derivative_steps. ph_bound_hd_functional_left_prefix_body_derivative_steps + S ff_i_ph_hd_functional_left_prefix_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_functional_left_prefix_body_derivative_steps ff_previous_ph_hd_functional_left_prefix_body_derivative_steps ff_current_ph_hd_functional_left_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_functional_left_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_functional_left_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_functional_left_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_functional_left_prefix_body_derivative_steps)) * ff_v_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_derivative_steps_coefficient. ff_u_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_functional_left_prefix_body_derivative_steps)) * ff_v_hd_functional_left_prefix) + (ff_coefficient_ph_hd_functional_left_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_functional_left_prefix_body_derivative_steps_before. fs_h_ph_hd_functional_left_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_functional_left_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_functional_left_prefix_body_derivative_steps)) * ff_e_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_derivative_steps_before. ff_d_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_functional_left_prefix_body_derivative_steps)) * ff_e_hd_functional_left_prefix) + (ff_previous_ph_hd_functional_left_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_functional_left_prefix_body_derivative_steps_after. fs_h_ph_hd_functional_left_prefix_body_derivative_steps_after + S (ff_current_ph_hd_functional_left_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_functional_left_prefix_body_derivative_steps)) * ff_e_hd_functional_left_prefix)) /\ exists fs_q_ph_hd_functional_left_prefix_body_derivative_steps_after. ff_d_hd_functional_left_prefix = fs_q_ph_hd_functional_left_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_functional_left_prefix_body_derivative_steps)) * ff_e_hd_functional_left_prefix) + (ff_current_ph_hd_functional_left_prefix_body_derivative_steps))) /\ ff_current_ph_hd_functional_left_prefix_body_derivative_steps = ff_previous_ph_hd_functional_left_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_functional_left_prefix_body_derivative_steps)))))))) /\ ((n = r * t + a) /\ z = q * t + r)))
  45. 0045specialize beta_horner_derivative_successor_decompose b
  46. 0046specialize beta_horner_derivative_successor_decompose c
  47. 0047specialize beta_horner_derivative_successor_decompose t
  48. 0048specialize beta_horner_derivative_successor_decompose l
  49. 0049specialize beta_horner_derivative_successor_decompose n
  50. 0050specialize beta_horner_derivative_successor_decompose z
  51. 0051apply beta_horner_derivative_successor_decompose
  52. 0052exact hleft
  53. 0053cases hfirst
  54. 0054cases hfirst_witness
  55. 0055cases hfirst_witness_witness
  56. 0056cases hfirst_witness_witness_witness
  57. 0057cases hfirst_witness_witness_witness_right
  58. 0058cases hfirst_witness_witness_witness_right_right
  59. 0059have hsecond : exists a r q. ((((exists fs_h_hd_functional_right_coefficient. fs_h_hd_functional_right_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_hd_functional_right_coefficient. b = fs_q_hd_functional_right_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_hd_functional_right_prefix ff_v_hd_functional_right_prefix ff_d_hd_functional_right_prefix ff_e_hd_functional_right_prefix. ((((((exists fs_h_ph_hd_functional_right_prefix_body_value_start. fs_h_ph_hd_functional_right_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_value_start. ff_u_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_value_start * S ((S (0)) * ff_v_hd_functional_right_prefix) + (0))) /\ ((((exists fs_h_ph_hd_functional_right_prefix_body_value_terminal. fs_h_ph_hd_functional_right_prefix_body_value_terminal + S (r) = S ((S (l)) * ff_v_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_value_terminal. ff_u_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_value_terminal * S ((S (l)) * ff_v_hd_functional_right_prefix) + (r))) /\ forall ff_i_ph_hd_functional_right_prefix_body_value_steps. (exists ph_bound_hd_functional_right_prefix_body_value_steps. ph_bound_hd_functional_right_prefix_body_value_steps + S ff_i_ph_hd_functional_right_prefix_body_value_steps = l) -> exists ff_coefficient_ph_hd_functional_right_prefix_body_value_steps ff_previous_ph_hd_functional_right_prefix_body_value_steps ff_current_ph_hd_functional_right_prefix_body_value_steps. ((((exists fs_h_ph_hd_functional_right_prefix_body_value_steps_coefficient. fs_h_ph_hd_functional_right_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_functional_right_prefix_body_value_steps) = S ((S (ff_i_ph_hd_functional_right_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_functional_right_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_functional_right_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_functional_right_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_functional_right_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_functional_right_prefix_body_value_steps_before. fs_h_ph_hd_functional_right_prefix_body_value_steps_before + S (ff_previous_ph_hd_functional_right_prefix_body_value_steps) = S ((S (ff_i_ph_hd_functional_right_prefix_body_value_steps)) * ff_v_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_value_steps_before. ff_u_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_functional_right_prefix_body_value_steps)) * ff_v_hd_functional_right_prefix) + (ff_previous_ph_hd_functional_right_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_functional_right_prefix_body_value_steps_after. fs_h_ph_hd_functional_right_prefix_body_value_steps_after + S (ff_current_ph_hd_functional_right_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_functional_right_prefix_body_value_steps)) * ff_v_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_value_steps_after. ff_u_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_functional_right_prefix_body_value_steps)) * ff_v_hd_functional_right_prefix) + (ff_current_ph_hd_functional_right_prefix_body_value_steps))) /\ ff_current_ph_hd_functional_right_prefix_body_value_steps = ff_previous_ph_hd_functional_right_prefix_body_value_steps * t + ff_coefficient_ph_hd_functional_right_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_functional_right_prefix_body_derivative_start. fs_h_ph_hd_functional_right_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_derivative_start. ff_d_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_functional_right_prefix) + (0))) /\ ((((exists fs_h_ph_hd_functional_right_prefix_body_derivative_terminal. fs_h_ph_hd_functional_right_prefix_body_derivative_terminal + S (q) = S ((S (l)) * ff_e_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_derivative_terminal. ff_d_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_derivative_terminal * S ((S (l)) * ff_e_hd_functional_right_prefix) + (q))) /\ forall ff_i_ph_hd_functional_right_prefix_body_derivative_steps. (exists ph_bound_hd_functional_right_prefix_body_derivative_steps. ph_bound_hd_functional_right_prefix_body_derivative_steps + S ff_i_ph_hd_functional_right_prefix_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_functional_right_prefix_body_derivative_steps ff_previous_ph_hd_functional_right_prefix_body_derivative_steps ff_current_ph_hd_functional_right_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_functional_right_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_functional_right_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_functional_right_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_functional_right_prefix_body_derivative_steps)) * ff_v_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_derivative_steps_coefficient. ff_u_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_functional_right_prefix_body_derivative_steps)) * ff_v_hd_functional_right_prefix) + (ff_coefficient_ph_hd_functional_right_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_functional_right_prefix_body_derivative_steps_before. fs_h_ph_hd_functional_right_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_functional_right_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_functional_right_prefix_body_derivative_steps)) * ff_e_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_derivative_steps_before. ff_d_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_functional_right_prefix_body_derivative_steps)) * ff_e_hd_functional_right_prefix) + (ff_previous_ph_hd_functional_right_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_functional_right_prefix_body_derivative_steps_after. fs_h_ph_hd_functional_right_prefix_body_derivative_steps_after + S (ff_current_ph_hd_functional_right_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_functional_right_prefix_body_derivative_steps)) * ff_e_hd_functional_right_prefix)) /\ exists fs_q_ph_hd_functional_right_prefix_body_derivative_steps_after. ff_d_hd_functional_right_prefix = fs_q_ph_hd_functional_right_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_functional_right_prefix_body_derivative_steps)) * ff_e_hd_functional_right_prefix) + (ff_current_ph_hd_functional_right_prefix_body_derivative_steps))) /\ ff_current_ph_hd_functional_right_prefix_body_derivative_steps = ff_previous_ph_hd_functional_right_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_functional_right_prefix_body_derivative_steps)))))))) /\ ((m = r * t + a) /\ w = q * t + r)))
  60. 0060specialize beta_horner_derivative_successor_decompose b
  61. 0061specialize beta_horner_derivative_successor_decompose c
  62. 0062specialize beta_horner_derivative_successor_decompose t
  63. 0063specialize beta_horner_derivative_successor_decompose l
  64. 0064specialize beta_horner_derivative_successor_decompose m
  65. 0065specialize beta_horner_derivative_successor_decompose w
  66. 0066apply beta_horner_derivative_successor_decompose
  67. 0067exact hright
  68. 0068cases hsecond
  69. 0069cases hsecond_witness
  70. 0070cases hsecond_witness_witness
  71. 0071cases hsecond_witness_witness_witness
  72. 0072cases hsecond_witness_witness_witness_right
  73. 0073cases hsecond_witness_witness_witness_right_right
  74. 0074have hprefix_equal : (x1 = x4 /\ x2 = x5)
  75. 0075specialize IH x1
  76. 0076specialize IH x2
  77. 0077specialize IH x4
  78. 0078specialize IH x5
  79. 0079apply IH
  80. 0080exact hfirst_witness_witness_witness_right_left
  81. 0081exact hsecond_witness_witness_witness_right_left
  82. 0082cases hprefix_equal
  83. 0083have hcoefficient_equal : x = x3
  84. 0084specialize beta_at_unique b
  85. 0085specialize beta_at_unique c
  86. 0086specialize beta_at_unique l
  87. 0087specialize beta_at_unique x
  88. 0088specialize beta_at_unique x3
  89. 0089apply beta_at_unique
  90. 0090exact hfirst_witness_witness_witness_left
  91. 0091exact hsecond_witness_witness_witness_left
  92. 0092split
  93. 0093trans x1 * t + x
  94. 0094exact hfirst_witness_witness_witness_right_right_left
  95. 0095trans x4 * t + x3
  96. 0096congr
  97. 0097congr
  98. 0098exact hprefix_equal_left
  99. 0099refl
  100. 0100exact hcoefficient_equal
  101. 0101symm
  102. 0102exact hsecond_witness_witness_witness_right_right_left
  103. 0103trans x2 * t + x1
  104. 0104exact hfirst_witness_witness_witness_right_right_right
  105. 0105trans x5 * t + x4
  106. 0106congr
  107. 0107congr
  108. 0108exact hprefix_equal_right
  109. 0109refl
  110. 0110exact hprefix_equal_left
  111. 0111symm
  112. 0112exact hsecond_witness_witness_witness_right_right_right

Separate complete second-wave branches: Full G095 proof · Alpha v27.