PH0003

beta_horner_trace_functional

Any two complete Horner traces over the same polynomial have equal values.

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. ∀ n. ∀ u. ∀ v. ∀ m. ∀ w. ∀ d. Beta(u,v,0,0) ∧ (Beta(u,v,l,n) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ k. Beta(b,c,x,y) ∧ (Beta(u,v,x,z) ∧ (Beta(u,v,S x,k) ∧ k = z · t + y)))) → Beta(w,d,0,0) ∧ (Beta(w,d,l,m) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ k. Beta(b,c,x,y) ∧ (Beta(w,d,x,z) ∧ (Beta(w,d,S x,k) ∧ k = z · t + y)))) → n = m

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

Definition DAG

Beta(b,c,i,x) · 10Lt(a,b) · 2

Actual proof prerequisites

beta_at_unique · checked external prerequisitele_refl · checked external prerequisitele_succ · checked external prerequisiteadd_congr · checked external prerequisitemul_congr · checked external prerequisite
Original expanded first-order statement 
forall b c t l n u v m w d. (((((exists fs_h_ph_left_start. fs_h_ph_left_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_ph_left_start. u = fs_q_ph_left_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_ph_left_terminal. fs_h_ph_left_terminal + S (n) = S ((S (l)) * v)) /\ exists fs_q_ph_left_terminal. u = fs_q_ph_left_terminal * S ((S (l)) * v) + (n))) /\ forall ff_i_ph_left_steps. (exists ph_bound_left_steps. ph_bound_left_steps + S ff_i_ph_left_steps = l) -> exists ff_coefficient_ph_left_steps ff_previous_ph_left_steps ff_current_ph_left_steps. ((((exists fs_h_ph_left_steps_coefficient. fs_h_ph_left_steps_coefficient + S (ff_coefficient_ph_left_steps) = S ((S (ff_i_ph_left_steps)) * c)) /\ exists fs_q_ph_left_steps_coefficient. b = fs_q_ph_left_steps_coefficient * S ((S (ff_i_ph_left_steps)) * c) + (ff_coefficient_ph_left_steps))) /\ ((((exists fs_h_ph_left_steps_before. fs_h_ph_left_steps_before + S (ff_previous_ph_left_steps) = S ((S (ff_i_ph_left_steps)) * v)) /\ exists fs_q_ph_left_steps_before. u = fs_q_ph_left_steps_before * S ((S (ff_i_ph_left_steps)) * v) + (ff_previous_ph_left_steps))) /\ ((((exists fs_h_ph_left_steps_after. fs_h_ph_left_steps_after + S (ff_current_ph_left_steps) = S ((S (S ff_i_ph_left_steps)) * v)) /\ exists fs_q_ph_left_steps_after. u = fs_q_ph_left_steps_after * S ((S (S ff_i_ph_left_steps)) * v) + (ff_current_ph_left_steps))) /\ ff_current_ph_left_steps = ff_previous_ph_left_steps * t + ff_coefficient_ph_left_steps)))))) -> (((((exists fs_h_ph_right_start. fs_h_ph_right_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_ph_right_start. w = fs_q_ph_right_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_ph_right_terminal. fs_h_ph_right_terminal + S (m) = S ((S (l)) * d)) /\ exists fs_q_ph_right_terminal. w = fs_q_ph_right_terminal * S ((S (l)) * d) + (m))) /\ forall ff_i_ph_right_steps. (exists ph_bound_right_steps. ph_bound_right_steps + S ff_i_ph_right_steps = l) -> exists ff_coefficient_ph_right_steps ff_previous_ph_right_steps ff_current_ph_right_steps. ((((exists fs_h_ph_right_steps_coefficient. fs_h_ph_right_steps_coefficient + S (ff_coefficient_ph_right_steps) = S ((S (ff_i_ph_right_steps)) * c)) /\ exists fs_q_ph_right_steps_coefficient. b = fs_q_ph_right_steps_coefficient * S ((S (ff_i_ph_right_steps)) * c) + (ff_coefficient_ph_right_steps))) /\ ((((exists fs_h_ph_right_steps_before. fs_h_ph_right_steps_before + S (ff_previous_ph_right_steps) = S ((S (ff_i_ph_right_steps)) * d)) /\ exists fs_q_ph_right_steps_before. w = fs_q_ph_right_steps_before * S ((S (ff_i_ph_right_steps)) * d) + (ff_previous_ph_right_steps))) /\ ((((exists fs_h_ph_right_steps_after. fs_h_ph_right_steps_after + S (ff_current_ph_right_steps) = S ((S (S ff_i_ph_right_steps)) * d)) /\ exists fs_q_ph_right_steps_after. w = fs_q_ph_right_steps_after * S ((S (S ff_i_ph_right_steps)) * d) + (ff_current_ph_right_steps))) /\ ff_current_ph_right_steps = ff_previous_ph_right_steps * t + ff_coefficient_ph_right_steps)))))) -> n = m

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

