BT008B · Bertrand theorem

beta_sum_trace_functional

Stable checked-use theorem · independently kernel verified

Two exact prefix-sum traces over one decoded prefix have equal endpoints.

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

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

12 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

18 occurrences

Exact expanded native-PA statement
forall b c l n u v m w d. (((((exists fs_h_functional_left_start. fs_h_functional_left_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_functional_left_start. u = fs_q_functional_left_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_functional_left_terminal. fs_h_functional_left_terminal + S (n) = S ((S (l)) * v)) /\ exists fs_q_functional_left_terminal. u = fs_q_functional_left_terminal * S ((S (l)) * v) + (n))) /\ forall fs_i_functional_left_steps. (exists fs_lt_functional_left_steps_bound. fs_lt_functional_left_steps_bound + S fs_i_functional_left_steps = l) -> exists fs_a_functional_left_steps fs_r_functional_left_steps fs_s_functional_left_steps. ((((exists fs_h_functional_left_steps_summand. fs_h_functional_left_steps_summand + S (fs_a_functional_left_steps) = S ((S (fs_i_functional_left_steps)) * c)) /\ exists fs_q_functional_left_steps_summand. b = fs_q_functional_left_steps_summand * S ((S (fs_i_functional_left_steps)) * c) + (fs_a_functional_left_steps))) /\ ((((exists fs_h_functional_left_steps_partial. fs_h_functional_left_steps_partial + S (fs_r_functional_left_steps) = S ((S (fs_i_functional_left_steps)) * v)) /\ exists fs_q_functional_left_steps_partial. u = fs_q_functional_left_steps_partial * S ((S (fs_i_functional_left_steps)) * v) + (fs_r_functional_left_steps))) /\ ((((exists fs_h_functional_left_steps_successor. fs_h_functional_left_steps_successor + S (fs_s_functional_left_steps) = S ((S (S fs_i_functional_left_steps)) * v)) /\ exists fs_q_functional_left_steps_successor. u = fs_q_functional_left_steps_successor * S ((S (S fs_i_functional_left_steps)) * v) + (fs_s_functional_left_steps))) /\ fs_s_functional_left_steps = fs_r_functional_left_steps + fs_a_functional_left_steps)))))) -> (((((exists fs_h_functional_right_start. fs_h_functional_right_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_functional_right_start. w = fs_q_functional_right_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_functional_right_terminal. fs_h_functional_right_terminal + S (m) = S ((S (l)) * d)) /\ exists fs_q_functional_right_terminal. w = fs_q_functional_right_terminal * S ((S (l)) * d) + (m))) /\ forall fs_i_functional_right_steps. (exists fs_lt_functional_right_steps_bound. fs_lt_functional_right_steps_bound + S fs_i_functional_right_steps = l) -> exists fs_a_functional_right_steps fs_r_functional_right_steps fs_s_functional_right_steps. ((((exists fs_h_functional_right_steps_summand. fs_h_functional_right_steps_summand + S (fs_a_functional_right_steps) = S ((S (fs_i_functional_right_steps)) * c)) /\ exists fs_q_functional_right_steps_summand. b = fs_q_functional_right_steps_summand * S ((S (fs_i_functional_right_steps)) * c) + (fs_a_functional_right_steps))) /\ ((((exists fs_h_functional_right_steps_partial. fs_h_functional_right_steps_partial + S (fs_r_functional_right_steps) = S ((S (fs_i_functional_right_steps)) * d)) /\ exists fs_q_functional_right_steps_partial. w = fs_q_functional_right_steps_partial * S ((S (fs_i_functional_right_steps)) * d) + (fs_r_functional_right_steps))) /\ ((((exists fs_h_functional_right_steps_successor. fs_h_functional_right_steps_successor + S (fs_s_functional_right_steps) = S ((S (S fs_i_functional_right_steps)) * d)) /\ exists fs_q_functional_right_steps_successor. w = fs_q_functional_right_steps_successor * S ((S (S fs_i_functional_right_steps)) * d) + (fs_s_functional_right_steps))) /\ fs_s_functional_right_steps = fs_r_functional_right_steps + fs_a_functional_right_steps)))))) -> n = m

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique BT000E le_refl BT0018 le_succ BT000S add_congr

