FS0016 · theorem body

four_square_cross_interleaved_prefix_exists

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Any two equally long beta-coded prefixes have an actual beta-coded even/odd interleaving with complete constructive source coverage.

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. ∀ d. ∀ e. ∀ l. ∃ z. ∃ t. ∀ x. ∀ y. Lt(x,l + l) → BetaAt(z,t,x,y) → (∃ n. Lt(n,l) ∧ (BetaAt(b,c,n,y) ∧ x = n + n)) ∨ (∃ n. Lt(n,l) ∧ (BetaAt(d,e,n,y) ∧ x = S (n + n)))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

In local proof propositions

PD0002 Lt PD0013 BetaAt
Exact expanded first-order statement
forall b c d e l. exists z t. (forall fscp_index_exists_result fscp_value_exists_result. (exists fscp_gap_exists_result_index. fscp_gap_exists_result_index + S (fscp_index_exists_result) = (l + l)) -> (((exists ff_h_fscp_exists_result_source. ff_h_fscp_exists_result_source + S (fscp_value_exists_result) = S ((S (fscp_index_exists_result)) * t)) /\ exists ff_q_fscp_exists_result_source. z = ff_q_fscp_exists_result_source * S ((S (fscp_index_exists_result)) * t) + (fscp_value_exists_result))) -> (((exists fscp_left_exists_result. ((exists fscp_gap_exists_result_left_bound. fscp_gap_exists_result_left_bound + S (fscp_left_exists_result) = (l)) /\ ((((exists ff_h_fscp_exists_result_left. ff_h_fscp_exists_result_left + S (fscp_value_exists_result) = S ((S (fscp_left_exists_result)) * c)) /\ exists ff_q_fscp_exists_result_left. b = ff_q_fscp_exists_result_left * S ((S (fscp_left_exists_result)) * c) + (fscp_value_exists_result))) /\ fscp_index_exists_result = fscp_left_exists_result + fscp_left_exists_result))) \/ (exists fscp_right_exists_result. ((exists fscp_gap_exists_result_right_bound. fscp_gap_exists_result_right_bound + S (fscp_right_exists_result) = (l)) /\ ((((exists ff_h_fscp_exists_result_right. ff_h_fscp_exists_result_right + S (fscp_value_exists_result) = S ((S (fscp_right_exists_result)) * e)) /\ exists ff_q_fscp_exists_result_right. d = ff_q_fscp_exists_result_right * S ((S (fscp_right_exists_result)) * e) + (fscp_value_exists_result))) /\ fscp_index_exists_result = S (fscp_right_exists_result + fscp_right_exists_result)))))))

Proof neighborhood

Direct theorem prerequisites

le_zero · Stable closed succ_ne_zero · Stable closed beta_at_exists · Stable closed beta_prefix_append_two_exists · Alpha closed pair_order_double_succ_length · Alpha closed finite_lt_succ_eq_or_lt · Stable closed beta_at_unique · Stable closed le_refl · Stable closed le_succ · Stable closed

Direct theorem dependents

FS0017 four_square_cross_intersection

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

164 script commands · 58 reading checkpoints · 16 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
02Induction on lL5–5

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

  1. L5
    induction l
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–11

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

  1. L8
    intro i
  2. L9
    intro v
  3. L10
    intro hibound
  4. L11
    intro hentry
05Separate the logical casesL12–12

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

  1. L12
    exfalso
06Establish hzeroL13–15

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

  1. L13
    have hzero : S i = 0
  2. L14
    specialize le_zero (S i)
  3. L15
    apply le_zero
07Establish hsumL16–22

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

  1. L16
    have hsum : 0 + 0 = 0
  2. L17
    apply PA3
  3. L18
    rewrite hsum at hibound
  4. L19
    exact hibound
  5. L20
    specialize succ_ne_zero i
  6. L21
    apply succ_ne_zero
  7. L22
    exact hzero
08Separate the logical casesL23–24

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

  1. L23
    cases IH
  2. L24
    cases IH_witness
09Establish hleftL25–26

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

  1. L25
    have hleft : ∃ a. BetaAt(b,c,l,a)Definitions: BetaAt(b,c,l,a)Original native command in the exact edition
  2. L26
    apply beta_at_exists
10Separate the logical casesL27–27

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

  1. L27
    cases hleft