160 script commands · 46 reading checkpoints · 11 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–12

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

  1. L4
    induction l
  2. L5
    intro n
  3. L6
    intro u
  4. L7
    intro v
  5. L8
    intro m
  6. L9
    intro w
  7. L10
    intro d
  8. L11
    intro h1
  9. L12
    intro h2
03Separate the logical casesL13–16

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

  1. L13
    cases h1
  2. L14
    cases h1_right
  3. L15
    cases h2
  4. L16
    cases h2_right
04Establish hnL17–25

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

  1. L17
    have hn : n = 0
  2. L18
    specialize beta_at_unique u
  3. L19
    specialize beta_at_unique v
  4. L20
    specialize beta_at_unique 0
  5. L21
    specialize beta_at_unique n
  6. L22
    specialize beta_at_unique 0
  7. L23
    apply beta_at_unique
  8. L24
    exact h1_right_left
  9. L25
    exact h1_left
05Establish hmL26–35

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

  1. L26
    have hm : m = 0
  2. L27
    specialize beta_at_unique w
  3. L28
    specialize beta_at_unique d
  4. L29
    specialize beta_at_unique 0
  5. L30
    specialize beta_at_unique m
  6. L31
    specialize beta_at_unique 0
  7. L32
    apply beta_at_unique
  8. L33
    exact h2_right_left
  9. L34
    exact h2_left
  10. L35
    trans 0
06Use earlier factsL36–36

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

  1. L36
    exact hn
07Calculate and transport equalitiesL37–37

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

  1. L37
    symm
08Use earlier factsL38–38

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

  1. L38
    exact hm
09Fix variables and assumptionsL39–46

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

  1. L39
    intro n
  2. L40
    intro u
  3. L41
    intro v
  4. L42
    intro m
  5. L43
    intro w
  6. L44
    intro d
  7. L45
    intro h1
  8. L46
    intro h2
10Separate the logical casesL47–50

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

  1. L47
    cases h1
  2. L48
    cases h1_right
  3. L49
    cases h2
  4. L50
    cases h2_right
11Establish hstep1L51–55

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

  1. L51
    have hstep1 : ∃ a. ∃ r. ∃ s. Beta(b,c,l,a) ∧ (Beta(u,v,l,r) ∧ (Beta(u,v,S l,s) ∧ s = r · t + a))Definitions: BetaOriginal native command in the exact edition
  2. L52
    specialize h1_right_right l
  3. L53
    apply h1_right_right
  4. L54
    specialize le_refl (S l)
  5. L55
    exact le_refl
12Separate the logical casesL56–61

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

  1. L56
    cases hstep1
  2. L57
    cases hstep1_witness
  3. L58
    cases hstep1_witness_witness
  4. L59
    cases hstep1_witness_witness_witness
  5. L60
    cases hstep1_witness_witness_witness_right
  6. L61
    cases hstep1_witness_witness_witness_right_right
13Establish hstep2L62–66

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

  1. L62
    have hstep2 : ∃ a. ∃ r. ∃ s. Beta(b,c,l,a) ∧ (Beta(w,d,l,r) ∧ (Beta(w,d,S l,s) ∧ s = r · t + a))Definitions: BetaOriginal native command in the exact edition
  2. L63
    specialize h2_right_right l
  3. L64
    apply h2_right_right
  4. L65
    specialize le_refl (S l)
  5. L66
    exact le_refl
14Separate the logical casesL67–72

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

  1. L67
    cases hstep2
  2. L68
    cases hstep2_witness
  3. L69
    cases hstep2_witness_witness
  4. L70
    cases hstep2_witness_witness_witness
  5. L71
    cases hstep2_witness_witness_witness_right
  6. L72
    cases hstep2_witness_witness_witness_right_right
