TH0005

beta_horner_derivative_mod_congruence

Every beta-coded natural polynomial and its exact formal derivative simultaneously preserve balanced congruence.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Historical partial components only: this chapter proves exact natural polynomial Taylor remainders, bounded corrections, and one-step divisibility lifts. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical representatives, and every positive prime power. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ m. ∀ t. ∀ s. ∀ l. ∀ n. ∀ d. ∀ z. ∀ e. ModEq(m,t,s) → HornerDerivative(b,c,t,l,n,d) → HornerDerivative(b,c,s,l,z,e) → ModEq(m,n,z) ∧ ModEq(m,d,e)

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

Definition DAG

HornerDerivative(b,c,t,l,n,z) · 2ModEq(m,a,b) · 3

Actual proof prerequisites

beta_horner_derivative_empty · checked external prerequisitebeta_horner_derivative_successor_decompose · checked external prerequisitebeta_at_unique · checked external prerequisitemod_eq_refl · checked external prerequisitehorner_mod_congruence_successor_stephorner_derivative_mod_congruence_successor_step
Original expanded first-order statement 
forall b c m t s l n d z e. (exists hgcrt_mod_left_pth_pair_base hgcrt_mod_right_pth_pair_base. t + m * hgcrt_mod_left_pth_pair_base = s + m * hgcrt_mod_right_pth_pair_base) -> (exists ff_u_hd_pth_pair_left ff_v_hd_pth_pair_left ff_d_hd_pth_pair_left ff_e_hd_pth_pair_left. ((((((exists fs_h_ph_hd_pth_pair_left_body_value_start. fs_h_ph_hd_pth_pair_left_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_value_start. ff_u_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_value_start * S ((S (0)) * ff_v_hd_pth_pair_left) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_left_body_value_terminal. fs_h_ph_hd_pth_pair_left_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_value_terminal. ff_u_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_value_terminal * S ((S (l)) * ff_v_hd_pth_pair_left) + (n))) /\ forall ff_i_ph_hd_pth_pair_left_body_value_steps. (exists ph_bound_hd_pth_pair_left_body_value_steps. ph_bound_hd_pth_pair_left_body_value_steps + S ff_i_ph_hd_pth_pair_left_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_left_body_value_steps ff_previous_ph_hd_pth_pair_left_body_value_steps ff_current_ph_hd_pth_pair_left_body_value_steps. ((((exists fs_h_ph_hd_pth_pair_left_body_value_steps_coefficient. fs_h_ph_hd_pth_pair_left_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_left_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_left_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_pair_left_body_value_steps_coefficient. b = fs_q_ph_hd_pth_pair_left_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_left_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_pair_left_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_left_body_value_steps_before. fs_h_ph_hd_pth_pair_left_body_value_steps_before + S (ff_previous_ph_hd_pth_pair_left_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_left_body_value_steps)) * ff_v_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_value_steps_before. ff_u_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_value_steps_before * S ((S (ff_i_ph_hd_pth_pair_left_body_value_steps)) * ff_v_hd_pth_pair_left) + (ff_previous_ph_hd_pth_pair_left_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_left_body_value_steps_after. fs_h_ph_hd_pth_pair_left_body_value_steps_after + S (ff_current_ph_hd_pth_pair_left_body_value_steps) = S ((S (S ff_i_ph_hd_pth_pair_left_body_value_steps)) * ff_v_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_value_steps_after. ff_u_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_pair_left_body_value_steps)) * ff_v_hd_pth_pair_left) + (ff_current_ph_hd_pth_pair_left_body_value_steps))) /\ ff_current_ph_hd_pth_pair_left_body_value_steps = ff_previous_ph_hd_pth_pair_left_body_value_steps * t + ff_coefficient_ph_hd_pth_pair_left_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_pair_left_body_derivative_start. fs_h_ph_hd_pth_pair_left_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_derivative_start. ff_d_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_derivative_start * S ((S (0)) * ff_e_hd_pth_pair_left) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_left_body_derivative_terminal. fs_h_ph_hd_pth_pair_left_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_derivative_terminal. ff_d_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_pair_left) + (d))) /\ forall ff_i_ph_hd_pth_pair_left_body_derivative_steps. (exists ph_bound_hd_pth_pair_left_body_derivative_steps. ph_bound_hd_pth_pair_left_body_derivative_steps + S ff_i_ph_hd_pth_pair_left_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_left_body_derivative_steps ff_previous_ph_hd_pth_pair_left_body_derivative_steps ff_current_ph_hd_pth_pair_left_body_derivative_steps. ((((exists fs_h_ph_hd_pth_pair_left_body_derivative_steps_coefficient. fs_h_ph_hd_pth_pair_left_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_left_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_left_body_derivative_steps)) * ff_v_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_derivative_steps_coefficient. ff_u_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_left_body_derivative_steps)) * ff_v_hd_pth_pair_left) + (ff_coefficient_ph_hd_pth_pair_left_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_left_body_derivative_steps_before. fs_h_ph_hd_pth_pair_left_body_derivative_steps_before + S (ff_previous_ph_hd_pth_pair_left_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_left_body_derivative_steps)) * ff_e_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_derivative_steps_before. ff_d_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_pair_left_body_derivative_steps)) * ff_e_hd_pth_pair_left) + (ff_previous_ph_hd_pth_pair_left_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_left_body_derivative_steps_after. fs_h_ph_hd_pth_pair_left_body_derivative_steps_after + S (ff_current_ph_hd_pth_pair_left_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_pair_left_body_derivative_steps)) * ff_e_hd_pth_pair_left)) /\ exists fs_q_ph_hd_pth_pair_left_body_derivative_steps_after. ff_d_hd_pth_pair_left = fs_q_ph_hd_pth_pair_left_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_pair_left_body_derivative_steps)) * ff_e_hd_pth_pair_left) + (ff_current_ph_hd_pth_pair_left_body_derivative_steps))) /\ ff_current_ph_hd_pth_pair_left_body_derivative_steps = ff_previous_ph_hd_pth_pair_left_body_derivative_steps * t + ff_coefficient_ph_hd_pth_pair_left_body_derivative_steps)))))))) -> (exists ff_u_hd_pth_pair_right ff_v_hd_pth_pair_right ff_d_hd_pth_pair_right ff_e_hd_pth_pair_right. ((((((exists fs_h_ph_hd_pth_pair_right_body_value_start. fs_h_ph_hd_pth_pair_right_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_value_start. ff_u_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_value_start * S ((S (0)) * ff_v_hd_pth_pair_right) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_right_body_value_terminal. fs_h_ph_hd_pth_pair_right_body_value_terminal + S (z) = S ((S (l)) * ff_v_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_value_terminal. ff_u_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_value_terminal * S ((S (l)) * ff_v_hd_pth_pair_right) + (z))) /\ forall ff_i_ph_hd_pth_pair_right_body_value_steps. (exists ph_bound_hd_pth_pair_right_body_value_steps. ph_bound_hd_pth_pair_right_body_value_steps + S ff_i_ph_hd_pth_pair_right_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_right_body_value_steps ff_previous_ph_hd_pth_pair_right_body_value_steps ff_current_ph_hd_pth_pair_right_body_value_steps. ((((exists fs_h_ph_hd_pth_pair_right_body_value_steps_coefficient. fs_h_ph_hd_pth_pair_right_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_right_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_right_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_pair_right_body_value_steps_coefficient. b = fs_q_ph_hd_pth_pair_right_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_right_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_pair_right_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_right_body_value_steps_before. fs_h_ph_hd_pth_pair_right_body_value_steps_before + S (ff_previous_ph_hd_pth_pair_right_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_right_body_value_steps)) * ff_v_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_value_steps_before. ff_u_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_value_steps_before * S ((S (ff_i_ph_hd_pth_pair_right_body_value_steps)) * ff_v_hd_pth_pair_right) + (ff_previous_ph_hd_pth_pair_right_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_right_body_value_steps_after. fs_h_ph_hd_pth_pair_right_body_value_steps_after + S (ff_current_ph_hd_pth_pair_right_body_value_steps) = S ((S (S ff_i_ph_hd_pth_pair_right_body_value_steps)) * ff_v_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_value_steps_after. ff_u_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_pair_right_body_value_steps)) * ff_v_hd_pth_pair_right) + (ff_current_ph_hd_pth_pair_right_body_value_steps))) /\ ff_current_ph_hd_pth_pair_right_body_value_steps = ff_previous_ph_hd_pth_pair_right_body_value_steps * s + ff_coefficient_ph_hd_pth_pair_right_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_pair_right_body_derivative_start. fs_h_ph_hd_pth_pair_right_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_derivative_start. ff_d_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_derivative_start * S ((S (0)) * ff_e_hd_pth_pair_right) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_right_body_derivative_terminal. fs_h_ph_hd_pth_pair_right_body_derivative_terminal + S (e) = S ((S (l)) * ff_e_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_derivative_terminal. ff_d_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_pair_right) + (e))) /\ forall ff_i_ph_hd_pth_pair_right_body_derivative_steps. (exists ph_bound_hd_pth_pair_right_body_derivative_steps. ph_bound_hd_pth_pair_right_body_derivative_steps + S ff_i_ph_hd_pth_pair_right_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_right_body_derivative_steps ff_previous_ph_hd_pth_pair_right_body_derivative_steps ff_current_ph_hd_pth_pair_right_body_derivative_steps. ((((exists fs_h_ph_hd_pth_pair_right_body_derivative_steps_coefficient. fs_h_ph_hd_pth_pair_right_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_right_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_right_body_derivative_steps)) * ff_v_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_derivative_steps_coefficient. ff_u_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_right_body_derivative_steps)) * ff_v_hd_pth_pair_right) + (ff_coefficient_ph_hd_pth_pair_right_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_right_body_derivative_steps_before. fs_h_ph_hd_pth_pair_right_body_derivative_steps_before + S (ff_previous_ph_hd_pth_pair_right_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_right_body_derivative_steps)) * ff_e_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_derivative_steps_before. ff_d_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_pair_right_body_derivative_steps)) * ff_e_hd_pth_pair_right) + (ff_previous_ph_hd_pth_pair_right_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_right_body_derivative_steps_after. fs_h_ph_hd_pth_pair_right_body_derivative_steps_after + S (ff_current_ph_hd_pth_pair_right_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_pair_right_body_derivative_steps)) * ff_e_hd_pth_pair_right)) /\ exists fs_q_ph_hd_pth_pair_right_body_derivative_steps_after. ff_d_hd_pth_pair_right = fs_q_ph_hd_pth_pair_right_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_pair_right_body_derivative_steps)) * ff_e_hd_pth_pair_right) + (ff_current_ph_hd_pth_pair_right_body_derivative_steps))) /\ ff_current_ph_hd_pth_pair_right_body_derivative_steps = ff_previous_ph_hd_pth_pair_right_body_derivative_steps * s + ff_coefficient_ph_hd_pth_pair_right_body_derivative_steps)))))))) -> ((exists hgcrt_mod_left_pth_pair_value_result hgcrt_mod_right_pth_pair_value_result. n + m * hgcrt_mod_left_pth_pair_value_result = z + m * hgcrt_mod_right_pth_pair_value_result) /\ (exists hgcrt_mod_left_pth_pair_derivative_result hgcrt_mod_right_pth_pair_derivative_result. d + m * hgcrt_mod_left_pth_pair_derivative_result = e + m * hgcrt_mod_right_pth_pair_derivative_result))