Direct theorem dependents

BT008C beta_sum_functional

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

153 script commands · 41 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.

Named ingredients (4)
beta at uniquele reflle succadd congr
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–11

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

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

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

  1. L12
    cases h1
  2. L13
    cases h1_right
  3. L14
    cases h2
  4. L15
    cases h2_right
04Establish hnL16–24

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

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

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

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

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

  1. L35
    exact hn
07Calculate and transport equalitiesL36–36

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

  1. L36
    symm
08Use earlier factsL37–37

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

  1. L37
    exact hm
09Fix variables and assumptionsL38–45

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

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

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

  1. L46
    cases h1
  2. L47
    cases h1_right
  3. L48
    cases h2
  4. L49
    cases h2_right
11Establish hstep1L50–54

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

  1. L50
    have hstep1 : ∃ a. ∃ r. ∃ s. BetaAt(b,c,l,a) ∧ (BetaAt(u,v,l,r) ∧ (BetaAt(u,v,S l,s) ∧ s = r + a))Definitions: BetaAt(b,c,l,a)BetaAt(u,v,l,r)BetaAt(u,v,S l,s)Original native command in the exact edition
  2. L51
    specialize h1_right_right l
  3. L52
    apply h1_right_right
  4. L53
    specialize le_refl (S l)
  5. L54
    exact le_refl
12Separate the logical casesL55–60

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

  1. L55
    cases hstep1
  2. L56
    cases hstep1_witness
  3. L57
    cases hstep1_witness_witness
  4. L58
    cases hstep1_witness_witness_witness
  5. L59
    cases hstep1_witness_witness_witness_right
  6. L60
    cases hstep1_witness_witness_witness_right_right
13Establish hstep2L61–65

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

  1. L61
    have hstep2 : ∃ a. ∃ r. ∃ s. BetaAt(b,c,l,a) ∧ (BetaAt(w,d,l,r) ∧ (BetaAt(w,d,S l,s) ∧ s = r + a))Definitions: BetaAt(b,c,l,a)BetaAt(w,d,l,r)BetaAt(w,d,S l,s)Original native command in the exact edition
  2. L62
    specialize h2_right_right l
  3. L63
    apply h2_right_right
  4. L64
    specialize le_refl (S l)
  5. L65
    exact le_refl
14Separate the logical casesL66–71

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

  1. L66
    cases hstep2
  2. L67
    cases hstep2_witness
  3. L68
    cases hstep2_witness_witness
  4. L69
    cases hstep2_witness_witness_witness
  5. L70
    cases hstep2_witness_witness_witness_right
  6. L71
    cases hstep2_witness_witness_witness_right_right
15Establish hnL72–80

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

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

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

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

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

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

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

  1. L99
    have hsum1 : BetaAt(u,v,0,0) ∧ (BetaAt(u,v,l,x1) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(u,v,x,z) ∧ (BetaAt(u,v,S x,n) ∧ n = z + y))))Definitions: BetaAt(u,v,0,0)BetaAt(u,v,l,x1)Lt(x,l)BetaAt(b,c,x,y)BetaAt(u,v,x,z)BetaAt(u,v,S x,n)Original native command in the exact edition
19Separate the logical casesL100–100

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

  1. L100
    split
20Use earlier factsL101–101

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

  1. L101
    exact h1_left
21Separate the logical casesL102–102

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

  1. L102
    split
22Use earlier factsL103–103

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

  1. L103
    exact hstep1_witness_witness_witness_right_left
23Fix variables and assumptionsL104–105

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

  1. L104
    intro i
  2. L105
    intro hi
24Use earlier factsL106–111

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

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

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

  1. L112
    have hsum2 : BetaAt(w,d,0,0) ∧ (BetaAt(w,d,l,x4) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(w,d,x,z) ∧ (BetaAt(w,d,S x,n) ∧ n = z + y))))Definitions: BetaAt(w,d,0,0)BetaAt(w,d,l,x4)Lt(x,l)BetaAt(b,c,x,y)BetaAt(w,d,x,z)BetaAt(w,d,S x,n)Original native command in the exact edition
26Separate the logical casesL113–113

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

  1. L113
    split
27Use earlier factsL114–114

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

  1. L114
    exact h2_left