15Establish hnL73–81

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

  1. L73
    have hn : n = x2
  2. L74
    specialize beta_at_unique u
  3. L75
    specialize beta_at_unique v
  4. L76
    specialize beta_at_unique (S l)
  5. L77
    specialize beta_at_unique n
  6. L78
    specialize beta_at_unique x2
  7. L79
    apply beta_at_unique
  8. L80
    exact h1_right_left
  9. L81
    exact hstep1_witness_witness_witness_right_right_left
16Establish hmL82–90

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

  1. L82
    have hm : m = x5
  2. L83
    specialize beta_at_unique w
  3. L84
    specialize beta_at_unique d
  4. L85
    specialize beta_at_unique (S l)
  5. L86
    specialize beta_at_unique m
  6. L87
    specialize beta_at_unique x5
  7. L88
    apply beta_at_unique
  8. L89
    exact h2_right_left
  9. L90
    exact hstep2_witness_witness_witness_right_right_left
17Establish haL91–99

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

  1. L91
    have ha : x = x3
  2. L92
    specialize beta_at_unique b
  3. L93
    specialize beta_at_unique c
  4. L94
    specialize beta_at_unique l
  5. L95
    specialize beta_at_unique x
  6. L96
    specialize beta_at_unique x3
  7. L97
    apply beta_at_unique
  8. L98
    exact hstep1_witness_witness_witness_left
  9. L99
    exact hstep2_witness_witness_witness_left
18Establish hsum1L100–100

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

  1. L100
    have hsum1 : Beta(u,v,0,0) ∧ (Beta(u,v,l,x1) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. Beta(b,c,x,y) ∧ (Beta(u,v,x,z) ∧ (Beta(u,v,S x,n) ∧ n = z · t + y))))Definitions: BetaLtOriginal native command in the exact edition
19Separate the logical casesL101–101

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

  1. L101
    split
20Use earlier factsL102–102

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

  1. L102
    exact h1_left
21Separate the logical casesL103–103

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

  1. L103
    split
22Use earlier factsL104–104

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

  1. L104
    exact hstep1_witness_witness_witness_right_left
23Fix variables and assumptionsL105–106

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

  1. L105
    intro i
  2. L106
    intro hi
24Use earlier factsL107–112

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

  1. L107
    specialize h1_right_right i
  2. L108
    apply h1_right_right
  3. L109
    specialize le_succ (S i)
  4. L110
    specialize le_succ l
  5. L111
    apply le_succ
  6. L112
    exact hi
25Establish hsum2L113–113

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

  1. L113
    have hsum2 : Beta(w,d,0,0) ∧ (Beta(w,d,l,x4) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. Beta(b,c,x,y) ∧ (Beta(w,d,x,z) ∧ (Beta(w,d,S x,n) ∧ n = z · t + y))))Definitions: BetaLtOriginal native command in the exact edition
26Separate the logical casesL114–114

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

  1. L114
    split
27Use earlier factsL115–115

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

  1. L115
    exact h2_left
28Separate the logical casesL116–116

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

  1. L116
    split
29Use earlier factsL117–117

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

  1. L117
    exact hstep2_witness_witness_witness_right_left
30Fix variables and assumptionsL118–119

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

  1. L118
    intro i
  2. L119
    intro hi
31Use earlier factsL120–125

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

  1. L120
    specialize h2_right_right i
  2. L121
    apply h2_right_right
  3. L122
    specialize le_succ (S i)
  4. L123
    specialize le_succ l
  5. L124
    apply le_succ
  6. L125
    exact hi
32Establish hprevL126–135

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

  1. L126
    have hprev : x1 = x4
  2. L127
    specialize IH x1
  3. L128
    specialize IH u
  4. L129
    specialize IH v
  5. L130
    specialize IH x4
  6. L131
    specialize IH w
  7. L132
    specialize IH d
  8. L133
    apply IH
  9. L134
    exact hsum1
  10. L135
    exact hsum2
33Establish haddL136–145

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

  1. L136
    have hadd : x1 * t + x = x4 * t + x3
  2. L137
    specialize add_congr (x1 * t)
  3. L138
    specialize add_congr (x4 * t)
  4. L139
    specialize add_congr x
  5. L140
    specialize add_congr x3
  6. L141
    apply add_congr
  7. L142
    specialize mul_congr x1
  8. L143
    specialize mul_congr x4
  9. L144
    specialize mul_congr t
  10. L145
    specialize mul_congr t
34Use earlier factsL146–147

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

  1. L146
    apply mul_congr
  2. L147
    exact hprev