Complete unchanged native tactic proof

All 128 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

128 script commands · 25 reading checkpoints · 8 local claims

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

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

Named ingredients (2)
horner mod congruence successor stephorner derivative mod congruence successor step

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

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro m
  4. L4
    intro t
  5. L5
    intro s
02Induction on lL6–13

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

  1. L6
    induction l
  2. L7
    intro n
  3. L8
    intro d
  4. L9
    intro z
  5. L10
    intro e
  6. L11
    intro hbase
  7. L12
    intro hleft
  8. L13
    intro hright
03Establish hzero_leftL14–21

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

  1. L14
    have hzero_left : (n = 0 /\ d = 0)
  2. L15
    specialize beta_horner_derivative_empty b
  3. L16
    specialize beta_horner_derivative_empty c
  4. L17
    specialize beta_horner_derivative_empty t
  5. L18
    specialize beta_horner_derivative_empty n
  6. L19
    specialize beta_horner_derivative_empty d
  7. L20
    apply beta_horner_derivative_empty
  8. L21
    exact hleft
04Establish hzero_rightL22–29

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

  1. L22
    have hzero_right : (z = 0 /\ e = 0)
  2. L23
    specialize beta_horner_derivative_empty b
  3. L24
    specialize beta_horner_derivative_empty c
  4. L25
    specialize beta_horner_derivative_empty s
  5. L26
    specialize beta_horner_derivative_empty z
  6. L27
    specialize beta_horner_derivative_empty e
  7. L28
    apply beta_horner_derivative_empty
  8. L29
    exact hright