28Separate the logical casesL115–115

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

  1. L115
    split
29Use earlier factsL116–116

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

  1. L116
    exact hstep2_witness_witness_witness_right_left
30Fix variables and assumptionsL117–118

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

  1. L117
    intro i
  2. L118
    intro hi
31Use earlier factsL119–124

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

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

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

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

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

  1. L135
    have hadd : x1 + x = x4 + x3
  2. L136
    specialize add_congr x1
  3. L137
    specialize add_congr x4
  4. L138
    specialize add_congr x
  5. L139
    specialize add_congr x3
  6. L140
    apply add_congr
  7. L141
    exact hprev
  8. L142
    exact ha
  9. L143
    trans x2
  10. L144
    exact hn
34Calculate and transport equalitiesL145–145

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

  1. L145
    trans x1 + x
35Use earlier factsL146–146

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

  1. L146
    exact hstep1_witness_witness_witness_right_right_right
36Calculate and transport equalitiesL147–147

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

  1. L147
    trans x4 + x3
37Use earlier factsL148–148

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

  1. L148
    exact hadd
38Calculate and transport equalitiesL149–150

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

  1. L149
    trans x5
  2. L150
    symm
39Use earlier factsL151–151

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

  1. L151
    exact hstep2_witness_witness_witness_right_right_right
40Calculate and transport equalitiesL152–152

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

  1. L152
    symm
41Use earlier factsL153–153

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

  1. L153
    exact hm

Library-wide reading audit

