PH0001

beta_prefix_horner_trace_exists

Every beta-coded coefficient prefix has a complete constructive Horner trace.

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

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ t. ∀ l. ∃ ff_u_ph_root_trace. ∃ ff_v_ph_root_trace. Beta(ff_u_ph_root_trace,ff_v_ph_root_trace,0,0) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. Beta(b,c,x,y) ∧ (Beta(ff_u_ph_root_trace,ff_v_ph_root_trace,x,z) ∧ (Beta(ff_u_ph_root_trace,ff_v_ph_root_trace,S x,n) ∧ n = z · t + y)))

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

Definition DAG

Beta(b,c,i,x) · 4Lt(a,b) · 1

Actual proof prerequisites

beta_at_self_of_bound · checked external prerequisiteadd_eq_zero_right · checked external prerequisitesucc_ne_zero · checked external prerequisitebeta_at_exists · checked external prerequisitebeta_prefix_extend · checked external prerequisitezero_le · checked external prerequisitesucc_le_succ · checked external prerequisitele_refl · checked external prerequisitele_of_succ_le_succ · checked external prerequisitele_eq_or_lt · checked external prerequisiteone_mul · checked external prerequisite
Original expanded first-order statement 
forall b c t l. exists ff_u_ph_root_trace ff_v_ph_root_trace. ((((exists fs_h_ph_root_trace_start. fs_h_ph_root_trace_start + S (0) = S ((S (0)) * ff_v_ph_root_trace)) /\ exists fs_q_ph_root_trace_start. ff_u_ph_root_trace = fs_q_ph_root_trace_start * S ((S (0)) * ff_v_ph_root_trace) + (0))) /\ forall ff_i_ph_root_trace_steps. (exists ph_bound_root_trace_steps. ph_bound_root_trace_steps + S ff_i_ph_root_trace_steps = l) -> exists ff_coefficient_ph_root_trace_steps ff_previous_ph_root_trace_steps ff_current_ph_root_trace_steps. ((((exists fs_h_ph_root_trace_steps_coefficient. fs_h_ph_root_trace_steps_coefficient + S (ff_coefficient_ph_root_trace_steps) = S ((S (ff_i_ph_root_trace_steps)) * c)) /\ exists fs_q_ph_root_trace_steps_coefficient. b = fs_q_ph_root_trace_steps_coefficient * S ((S (ff_i_ph_root_trace_steps)) * c) + (ff_coefficient_ph_root_trace_steps))) /\ ((((exists fs_h_ph_root_trace_steps_before. fs_h_ph_root_trace_steps_before + S (ff_previous_ph_root_trace_steps) = S ((S (ff_i_ph_root_trace_steps)) * ff_v_ph_root_trace)) /\ exists fs_q_ph_root_trace_steps_before. ff_u_ph_root_trace = fs_q_ph_root_trace_steps_before * S ((S (ff_i_ph_root_trace_steps)) * ff_v_ph_root_trace) + (ff_previous_ph_root_trace_steps))) /\ ((((exists fs_h_ph_root_trace_steps_after. fs_h_ph_root_trace_steps_after + S (ff_current_ph_root_trace_steps) = S ((S (S ff_i_ph_root_trace_steps)) * ff_v_ph_root_trace)) /\ exists fs_q_ph_root_trace_steps_after. ff_u_ph_root_trace = fs_q_ph_root_trace_steps_after * S ((S (S ff_i_ph_root_trace_steps)) * ff_v_ph_root_trace) + (ff_current_ph_root_trace_steps))) /\ ff_current_ph_root_trace_steps = ff_previous_ph_root_trace_steps * t + ff_coefficient_ph_root_trace_steps))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

137 script commands · 47 reading checkpoints · 10 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.

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

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

  1. L4
    induction l
03Construct an explicit witnessL5–6

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

  1. L5
    exists 0
  2. L6
    exists 1
04Separate the logical casesL7–7

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

  1. L7
    split
05Use earlier factsL8–12

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

  1. L8
    specialize beta_at_self_of_bound 1
  2. L9
    specialize beta_at_self_of_bound 0
  3. L10
    specialize beta_at_self_of_bound 0
  4. L11
    apply beta_at_self_of_bound
  5. L12
    specialize one_mul 1
06Calculate and transport equalitiesL13–13

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

  1. L13
    rewrite one_mul
07Use earlier factsL14–18

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

  1. L14
    specialize succ_le_succ 0
  2. L15
    specialize succ_le_succ (S 0)
  3. L16
    apply succ_le_succ
  4. L17
    specialize zero_le (S 0)
  5. L18
    exact zero_le
08Fix variables and assumptionsL19–20

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

  1. L19
    intro i
  2. L20
    intro hi
09Separate the logical casesL21–22

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

  1. L21
    exfalso
  2. L22
    cases hi
10Establish hsi0L23–30

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

  1. L23
    have hsi0 : S i = 0
  2. L24
    specialize add_eq_zero_right x
  3. L25
    specialize add_eq_zero_right (S i)
  4. L26
    apply add_eq_zero_right
  5. L27
    exact hi_witness
  6. L28
    specialize succ_ne_zero i
  7. L29
    apply succ_ne_zero
  8. L30
    exact hsi0
11Establish htraceL31–32

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

  1. L31
    have htrace : ∃ ff_u_ph_induction. ∃ ff_v_ph_induction. Beta(ff_u_ph_induction,ff_v_ph_induction,0,0) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. Beta(b,c,x,y) ∧ (Beta(ff_u_ph_induction,ff_v_ph_induction,x,z) ∧ (Beta(ff_u_ph_induction,ff_v_ph_induction,S x,n) ∧ n = z · t + y)))Definitions: BetaLtOriginal native command in the exact edition
  2. L32
    apply IH
12Separate the logical casesL33–35

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

  1. L33
    cases htrace
  2. L34
    cases htrace_witness
  3. L35
    cases htrace_witness_witness
13Establish hfactorL36–40

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

  1. L36
    have hfactor : exists p. ((exists fs_h_trace_factor. fs_h_trace_factor + S (p) = S ((S (l)) * c)) /\ exists fs_q_trace_factor. b = fs_q_trace_factor * S ((S (l)) * c) + (p))
  2. L37
    specialize beta_at_exists b
  3. L38
    specialize beta_at_exists c
  4. L39
    specialize beta_at_exists l
  5. L40
    exact beta_at_exists
14Separate the logical casesL41–41

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

  1. L41
    cases hfactor
15Establish hlastL42–46

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

  1. L42
    have hlast : exists r. ((exists fs_h_trace_last. fs_h_trace_last + S (r) = S ((S (l)) * x1)) /\ exists fs_q_trace_last. x = fs_q_trace_last * S ((S (l)) * x1) + (r))
  2. L43
    specialize beta_at_exists x
  3. L44
    specialize beta_at_exists x1
  4. L45
    specialize beta_at_exists l
  5. L46
    exact beta_at_exists
16Separate the logical casesL47–47

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

  1. L47
    cases hlast
17Establish hextL48–53

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

  1. L48
    have hext : exists z v. ((((exists fs_h_trace_extension. fs_h_trace_extension + S (x3 * t + x2) = S ((S (S l)) * v)) /\ exists fs_q_trace_extension. z = fs_q_trace_extension * S ((S (S l)) * v) + (x3 * t + x2))) /\ forall i a. (exists h. h + S i = S l) -> (((exists fs_h_trace_old. fs_h_trace_old + S (a) = S ((S (i)) * x1)) /\ exists fs_q_trace_old. x = fs_q_trace_old * S ((S (i)) * x1) + (a))) -> (((exists fs_h_trace_new. fs_h_trace_new + S (a) = S ((S (i)) * v)) /\ exists fs_q_trace_new. z = fs_q_trace_new * S ((S (i)) * v) + (a))))
  2. L49
    specialize beta_prefix_extend (S l)
  3. L50
    specialize beta_prefix_extend x
  4. L51
    specialize beta_prefix_extend x1
  5. L52
    specialize beta_prefix_extend (x3 * t + x2)
  6. L53
    exact beta_prefix_extend
18Separate the logical casesL54–56

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

  1. L54
    cases hext
  2. L55
    cases hext_witness
  3. L56
    cases hext_witness_witness
19Construct an explicit witnessL57–58

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

  1. L57
    exists x4
  2. L58
    exists x5
20Separate the logical casesL59–59

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

  1. L59
    split
21Use earlier factsL60–62

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

  1. L60
    specialize hext_witness_witness_right 0
  2. L61
    specialize hext_witness_witness_right 0
  3. L62
    apply hext_witness_witness_right
22Establish h0L63–63

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

  1. L63
    have h0 : exists h. h + S 0 = S l
23Establish hzeroL64–73

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

  1. L64
    have hzero : exists h. h + 0 = l
  2. L65
    specialize zero_le l
  3. L66
    exact zero_le
  4. L67
    specialize succ_le_succ 0
  5. L68
    specialize succ_le_succ l
  6. L69
    apply succ_le_succ
  7. L70
    exact hzero
  8. L71
    exact h0
  9. L72
    exact htrace_witness_witness_left
  10. L73
    intro i
24Fix variables and assumptionsL74–74

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

  1. L74
    intro hi
25Establish hilL75–79

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

  1. L75
    have hil : exists h. h + i = l
  2. L76
    specialize le_of_succ_le_succ i
  3. L77
    specialize le_of_succ_le_succ l
  4. L78
    apply le_of_succ_le_succ
  5. L79
    exact hi
26Establish hsplitL80–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L80
    have hsplit : i = l \/ exists h. h + S i = l
  2. L81
    specialize le_eq_or_lt i
  3. L82
    specialize le_eq_or_lt l
  4. L83
    apply le_eq_or_lt
  5. L84
    exact hil
27Separate the logical casesL85–85

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

  1. L85
    cases hsplit
28Construct an explicit witnessL86–88

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

  1. L86
    exists x2
  2. L87
    exists x3
  3. L88
    exists x3 * t + x2
29Separate the logical casesL89–89

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

  1. L89
    split
30Calculate and transport equalitiesL90–91

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

  1. L90
    rewrite hsplit_left
  2. L91
    rewrite hsplit_left
31Use earlier factsL92–92

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

  1. L92
    exact hfactor_witness
32Separate the logical casesL93–93

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

  1. L93
    split
33Calculate and transport equalitiesL94–95

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

  1. L94
    rewrite hsplit_left
  2. L95
    rewrite hsplit_left
34Use earlier factsL96–101

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

  1. L96
    specialize hext_witness_witness_right l
  2. L97
    specialize hext_witness_witness_right x3
  3. L98
    apply hext_witness_witness_right
  4. L99
    specialize le_refl (S l)
  5. L100
    exact le_refl
  6. L101
    exact hlast_witness
35Separate the logical casesL102–102

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

  1. L102
    split
36Calculate and transport equalitiesL103–104

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

  1. L103
    rewrite hsplit_left
  2. L104
    rewrite hsplit_left
37Use earlier factsL105–105

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

  1. L105
    exact hext_witness_witness_left
38Calculate and transport equalitiesL106–106

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

  1. L106
    refl
39Establish holdL107–110

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

  1. L107
    have hold : exists p r s. ((((exists fs_h_ph_hold_coefficient. fs_h_ph_hold_coefficient + S (p) = S ((S (i)) * c)) /\ exists fs_q_ph_hold_coefficient. b = fs_q_ph_hold_coefficient * S ((S (i)) * c) + (p))) /\ ((((exists fs_h_ph_hold_previous. fs_h_ph_hold_previous + S (r) = S ((S (i)) * x1)) /\ exists fs_q_ph_hold_previous. x = fs_q_ph_hold_previous * S ((S (i)) * x1) + (r))) /\ ((((exists fs_h_ph_hold_current. fs_h_ph_hold_current + S (s) = S ((S (S i)) * x1)) /\ exists fs_q_ph_hold_current. x = fs_q_ph_hold_current * S ((S (S i)) * x1) + (s))) /\ s = r * t + p)))
  2. L108
    specialize htrace_witness_witness_right i
  3. L109
    apply htrace_witness_witness_right
  4. L110
    exact hsplit_right
40Separate the logical casesL111–116

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

  1. L111
    cases hold
  2. L112
    cases hold_witness
  3. L113
    cases hold_witness_witness
  4. L114
    cases hold_witness_witness_witness
  5. L115
    cases hold_witness_witness_witness_right
  6. L116
    cases hold_witness_witness_witness_right_right
41Construct an explicit witnessL117–119

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

  1. L117
    exists x6
  2. L118
    exists x7
  3. L119
    exists x8
42Separate the logical casesL120–120

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

  1. L120
    split
43Use earlier factsL121–121

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

  1. L121
    exact hold_witness_witness_witness_left
44Separate the logical casesL122–122

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

  1. L122
    split
45Use earlier factsL123–127

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

  1. L123
    specialize hext_witness_witness_right i
  2. L124
    specialize hext_witness_witness_right x7
  3. L125
    apply hext_witness_witness_right
  4. L126
    exact hi
  5. L127
    exact hold_witness_witness_witness_right_left
46Separate the logical casesL128–128

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

  1. L128
    split
47Use earlier factsL129–137

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

  1. L129
    specialize hext_witness_witness_right (S i)
  2. L130
    specialize hext_witness_witness_right x8
  3. L131
    apply hext_witness_witness_right
  4. L132
    specialize succ_le_succ (S i)
  5. L133
    specialize succ_le_succ l
  6. L134
    apply succ_le_succ
  7. L135
    exact hsplit_right
  8. L136
    exact hold_witness_witness_witness_right_right_left
  9. L137
    exact hold_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 137 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004induction l
  5. 0005exists 0
  6. 0006exists 1
  7. 0007split
  8. 0008specialize beta_at_self_of_bound 1
  9. 0009specialize beta_at_self_of_bound 0
  10. 0010specialize beta_at_self_of_bound 0
  11. 0011apply beta_at_self_of_bound
  12. 0012specialize one_mul 1
  13. 0013rewrite one_mul
  14. 0014specialize succ_le_succ 0
  15. 0015specialize succ_le_succ (S 0)
  16. 0016apply succ_le_succ
  17. 0017specialize zero_le (S 0)
  18. 0018exact zero_le
  19. 0019intro i
  20. 0020intro hi
  21. 0021exfalso
  22. 0022cases hi
  23. 0023have hsi0 : S i = 0
  24. 0024specialize add_eq_zero_right x
  25. 0025specialize add_eq_zero_right (S i)
  26. 0026apply add_eq_zero_right
  27. 0027exact hi_witness
  28. 0028specialize succ_ne_zero i
  29. 0029apply succ_ne_zero
  30. 0030exact hsi0
  31. 0031have htrace : exists ff_u_ph_induction ff_v_ph_induction. ((((exists fs_h_ph_induction_start. fs_h_ph_induction_start + S (0) = S ((S (0)) * ff_v_ph_induction)) /\ exists fs_q_ph_induction_start. ff_u_ph_induction = fs_q_ph_induction_start * S ((S (0)) * ff_v_ph_induction) + (0))) /\ forall ff_i_ph_induction_steps. (exists ph_bound_induction_steps. ph_bound_induction_steps + S ff_i_ph_induction_steps = l) -> exists ff_coefficient_ph_induction_steps ff_previous_ph_induction_steps ff_current_ph_induction_steps. ((((exists fs_h_ph_induction_steps_coefficient. fs_h_ph_induction_steps_coefficient + S (ff_coefficient_ph_induction_steps) = S ((S (ff_i_ph_induction_steps)) * c)) /\ exists fs_q_ph_induction_steps_coefficient. b = fs_q_ph_induction_steps_coefficient * S ((S (ff_i_ph_induction_steps)) * c) + (ff_coefficient_ph_induction_steps))) /\ ((((exists fs_h_ph_induction_steps_before. fs_h_ph_induction_steps_before + S (ff_previous_ph_induction_steps) = S ((S (ff_i_ph_induction_steps)) * ff_v_ph_induction)) /\ exists fs_q_ph_induction_steps_before. ff_u_ph_induction = fs_q_ph_induction_steps_before * S ((S (ff_i_ph_induction_steps)) * ff_v_ph_induction) + (ff_previous_ph_induction_steps))) /\ ((((exists fs_h_ph_induction_steps_after. fs_h_ph_induction_steps_after + S (ff_current_ph_induction_steps) = S ((S (S ff_i_ph_induction_steps)) * ff_v_ph_induction)) /\ exists fs_q_ph_induction_steps_after. ff_u_ph_induction = fs_q_ph_induction_steps_after * S ((S (S ff_i_ph_induction_steps)) * ff_v_ph_induction) + (ff_current_ph_induction_steps))) /\ ff_current_ph_induction_steps = ff_previous_ph_induction_steps * t + ff_coefficient_ph_induction_steps))))
  32. 0032apply IH
  33. 0033cases htrace
  34. 0034cases htrace_witness
  35. 0035cases htrace_witness_witness
  36. 0036have hfactor : exists p. ((exists fs_h_trace_factor. fs_h_trace_factor + S (p) = S ((S (l)) * c)) /\ exists fs_q_trace_factor. b = fs_q_trace_factor * S ((S (l)) * c) + (p))
  37. 0037specialize beta_at_exists b
  38. 0038specialize beta_at_exists c
  39. 0039specialize beta_at_exists l
  40. 0040exact beta_at_exists
  41. 0041cases hfactor
  42. 0042have hlast : exists r. ((exists fs_h_trace_last. fs_h_trace_last + S (r) = S ((S (l)) * x1)) /\ exists fs_q_trace_last. x = fs_q_trace_last * S ((S (l)) * x1) + (r))
  43. 0043specialize beta_at_exists x
  44. 0044specialize beta_at_exists x1
  45. 0045specialize beta_at_exists l
  46. 0046exact beta_at_exists
  47. 0047cases hlast
  48. 0048have hext : exists z v. ((((exists fs_h_trace_extension. fs_h_trace_extension + S (x3 * t + x2) = S ((S (S l)) * v)) /\ exists fs_q_trace_extension. z = fs_q_trace_extension * S ((S (S l)) * v) + (x3 * t + x2))) /\ forall i a. (exists h. h + S i = S l) -> (((exists fs_h_trace_old. fs_h_trace_old + S (a) = S ((S (i)) * x1)) /\ exists fs_q_trace_old. x = fs_q_trace_old * S ((S (i)) * x1) + (a))) -> (((exists fs_h_trace_new. fs_h_trace_new + S (a) = S ((S (i)) * v)) /\ exists fs_q_trace_new. z = fs_q_trace_new * S ((S (i)) * v) + (a))))
  49. 0049specialize beta_prefix_extend (S l)
  50. 0050specialize beta_prefix_extend x
  51. 0051specialize beta_prefix_extend x1
  52. 0052specialize beta_prefix_extend (x3 * t + x2)
  53. 0053exact beta_prefix_extend
  54. 0054cases hext
  55. 0055cases hext_witness
  56. 0056cases hext_witness_witness
  57. 0057exists x4
  58. 0058exists x5
  59. 0059split
  60. 0060specialize hext_witness_witness_right 0
  61. 0061specialize hext_witness_witness_right 0
  62. 0062apply hext_witness_witness_right
  63. 0063have h0 : exists h. h + S 0 = S l
  64. 0064have hzero : exists h. h + 0 = l
  65. 0065specialize zero_le l
  66. 0066exact zero_le
  67. 0067specialize succ_le_succ 0
  68. 0068specialize succ_le_succ l
  69. 0069apply succ_le_succ
  70. 0070exact hzero
  71. 0071exact h0
  72. 0072exact htrace_witness_witness_left
  73. 0073intro i
  74. 0074intro hi
  75. 0075have hil : exists h. h + i = l
  76. 0076specialize le_of_succ_le_succ i
  77. 0077specialize le_of_succ_le_succ l
  78. 0078apply le_of_succ_le_succ
  79. 0079exact hi
  80. 0080have hsplit : i = l \/ exists h. h + S i = l
  81. 0081specialize le_eq_or_lt i
  82. 0082specialize le_eq_or_lt l
  83. 0083apply le_eq_or_lt
  84. 0084exact hil
  85. 0085cases hsplit
  86. 0086exists x2
  87. 0087exists x3
  88. 0088exists x3 * t + x2
  89. 0089split
  90. 0090rewrite hsplit_left
  91. 0091rewrite hsplit_left
  92. 0092exact hfactor_witness
  93. 0093split
  94. 0094rewrite hsplit_left
  95. 0095rewrite hsplit_left
  96. 0096specialize hext_witness_witness_right l
  97. 0097specialize hext_witness_witness_right x3
  98. 0098apply hext_witness_witness_right
  99. 0099specialize le_refl (S l)
  100. 0100exact le_refl
  101. 0101exact hlast_witness
  102. 0102split
  103. 0103rewrite hsplit_left
  104. 0104rewrite hsplit_left
  105. 0105exact hext_witness_witness_left
  106. 0106refl
  107. 0107have hold : exists p r s. ((((exists fs_h_ph_hold_coefficient. fs_h_ph_hold_coefficient + S (p) = S ((S (i)) * c)) /\ exists fs_q_ph_hold_coefficient. b = fs_q_ph_hold_coefficient * S ((S (i)) * c) + (p))) /\ ((((exists fs_h_ph_hold_previous. fs_h_ph_hold_previous + S (r) = S ((S (i)) * x1)) /\ exists fs_q_ph_hold_previous. x = fs_q_ph_hold_previous * S ((S (i)) * x1) + (r))) /\ ((((exists fs_h_ph_hold_current. fs_h_ph_hold_current + S (s) = S ((S (S i)) * x1)) /\ exists fs_q_ph_hold_current. x = fs_q_ph_hold_current * S ((S (S i)) * x1) + (s))) /\ s = r * t + p)))
  108. 0108specialize htrace_witness_witness_right i
  109. 0109apply htrace_witness_witness_right
  110. 0110exact hsplit_right
  111. 0111cases hold
  112. 0112cases hold_witness
  113. 0113cases hold_witness_witness
  114. 0114cases hold_witness_witness_witness
  115. 0115cases hold_witness_witness_witness_right
  116. 0116cases hold_witness_witness_witness_right_right
  117. 0117exists x6
  118. 0118exists x7
  119. 0119exists x8
  120. 0120split
  121. 0121exact hold_witness_witness_witness_left
  122. 0122split
  123. 0123specialize hext_witness_witness_right i
  124. 0124specialize hext_witness_witness_right x7
  125. 0125apply hext_witness_witness_right
  126. 0126exact hi
  127. 0127exact hold_witness_witness_witness_right_left
  128. 0128split
  129. 0129specialize hext_witness_witness_right (S i)
  130. 0130specialize hext_witness_witness_right x8
  131. 0131apply hext_witness_witness_right
  132. 0132specialize succ_le_succ (S i)
  133. 0133specialize succ_le_succ l
  134. 0134apply succ_le_succ
  135. 0135exact hsplit_right
  136. 0136exact hold_witness_witness_witness_right_right_left
  137. 0137exact hold_witness_witness_witness_right_right_right