05Separate the logical casesL30–32

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

  1. L30
    cases hzero_left
  2. L31
    cases hzero_right
  3. L32
    split
06Calculate and transport equalitiesL33–34

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

  1. L33
    rewrite hzero_left_left
  2. L34
    rewrite hzero_right_left
07Use earlier factsL35–37

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

  1. L35
    specialize mod_eq_refl m
  2. L36
    specialize mod_eq_refl 0
  3. L37
    apply mod_eq_refl
08Calculate and transport equalitiesL38–39

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

  1. L38
    rewrite hzero_left_right
  2. L39
    rewrite hzero_right_right
09Use earlier factsL40–42

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

  1. L40
    specialize mod_eq_refl m
  2. L41
    specialize mod_eq_refl 0
  3. L42
    apply mod_eq_refl
10Fix variables and assumptionsL43–49

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

  1. L43
    intro n
  2. L44
    intro d
  3. L45
    intro z
  4. L46
    intro e
  5. L47
    intro hbase
  6. L48
    intro hleft
  7. L49
    intro hright
11Establish hfirstL50–58

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

  1. L50
    have hfirst : ∃ a. ∃ r. ∃ q. Beta(b,c,l,a) ∧ (HornerDerivative(b,c,t,l,r,q) ∧ (n = r · t + a ∧ d = q · t + r))Definitions: BetaHornerDerivativeOriginal native command in the exact edition
  2. L51
    specialize beta_horner_derivative_successor_decompose b
  3. L52
    specialize beta_horner_derivative_successor_decompose c
  4. L53
    specialize beta_horner_derivative_successor_decompose t
  5. L54
    specialize beta_horner_derivative_successor_decompose l
  6. L55
    specialize beta_horner_derivative_successor_decompose n
  7. L56
    specialize beta_horner_derivative_successor_decompose d
  8. L57
    apply beta_horner_derivative_successor_decompose
  9. L58
    exact hleft