Original defined command ledger · 153 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro n
  5. 0005intro u
  6. 0006intro v
  7. 0007intro m
  8. 0008intro w
  9. 0009intro d
  10. 0010intro h1
  11. 0011intro h2
  12. 0012cases h1
  13. 0013cases h1_right
  14. 0014cases h2
  15. 0015cases h2_right
  16. 0016have hn : n = 0
  17. 0017specialize beta_at_unique u
  18. 0018specialize beta_at_unique v
  19. 0019specialize beta_at_unique 0
  20. 0020specialize beta_at_unique n
  21. 0021specialize beta_at_unique 0
  22. 0022apply beta_at_unique
  23. 0023exact h1_right_left
  24. 0024exact h1_left
  25. 0025have hm : m = 0
  26. 0026specialize beta_at_unique w
  27. 0027specialize beta_at_unique d
  28. 0028specialize beta_at_unique 0
  29. 0029specialize beta_at_unique m
  30. 0030specialize beta_at_unique 0
  31. 0031apply beta_at_unique
  32. 0032exact h2_right_left
  33. 0033exact h2_left
  34. 0034trans 0
  35. 0035exact hn
  36. 0036symm
  37. 0037exact hm
  38. 0038intro n
  39. 0039intro u
  40. 0040intro v
  41. 0041intro m
  42. 0042intro w
  43. 0043intro d
  44. 0044intro h1
  45. 0045intro h2
  46. 0046cases h1
  47. 0047cases h1_right
  48. 0048cases h2
  49. 0049cases h2_right
  50. 0050have hstep1 : ∃ a. ∃ r. ∃ s. BetaAt(b,c,l,a) ∧ (BetaAt(u,v,l,r) ∧ (BetaAt(u,v,S l,s) ∧ s = r + a))
    Exact native replay linehave 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 + a)))
  51. 0051specialize h1_right_right l
  52. 0052apply h1_right_right
  53. 0053specialize le_refl (S l)
  54. 0054exact le_refl
  55. 0055cases hstep1
  56. 0056cases hstep1_witness
  57. 0057cases hstep1_witness_witness
  58. 0058cases hstep1_witness_witness_witness
  59. 0059cases hstep1_witness_witness_witness_right
  60. 0060cases hstep1_witness_witness_witness_right_right
  61. 0061have hstep2 : ∃ a. ∃ r. ∃ s. BetaAt(b,c,l,a) ∧ (BetaAt(w,d,l,r) ∧ (BetaAt(w,d,S l,s) ∧ s = r + a))
    Exact native replay linehave 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 + a)))
  62. 0062specialize h2_right_right l
  63. 0063apply h2_right_right
  64. 0064specialize le_refl (S l)
  65. 0065exact le_refl
  66. 0066cases hstep2
  67. 0067cases hstep2_witness
  68. 0068cases hstep2_witness_witness
  69. 0069cases hstep2_witness_witness_witness
  70. 0070cases hstep2_witness_witness_witness_right
  71. 0071cases hstep2_witness_witness_witness_right_right
  72. 0072have hn : n = x2
  73. 0073specialize beta_at_unique u
  74. 0074specialize beta_at_unique v
  75. 0075specialize beta_at_unique (S l)
  76. 0076specialize beta_at_unique n
  77. 0077specialize beta_at_unique x2
  78. 0078apply beta_at_unique
  79. 0079exact h1_right_left
  80. 0080exact hstep1_witness_witness_witness_right_right_left
  81. 0081have hm : m = x5
  82. 0082specialize beta_at_unique w
  83. 0083specialize beta_at_unique d
  84. 0084specialize beta_at_unique (S l)
  85. 0085specialize beta_at_unique m
  86. 0086specialize beta_at_unique x5
  87. 0087apply beta_at_unique
  88. 0088exact h2_right_left
  89. 0089exact hstep2_witness_witness_witness_right_right_left
  90. 0090have ha : x = x3
  91. 0091specialize beta_at_unique b
  92. 0092specialize beta_at_unique c
  93. 0093specialize beta_at_unique l
  94. 0094specialize beta_at_unique x
  95. 0095specialize beta_at_unique x3
  96. 0096apply beta_at_unique
  97. 0097exact hstep1_witness_witness_witness_left
  98. 0098exact hstep2_witness_witness_witness_left
  99. 0099have hsum1 : BetaAt(u,v,0,0) ∧ (BetaAt(u,v,l,x1) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(u,v,x,z) ∧ (BetaAt(u,v,S x,n) ∧ n = z + y))))
    Exact native replay linehave hsum1 : ((((exists fs_h_functional_prefix1_start. fs_h_functional_prefix1_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_functional_prefix1_start. u = fs_q_functional_prefix1_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_functional_prefix1_terminal. fs_h_functional_prefix1_terminal + S (x1) = S ((S (l)) * v)) /\ exists fs_q_functional_prefix1_terminal. u = fs_q_functional_prefix1_terminal * S ((S (l)) * v) + (x1))) /\ forall fs_i_functional_prefix1_steps. (exists fs_lt_functional_prefix1_steps_bound. fs_lt_functional_prefix1_steps_bound + S fs_i_functional_prefix1_steps = l) -> exists fs_a_functional_prefix1_steps fs_r_functional_prefix1_steps fs_s_functional_prefix1_steps. ((((exists fs_h_functional_prefix1_steps_summand. fs_h_functional_prefix1_steps_summand + S (fs_a_functional_prefix1_steps) = S ((S (fs_i_functional_prefix1_steps)) * c)) /\ exists fs_q_functional_prefix1_steps_summand. b = fs_q_functional_prefix1_steps_summand * S ((S (fs_i_functional_prefix1_steps)) * c) + (fs_a_functional_prefix1_steps))) /\ ((((exists fs_h_functional_prefix1_steps_partial. fs_h_functional_prefix1_steps_partial + S (fs_r_functional_prefix1_steps) = S ((S (fs_i_functional_prefix1_steps)) * v)) /\ exists fs_q_functional_prefix1_steps_partial. u = fs_q_functional_prefix1_steps_partial * S ((S (fs_i_functional_prefix1_steps)) * v) + (fs_r_functional_prefix1_steps))) /\ ((((exists fs_h_functional_prefix1_steps_successor. fs_h_functional_prefix1_steps_successor + S (fs_s_functional_prefix1_steps) = S ((S (S fs_i_functional_prefix1_steps)) * v)) /\ exists fs_q_functional_prefix1_steps_successor. u = fs_q_functional_prefix1_steps_successor * S ((S (S fs_i_functional_prefix1_steps)) * v) + (fs_s_functional_prefix1_steps))) /\ fs_s_functional_prefix1_steps = fs_r_functional_prefix1_steps + fs_a_functional_prefix1_steps)))))
  100. 0100split
  101. 0101exact h1_left
  102. 0102split
  103. 0103exact hstep1_witness_witness_witness_right_left
  104. 0104intro i
  105. 0105intro hi
  106. 0106specialize h1_right_right i
  107. 0107apply h1_right_right
  108. 0108specialize le_succ (S i)
  109. 0109specialize le_succ l
  110. 0110apply le_succ
  111. 0111exact hi
  112. 0112have hsum2 : BetaAt(w,d,0,0) ∧ (BetaAt(w,d,l,x4) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(w,d,x,z) ∧ (BetaAt(w,d,S x,n) ∧ n = z + y))))
    Exact native replay linehave hsum2 : ((((exists fs_h_functional_prefix2_start. fs_h_functional_prefix2_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_functional_prefix2_start. w = fs_q_functional_prefix2_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_functional_prefix2_terminal. fs_h_functional_prefix2_terminal + S (x4) = S ((S (l)) * d)) /\ exists fs_q_functional_prefix2_terminal. w = fs_q_functional_prefix2_terminal * S ((S (l)) * d) + (x4))) /\ forall fs_i_functional_prefix2_steps. (exists fs_lt_functional_prefix2_steps_bound. fs_lt_functional_prefix2_steps_bound + S fs_i_functional_prefix2_steps = l) -> exists fs_a_functional_prefix2_steps fs_r_functional_prefix2_steps fs_s_functional_prefix2_steps. ((((exists fs_h_functional_prefix2_steps_summand. fs_h_functional_prefix2_steps_summand + S (fs_a_functional_prefix2_steps) = S ((S (fs_i_functional_prefix2_steps)) * c)) /\ exists fs_q_functional_prefix2_steps_summand. b = fs_q_functional_prefix2_steps_summand * S ((S (fs_i_functional_prefix2_steps)) * c) + (fs_a_functional_prefix2_steps))) /\ ((((exists fs_h_functional_prefix2_steps_partial. fs_h_functional_prefix2_steps_partial + S (fs_r_functional_prefix2_steps) = S ((S (fs_i_functional_prefix2_steps)) * d)) /\ exists fs_q_functional_prefix2_steps_partial. w = fs_q_functional_prefix2_steps_partial * S ((S (fs_i_functional_prefix2_steps)) * d) + (fs_r_functional_prefix2_steps))) /\ ((((exists fs_h_functional_prefix2_steps_successor. fs_h_functional_prefix2_steps_successor + S (fs_s_functional_prefix2_steps) = S ((S (S fs_i_functional_prefix2_steps)) * d)) /\ exists fs_q_functional_prefix2_steps_successor. w = fs_q_functional_prefix2_steps_successor * S ((S (S fs_i_functional_prefix2_steps)) * d) + (fs_s_functional_prefix2_steps))) /\ fs_s_functional_prefix2_steps = fs_r_functional_prefix2_steps + fs_a_functional_prefix2_steps)))))
  113. 0113split
  114. 0114exact h2_left
  115. 0115split
  116. 0116exact hstep2_witness_witness_witness_right_left
  117. 0117intro i
  118. 0118intro hi
  119. 0119specialize h2_right_right i
  120. 0120apply h2_right_right
  121. 0121specialize le_succ (S i)
  122. 0122specialize le_succ l
  123. 0123apply le_succ
  124. 0124exact hi
  125. 0125have hprev : x1 = x4
  126. 0126specialize IH x1
  127. 0127specialize IH u
  128. 0128specialize IH v
  129. 0129specialize IH x4
  130. 0130specialize IH w
  131. 0131specialize IH d
  132. 0132apply IH
  133. 0133exact hsum1
  134. 0134exact hsum2
  135. 0135have hadd : x1 + x = x4 + x3
  136. 0136specialize add_congr x1
  137. 0137specialize add_congr x4
  138. 0138specialize add_congr x
  139. 0139specialize add_congr x3
  140. 0140apply add_congr
  141. 0141exact hprev
  142. 0142exact ha
  143. 0143trans x2
  144. 0144exact hn
  145. 0145trans x1 + x
  146. 0146exact hstep1_witness_witness_witness_right_right_right
  147. 0147trans x4 + x3
  148. 0148exact hadd
  149. 0149trans x5
  150. 0150symm
  151. 0151exact hstep2_witness_witness_witness_right_right_right
  152. 0152symm
  153. 0153exact hm