11Establish hrightL28–29

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

  1. L28
    have hright : ∃ a. BetaAt(d,e,l,a)Definitions: BetaAt(d,e,l,a)Original native command in the exact edition
  2. L29
    apply beta_at_exists
12Separate the logical casesL30–30

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

  1. L30
    cases hright
13Establish hpairL31–37

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

  1. L31
    have hpair : ∃ z. ∃ t. BetaAt(z,t,l + l,x2) ∧ (BetaAt(z,t,S (l + l),x3) ∧ (∀ y. ∀ n. Lt(y,l + l) → BetaAt(x,x1,y,n) → BetaAt(z,t,y,n)))Definitions: BetaAt(z,t,l + l,x2)BetaAt(z,t,S (l + l),x3)Lt(y,l + l)BetaAt(x,x1,y,n)BetaAt(z,t,y,n)Original native command in the exact edition
  2. L32
    specialize beta_prefix_append_two_exists x
  3. L33
    specialize beta_prefix_append_two_exists x1
  4. L34
    specialize beta_prefix_append_two_exists (l + l)
  5. L35
    specialize beta_prefix_append_two_exists x2
  6. L36
    specialize beta_prefix_append_two_exists x3
  7. L37
    exact beta_prefix_append_two_exists
14Separate the logical casesL38–41

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

  1. L38
    cases hpair
  2. L39
    cases hpair_witness
  3. L40
    cases hpair_witness_witness
  4. L41
    cases hpair_witness_witness_right
15Construct an explicit witnessL42–43

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

  1. L42
    exists x4
  2. L43
    exists x5
16Fix variables and assumptionsL44–47

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

  1. L44
    intro i
  2. L45
    intro v
  3. L46
    intro hibound
  4. L47
    intro hentry
17Establish hshapeL48–53

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

  1. L48
    have hshape : S (S (l + l)) = S l + S l
  2. L49
    specialize pair_order_double_succ_length (l + l)
  3. L50
    specialize pair_order_double_succ_length l
  4. L51
    apply pair_order_double_succ_length
  5. L52
    refl
  6. L53
    rewrite <- hshape at hibound
18Establish hlastL54–58

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

  1. L54
    have hlast : i = S (l + l) ∨ Lt(i,S (l + l))Definitions: Lt(i,S (l + l))Original native command in the exact edition
  2. L55
    specialize finite_lt_succ_eq_or_lt (S (l + l))
  3. L56
    specialize finite_lt_succ_eq_or_lt i
  4. L57
    apply finite_lt_succ_eq_or_lt
  5. L58
    exact hibound
19Separate the logical casesL59–59

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

  1. L59
    cases hlast
20Establish hnormalizedL60–63

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

  1. L60
    have hnormalized : BetaAt(x4,x5,S (l + l),v)Definitions: BetaAt(x4,x5,S (l + l),v)Original native command in the exact edition
  2. L61
    rewrite <- hlast_left
  3. L62
    rewrite <- hlast_left
  4. L63
    exact hentry
21Establish hequalL64–72

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

  1. L64
    have hequal : v = x3
  2. L65
    specialize beta_at_unique x4
  3. L66
    specialize beta_at_unique x5
  4. L67
    specialize beta_at_unique (S (l + l))
  5. L68
    specialize beta_at_unique v
  6. L69
    specialize beta_at_unique x3
  7. L70
    apply beta_at_unique
  8. L71
    exact hnormalized
  9. L72
    exact hpair_witness_witness_right_left
22Separate the logical casesL73–73

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

  1. L73
    right
23Construct an explicit witnessL74–74

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

  1. L74
    exists l
24Separate the logical casesL75–75

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

  1. L75
    split
25Use earlier factsL76–76

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

  1. L76
    apply le_refl
26Separate the logical casesL77–77

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

  1. L77
    split
27Calculate and transport equalitiesL78–79

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

  1. L78
    rewrite hequal
  2. L79
    rewrite hequal
28Use earlier factsL80–81

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

  1. L80
    exact hright_witness
  2. L81
    exact hlast_left
29Establish hpreviousL82–86

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

  1. L82
    have hprevious : i = l + l ∨ Lt(i,l + l)Definitions: Lt(i,l + l)Original native command in the exact edition
  2. L83
    specialize finite_lt_succ_eq_or_lt (l + l)
  3. L84
    specialize finite_lt_succ_eq_or_lt i
  4. L85
    apply finite_lt_succ_eq_or_lt
  5. L86
    exact hlast_right