12Separate the logical casesL59–64

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

  1. L59
    cases hfirst
  2. L60
    cases hfirst_witness
  3. L61
    cases hfirst_witness_witness
  4. L62
    cases hfirst_witness_witness_witness
  5. L63
    cases hfirst_witness_witness_witness_right
  6. L64
    cases hfirst_witness_witness_witness_right_right
13Establish hsecondL65–73

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

  1. L65
    have hsecond : ∃ a. ∃ r. ∃ q. Beta(b,c,l,a) ∧ (HornerDerivative(b,c,s,l,r,q) ∧ (z = r · s + a ∧ e = q · s + r))Definitions: BetaHornerDerivativeOriginal native command in the exact edition
  2. L66
    specialize beta_horner_derivative_successor_decompose b
  3. L67
    specialize beta_horner_derivative_successor_decompose c
  4. L68
    specialize beta_horner_derivative_successor_decompose s
  5. L69
    specialize beta_horner_derivative_successor_decompose l
  6. L70
    specialize beta_horner_derivative_successor_decompose z
  7. L71
    specialize beta_horner_derivative_successor_decompose e
  8. L72
    apply beta_horner_derivative_successor_decompose
  9. L73
    exact hright
14Separate the logical casesL74–79

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

  1. L74
    cases hsecond
  2. L75
    cases hsecond_witness
  3. L76
    cases hsecond_witness_witness
  4. L77
    cases hsecond_witness_witness_witness
  5. L78
    cases hsecond_witness_witness_witness_right
  6. L79
    cases hsecond_witness_witness_witness_right_right
15Establish hcoefficientL80–88

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

  1. L80
    have hcoefficient : x = x3
  2. L81
    specialize beta_at_unique b
  3. L82
    specialize beta_at_unique c
  4. L83
    specialize beta_at_unique l
  5. L84
    specialize beta_at_unique x
  6. L85
    specialize beta_at_unique x3
  7. L86
    apply beta_at_unique
  8. L87
    exact hfirst_witness_witness_witness_left
  9. L88
    exact hsecond_witness_witness_witness_left
16Establish hprefixL89–97

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

  1. L89
    have hprefix : ((exists hgcrt_mod_left_pth_pair_prefix_value hgcrt_mod_right_pth_pair_prefix_value. x1 + m * hgcrt_mod_left_pth_pair_prefix_value = x4 + m * hgcrt_mod_right_pth_pair_prefix_value) /\ (exists hgcrt_mod_left_pth_pair_prefix_derivative hgcrt_mod_right_pth_pair_prefix_derivative. x2 + m * hgcrt_mod_left_pth_pair_prefix_derivative = x5 + m * hgcrt_mod_right_pth_pair_prefix_derivative))
  2. L90
    specialize IH x1
  3. L91
    specialize IH x2
  4. L92
    specialize IH x4
  5. L93
    specialize IH x5
  6. L94
    apply IH
  7. L95
    exact hbase
  8. L96
    exact hfirst_witness_witness_witness_right_left
  9. L97
    exact hsecond_witness_witness_witness_right_left
17Separate the logical casesL98–98

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

  1. L98
    cases hprefix
18Establish hvalueL99–108

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply horner mod congruence successor step.

  1. L99
    have hvalue : exists hgcrt_mod_left_pth_pair_value_step hgcrt_mod_right_pth_pair_value_step. (x1 * t + x) + m * hgcrt_mod_left_pth_pair_value_step = (x4 * s + x) + m * hgcrt_mod_right_pth_pair_value_step
  2. L100
    specialize horner_mod_congruence_successor_step m
  3. L101
    specialize horner_mod_congruence_successor_step t
  4. L102
    specialize horner_mod_congruence_successor_step s
  5. L103
    specialize horner_mod_congruence_successor_step x1
  6. L104
    specialize horner_mod_congruence_successor_step x4
  7. L105
    specialize horner_mod_congruence_successor_step x
  8. L106
    apply horner_mod_congruence_successor_step
  9. L107
    exact hbase
  10. L108
    exact hprefix_left