35Calculate and transport equalitiesL148–148

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

  1. L148
    refl
36Use earlier factsL149–149

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

  1. L149
    exact ha
37Calculate and transport equalitiesL150–150

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

  1. L150
    trans x2
38Use earlier factsL151–151

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

  1. L151
    exact hn
39Calculate and transport equalitiesL152–152

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

  1. L152
    trans x1 * t + x
40Use earlier factsL153–153

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

  1. L153
    exact hstep1_witness_witness_witness_right_right_right
41Calculate and transport equalitiesL154–154

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

  1. L154
    trans x4 * t + x3
42Use earlier factsL155–155

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

  1. L155
    exact hadd
43Calculate and transport equalitiesL156–157

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

  1. L156
    trans x5
  2. L157
    symm
44Use earlier factsL158–158

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

  1. L158
    exact hstep2_witness_witness_witness_right_right_right
45Calculate and transport equalitiesL159–159

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

  1. L159
    symm
46Use earlier factsL160–160

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

  1. L160
    exact hm

Library-wide reading audit

Original defined command ledger · 160 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004induction l
  5. 0005intro n
  6. 0006intro u
  7. 0007intro v
  8. 0008intro m
  9. 0009intro w
  10. 0010intro d
  11. 0011intro h1
  12. 0012intro h2
  13. 0013cases h1
  14. 0014cases h1_right
  15. 0015cases h2
  16. 0016cases h2_right
  17. 0017have hn : n = 0
  18. 0018specialize beta_at_unique u
  19. 0019specialize beta_at_unique v
  20. 0020specialize beta_at_unique 0
  21. 0021specialize beta_at_unique n
  22. 0022specialize beta_at_unique 0
  23. 0023apply beta_at_unique
  24. 0024exact h1_right_left
  25. 0025exact h1_left
  26. 0026have hm : m = 0
  27. 0027specialize beta_at_unique w
  28. 0028specialize beta_at_unique d
  29. 0029specialize beta_at_unique 0
  30. 0030specialize beta_at_unique m
  31. 0031specialize beta_at_unique 0
  32. 0032apply beta_at_unique
  33. 0033exact h2_right_left
  34. 0034exact h2_left
  35. 0035trans 0
  36. 0036exact hn
  37. 0037symm
  38. 0038exact hm
  39. 0039intro n
  40. 0040intro u
  41. 0041intro v
  42. 0042intro m
  43. 0043intro w
  44. 0044intro d
  45. 0045intro h1
  46. 0046intro h2
  47. 0047cases h1
  48. 0048cases h1_right
  49. 0049cases h2
  50. 0050cases h2_right
  51. 0051have hstep1 : exists a r s. ((((exists fs_h_functional_step1_factor. fs_h_functional_step1_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_functional_step1_factor. b = fs_q_functional_step1_factor * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_functional_step1_partial. fs_h_functional_step1_partial + S (r) = S ((S (l)) * v)) /\ exists fs_q_functional_step1_partial. u = fs_q_functional_step1_partial * S ((S (l)) * v) + (r))) /\ ((((exists fs_h_functional_step1_successor. fs_h_functional_step1_successor + S (s) = S ((S (S l)) * v)) /\ exists fs_q_functional_step1_successor. u = fs_q_functional_step1_successor * S ((S (S l)) * v) + (s))) /\ s = r * t + a)))
  52. 0052specialize h1_right_right l
  53. 0053apply h1_right_right
  54. 0054specialize le_refl (S l)
  55. 0055exact le_refl
  56. 0056cases hstep1
  57. 0057cases hstep1_witness
  58. 0058cases hstep1_witness_witness
  59. 0059cases hstep1_witness_witness_witness
  60. 0060cases hstep1_witness_witness_witness_right
  61. 0061cases hstep1_witness_witness_witness_right_right
  62. 0062have hstep2 : exists a r s. ((((exists fs_h_functional_step2_factor. fs_h_functional_step2_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_functional_step2_factor. b = fs_q_functional_step2_factor * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_functional_step2_partial. fs_h_functional_step2_partial + S (r) = S ((S (l)) * d)) /\ exists fs_q_functional_step2_partial. w = fs_q_functional_step2_partial * S ((S (l)) * d) + (r))) /\ ((((exists fs_h_functional_step2_successor. fs_h_functional_step2_successor + S (s) = S ((S (S l)) * d)) /\ exists fs_q_functional_step2_successor. w = fs_q_functional_step2_successor * S ((S (S l)) * d) + (s))) /\ s = r * t + a)))
  63. 0063specialize h2_right_right l
  64. 0064apply h2_right_right
  65. 0065specialize le_refl (S l)
  66. 0066exact le_refl
  67. 0067cases hstep2
  68. 0068cases hstep2_witness
  69. 0069cases hstep2_witness_witness
  70. 0070cases hstep2_witness_witness_witness
  71. 0071cases hstep2_witness_witness_witness_right
  72. 0072cases hstep2_witness_witness_witness_right_right
  73. 0073have hn : n = x2
  74. 0074specialize beta_at_unique u
  75. 0075specialize beta_at_unique v
  76. 0076specialize beta_at_unique (S l)
  77. 0077specialize beta_at_unique n
  78. 0078specialize beta_at_unique x2
  79. 0079apply beta_at_unique
  80. 0080exact h1_right_left
  81. 0081exact hstep1_witness_witness_witness_right_right_left
  82. 0082have hm : m = x5
  83. 0083specialize beta_at_unique w
  84. 0084specialize beta_at_unique d
  85. 0085specialize beta_at_unique (S l)
  86. 0086specialize beta_at_unique m
  87. 0087specialize beta_at_unique x5
  88. 0088apply beta_at_unique
  89. 0089exact h2_right_left
  90. 0090exact hstep2_witness_witness_witness_right_right_left
  91. 0091have ha : x = x3
  92. 0092specialize beta_at_unique b
  93. 0093specialize beta_at_unique c
  94. 0094specialize beta_at_unique l
  95. 0095specialize beta_at_unique x
  96. 0096specialize beta_at_unique x3
  97. 0097apply beta_at_unique
  98. 0098exact hstep1_witness_witness_witness_left
  99. 0099exact hstep2_witness_witness_witness_left
  100. 0100have hsum1 : ((((exists fs_h_ph_prefix_left_start. fs_h_ph_prefix_left_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_ph_prefix_left_start. u = fs_q_ph_prefix_left_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_ph_prefix_left_terminal. fs_h_ph_prefix_left_terminal + S (x1) = S ((S (l)) * v)) /\ exists fs_q_ph_prefix_left_terminal. u = fs_q_ph_prefix_left_terminal * S ((S (l)) * v) + (x1))) /\ forall ff_i_ph_prefix_left_steps. (exists ph_bound_prefix_left_steps. ph_bound_prefix_left_steps + S ff_i_ph_prefix_left_steps = l) -> exists ff_coefficient_ph_prefix_left_steps ff_previous_ph_prefix_left_steps ff_current_ph_prefix_left_steps. ((((exists fs_h_ph_prefix_left_steps_coefficient. fs_h_ph_prefix_left_steps_coefficient + S (ff_coefficient_ph_prefix_left_steps) = S ((S (ff_i_ph_prefix_left_steps)) * c)) /\ exists fs_q_ph_prefix_left_steps_coefficient. b = fs_q_ph_prefix_left_steps_coefficient * S ((S (ff_i_ph_prefix_left_steps)) * c) + (ff_coefficient_ph_prefix_left_steps))) /\ ((((exists fs_h_ph_prefix_left_steps_before. fs_h_ph_prefix_left_steps_before + S (ff_previous_ph_prefix_left_steps) = S ((S (ff_i_ph_prefix_left_steps)) * v)) /\ exists fs_q_ph_prefix_left_steps_before. u = fs_q_ph_prefix_left_steps_before * S ((S (ff_i_ph_prefix_left_steps)) * v) + (ff_previous_ph_prefix_left_steps))) /\ ((((exists fs_h_ph_prefix_left_steps_after. fs_h_ph_prefix_left_steps_after + S (ff_current_ph_prefix_left_steps) = S ((S (S ff_i_ph_prefix_left_steps)) * v)) /\ exists fs_q_ph_prefix_left_steps_after. u = fs_q_ph_prefix_left_steps_after * S ((S (S ff_i_ph_prefix_left_steps)) * v) + (ff_current_ph_prefix_left_steps))) /\ ff_current_ph_prefix_left_steps = ff_previous_ph_prefix_left_steps * t + ff_coefficient_ph_prefix_left_steps)))))
  101. 0101split
  102. 0102exact h1_left
  103. 0103split
  104. 0104exact hstep1_witness_witness_witness_right_left
  105. 0105intro i
  106. 0106intro hi
  107. 0107specialize h1_right_right i
  108. 0108apply h1_right_right
  109. 0109specialize le_succ (S i)
  110. 0110specialize le_succ l
  111. 0111apply le_succ
  112. 0112exact hi
  113. 0113have hsum2 : ((((exists fs_h_ph_prefix_right_start. fs_h_ph_prefix_right_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_ph_prefix_right_start. w = fs_q_ph_prefix_right_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_ph_prefix_right_terminal. fs_h_ph_prefix_right_terminal + S (x4) = S ((S (l)) * d)) /\ exists fs_q_ph_prefix_right_terminal. w = fs_q_ph_prefix_right_terminal * S ((S (l)) * d) + (x4))) /\ forall ff_i_ph_prefix_right_steps. (exists ph_bound_prefix_right_steps. ph_bound_prefix_right_steps + S ff_i_ph_prefix_right_steps = l) -> exists ff_coefficient_ph_prefix_right_steps ff_previous_ph_prefix_right_steps ff_current_ph_prefix_right_steps. ((((exists fs_h_ph_prefix_right_steps_coefficient. fs_h_ph_prefix_right_steps_coefficient + S (ff_coefficient_ph_prefix_right_steps) = S ((S (ff_i_ph_prefix_right_steps)) * c)) /\ exists fs_q_ph_prefix_right_steps_coefficient. b = fs_q_ph_prefix_right_steps_coefficient * S ((S (ff_i_ph_prefix_right_steps)) * c) + (ff_coefficient_ph_prefix_right_steps))) /\ ((((exists fs_h_ph_prefix_right_steps_before. fs_h_ph_prefix_right_steps_before + S (ff_previous_ph_prefix_right_steps) = S ((S (ff_i_ph_prefix_right_steps)) * d)) /\ exists fs_q_ph_prefix_right_steps_before. w = fs_q_ph_prefix_right_steps_before * S ((S (ff_i_ph_prefix_right_steps)) * d) + (ff_previous_ph_prefix_right_steps))) /\ ((((exists fs_h_ph_prefix_right_steps_after. fs_h_ph_prefix_right_steps_after + S (ff_current_ph_prefix_right_steps) = S ((S (S ff_i_ph_prefix_right_steps)) * d)) /\ exists fs_q_ph_prefix_right_steps_after. w = fs_q_ph_prefix_right_steps_after * S ((S (S ff_i_ph_prefix_right_steps)) * d) + (ff_current_ph_prefix_right_steps))) /\ ff_current_ph_prefix_right_steps = ff_previous_ph_prefix_right_steps * t + ff_coefficient_ph_prefix_right_steps)))))
  114. 0114split
  115. 0115exact h2_left
  116. 0116split
  117. 0117exact hstep2_witness_witness_witness_right_left
  118. 0118intro i
  119. 0119intro hi
  120. 0120specialize h2_right_right i
  121. 0121apply h2_right_right
  122. 0122specialize le_succ (S i)
  123. 0123specialize le_succ l
  124. 0124apply le_succ
  125. 0125exact hi
  126. 0126have hprev : x1 = x4
  127. 0127specialize IH x1
  128. 0128specialize IH u
  129. 0129specialize IH v
  130. 0130specialize IH x4
  131. 0131specialize IH w
  132. 0132specialize IH d
  133. 0133apply IH
  134. 0134exact hsum1
  135. 0135exact hsum2
  136. 0136have hadd : x1 * t + x = x4 * t + x3
  137. 0137specialize add_congr (x1 * t)
  138. 0138specialize add_congr (x4 * t)
  139. 0139specialize add_congr x
  140. 0140specialize add_congr x3
  141. 0141apply add_congr
  142. 0142specialize mul_congr x1
  143. 0143specialize mul_congr x4
  144. 0144specialize mul_congr t
  145. 0145specialize mul_congr t
  146. 0146apply mul_congr
  147. 0147exact hprev
  148. 0148refl
  149. 0149exact ha
  150. 0150trans x2
  151. 0151exact hn
  152. 0152trans x1 * t + x
  153. 0153exact hstep1_witness_witness_witness_right_right_right
  154. 0154trans x4 * t + x3
  155. 0155exact hadd
  156. 0156trans x5
  157. 0157symm
  158. 0158exact hstep2_witness_witness_witness_right_right_right
  159. 0159symm
  160. 0160exact hm