BT0089 · Bertrand theorem

beta_prefix_sum_trace_exists

Stable checked-use theorem · independently kernel verified

Every decoded beta prefix admits an exact beta-coded prefix-sum trace.

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.

Statement with defined notation

∀ b. ∀ c. ∀ l. ∃ fs_u_trace. ∃ fs_v_trace. BetaAt(fs_u_trace,fs_v_trace,0,0) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(fs_u_trace,fs_v_trace,x,z) ∧ (BetaAt(fs_u_trace,fs_v_trace,S x,n) ∧ n = z + y)))

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

5 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

18 occurrences

Exact expanded native-PA statement
forall b c l. exists fs_u_trace fs_v_trace. ((((exists fs_h_trace_start. fs_h_trace_start + S (0) = S ((S (0)) * fs_v_trace)) /\ exists fs_q_trace_start. fs_u_trace = fs_q_trace_start * S ((S (0)) * fs_v_trace) + (0))) /\ forall fs_i_trace_steps. (exists fs_lt_trace_steps_bound. fs_lt_trace_steps_bound + S fs_i_trace_steps = l) -> exists fs_a_trace_steps fs_r_trace_steps fs_s_trace_steps. ((((exists fs_h_trace_steps_summand. fs_h_trace_steps_summand + S (fs_a_trace_steps) = S ((S (fs_i_trace_steps)) * c)) /\ exists fs_q_trace_steps_summand. b = fs_q_trace_steps_summand * S ((S (fs_i_trace_steps)) * c) + (fs_a_trace_steps))) /\ ((((exists fs_h_trace_steps_partial. fs_h_trace_steps_partial + S (fs_r_trace_steps) = S ((S (fs_i_trace_steps)) * fs_v_trace)) /\ exists fs_q_trace_steps_partial. fs_u_trace = fs_q_trace_steps_partial * S ((S (fs_i_trace_steps)) * fs_v_trace) + (fs_r_trace_steps))) /\ ((((exists fs_h_trace_steps_successor. fs_h_trace_steps_successor + S (fs_s_trace_steps) = S ((S (S fs_i_trace_steps)) * fs_v_trace)) /\ exists fs_q_trace_steps_successor. fs_u_trace = fs_q_trace_steps_successor * S ((S (S fs_i_trace_steps)) * fs_v_trace) + (fs_s_trace_steps))) /\ fs_s_trace_steps = fs_r_trace_steps + fs_a_trace_steps))))

Proof neighborhood

Direct theorem prerequisites

BT0040 beta_at_self_of_bound BT000L add_eq_zero_right BT000C succ_ne_zero BT0041 beta_at_exists BT005D beta_prefix_extend BT000W zero_le BT0016 succ_le_succ BT000E le_refl BT0017 le_of_succ_le_succ BT001C le_eq_or_lt BT0009 one_mul

Direct theorem dependents

BT008A beta_sum_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

136 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.

Named ingredients (11)
beta at self of boundadd eq zero rightsucc ne zerobeta at existsbeta prefix extendzero lesucc le succle reflle of succ le succle eq or ltone mul
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–3

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

  1. L3
    induction l
03Construct an explicit witnessL4–5

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

  1. L4
    exists 0
  2. L5
    exists 1
04Separate the logical casesL6–6

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

  1. L6
    split
05Use earlier factsL7–11

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

  1. L7
    specialize beta_at_self_of_bound 1
  2. L8
    specialize beta_at_self_of_bound 0
  3. L9
    specialize beta_at_self_of_bound 0
  4. L10
    apply beta_at_self_of_bound
  5. L11
    specialize one_mul 1
06Calculate and transport equalitiesL12–12

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

  1. L12
    rewrite one_mul
07Use earlier factsL13–17

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

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

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

  1. L18
    intro i
  2. L19
    intro hi
09Separate the logical casesL20–21

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

  1. L20
    exfalso
  2. L21
    cases hi
10Establish hsi0L22–29

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

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

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

  1. L30
    have htrace : ∃ fs_u_induction. ∃ fs_v_induction. BetaAt(fs_u_induction,fs_v_induction,0,0) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(fs_u_induction,fs_v_induction,x,z) ∧ (BetaAt(fs_u_induction,fs_v_induction,S x,n) ∧ n = z + y)))Definitions: BetaAt(fs_u_induction,fs_v_induction,0,0)Lt(x,l)BetaAt(b,c,x,y)BetaAt(fs_u_induction,fs_v_induction,x,z)BetaAt(fs_u_induction,fs_v_induction,S x,n)Original native command in the exact edition
  2. L31
    apply IH
12Separate the logical casesL32–34

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

  1. L32
    cases htrace
  2. L33
    cases htrace_witness
  3. L34
    cases htrace_witness_witness
13Establish hfactorL35–39

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

  1. L35
    have hfactor : ∃ p. BetaAt(b,c,l,p)Definitions: BetaAt(b,c,l,p)Original native command in the exact edition
  2. L36
    specialize beta_at_exists b
  3. L37
    specialize beta_at_exists c
  4. L38
    specialize beta_at_exists l
  5. L39
    exact beta_at_exists
14Separate the logical casesL40–40

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

  1. L40
    cases hfactor