19Establish hderivativeL109–118

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

  1. L109
    have hderivative : exists hgcrt_mod_left_pth_pair_derivative_step hgcrt_mod_right_pth_pair_derivative_step. (x2 * t + x1) + m * hgcrt_mod_left_pth_pair_derivative_step = (x5 * s + x4) + m * hgcrt_mod_right_pth_pair_derivative_step
  2. L110
    specialize horner_derivative_mod_congruence_successor_step m
  3. L111
    specialize horner_derivative_mod_congruence_successor_step t
  4. L112
    specialize horner_derivative_mod_congruence_successor_step s
  5. L113
    specialize horner_derivative_mod_congruence_successor_step x1
  6. L114
    specialize horner_derivative_mod_congruence_successor_step x4
  7. L115
    specialize horner_derivative_mod_congruence_successor_step x2
  8. L116
    specialize horner_derivative_mod_congruence_successor_step x5
  9. L117
    apply horner_derivative_mod_congruence_successor_step
  10. L118
    exact hbase
20Use earlier factsL119–120

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

  1. L119
    exact hprefix_left
  2. L120
    exact hprefix_right
21Separate the logical casesL121–121

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

  1. L121
    split
22Calculate and transport equalitiesL122–124

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

  1. L122
    rewrite hfirst_witness_witness_witness_right_right_left
  2. L123
    rewrite hsecond_witness_witness_witness_right_right_left
  3. L124
    rewrite <- hcoefficient
23Use earlier factsL125–125

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

  1. L125
    exact hvalue
24Calculate and transport equalitiesL126–127

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

  1. L126
    rewrite hfirst_witness_witness_witness_right_right_right
  2. L127
    rewrite hsecond_witness_witness_witness_right_right_right
25Use earlier factsL128–128

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

  1. L128
    exact hderivative

Library-wide reading audit