30Separate the logical casesL87–87

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

  1. L87
    cases hprevious
31Establish hnormalizedL88–91

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

  1. L88
    have hnormalized : BetaAt(x4,x5,l + l,v)Definitions: BetaAt(x4,x5,l + l,v)Original native command in the exact edition
  2. L89
    rewrite <- hprevious_left
  3. L90
    rewrite <- hprevious_left
  4. L91
    exact hentry
32Establish hequalL92–100

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

  1. L92
    have hequal : v = x2
  2. L93
    specialize beta_at_unique x4
  3. L94
    specialize beta_at_unique x5
  4. L95
    specialize beta_at_unique (l + l)
  5. L96
    specialize beta_at_unique v
  6. L97
    specialize beta_at_unique x2
  7. L98
    apply beta_at_unique
  8. L99
    exact hnormalized
  9. L100
    exact hpair_witness_witness_left
33Separate the logical casesL101–101

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

  1. L101
    left
34Construct an explicit witnessL102–102

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

  1. L102
    exists l
35Separate the logical casesL103–103

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

  1. L103
    split
36Use earlier factsL104–104

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

  1. L104
    apply le_refl
37Separate the logical casesL105–105

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

  1. L105
    split
38Calculate and transport equalitiesL106–107

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

  1. L106
    rewrite hequal
  2. L107
    rewrite hequal
39Use earlier factsL108–109

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

  1. L108
    exact hleft_witness
  2. L109
    exact hprevious_left
40Establish holdL110–111

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

  1. L110
    have hold : ∃ u. BetaAt(x,x1,i,u)Definitions: BetaAt(x,x1,i,u)Original native command in the exact edition
  2. L111
    apply beta_at_exists
41Separate the logical casesL112–112

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

  1. L112
    cases hold
42Establish hpreservedL113–118

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

  1. L113
    have hpreserved : BetaAt(x4,x5,i,x6)Definitions: BetaAt(x4,x5,i,x6)Original native command in the exact edition
  2. L114
    specialize hpair_witness_witness_right_right i
  3. L115
    specialize hpair_witness_witness_right_right x6
  4. L116
    apply hpair_witness_witness_right_right
  5. L117
    exact hprevious_right
  6. L118
    exact hold_witness
43Establish hequalL119–127

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

  1. L119
    have hequal : v = x6
  2. L120
    specialize beta_at_unique x4
  3. L121
    specialize beta_at_unique x5
  4. L122
    specialize beta_at_unique i
  5. L123
    specialize beta_at_unique v
  6. L124
    specialize beta_at_unique x6
  7. L125
    apply beta_at_unique
  8. L126
    exact hentry
  9. L127
    exact hpreserved
44Establish holdcaseL128–133

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

  1. L128
    have holdcase : (∃ x. Lt(x,l) ∧ (BetaAt(b,c,x,x6) ∧ i = x + x)) ∨ (∃ x. Lt(x,l) ∧ (BetaAt(d,e,x,x6) ∧ i = S (x + x)))Definitions: Lt(x,l)BetaAt(b,c,x,x6)BetaAt(d,e,x,x6)Original native command in the exact edition
  2. L129
    specialize IH_witness_witness i
  3. L130
    specialize IH_witness_witness x6
  4. L131
    apply IH_witness_witness
  5. L132
    exact hprevious_right
  6. L133
    exact hold_witness
45Separate the logical casesL134–138

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

  1. L134
    cases holdcase
  2. L135
    cases holdcase_left
  3. L136
    cases holdcase_left_witness
  4. L137
    cases holdcase_left_witness_right
  5. L138
    left
46Construct an explicit witnessL139–139

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

  1. L139
    exists x7
47Separate the logical casesL140–140

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

  1. L140
    split
48Use earlier factsL141–144

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

  1. L141
    specialize le_succ (S x7)
  2. L142
    specialize le_succ l
  3. L143
    apply le_succ
  4. L144
    exact holdcase_left_witness_left
49Separate the logical casesL145–145

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

  1. L145
    split
50Calculate and transport equalitiesL146–147

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

  1. L146
    rewrite hequal
  2. L147
    rewrite hequal
51Use earlier factsL148–149

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

  1. L148
    exact holdcase_left_witness_right_left
  2. L149
    exact holdcase_left_witness_right_right