15Establish hlastL41–45

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

  1. L41
    have hlast : ∃ r. BetaAt(x,x1,l,r)Definitions: BetaAt(x,x1,l,r)Original native command in the exact edition
  2. L42
    specialize beta_at_exists x
  3. L43
    specialize beta_at_exists x1
  4. L44
    specialize beta_at_exists l
  5. L45
    exact beta_at_exists
16Separate the logical casesL46–46

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

  1. L46
    cases hlast
17Establish hextL47–52

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

  1. L47
    have hext : ∃ z. ∃ v. BetaAt(z,v,S l,x3 + x2) ∧ (∀ y. ∀ n. Lt(y,S l) → BetaAt(x,x1,y,n) → BetaAt(z,v,y,n))Definitions: BetaAt(z,v,S l,x3 + x2)Lt(y,S l)BetaAt(x,x1,y,n)BetaAt(z,v,y,n)Original native command in the exact edition
  2. L48
    specialize beta_prefix_extend (S l)
  3. L49
    specialize beta_prefix_extend x
  4. L50
    specialize beta_prefix_extend x1
  5. L51
    specialize beta_prefix_extend (x3 + x2)
  6. L52
    exact beta_prefix_extend
18Separate the logical casesL53–55

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

  1. L53
    cases hext
  2. L54
    cases hext_witness
  3. L55
    cases hext_witness_witness
19Construct an explicit witnessL56–57

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

  1. L56
    exists x4
  2. L57
    exists x5
20Separate the logical casesL58–58

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

  1. L58
    split
21Use earlier factsL59–61

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

  1. L59
    specialize hext_witness_witness_right 0
  2. L60
    specialize hext_witness_witness_right 0
  3. L61
    apply hext_witness_witness_right
22Establish h0L62–62

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

  1. L62
23Establish hzeroL63–72

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

  1. L63
  2. L64
    specialize zero_le l
  3. L65
    exact zero_le
  4. L66
    specialize succ_le_succ 0
  5. L67
    specialize succ_le_succ l
  6. L68
    apply succ_le_succ
  7. L69
    exact hzero
  8. L70
    exact h0
  9. L71
    exact htrace_witness_witness_left
  10. L72
    intro i
24Fix variables and assumptionsL73–73

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

  1. L73
    intro hi
25Establish hilL74–78

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

  1. L74
  2. L75
    specialize le_of_succ_le_succ i
  3. L76
    specialize le_of_succ_le_succ l
  4. L77
    apply le_of_succ_le_succ
  5. L78
    exact hi
26Establish hsplitL79–83

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

  1. L79
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L80
    specialize le_eq_or_lt i
  3. L81
    specialize le_eq_or_lt l
  4. L82
    apply le_eq_or_lt
  5. L83
    exact hil
27Separate the logical casesL84–84

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

  1. L84
    cases hsplit
28Construct an explicit witnessL85–87

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

  1. L85
    exists x2
  2. L86
    exists x3
  3. L87
    exists x3 + x2
29Separate the logical casesL88–88

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

  1. L88
    split
30Calculate and transport equalitiesL89–90

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

  1. L89
    rewrite hsplit_left
  2. L90
    rewrite hsplit_left
31Use earlier factsL91–91

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

  1. L91
    exact hfactor_witness
32Separate the logical casesL92–92

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

  1. L92
    split
33Calculate and transport equalitiesL93–94

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

  1. L93
    rewrite hsplit_left
  2. L94
    rewrite hsplit_left
34Use earlier factsL95–100

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

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

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

  1. L101
    split
36Calculate and transport equalitiesL102–103

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

  1. L102
    rewrite hsplit_left
  2. L103
    rewrite hsplit_left
37Use earlier factsL104–104

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

  1. L104
    exact hext_witness_witness_left
38Calculate and transport equalitiesL105–105

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

  1. L105
    refl
39Establish holdL106–109

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

  1. L106
    have hold : ∃ p. ∃ r. ∃ s. BetaAt(b,c,i,p) ∧ (BetaAt(x,x1,i,r) ∧ (BetaAt(x,x1,S i,s) ∧ s = r + p))Definitions: BetaAt(b,c,i,p)BetaAt(x,x1,i,r)BetaAt(x,x1,S i,s)Original native command in the exact edition
  2. L107
    specialize htrace_witness_witness_right i
  3. L108
    apply htrace_witness_witness_right
  4. L109
    exact hsplit_right
40Separate the logical casesL110–115

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

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

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

  1. L116
    exists x6
  2. L117
    exists x7
  3. L118
    exists x8
42Separate the logical casesL119–119

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

  1. L119
    split
43Use earlier factsL120–120

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

  1. L120
    exact hold_witness_witness_witness_left
44Separate the logical casesL121–121

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

  1. L121
    split
45Use earlier factsL122–126

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

  1. L122
    specialize hext_witness_witness_right i
  2. L123
    specialize hext_witness_witness_right x7
  3. L124
    apply hext_witness_witness_right
  4. L125
    exact hi
  5. L126
    exact hold_witness_witness_witness_right_left
46Separate the logical casesL127–127

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

  1. L127
    split
47Use earlier factsL128–136

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

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

Library-wide reading audit

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