Original defined command ledger · 128 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro m
  4. 0004intro t
  5. 0005intro s
  6. 0006induction l
  7. 0007intro n
  8. 0008intro d
  9. 0009intro z
  10. 0010intro e
  11. 0011intro hbase
  12. 0012intro hleft
  13. 0013intro hright
  14. 0014have hzero_left : (n = 0 /\ d = 0)
  15. 0015specialize beta_horner_derivative_empty b
  16. 0016specialize beta_horner_derivative_empty c
  17. 0017specialize beta_horner_derivative_empty t
  18. 0018specialize beta_horner_derivative_empty n
  19. 0019specialize beta_horner_derivative_empty d
  20. 0020apply beta_horner_derivative_empty
  21. 0021exact hleft
  22. 0022have hzero_right : (z = 0 /\ e = 0)
  23. 0023specialize beta_horner_derivative_empty b
  24. 0024specialize beta_horner_derivative_empty c
  25. 0025specialize beta_horner_derivative_empty s
  26. 0026specialize beta_horner_derivative_empty z
  27. 0027specialize beta_horner_derivative_empty e
  28. 0028apply beta_horner_derivative_empty
  29. 0029exact hright
  30. 0030cases hzero_left
  31. 0031cases hzero_right
  32. 0032split
  33. 0033rewrite hzero_left_left
  34. 0034rewrite hzero_right_left
  35. 0035specialize mod_eq_refl m
  36. 0036specialize mod_eq_refl 0
  37. 0037apply mod_eq_refl
  38. 0038rewrite hzero_left_right
  39. 0039rewrite hzero_right_right
  40. 0040specialize mod_eq_refl m
  41. 0041specialize mod_eq_refl 0
  42. 0042apply mod_eq_refl
  43. 0043intro n
  44. 0044intro d
  45. 0045intro z
  46. 0046intro e
  47. 0047intro hbase
  48. 0048intro hleft
  49. 0049intro hright
  50. 0050have hfirst : exists a r q. ((((exists fs_h_pth_pair_first_coefficient. fs_h_pth_pair_first_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_pth_pair_first_coefficient. b = fs_q_pth_pair_first_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_hd_pth_pair_first_prefix ff_v_hd_pth_pair_first_prefix ff_d_hd_pth_pair_first_prefix ff_e_hd_pth_pair_first_prefix. ((((((exists fs_h_ph_hd_pth_pair_first_prefix_body_value_start. fs_h_ph_hd_pth_pair_first_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_value_start. ff_u_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_value_start * S ((S (0)) * ff_v_hd_pth_pair_first_prefix) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_value_terminal. fs_h_ph_hd_pth_pair_first_prefix_body_value_terminal + S (r) = S ((S (l)) * ff_v_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_value_terminal. ff_u_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_value_terminal * S ((S (l)) * ff_v_hd_pth_pair_first_prefix) + (r))) /\ forall ff_i_ph_hd_pth_pair_first_prefix_body_value_steps. (exists ph_bound_hd_pth_pair_first_prefix_body_value_steps. ph_bound_hd_pth_pair_first_prefix_body_value_steps + S ff_i_ph_hd_pth_pair_first_prefix_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_first_prefix_body_value_steps ff_previous_ph_hd_pth_pair_first_prefix_body_value_steps ff_current_ph_hd_pth_pair_first_prefix_body_value_steps. ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_value_steps_coefficient. fs_h_ph_hd_pth_pair_first_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_first_prefix_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_pth_pair_first_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_pair_first_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_value_steps_before. fs_h_ph_hd_pth_pair_first_prefix_body_value_steps_before + S (ff_previous_ph_hd_pth_pair_first_prefix_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_value_steps)) * ff_v_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_value_steps_before. ff_u_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_value_steps)) * ff_v_hd_pth_pair_first_prefix) + (ff_previous_ph_hd_pth_pair_first_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_value_steps_after. fs_h_ph_hd_pth_pair_first_prefix_body_value_steps_after + S (ff_current_ph_hd_pth_pair_first_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_pth_pair_first_prefix_body_value_steps)) * ff_v_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_value_steps_after. ff_u_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_pair_first_prefix_body_value_steps)) * ff_v_hd_pth_pair_first_prefix) + (ff_current_ph_hd_pth_pair_first_prefix_body_value_steps))) /\ ff_current_ph_hd_pth_pair_first_prefix_body_value_steps = ff_previous_ph_hd_pth_pair_first_prefix_body_value_steps * t + ff_coefficient_ph_hd_pth_pair_first_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_pair_first_prefix_body_derivative_start. fs_h_ph_hd_pth_pair_first_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_derivative_start. ff_d_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_pth_pair_first_prefix) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_derivative_terminal. fs_h_ph_hd_pth_pair_first_prefix_body_derivative_terminal + S (q) = S ((S (l)) * ff_e_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_derivative_terminal. ff_d_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_pair_first_prefix) + (q))) /\ forall ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps. (exists ph_bound_hd_pth_pair_first_prefix_body_derivative_steps. ph_bound_hd_pth_pair_first_prefix_body_derivative_steps + S ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_first_prefix_body_derivative_steps ff_previous_ph_hd_pth_pair_first_prefix_body_derivative_steps ff_current_ph_hd_pth_pair_first_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_pth_pair_first_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_first_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps)) * ff_v_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_derivative_steps_coefficient. ff_u_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps)) * ff_v_hd_pth_pair_first_prefix) + (ff_coefficient_ph_hd_pth_pair_first_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_derivative_steps_before. fs_h_ph_hd_pth_pair_first_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_pth_pair_first_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_derivative_steps_before. ff_d_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_first_prefix) + (ff_previous_ph_hd_pth_pair_first_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_first_prefix_body_derivative_steps_after. fs_h_ph_hd_pth_pair_first_prefix_body_derivative_steps_after + S (ff_current_ph_hd_pth_pair_first_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_first_prefix)) /\ exists fs_q_ph_hd_pth_pair_first_prefix_body_derivative_steps_after. ff_d_hd_pth_pair_first_prefix = fs_q_ph_hd_pth_pair_first_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_pair_first_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_first_prefix) + (ff_current_ph_hd_pth_pair_first_prefix_body_derivative_steps))) /\ ff_current_ph_hd_pth_pair_first_prefix_body_derivative_steps = ff_previous_ph_hd_pth_pair_first_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_pth_pair_first_prefix_body_derivative_steps)))))))) /\ ((n = r * t + a) /\ d = q * t + r)))
  51. 0051specialize beta_horner_derivative_successor_decompose b
  52. 0052specialize beta_horner_derivative_successor_decompose c
  53. 0053specialize beta_horner_derivative_successor_decompose t
  54. 0054specialize beta_horner_derivative_successor_decompose l
  55. 0055specialize beta_horner_derivative_successor_decompose n
  56. 0056specialize beta_horner_derivative_successor_decompose d
  57. 0057apply beta_horner_derivative_successor_decompose
  58. 0058exact hleft
  59. 0059cases hfirst
  60. 0060cases hfirst_witness
  61. 0061cases hfirst_witness_witness
  62. 0062cases hfirst_witness_witness_witness
  63. 0063cases hfirst_witness_witness_witness_right
  64. 0064cases hfirst_witness_witness_witness_right_right
  65. 0065have hsecond : exists a r q. ((((exists fs_h_pth_pair_second_coefficient. fs_h_pth_pair_second_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_pth_pair_second_coefficient. b = fs_q_pth_pair_second_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_hd_pth_pair_second_prefix ff_v_hd_pth_pair_second_prefix ff_d_hd_pth_pair_second_prefix ff_e_hd_pth_pair_second_prefix. ((((((exists fs_h_ph_hd_pth_pair_second_prefix_body_value_start. fs_h_ph_hd_pth_pair_second_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_value_start. ff_u_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_value_start * S ((S (0)) * ff_v_hd_pth_pair_second_prefix) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_value_terminal. fs_h_ph_hd_pth_pair_second_prefix_body_value_terminal + S (r) = S ((S (l)) * ff_v_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_value_terminal. ff_u_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_value_terminal * S ((S (l)) * ff_v_hd_pth_pair_second_prefix) + (r))) /\ forall ff_i_ph_hd_pth_pair_second_prefix_body_value_steps. (exists ph_bound_hd_pth_pair_second_prefix_body_value_steps. ph_bound_hd_pth_pair_second_prefix_body_value_steps + S ff_i_ph_hd_pth_pair_second_prefix_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_second_prefix_body_value_steps ff_previous_ph_hd_pth_pair_second_prefix_body_value_steps ff_current_ph_hd_pth_pair_second_prefix_body_value_steps. ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_value_steps_coefficient. fs_h_ph_hd_pth_pair_second_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_second_prefix_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_pth_pair_second_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_pair_second_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_value_steps_before. fs_h_ph_hd_pth_pair_second_prefix_body_value_steps_before + S (ff_previous_ph_hd_pth_pair_second_prefix_body_value_steps) = S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_value_steps)) * ff_v_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_value_steps_before. ff_u_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_value_steps)) * ff_v_hd_pth_pair_second_prefix) + (ff_previous_ph_hd_pth_pair_second_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_value_steps_after. fs_h_ph_hd_pth_pair_second_prefix_body_value_steps_after + S (ff_current_ph_hd_pth_pair_second_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_pth_pair_second_prefix_body_value_steps)) * ff_v_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_value_steps_after. ff_u_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_pair_second_prefix_body_value_steps)) * ff_v_hd_pth_pair_second_prefix) + (ff_current_ph_hd_pth_pair_second_prefix_body_value_steps))) /\ ff_current_ph_hd_pth_pair_second_prefix_body_value_steps = ff_previous_ph_hd_pth_pair_second_prefix_body_value_steps * s + ff_coefficient_ph_hd_pth_pair_second_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_pair_second_prefix_body_derivative_start. fs_h_ph_hd_pth_pair_second_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_derivative_start. ff_d_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_pth_pair_second_prefix) + (0))) /\ ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_derivative_terminal. fs_h_ph_hd_pth_pair_second_prefix_body_derivative_terminal + S (q) = S ((S (l)) * ff_e_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_derivative_terminal. ff_d_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_pair_second_prefix) + (q))) /\ forall ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps. (exists ph_bound_hd_pth_pair_second_prefix_body_derivative_steps. ph_bound_hd_pth_pair_second_prefix_body_derivative_steps + S ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_pair_second_prefix_body_derivative_steps ff_previous_ph_hd_pth_pair_second_prefix_body_derivative_steps ff_current_ph_hd_pth_pair_second_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_pth_pair_second_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_pair_second_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps)) * ff_v_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_derivative_steps_coefficient. ff_u_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps)) * ff_v_hd_pth_pair_second_prefix) + (ff_coefficient_ph_hd_pth_pair_second_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_derivative_steps_before. fs_h_ph_hd_pth_pair_second_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_pth_pair_second_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_derivative_steps_before. ff_d_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_second_prefix) + (ff_previous_ph_hd_pth_pair_second_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_pair_second_prefix_body_derivative_steps_after. fs_h_ph_hd_pth_pair_second_prefix_body_derivative_steps_after + S (ff_current_ph_hd_pth_pair_second_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_second_prefix)) /\ exists fs_q_ph_hd_pth_pair_second_prefix_body_derivative_steps_after. ff_d_hd_pth_pair_second_prefix = fs_q_ph_hd_pth_pair_second_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_pair_second_prefix_body_derivative_steps)) * ff_e_hd_pth_pair_second_prefix) + (ff_current_ph_hd_pth_pair_second_prefix_body_derivative_steps))) /\ ff_current_ph_hd_pth_pair_second_prefix_body_derivative_steps = ff_previous_ph_hd_pth_pair_second_prefix_body_derivative_steps * s + ff_coefficient_ph_hd_pth_pair_second_prefix_body_derivative_steps)))))))) /\ ((z = r * s + a) /\ e = q * s + r)))
  66. 0066specialize beta_horner_derivative_successor_decompose b
  67. 0067specialize beta_horner_derivative_successor_decompose c
  68. 0068specialize beta_horner_derivative_successor_decompose s
  69. 0069specialize beta_horner_derivative_successor_decompose l
  70. 0070specialize beta_horner_derivative_successor_decompose z
  71. 0071specialize beta_horner_derivative_successor_decompose e
  72. 0072apply beta_horner_derivative_successor_decompose
  73. 0073exact hright
  74. 0074cases hsecond
  75. 0075cases hsecond_witness
  76. 0076cases hsecond_witness_witness
  77. 0077cases hsecond_witness_witness_witness
  78. 0078cases hsecond_witness_witness_witness_right
  79. 0079cases hsecond_witness_witness_witness_right_right
  80. 0080have hcoefficient : x = x3
  81. 0081specialize beta_at_unique b
  82. 0082specialize beta_at_unique c
  83. 0083specialize beta_at_unique l
  84. 0084specialize beta_at_unique x
  85. 0085specialize beta_at_unique x3
  86. 0086apply beta_at_unique
  87. 0087exact hfirst_witness_witness_witness_left
  88. 0088exact hsecond_witness_witness_witness_left
  89. 0089have hprefix : ((exists hgcrt_mod_left_pth_pair_prefix_value hgcrt_mod_right_pth_pair_prefix_value. x1 + m * hgcrt_mod_left_pth_pair_prefix_value = x4 + m * hgcrt_mod_right_pth_pair_prefix_value) /\ (exists hgcrt_mod_left_pth_pair_prefix_derivative hgcrt_mod_right_pth_pair_prefix_derivative. x2 + m * hgcrt_mod_left_pth_pair_prefix_derivative = x5 + m * hgcrt_mod_right_pth_pair_prefix_derivative))
  90. 0090specialize IH x1
  91. 0091specialize IH x2
  92. 0092specialize IH x4
  93. 0093specialize IH x5
  94. 0094apply IH
  95. 0095exact hbase
  96. 0096exact hfirst_witness_witness_witness_right_left
  97. 0097exact hsecond_witness_witness_witness_right_left
  98. 0098cases hprefix
  99. 0099have hvalue : exists hgcrt_mod_left_pth_pair_value_step hgcrt_mod_right_pth_pair_value_step. (x1 * t + x) + m * hgcrt_mod_left_pth_pair_value_step = (x4 * s + x) + m * hgcrt_mod_right_pth_pair_value_step
  100. 0100specialize horner_mod_congruence_successor_step m
  101. 0101specialize horner_mod_congruence_successor_step t
  102. 0102specialize horner_mod_congruence_successor_step s
  103. 0103specialize horner_mod_congruence_successor_step x1
  104. 0104specialize horner_mod_congruence_successor_step x4
  105. 0105specialize horner_mod_congruence_successor_step x
  106. 0106apply horner_mod_congruence_successor_step
  107. 0107exact hbase
  108. 0108exact hprefix_left
  109. 0109have hderivative : exists hgcrt_mod_left_pth_pair_derivative_step hgcrt_mod_right_pth_pair_derivative_step. (x2 * t + x1) + m * hgcrt_mod_left_pth_pair_derivative_step = (x5 * s + x4) + m * hgcrt_mod_right_pth_pair_derivative_step
  110. 0110specialize horner_derivative_mod_congruence_successor_step m
  111. 0111specialize horner_derivative_mod_congruence_successor_step t
  112. 0112specialize horner_derivative_mod_congruence_successor_step s
  113. 0113specialize horner_derivative_mod_congruence_successor_step x1
  114. 0114specialize horner_derivative_mod_congruence_successor_step x4
  115. 0115specialize horner_derivative_mod_congruence_successor_step x2
  116. 0116specialize horner_derivative_mod_congruence_successor_step x5
  117. 0117apply horner_derivative_mod_congruence_successor_step
  118. 0118exact hbase
  119. 0119exact hprefix_left
  120. 0120exact hprefix_right
  121. 0121split
  122. 0122rewrite hfirst_witness_witness_witness_right_right_left
  123. 0123rewrite hsecond_witness_witness_witness_right_right_left
  124. 0124rewrite <- hcoefficient
  125. 0125exact hvalue
  126. 0126rewrite hfirst_witness_witness_witness_right_right_right
  127. 0127rewrite hsecond_witness_witness_witness_right_right_right
  128. 0128exact hderivative