52Separate the logical casesL150–153

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

  1. L150
    cases holdcase_right
  2. L151
    cases holdcase_right_witness
  3. L152
    cases holdcase_right_witness_right
  4. L153
    right
53Construct an explicit witnessL154–154

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

  1. L154
    exists x7
54Separate the logical casesL155–155

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

  1. L155
    split
55Use earlier factsL156–159

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

  1. L156
    specialize le_succ (S x7)
  2. L157
    specialize le_succ l
  3. L158
    apply le_succ
  4. L159
    exact holdcase_right_witness_left
56Separate the logical casesL160–160

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

  1. L160
    split
57Calculate and transport equalitiesL161–162

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

  1. L161
    rewrite hequal
  2. L162
    rewrite hequal
58Use earlier factsL163–164

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

  1. L163
    exact holdcase_right_witness_right_left
  2. L164
    exact holdcase_right_witness_right_right

Library-wide reading audit

Original defined command ledger · 164 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005induction l
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro v
  10. 0010intro hibound
  11. 0011intro hentry
  12. 0012exfalso
  13. 0013have hzero : S i = 0
  14. 0014specialize le_zero (S i)
  15. 0015apply le_zero
  16. 0016have hsum : 0 + 0 = 0
  17. 0017apply PA3
  18. 0018rewrite hsum at hibound
  19. 0019exact hibound
  20. 0020specialize succ_ne_zero i
  21. 0021apply succ_ne_zero
  22. 0022exact hzero
  23. 0023cases IH
  24. 0024cases IH_witness
  25. 0025have hleft : ∃ a. BetaAt(b,c,l,a)
    Exact native replay linehave hleft : exists a. ((exists ff_h_fscp_exists_left. ff_h_fscp_exists_left + S (a) = S ((S (l)) * c)) /\ exists ff_q_fscp_exists_left. b = ff_q_fscp_exists_left * S ((S (l)) * c) + (a))
  26. 0026apply beta_at_exists
  27. 0027cases hleft
  28. 0028have hright : ∃ a. BetaAt(d,e,l,a)
    Exact native replay linehave hright : exists a. ((exists ff_h_fscp_exists_right. ff_h_fscp_exists_right + S (a) = S ((S (l)) * e)) /\ exists ff_q_fscp_exists_right. d = ff_q_fscp_exists_right * S ((S (l)) * e) + (a))
  29. 0029apply beta_at_exists
  30. 0030cases hright
  31. 0031have hpair : ∃ z. ∃ t. BetaAt(z,t,l + l,x2) ∧ (BetaAt(z,t,S (l + l),x3) ∧ (∀ y. ∀ n. Lt(y,l + l) → BetaAt(x,x1,y,n) → BetaAt(z,t,y,n)))
    Exact native replay linehave hpair : exists z t. ((((exists ff_h_fscp_exists_pair_first. ff_h_fscp_exists_pair_first + S (x2) = S ((S (l + l)) * t)) /\ exists ff_q_fscp_exists_pair_first. z = ff_q_fscp_exists_pair_first * S ((S (l + l)) * t) + (x2))) /\ ((((exists ff_h_fscp_exists_pair_second. ff_h_fscp_exists_pair_second + S (x3) = S ((S (S (l + l))) * t)) /\ exists ff_q_fscp_exists_pair_second. z = ff_q_fscp_exists_pair_second * S ((S (S (l + l))) * t) + (x3))) /\ (forall i v. (exists fscp_gap_exists_pair_before. fscp_gap_exists_pair_before + S (i) = (l + l)) -> (((exists ff_h_fscp_exists_pair_old. ff_h_fscp_exists_pair_old + S (v) = S ((S (i)) * x1)) /\ exists ff_q_fscp_exists_pair_old. x = ff_q_fscp_exists_pair_old * S ((S (i)) * x1) + (v))) -> (((exists ff_h_fscp_exists_pair_new. ff_h_fscp_exists_pair_new + S (v) = S ((S (i)) * t)) /\ exists ff_q_fscp_exists_pair_new. z = ff_q_fscp_exists_pair_new * S ((S (i)) * t) + (v))))))
  32. 0032specialize beta_prefix_append_two_exists x
  33. 0033specialize beta_prefix_append_two_exists x1
  34. 0034specialize beta_prefix_append_two_exists (l + l)
  35. 0035specialize beta_prefix_append_two_exists x2
  36. 0036specialize beta_prefix_append_two_exists x3
  37. 0037exact beta_prefix_append_two_exists
  38. 0038cases hpair
  39. 0039cases hpair_witness
  40. 0040cases hpair_witness_witness
  41. 0041cases hpair_witness_witness_right
  42. 0042exists x4
  43. 0043exists x5
  44. 0044intro i
  45. 0045intro v
  46. 0046intro hibound
  47. 0047intro hentry
  48. 0048have hshape : S (S (l + l)) = S l + S l
  49. 0049specialize pair_order_double_succ_length (l + l)
  50. 0050specialize pair_order_double_succ_length l
  51. 0051apply pair_order_double_succ_length
  52. 0052refl
  53. 0053rewrite <- hshape at hibound
  54. 0054have hlast : i = S (l + l) ∨ Lt(i,S (l + l))
    Exact native replay linehave hlast : i = S (l + l) \/ (exists fscp_gap_exists_last_before. fscp_gap_exists_last_before + S (i) = (S (l + l)))
  55. 0055specialize finite_lt_succ_eq_or_lt (S (l + l))
  56. 0056specialize finite_lt_succ_eq_or_lt i
  57. 0057apply finite_lt_succ_eq_or_lt
  58. 0058exact hibound
  59. 0059cases hlast
  60. 0060have hnormalized : BetaAt(x4,x5,S (l + l),v)
    Exact native replay linehave hnormalized : ((exists ff_h_fscp_exists_last_normal. ff_h_fscp_exists_last_normal + S (v) = S ((S (S (l + l))) * x5)) /\ exists ff_q_fscp_exists_last_normal. x4 = ff_q_fscp_exists_last_normal * S ((S (S (l + l))) * x5) + (v))
  61. 0061rewrite <- hlast_left
  62. 0062rewrite <- hlast_left
  63. 0063exact hentry
  64. 0064have hequal : v = x3
  65. 0065specialize beta_at_unique x4
  66. 0066specialize beta_at_unique x5
  67. 0067specialize beta_at_unique (S (l + l))
  68. 0068specialize beta_at_unique v
  69. 0069specialize beta_at_unique x3
  70. 0070apply beta_at_unique
  71. 0071exact hnormalized
  72. 0072exact hpair_witness_witness_right_left
  73. 0073right
  74. 0074exists l
  75. 0075split
  76. 0076apply le_refl
  77. 0077split
  78. 0078rewrite hequal
  79. 0079rewrite hequal
  80. 0080exact hright_witness
  81. 0081exact hlast_left
  82. 0082have hprevious : i = l + l ∨ Lt(i,l + l)
    Exact native replay linehave hprevious : i = l + l \/ (exists fscp_gap_exists_previous_before. fscp_gap_exists_previous_before + S (i) = (l + l))
  83. 0083specialize finite_lt_succ_eq_or_lt (l + l)
  84. 0084specialize finite_lt_succ_eq_or_lt i
  85. 0085apply finite_lt_succ_eq_or_lt
  86. 0086exact hlast_right
  87. 0087cases hprevious
  88. 0088have hnormalized : BetaAt(x4,x5,l + l,v)
    Exact native replay linehave hnormalized : ((exists ff_h_fscp_exists_previous_normal. ff_h_fscp_exists_previous_normal + S (v) = S ((S (l + l)) * x5)) /\ exists ff_q_fscp_exists_previous_normal. x4 = ff_q_fscp_exists_previous_normal * S ((S (l + l)) * x5) + (v))
  89. 0089rewrite <- hprevious_left
  90. 0090rewrite <- hprevious_left
  91. 0091exact hentry
  92. 0092have hequal : v = x2
  93. 0093specialize beta_at_unique x4
  94. 0094specialize beta_at_unique x5
  95. 0095specialize beta_at_unique (l + l)
  96. 0096specialize beta_at_unique v
  97. 0097specialize beta_at_unique x2
  98. 0098apply beta_at_unique
  99. 0099exact hnormalized
  100. 0100exact hpair_witness_witness_left
  101. 0101left
  102. 0102exists l
  103. 0103split
  104. 0104apply le_refl
  105. 0105split
  106. 0106rewrite hequal
  107. 0107rewrite hequal
  108. 0108exact hleft_witness
  109. 0109exact hprevious_left
  110. 0110have hold : ∃ u. BetaAt(x,x1,i,u)
    Exact native replay linehave hold : exists u. ((exists ff_h_fscp_exists_old. ff_h_fscp_exists_old + S (u) = S ((S (i)) * x1)) /\ exists ff_q_fscp_exists_old. x = ff_q_fscp_exists_old * S ((S (i)) * x1) + (u))
  111. 0111apply beta_at_exists
  112. 0112cases hold
  113. 0113have hpreserved : BetaAt(x4,x5,i,x6)
    Exact native replay linehave hpreserved : ((exists ff_h_fscp_exists_preserved. ff_h_fscp_exists_preserved + S (x6) = S ((S (i)) * x5)) /\ exists ff_q_fscp_exists_preserved. x4 = ff_q_fscp_exists_preserved * S ((S (i)) * x5) + (x6))
  114. 0114specialize hpair_witness_witness_right_right i
  115. 0115specialize hpair_witness_witness_right_right x6
  116. 0116apply hpair_witness_witness_right_right
  117. 0117exact hprevious_right
  118. 0118exact hold_witness
  119. 0119have hequal : v = x6
  120. 0120specialize beta_at_unique x4
  121. 0121specialize beta_at_unique x5
  122. 0122specialize beta_at_unique i
  123. 0123specialize beta_at_unique v
  124. 0124specialize beta_at_unique x6
  125. 0125apply beta_at_unique
  126. 0126exact hentry
  127. 0127exact hpreserved
  128. 0128have holdcase : (∃ x. Lt(x,l) ∧ (BetaAt(b,c,x,x6) ∧ i = x + x)) ∨ (∃ x. Lt(x,l) ∧ (BetaAt(d,e,x,x6) ∧ i = S (x + x)))
    Exact native replay linehave holdcase : ((exists fscp_left_exists_old_case. ((exists fscp_gap_exists_old_case_left_bound. fscp_gap_exists_old_case_left_bound + S (fscp_left_exists_old_case) = (l)) /\ ((((exists ff_h_fscp_exists_old_case_left. ff_h_fscp_exists_old_case_left + S (x6) = S ((S (fscp_left_exists_old_case)) * c)) /\ exists ff_q_fscp_exists_old_case_left. b = ff_q_fscp_exists_old_case_left * S ((S (fscp_left_exists_old_case)) * c) + (x6))) /\ i = fscp_left_exists_old_case + fscp_left_exists_old_case))) \/ (exists fscp_right_exists_old_case. ((exists fscp_gap_exists_old_case_right_bound. fscp_gap_exists_old_case_right_bound + S (fscp_right_exists_old_case) = (l)) /\ ((((exists ff_h_fscp_exists_old_case_right. ff_h_fscp_exists_old_case_right + S (x6) = S ((S (fscp_right_exists_old_case)) * e)) /\ exists ff_q_fscp_exists_old_case_right. d = ff_q_fscp_exists_old_case_right * S ((S (fscp_right_exists_old_case)) * e) + (x6))) /\ i = S (fscp_right_exists_old_case + fscp_right_exists_old_case)))))
  129. 0129specialize IH_witness_witness i
  130. 0130specialize IH_witness_witness x6
  131. 0131apply IH_witness_witness
  132. 0132exact hprevious_right
  133. 0133exact hold_witness
  134. 0134cases holdcase
  135. 0135cases holdcase_left
  136. 0136cases holdcase_left_witness
  137. 0137cases holdcase_left_witness_right
  138. 0138left
  139. 0139exists x7
  140. 0140split
  141. 0141specialize le_succ (S x7)
  142. 0142specialize le_succ l
  143. 0143apply le_succ
  144. 0144exact holdcase_left_witness_left
  145. 0145split
  146. 0146rewrite hequal
  147. 0147rewrite hequal
  148. 0148exact holdcase_left_witness_right_left
  149. 0149exact holdcase_left_witness_right_right
  150. 0150cases holdcase_right
  151. 0151cases holdcase_right_witness
  152. 0152cases holdcase_right_witness_right
  153. 0153right
  154. 0154exists x7
  155. 0155split
  156. 0156specialize le_succ (S x7)
  157. 0157specialize le_succ l
  158. 0158apply le_succ
  159. 0159exact holdcase_right_witness_left
  160. 0160split
  161. 0161rewrite hequal
  162. 0162rewrite hequal
  163. 0163exact holdcase_right_witness_right_left
  164. 0164exact holdcase_right_witness_right_right