BD0005

binary_digit_horner_append

Append a witnessed zero-or-one beta digit and prove that its new Horner value is exactly twice the prior exponent plus that digit.

Alpha v34 checked-use · first admitted v23 · 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.

The exact G102 milestone is fully proved for every natural exponent and every modulus greater than one, including actual canonical digits, a beta-coded accumulator execution, modular-power correctness, and the formal bound k≤3·BitLen(e)+2. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ h. ∀ d. ∀ n. BinaryDigitPrefix(b,c,l) → Horner(b,c,2,l,h) → d = 0 ∨ d = 1 → n = h + h + d → ∃ x. ∃ y. BinaryExponentDigitCode(n,S l,x,y)

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

Definition DAG

Horner(b,c,x,ell,z) · 1BinaryDigitPrefix(d,s,n) · 1BinaryExponentDigitCode(e,ell,b,c) · 1

Actual proof prerequisites

binary_digit_prefix_appendbinary_horner_prefix_recodebeta_horner_eval_exists · checked external prerequisitebeta_horner_eval_successor_decompose · checked external prerequisitebeta_at_unique · checked external prerequisitebeta_horner_eval_functional · checked external prerequisitemul_comm · checked external prerequisitetwo_mul_eq_add_self · checked external prerequisite
Original expanded first-order statement 
forall b c l h d n. (forall ff_index_be_bd_old ff_digit_be_bd_old. (exists ff_lt_be_bd_old_bound. ff_lt_be_bd_old_bound + S ff_index_be_bd_old = l) -> (((exists ff_h_be_bd_old_digit. ff_h_be_bd_old_digit + S (ff_digit_be_bd_old) = S ((S (ff_index_be_bd_old)) * c)) /\ exists ff_q_be_bd_old_digit. b = ff_q_be_bd_old_digit * S ((S (ff_index_be_bd_old)) * c) + (ff_digit_be_bd_old))) -> (ff_digit_be_bd_old = 0 \/ ff_digit_be_bd_old = 1)) -> (exists ff_u_ph_bd_append_old_horner ff_v_ph_bd_append_old_horner. ((((exists fs_h_ph_bd_append_old_horner_body_start. fs_h_ph_bd_append_old_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_append_old_horner)) /\ exists fs_q_ph_bd_append_old_horner_body_start. ff_u_ph_bd_append_old_horner = fs_q_ph_bd_append_old_horner_body_start * S ((S (0)) * ff_v_ph_bd_append_old_horner) + (0))) /\ ((((exists fs_h_ph_bd_append_old_horner_body_terminal. fs_h_ph_bd_append_old_horner_body_terminal + S (h) = S ((S (l)) * ff_v_ph_bd_append_old_horner)) /\ exists fs_q_ph_bd_append_old_horner_body_terminal. ff_u_ph_bd_append_old_horner = fs_q_ph_bd_append_old_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_append_old_horner) + (h))) /\ forall ff_i_ph_bd_append_old_horner_body_steps. (exists ph_bound_bd_append_old_horner_body_steps. ph_bound_bd_append_old_horner_body_steps + S ff_i_ph_bd_append_old_horner_body_steps = l) -> exists ff_coefficient_ph_bd_append_old_horner_body_steps ff_previous_ph_bd_append_old_horner_body_steps ff_current_ph_bd_append_old_horner_body_steps. ((((exists fs_h_ph_bd_append_old_horner_body_steps_coefficient. fs_h_ph_bd_append_old_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_append_old_horner_body_steps) = S ((S (ff_i_ph_bd_append_old_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_append_old_horner_body_steps_coefficient. b = fs_q_ph_bd_append_old_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_append_old_horner_body_steps)) * c) + (ff_coefficient_ph_bd_append_old_horner_body_steps))) /\ ((((exists fs_h_ph_bd_append_old_horner_body_steps_before. fs_h_ph_bd_append_old_horner_body_steps_before + S (ff_previous_ph_bd_append_old_horner_body_steps) = S ((S (ff_i_ph_bd_append_old_horner_body_steps)) * ff_v_ph_bd_append_old_horner)) /\ exists fs_q_ph_bd_append_old_horner_body_steps_before. ff_u_ph_bd_append_old_horner = fs_q_ph_bd_append_old_horner_body_steps_before * S ((S (ff_i_ph_bd_append_old_horner_body_steps)) * ff_v_ph_bd_append_old_horner) + (ff_previous_ph_bd_append_old_horner_body_steps))) /\ ((((exists fs_h_ph_bd_append_old_horner_body_steps_after. fs_h_ph_bd_append_old_horner_body_steps_after + S (ff_current_ph_bd_append_old_horner_body_steps) = S ((S (S ff_i_ph_bd_append_old_horner_body_steps)) * ff_v_ph_bd_append_old_horner)) /\ exists fs_q_ph_bd_append_old_horner_body_steps_after. ff_u_ph_bd_append_old_horner = fs_q_ph_bd_append_old_horner_body_steps_after * S ((S (S ff_i_ph_bd_append_old_horner_body_steps)) * ff_v_ph_bd_append_old_horner) + (ff_current_ph_bd_append_old_horner_body_steps))) /\ ff_current_ph_bd_append_old_horner_body_steps = ff_previous_ph_bd_append_old_horner_body_steps * 2 + ff_coefficient_ph_bd_append_old_horner_body_steps)))))) -> (d = 0 \/ d = 1) -> n = (h + h) + d -> (exists z e. ((forall ff_index_be_bd_horner_append_digits ff_digit_be_bd_horner_append_digits. (exists ff_lt_be_bd_horner_append_digits_bound. ff_lt_be_bd_horner_append_digits_bound + S ff_index_be_bd_horner_append_digits = S l) -> (((exists ff_h_be_bd_horner_append_digits_digit. ff_h_be_bd_horner_append_digits_digit + S (ff_digit_be_bd_horner_append_digits) = S ((S (ff_index_be_bd_horner_append_digits)) * e)) /\ exists ff_q_be_bd_horner_append_digits_digit. z = ff_q_be_bd_horner_append_digits_digit * S ((S (ff_index_be_bd_horner_append_digits)) * e) + (ff_digit_be_bd_horner_append_digits))) -> (ff_digit_be_bd_horner_append_digits = 0 \/ ff_digit_be_bd_horner_append_digits = 1)) /\ (exists ff_u_ph_bd_horner_append_value ff_v_ph_bd_horner_append_value. ((((exists fs_h_ph_bd_horner_append_value_body_start. fs_h_ph_bd_horner_append_value_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_horner_append_value)) /\ exists fs_q_ph_bd_horner_append_value_body_start. ff_u_ph_bd_horner_append_value = fs_q_ph_bd_horner_append_value_body_start * S ((S (0)) * ff_v_ph_bd_horner_append_value) + (0))) /\ ((((exists fs_h_ph_bd_horner_append_value_body_terminal. fs_h_ph_bd_horner_append_value_body_terminal + S (n) = S ((S (S l)) * ff_v_ph_bd_horner_append_value)) /\ exists fs_q_ph_bd_horner_append_value_body_terminal. ff_u_ph_bd_horner_append_value = fs_q_ph_bd_horner_append_value_body_terminal * S ((S (S l)) * ff_v_ph_bd_horner_append_value) + (n))) /\ forall ff_i_ph_bd_horner_append_value_body_steps. (exists ph_bound_bd_horner_append_value_body_steps. ph_bound_bd_horner_append_value_body_steps + S ff_i_ph_bd_horner_append_value_body_steps = S l) -> exists ff_coefficient_ph_bd_horner_append_value_body_steps ff_previous_ph_bd_horner_append_value_body_steps ff_current_ph_bd_horner_append_value_body_steps. ((((exists fs_h_ph_bd_horner_append_value_body_steps_coefficient. fs_h_ph_bd_horner_append_value_body_steps_coefficient + S (ff_coefficient_ph_bd_horner_append_value_body_steps) = S ((S (ff_i_ph_bd_horner_append_value_body_steps)) * e)) /\ exists fs_q_ph_bd_horner_append_value_body_steps_coefficient. z = fs_q_ph_bd_horner_append_value_body_steps_coefficient * S ((S (ff_i_ph_bd_horner_append_value_body_steps)) * e) + (ff_coefficient_ph_bd_horner_append_value_body_steps))) /\ ((((exists fs_h_ph_bd_horner_append_value_body_steps_before. fs_h_ph_bd_horner_append_value_body_steps_before + S (ff_previous_ph_bd_horner_append_value_body_steps) = S ((S (ff_i_ph_bd_horner_append_value_body_steps)) * ff_v_ph_bd_horner_append_value)) /\ exists fs_q_ph_bd_horner_append_value_body_steps_before. ff_u_ph_bd_horner_append_value = fs_q_ph_bd_horner_append_value_body_steps_before * S ((S (ff_i_ph_bd_horner_append_value_body_steps)) * ff_v_ph_bd_horner_append_value) + (ff_previous_ph_bd_horner_append_value_body_steps))) /\ ((((exists fs_h_ph_bd_horner_append_value_body_steps_after. fs_h_ph_bd_horner_append_value_body_steps_after + S (ff_current_ph_bd_horner_append_value_body_steps) = S ((S (S ff_i_ph_bd_horner_append_value_body_steps)) * ff_v_ph_bd_horner_append_value)) /\ exists fs_q_ph_bd_horner_append_value_body_steps_after. ff_u_ph_bd_horner_append_value = fs_q_ph_bd_horner_append_value_body_steps_after * S ((S (S ff_i_ph_bd_horner_append_value_body_steps)) * ff_v_ph_bd_horner_append_value) + (ff_current_ph_bd_horner_append_value_body_steps))) /\ ff_current_ph_bd_horner_append_value_body_steps = ff_previous_ph_bd_horner_append_value_body_steps * 2 + ff_coefficient_ph_bd_horner_append_value_body_steps))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

92 script commands · 17 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)
binary digit prefix appendbinary horner prefix recode

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 b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro h
  5. L5
    intro d
  6. L6
    intro n
  7. L7
    intro hdigits
  8. L8
    intro hhorner
  9. L9
    intro hdigit
  10. L10
    intro htarget
02Establish happendL11–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary digit prefix append.

  1. L11
    have happend : ∃ z. ∃ e. Beta(z,e,l,d) ∧ (BinaryDigitPrefix(z,e,S l) ∧ (∀ x. ∀ y. Lt(x,l) → Beta(b,c,x,y) → Beta(z,e,x,y)))Definitions: BetaBinaryDigitPrefixLtOriginal native command in the exact edition
  2. L12
    specialize binary_digit_prefix_append b
  3. L13
    specialize binary_digit_prefix_append c
  4. L14
    specialize binary_digit_prefix_append l
  5. L15
    specialize binary_digit_prefix_append d
  6. L16
    apply binary_digit_prefix_append
  7. L17
    exact hdigits
  8. L18
    exact hdigit
03Separate the logical casesL19–22

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

  1. L19
    cases happend
  2. L20
    cases happend_witness
  3. L21
    cases happend_witness_witness
  4. L22
    cases happend_witness_witness_right
04Establish hprefixL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary horner prefix recode.

  1. L23
    have hprefix : Horner(x,x1,2,l,h)Definitions: HornerOriginal native command in the exact edition
  2. L24
    specialize binary_horner_prefix_recode b
  3. L25
    specialize binary_horner_prefix_recode c
  4. L26
    specialize binary_horner_prefix_recode x
  5. L27
    specialize binary_horner_prefix_recode x1
  6. L28
    specialize binary_horner_prefix_recode l
  7. L29
    specialize binary_horner_prefix_recode h
  8. L30
    apply binary_horner_prefix_recode
  9. L31
    exact happend_witness_witness_right_right
  10. L32
    exact hhorner
05Establish hevaluationL33–38

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

  1. L33
    have hevaluation : ∃ value. Horner(x,x1,2,S l,value)Definitions: HornerOriginal native command in the exact edition
  2. L34
    specialize beta_horner_eval_exists x
  3. L35
    specialize beta_horner_eval_exists x1
  4. L36
    specialize beta_horner_eval_exists 2
  5. L37
    specialize beta_horner_eval_exists (S l)
  6. L38
    exact beta_horner_eval_exists
06Separate the logical casesL39–39

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

  1. L39
    cases hevaluation
07Establish hdecomposeL40–47

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

  1. L40
    have hdecompose : ∃ digit. ∃ half. Beta(x,x1,l,digit) ∧ (Horner(x,x1,2,l,half) ∧ x2 = half · 2 + digit)Definitions: BetaHornerOriginal native command in the exact edition
  2. L41
    specialize beta_horner_eval_successor_decompose x
  3. L42
    specialize beta_horner_eval_successor_decompose x1
  4. L43
    specialize beta_horner_eval_successor_decompose 2
  5. L44
    specialize beta_horner_eval_successor_decompose l
  6. L45
    specialize beta_horner_eval_successor_decompose x2
  7. L46
    apply beta_horner_eval_successor_decompose
  8. L47
    exact hevaluation_witness
08Separate the logical casesL48–51

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

  1. L48
    cases hdecompose
  2. L49
    cases hdecompose_witness
  3. L50
    cases hdecompose_witness_witness
  4. L51
    cases hdecompose_witness_witness_right
09Establish hlastL52–60

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

  1. L52
    have hlast : x3 = d
  2. L53
    specialize beta_at_unique x
  3. L54
    specialize beta_at_unique x1
  4. L55
    specialize beta_at_unique l
  5. L56
    specialize beta_at_unique x3
  6. L57
    specialize beta_at_unique d
  7. L58
    apply beta_at_unique
  8. L59
    exact hdecompose_witness_witness_left
  9. L60
    exact happend_witness_witness_left
10Establish hhalfL61–70

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

  1. L61
    have hhalf : x4 = h
  2. L62
    specialize beta_horner_eval_functional x
  3. L63
    specialize beta_horner_eval_functional x1
  4. L64
    specialize beta_horner_eval_functional 2
  5. L65
    specialize beta_horner_eval_functional l
  6. L66
    specialize beta_horner_eval_functional x4
  7. L67
    specialize beta_horner_eval_functional h
  8. L68
    apply beta_horner_eval_functional
  9. L69
    exact hdecompose_witness_witness_right_left
  10. L70
    exact hprefix
11Establish hdoubleL71–80

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

  1. L71
    have hdouble : h * 2 = h + h
  2. L72
    trans 2 * h
  3. L73
    specialize mul_comm h
  4. L74
    specialize mul_comm 2
  5. L75
    exact mul_comm
  6. L76
    specialize two_mul_eq_add_self h
  7. L77
    exact two_mul_eq_add_self
  8. L78
    rewrite hhalf at hdecompose_witness_witness_right_right
  9. L79
    rewrite hlast at hdecompose_witness_witness_right_right
  10. L80
    rewrite hdouble at hdecompose_witness_witness_right_right
12Establish hvalueL81–85

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

  1. L81
    have hvalue : x2 = n
  2. L82
    trans (h + h) + d
  3. L83
    exact hdecompose_witness_witness_right_right
  4. L84
    symm
  5. L85
    exact htarget
13Construct an explicit witnessL86–87

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

  1. L86
    exists x
  2. L87
    exists x1
14Separate the logical casesL88–88

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

  1. L88
    split
15Use earlier factsL89–89

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

  1. L89
    exact happend_witness_witness_right_left
16Calculate and transport equalitiesL90–91

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

  1. L90
    rewrite <- hvalue
  2. L91
    rewrite <- hvalue
17Use earlier factsL92–92

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

  1. L92
    exact hevaluation_witness

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro h
  5. 0005intro d
  6. 0006intro n
  7. 0007intro hdigits
  8. 0008intro hhorner
  9. 0009intro hdigit
  10. 0010intro htarget
  11. 0011have happend : exists z e. ((((exists ff_h_bd_append_terminal. ff_h_bd_append_terminal + S (d) = S ((S (l)) * e)) /\ exists ff_q_bd_append_terminal. z = ff_q_bd_append_terminal * S ((S (l)) * e) + (d))) /\ ((forall ff_index_be_bd_append ff_digit_be_bd_append. (exists ff_lt_be_bd_append_bound. ff_lt_be_bd_append_bound + S ff_index_be_bd_append = S l) -> (((exists ff_h_be_bd_append_digit. ff_h_be_bd_append_digit + S (ff_digit_be_bd_append) = S ((S (ff_index_be_bd_append)) * e)) /\ exists ff_q_be_bd_append_digit. z = ff_q_be_bd_append_digit * S ((S (ff_index_be_bd_append)) * e) + (ff_digit_be_bd_append))) -> (ff_digit_be_bd_append = 0 \/ ff_digit_be_bd_append = 1)) /\ (forall bd_index_append_recode bd_value_append_recode. (exists bd_gap_append_recode. bd_gap_append_recode + S bd_index_append_recode = l) -> (((exists ff_h_bd_append_recode_old. ff_h_bd_append_recode_old + S (bd_value_append_recode) = S ((S (bd_index_append_recode)) * c)) /\ exists ff_q_bd_append_recode_old. b = ff_q_bd_append_recode_old * S ((S (bd_index_append_recode)) * c) + (bd_value_append_recode))) -> (((exists ff_h_bd_append_recode_new. ff_h_bd_append_recode_new + S (bd_value_append_recode) = S ((S (bd_index_append_recode)) * e)) /\ exists ff_q_bd_append_recode_new. z = ff_q_bd_append_recode_new * S ((S (bd_index_append_recode)) * e) + (bd_value_append_recode))))))
  12. 0012specialize binary_digit_prefix_append b
  13. 0013specialize binary_digit_prefix_append c
  14. 0014specialize binary_digit_prefix_append l
  15. 0015specialize binary_digit_prefix_append d
  16. 0016apply binary_digit_prefix_append
  17. 0017exact hdigits
  18. 0018exact hdigit
  19. 0019cases happend
  20. 0020cases happend_witness
  21. 0021cases happend_witness_witness
  22. 0022cases happend_witness_witness_right
  23. 0023have hprefix : (exists ff_u_ph_bd_append_prefix ff_v_ph_bd_append_prefix. ((((exists fs_h_ph_bd_append_prefix_body_start. fs_h_ph_bd_append_prefix_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_append_prefix)) /\ exists fs_q_ph_bd_append_prefix_body_start. ff_u_ph_bd_append_prefix = fs_q_ph_bd_append_prefix_body_start * S ((S (0)) * ff_v_ph_bd_append_prefix) + (0))) /\ ((((exists fs_h_ph_bd_append_prefix_body_terminal. fs_h_ph_bd_append_prefix_body_terminal + S (h) = S ((S (l)) * ff_v_ph_bd_append_prefix)) /\ exists fs_q_ph_bd_append_prefix_body_terminal. ff_u_ph_bd_append_prefix = fs_q_ph_bd_append_prefix_body_terminal * S ((S (l)) * ff_v_ph_bd_append_prefix) + (h))) /\ forall ff_i_ph_bd_append_prefix_body_steps. (exists ph_bound_bd_append_prefix_body_steps. ph_bound_bd_append_prefix_body_steps + S ff_i_ph_bd_append_prefix_body_steps = l) -> exists ff_coefficient_ph_bd_append_prefix_body_steps ff_previous_ph_bd_append_prefix_body_steps ff_current_ph_bd_append_prefix_body_steps. ((((exists fs_h_ph_bd_append_prefix_body_steps_coefficient. fs_h_ph_bd_append_prefix_body_steps_coefficient + S (ff_coefficient_ph_bd_append_prefix_body_steps) = S ((S (ff_i_ph_bd_append_prefix_body_steps)) * x1)) /\ exists fs_q_ph_bd_append_prefix_body_steps_coefficient. x = fs_q_ph_bd_append_prefix_body_steps_coefficient * S ((S (ff_i_ph_bd_append_prefix_body_steps)) * x1) + (ff_coefficient_ph_bd_append_prefix_body_steps))) /\ ((((exists fs_h_ph_bd_append_prefix_body_steps_before. fs_h_ph_bd_append_prefix_body_steps_before + S (ff_previous_ph_bd_append_prefix_body_steps) = S ((S (ff_i_ph_bd_append_prefix_body_steps)) * ff_v_ph_bd_append_prefix)) /\ exists fs_q_ph_bd_append_prefix_body_steps_before. ff_u_ph_bd_append_prefix = fs_q_ph_bd_append_prefix_body_steps_before * S ((S (ff_i_ph_bd_append_prefix_body_steps)) * ff_v_ph_bd_append_prefix) + (ff_previous_ph_bd_append_prefix_body_steps))) /\ ((((exists fs_h_ph_bd_append_prefix_body_steps_after. fs_h_ph_bd_append_prefix_body_steps_after + S (ff_current_ph_bd_append_prefix_body_steps) = S ((S (S ff_i_ph_bd_append_prefix_body_steps)) * ff_v_ph_bd_append_prefix)) /\ exists fs_q_ph_bd_append_prefix_body_steps_after. ff_u_ph_bd_append_prefix = fs_q_ph_bd_append_prefix_body_steps_after * S ((S (S ff_i_ph_bd_append_prefix_body_steps)) * ff_v_ph_bd_append_prefix) + (ff_current_ph_bd_append_prefix_body_steps))) /\ ff_current_ph_bd_append_prefix_body_steps = ff_previous_ph_bd_append_prefix_body_steps * 2 + ff_coefficient_ph_bd_append_prefix_body_steps))))))
  24. 0024specialize binary_horner_prefix_recode b
  25. 0025specialize binary_horner_prefix_recode c
  26. 0026specialize binary_horner_prefix_recode x
  27. 0027specialize binary_horner_prefix_recode x1
  28. 0028specialize binary_horner_prefix_recode l
  29. 0029specialize binary_horner_prefix_recode h
  30. 0030apply binary_horner_prefix_recode
  31. 0031exact happend_witness_witness_right_right
  32. 0032exact hhorner
  33. 0033have hevaluation : exists value. (exists ff_u_ph_bd_append_evaluation ff_v_ph_bd_append_evaluation. ((((exists fs_h_ph_bd_append_evaluation_body_start. fs_h_ph_bd_append_evaluation_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_append_evaluation)) /\ exists fs_q_ph_bd_append_evaluation_body_start. ff_u_ph_bd_append_evaluation = fs_q_ph_bd_append_evaluation_body_start * S ((S (0)) * ff_v_ph_bd_append_evaluation) + (0))) /\ ((((exists fs_h_ph_bd_append_evaluation_body_terminal. fs_h_ph_bd_append_evaluation_body_terminal + S (value) = S ((S (S l)) * ff_v_ph_bd_append_evaluation)) /\ exists fs_q_ph_bd_append_evaluation_body_terminal. ff_u_ph_bd_append_evaluation = fs_q_ph_bd_append_evaluation_body_terminal * S ((S (S l)) * ff_v_ph_bd_append_evaluation) + (value))) /\ forall ff_i_ph_bd_append_evaluation_body_steps. (exists ph_bound_bd_append_evaluation_body_steps. ph_bound_bd_append_evaluation_body_steps + S ff_i_ph_bd_append_evaluation_body_steps = S l) -> exists ff_coefficient_ph_bd_append_evaluation_body_steps ff_previous_ph_bd_append_evaluation_body_steps ff_current_ph_bd_append_evaluation_body_steps. ((((exists fs_h_ph_bd_append_evaluation_body_steps_coefficient. fs_h_ph_bd_append_evaluation_body_steps_coefficient + S (ff_coefficient_ph_bd_append_evaluation_body_steps) = S ((S (ff_i_ph_bd_append_evaluation_body_steps)) * x1)) /\ exists fs_q_ph_bd_append_evaluation_body_steps_coefficient. x = fs_q_ph_bd_append_evaluation_body_steps_coefficient * S ((S (ff_i_ph_bd_append_evaluation_body_steps)) * x1) + (ff_coefficient_ph_bd_append_evaluation_body_steps))) /\ ((((exists fs_h_ph_bd_append_evaluation_body_steps_before. fs_h_ph_bd_append_evaluation_body_steps_before + S (ff_previous_ph_bd_append_evaluation_body_steps) = S ((S (ff_i_ph_bd_append_evaluation_body_steps)) * ff_v_ph_bd_append_evaluation)) /\ exists fs_q_ph_bd_append_evaluation_body_steps_before. ff_u_ph_bd_append_evaluation = fs_q_ph_bd_append_evaluation_body_steps_before * S ((S (ff_i_ph_bd_append_evaluation_body_steps)) * ff_v_ph_bd_append_evaluation) + (ff_previous_ph_bd_append_evaluation_body_steps))) /\ ((((exists fs_h_ph_bd_append_evaluation_body_steps_after. fs_h_ph_bd_append_evaluation_body_steps_after + S (ff_current_ph_bd_append_evaluation_body_steps) = S ((S (S ff_i_ph_bd_append_evaluation_body_steps)) * ff_v_ph_bd_append_evaluation)) /\ exists fs_q_ph_bd_append_evaluation_body_steps_after. ff_u_ph_bd_append_evaluation = fs_q_ph_bd_append_evaluation_body_steps_after * S ((S (S ff_i_ph_bd_append_evaluation_body_steps)) * ff_v_ph_bd_append_evaluation) + (ff_current_ph_bd_append_evaluation_body_steps))) /\ ff_current_ph_bd_append_evaluation_body_steps = ff_previous_ph_bd_append_evaluation_body_steps * 2 + ff_coefficient_ph_bd_append_evaluation_body_steps))))))
  34. 0034specialize beta_horner_eval_exists x
  35. 0035specialize beta_horner_eval_exists x1
  36. 0036specialize beta_horner_eval_exists 2
  37. 0037specialize beta_horner_eval_exists (S l)
  38. 0038exact beta_horner_eval_exists
  39. 0039cases hevaluation
  40. 0040have hdecompose : exists digit half. ((((exists ff_h_bd_bd_append_last. ff_h_bd_bd_append_last + S (digit) = S ((S (l)) * x1)) /\ exists ff_q_bd_bd_append_last. x = ff_q_bd_bd_append_last * S ((S (l)) * x1) + (digit))) /\ ((exists ff_u_ph_bd_append_half ff_v_ph_bd_append_half. ((((exists fs_h_ph_bd_append_half_body_start. fs_h_ph_bd_append_half_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_append_half)) /\ exists fs_q_ph_bd_append_half_body_start. ff_u_ph_bd_append_half = fs_q_ph_bd_append_half_body_start * S ((S (0)) * ff_v_ph_bd_append_half) + (0))) /\ ((((exists fs_h_ph_bd_append_half_body_terminal. fs_h_ph_bd_append_half_body_terminal + S (half) = S ((S (l)) * ff_v_ph_bd_append_half)) /\ exists fs_q_ph_bd_append_half_body_terminal. ff_u_ph_bd_append_half = fs_q_ph_bd_append_half_body_terminal * S ((S (l)) * ff_v_ph_bd_append_half) + (half))) /\ forall ff_i_ph_bd_append_half_body_steps. (exists ph_bound_bd_append_half_body_steps. ph_bound_bd_append_half_body_steps + S ff_i_ph_bd_append_half_body_steps = l) -> exists ff_coefficient_ph_bd_append_half_body_steps ff_previous_ph_bd_append_half_body_steps ff_current_ph_bd_append_half_body_steps. ((((exists fs_h_ph_bd_append_half_body_steps_coefficient. fs_h_ph_bd_append_half_body_steps_coefficient + S (ff_coefficient_ph_bd_append_half_body_steps) = S ((S (ff_i_ph_bd_append_half_body_steps)) * x1)) /\ exists fs_q_ph_bd_append_half_body_steps_coefficient. x = fs_q_ph_bd_append_half_body_steps_coefficient * S ((S (ff_i_ph_bd_append_half_body_steps)) * x1) + (ff_coefficient_ph_bd_append_half_body_steps))) /\ ((((exists fs_h_ph_bd_append_half_body_steps_before. fs_h_ph_bd_append_half_body_steps_before + S (ff_previous_ph_bd_append_half_body_steps) = S ((S (ff_i_ph_bd_append_half_body_steps)) * ff_v_ph_bd_append_half)) /\ exists fs_q_ph_bd_append_half_body_steps_before. ff_u_ph_bd_append_half = fs_q_ph_bd_append_half_body_steps_before * S ((S (ff_i_ph_bd_append_half_body_steps)) * ff_v_ph_bd_append_half) + (ff_previous_ph_bd_append_half_body_steps))) /\ ((((exists fs_h_ph_bd_append_half_body_steps_after. fs_h_ph_bd_append_half_body_steps_after + S (ff_current_ph_bd_append_half_body_steps) = S ((S (S ff_i_ph_bd_append_half_body_steps)) * ff_v_ph_bd_append_half)) /\ exists fs_q_ph_bd_append_half_body_steps_after. ff_u_ph_bd_append_half = fs_q_ph_bd_append_half_body_steps_after * S ((S (S ff_i_ph_bd_append_half_body_steps)) * ff_v_ph_bd_append_half) + (ff_current_ph_bd_append_half_body_steps))) /\ ff_current_ph_bd_append_half_body_steps = ff_previous_ph_bd_append_half_body_steps * 2 + ff_coefficient_ph_bd_append_half_body_steps)))))) /\ x2 = half * 2 + digit))
  41. 0041specialize beta_horner_eval_successor_decompose x
  42. 0042specialize beta_horner_eval_successor_decompose x1
  43. 0043specialize beta_horner_eval_successor_decompose 2
  44. 0044specialize beta_horner_eval_successor_decompose l
  45. 0045specialize beta_horner_eval_successor_decompose x2
  46. 0046apply beta_horner_eval_successor_decompose
  47. 0047exact hevaluation_witness
  48. 0048cases hdecompose
  49. 0049cases hdecompose_witness
  50. 0050cases hdecompose_witness_witness
  51. 0051cases hdecompose_witness_witness_right
  52. 0052have hlast : x3 = d
  53. 0053specialize beta_at_unique x
  54. 0054specialize beta_at_unique x1
  55. 0055specialize beta_at_unique l
  56. 0056specialize beta_at_unique x3
  57. 0057specialize beta_at_unique d
  58. 0058apply beta_at_unique
  59. 0059exact hdecompose_witness_witness_left
  60. 0060exact happend_witness_witness_left
  61. 0061have hhalf : x4 = h
  62. 0062specialize beta_horner_eval_functional x
  63. 0063specialize beta_horner_eval_functional x1
  64. 0064specialize beta_horner_eval_functional 2
  65. 0065specialize beta_horner_eval_functional l
  66. 0066specialize beta_horner_eval_functional x4
  67. 0067specialize beta_horner_eval_functional h
  68. 0068apply beta_horner_eval_functional
  69. 0069exact hdecompose_witness_witness_right_left
  70. 0070exact hprefix
  71. 0071have hdouble : h * 2 = h + h
  72. 0072trans 2 * h
  73. 0073specialize mul_comm h
  74. 0074specialize mul_comm 2
  75. 0075exact mul_comm
  76. 0076specialize two_mul_eq_add_self h
  77. 0077exact two_mul_eq_add_self
  78. 0078rewrite hhalf at hdecompose_witness_witness_right_right
  79. 0079rewrite hlast at hdecompose_witness_witness_right_right
  80. 0080rewrite hdouble at hdecompose_witness_witness_right_right
  81. 0081have hvalue : x2 = n
  82. 0082trans (h + h) + d
  83. 0083exact hdecompose_witness_witness_right_right
  84. 0084symm
  85. 0085exact htarget
  86. 0086exists x
  87. 0087exists x1
  88. 0088split
  89. 0089exact happend_witness_witness_right_left
  90. 0090rewrite <- hvalue
  91. 0091rewrite <- hvalue
  92. 0092exact hevaluation_witness