PA0097 · theorem

finite_short_cover_impossible

Alpha v34 checked-use theorem · independently closed; not Stable

A prefix shorter than the target interval cannot cover every target value.

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. Lt(l,n) → ¬(∀ x. Lt(x,n) → ContainsPrefix(b,c,l,x))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0027 ContainsPrefix

3 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0024 BoundedPrefix PD0025 InjectivePrefix PD0026 SurjectivePrefix PD0027 ContainsPrefix

21 occurrences

Exact expanded native-PA statement
forall b c l n. (exists h. h + S l = n) -> ~(forall fom_value_impossible_cover. (exists fom_gap_impossible_cover_value_bound. fom_gap_impossible_cover_value_bound + S (fom_value_impossible_cover) = n) -> exists fom_index_impossible_cover. ((exists fom_gap_impossible_cover_index_bound. fom_gap_impossible_cover_index_bound + S (fom_index_impossible_cover) = l) /\ (((exists fom_beta_height_impossible_cover_entry. fom_beta_height_impossible_cover_entry + S (fom_value_impossible_cover) = S ((S (fom_index_impossible_cover)) * c)) /\ exists fom_beta_quotient_impossible_cover_entry. b = fom_beta_quotient_impossible_cover_entry * S ((S (fom_index_impossible_cover)) * c) + (fom_value_impossible_cover)))))

Proof neighborhood

Direct theorem prerequisites

PA0094 finite_inverse_choice_prefix_exists PA0095 finite_inverse_choice_bounded_into PA0096 finite_inverse_choice_injective PA004W finite_bounded_injective_surjective PA000R le_trans PA002O le_succ PA001A le_refl PA002F beta_at_unique PA0010 lt_irrefl_expanded

Direct theorem dependents

PA0098 finite_short_prefix_omits

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

124 script commands · 24 reading checkpoints · 13 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 (9)
finite inverse choice prefix existsfinite inverse choice bounded intofinite inverse choice injectivefinite bounded injective surjectivele transle succle reflbeta at uniquelt irrefl expanded
01Fix variables and assumptionsL1–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro hln
  6. L6
    intro hcover
02Establish hchoice_existsL7–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite inverse choice prefix exists.

  1. L7
    have hchoice_exists : ∃ z. ∃ d. ∀ x. Lt(x,n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))Definitions: Lt(x,n)BetaAt(z,d,x,y)Lt(y,l)BetaAt(b,c,y,x)Original native command in the exact edition
  2. L8
    specialize finite_inverse_choice_prefix_exists b
  3. L9
    specialize finite_inverse_choice_prefix_exists c
  4. L10
    specialize finite_inverse_choice_prefix_exists l
  5. L11
    specialize finite_inverse_choice_prefix_exists n
  6. L12
    apply finite_inverse_choice_prefix_exists
  7. L13
    exact hcover
03Separate the logical casesL14–15

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

  1. L14
    cases hchoice_exists
  2. L15
    cases hchoice_exists_witness
04Establish hboundedL16–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite inverse choice bounded into.

  1. L16
    have hbounded : ∀ fom_index_impossible_bounded. Lt(fom_index_impossible_bounded,n) → ∃ y. BetaAt(x,x1,fom_index_impossible_bounded,y) ∧ Lt(y,l)Definitions: Lt(fom_index_impossible_bounded,n)BetaAt(x,x1,fom_index_impossible_bounded,y)Lt(y,l)Original native command in the exact edition
  2. L17
    specialize finite_inverse_choice_bounded_into b
  3. L18
    specialize finite_inverse_choice_bounded_into c
  4. L19
    specialize finite_inverse_choice_bounded_into l
  5. L20
    specialize finite_inverse_choice_bounded_into x
  6. L21
    specialize finite_inverse_choice_bounded_into x1
  7. L22
    specialize finite_inverse_choice_bounded_into n
  8. L23
    apply finite_inverse_choice_bounded_into
  9. L24
    exact hchoice_exists_witness_witness
05Establish hinjectiveL25–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite inverse choice injective.

  1. L25
    have hinjective : InjectivePrefix(x,x1,n)Definitions: InjectivePrefix(x,x1,n)Original native command in the exact edition
  2. L26
    specialize finite_inverse_choice_injective b
  3. L27
    specialize finite_inverse_choice_injective c
  4. L28
    specialize finite_inverse_choice_injective l
  5. L29
    specialize finite_inverse_choice_injective x
  6. L30
    specialize finite_inverse_choice_injective x1
  7. L31
    specialize finite_inverse_choice_injective n
  8. L32
    apply finite_inverse_choice_injective
  9. L33
    exact hchoice_exists_witness_witness
06Establish hbounded_allL34–35

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

  1. L34
    have hbounded_all : ∀ fom_index_impossible_bounded. Lt(fom_index_impossible_bounded,n) → ∃ y. BetaAt(x,x1,fom_index_impossible_bounded,y) ∧ Lt(y,l)Definitions: Lt(fom_index_impossible_bounded,n)BetaAt(x,x1,fom_index_impossible_bounded,y)Lt(y,l)Original native command in the exact edition
  2. L35
    exact hbounded
07Establish hbounded_smallL36–38

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

  1. L36
    have hbounded_small : BoundedPrefix(x,x1,S l)Definitions: BoundedPrefix(x,x1,S l)Original native command in the exact edition
  2. L37
    intro i
  3. L38
    intro hi
08Establish hinL39–46

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

  1. L39
  2. L40
    specialize le_trans (S i)
  3. L41
    specialize le_trans (S l)
  4. L42
    specialize le_trans n
  5. L43
    apply le_trans
  6. L44
    exact hi
  7. L45
    exact hln
  8. L46
    specialize hbounded_all i
09Establish hentryL47–49

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

  1. L47
    have hentry : ∃ v. BetaAt(x,x1,i,v) ∧ Lt(v,l)Definitions: BetaAt(x,x1,i,v)Lt(v,l)Original native command in the exact edition
  2. L48
    apply hbounded_all
  3. L49
    exact hin
10Separate the logical casesL50–51

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

  1. L50
    cases hentry
  2. L51
    cases hentry_witness
11Construct an explicit witnessL52–52

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

  1. L52
    exists x2
12Separate the logical casesL53–53

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

  1. L53
    split
13Use earlier factsL54–58

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

  1. L54
    exact hentry_witness_left
  2. L55
    specialize le_succ (S x2)
  3. L56
    specialize le_succ l
  4. L57
    apply le_succ
  5. L58
    exact hentry_witness_right
14Establish hinjective_smallL59–68

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

  1. L59
    have hinjective_small : InjectivePrefix(x,x1,S l)Definitions: InjectivePrefix(x,x1,S l)Original native command in the exact edition
  2. L60
    intro i
  3. L61
    intro j
  4. L62
    intro v
  5. L63
    intro hi
  6. L64
    intro hj
  7. L65
    intro hvi
  8. L66
    intro hvj
  9. L67
    specialize hinjective i
  10. L68
    specialize hinjective j
15Use earlier factsL69–78

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

  1. L69
    specialize hinjective v
  2. L70
    apply hinjective
  3. L71
    specialize le_trans (S i)
  4. L72
    specialize le_trans (S l)
  5. L73
    specialize le_trans n
  6. L74
    apply le_trans
  7. L75
    exact hi
  8. L76
    exact hln
  9. L77
    specialize le_trans (S j)
  10. L78
    specialize le_trans (S l)
16Use earlier factsL79–84

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

  1. L79
    specialize le_trans n
  2. L80
    apply le_trans
  3. L81
    exact hj
  4. L82
    exact hln
  5. L83
    exact hvi
  6. L84
    exact hvj
17Establish hsurjectiveL85–92

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bounded injective surjective.

  1. L85
    have hsurjective : SurjectivePrefix(x,x1,S l)Definitions: SurjectivePrefix(x,x1,S l)Original native command in the exact edition
  2. L86
    specialize finite_bounded_injective_surjective (S l)
  3. L87
    specialize finite_bounded_injective_surjective x
  4. L88
    specialize finite_bounded_injective_surjective x1
  5. L89
    apply finite_bounded_injective_surjective
  6. L90
    exact hbounded_small
  7. L91
    exact hinjective_small
  8. L92
    specialize hsurjective l
18Establish hoccursL93–96

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

  1. L93
    have hoccurs : ContainsPrefix(x,x1,S l,l)Definitions: ContainsPrefix(x,x1,S l,l)Original native command in the exact edition
  2. L94
    apply hsurjective
  3. L95
    specialize le_refl (S l)
  4. L96
    exact le_refl
19Separate the logical casesL97–98

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

  1. L97
    cases hoccurs
  2. L98
    cases hoccurs_witness
20Establish hindex_nL99–106

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

  1. L99
    have hindex_n : Lt(x2,n)Definitions: Lt(x2,n)Original native command in the exact edition
  2. L100
    specialize le_trans (S x2)
  3. L101
    specialize le_trans (S l)
  4. L102
    specialize le_trans n
  5. L103
    apply le_trans
  6. L104
    exact hoccurs_witness_left
  7. L105
    exact hln
  8. L106
    specialize hbounded x2
21Establish hstoredL107–109

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

  1. L107
    have hstored : ∃ v. BetaAt(x,x1,x2,v) ∧ Lt(v,l)Definitions: BetaAt(x,x1,x2,v)Lt(v,l)Original native command in the exact edition
  2. L108
    apply hbounded
  3. L109
    exact hindex_n
22Separate the logical casesL110–111

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

  1. L110
    cases hstored
  2. L111
    cases hstored_witness
23Establish hlvL112–121

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

  1. L112
    have hlv : l = x3
  2. L113
    specialize beta_at_unique x
  3. L114
    specialize beta_at_unique x1
  4. L115
    specialize beta_at_unique x2
  5. L116
    specialize beta_at_unique l
  6. L117
    specialize beta_at_unique x3
  7. L118
    apply beta_at_unique
  8. L119
    exact hoccurs_witness_right
  9. L120
    exact hstored_witness_left
  10. L121
    rewrite <- hlv at hstored_witness_right
24Use earlier factsL122–124

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

  1. L122
    specialize lt_irrefl_expanded l
  2. L123
    apply lt_irrefl_expanded
  3. L124
    exact hstored_witness_right

Library-wide reading audit

Original defined command ledger · 124 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hln
  6. 0006intro hcover
  7. 0007have hchoice_exists : ∃ z. ∃ d. ∀ x. Lt(x,n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))
    Exact native replay linehave hchoice_exists : exists z d. (forall fom_value_impossible_choice. (exists fom_gap_impossible_choice_value_bound. fom_gap_impossible_choice_value_bound + S (fom_value_impossible_choice) = n) -> exists fom_index_impossible_choice. ((((exists fom_beta_height_impossible_choice_choice_entry. fom_beta_height_impossible_choice_choice_entry + S (fom_index_impossible_choice) = S ((S (fom_value_impossible_choice)) * d)) /\ exists fom_beta_quotient_impossible_choice_choice_entry. z = fom_beta_quotient_impossible_choice_choice_entry * S ((S (fom_value_impossible_choice)) * d) + (fom_index_impossible_choice))) /\ ((exists fom_gap_impossible_choice_index_bound. fom_gap_impossible_choice_index_bound + S (fom_index_impossible_choice) = l) /\ (((exists fom_beta_height_impossible_choice_source_entry. fom_beta_height_impossible_choice_source_entry + S (fom_value_impossible_choice) = S ((S (fom_index_impossible_choice)) * c)) /\ exists fom_beta_quotient_impossible_choice_source_entry. b = fom_beta_quotient_impossible_choice_source_entry * S ((S (fom_index_impossible_choice)) * c) + (fom_value_impossible_choice))))))
  8. 0008specialize finite_inverse_choice_prefix_exists b
  9. 0009specialize finite_inverse_choice_prefix_exists c
  10. 0010specialize finite_inverse_choice_prefix_exists l
  11. 0011specialize finite_inverse_choice_prefix_exists n
  12. 0012apply finite_inverse_choice_prefix_exists
  13. 0013exact hcover
  14. 0014cases hchoice_exists
  15. 0015cases hchoice_exists_witness
  16. 0016have hbounded : ∀ fom_index_impossible_bounded. Lt(fom_index_impossible_bounded,n) → ∃ y. BetaAt(x,x1,fom_index_impossible_bounded,y) ∧ Lt(y,l)
    Exact native replay linehave hbounded : forall fom_index_impossible_bounded. (exists fom_gap_impossible_bounded_index_bound. fom_gap_impossible_bounded_index_bound + S (fom_index_impossible_bounded) = n) -> exists fom_value_impossible_bounded. ((((exists fom_beta_height_impossible_bounded_entry. fom_beta_height_impossible_bounded_entry + S (fom_value_impossible_bounded) = S ((S (fom_index_impossible_bounded)) * x1)) /\ exists fom_beta_quotient_impossible_bounded_entry. x = fom_beta_quotient_impossible_bounded_entry * S ((S (fom_index_impossible_bounded)) * x1) + (fom_value_impossible_bounded))) /\ (exists fom_gap_impossible_bounded_value_bound. fom_gap_impossible_bounded_value_bound + S (fom_value_impossible_bounded) = l))
  17. 0017specialize finite_inverse_choice_bounded_into b
  18. 0018specialize finite_inverse_choice_bounded_into c
  19. 0019specialize finite_inverse_choice_bounded_into l
  20. 0020specialize finite_inverse_choice_bounded_into x
  21. 0021specialize finite_inverse_choice_bounded_into x1
  22. 0022specialize finite_inverse_choice_bounded_into n
  23. 0023apply finite_inverse_choice_bounded_into
  24. 0024exact hchoice_exists_witness_witness
  25. 0025have hinjective : InjectivePrefix(x,x1,n)
    Exact native replay linehave hinjective : forall fp_i_impossible_injective fp_j_impossible_injective fp_value_impossible_injective. (exists fp_gap_impossible_injective_i. fp_gap_impossible_injective_i + S fp_i_impossible_injective = n) -> (exists fp_gap_impossible_injective_j. fp_gap_impossible_injective_j + S fp_j_impossible_injective = n) -> (((exists ff_h_impossible_injective_left. ff_h_impossible_injective_left + S (fp_value_impossible_injective) = S ((S (fp_i_impossible_injective)) * x1)) /\ exists ff_q_impossible_injective_left. x = ff_q_impossible_injective_left * S ((S (fp_i_impossible_injective)) * x1) + (fp_value_impossible_injective))) -> (((exists ff_h_impossible_injective_right. ff_h_impossible_injective_right + S (fp_value_impossible_injective) = S ((S (fp_j_impossible_injective)) * x1)) /\ exists ff_q_impossible_injective_right. x = ff_q_impossible_injective_right * S ((S (fp_j_impossible_injective)) * x1) + (fp_value_impossible_injective))) -> fp_i_impossible_injective = fp_j_impossible_injective
  26. 0026specialize finite_inverse_choice_injective b
  27. 0027specialize finite_inverse_choice_injective c
  28. 0028specialize finite_inverse_choice_injective l
  29. 0029specialize finite_inverse_choice_injective x
  30. 0030specialize finite_inverse_choice_injective x1
  31. 0031specialize finite_inverse_choice_injective n
  32. 0032apply finite_inverse_choice_injective
  33. 0033exact hchoice_exists_witness_witness
  34. 0034have hbounded_all : ∀ fom_index_impossible_bounded. Lt(fom_index_impossible_bounded,n) → ∃ y. BetaAt(x,x1,fom_index_impossible_bounded,y) ∧ Lt(y,l)
    Exact native replay linehave hbounded_all : forall fom_index_impossible_bounded. (exists fom_gap_impossible_bounded_index_bound. fom_gap_impossible_bounded_index_bound + S (fom_index_impossible_bounded) = n) -> exists fom_value_impossible_bounded. ((((exists fom_beta_height_impossible_bounded_entry. fom_beta_height_impossible_bounded_entry + S (fom_value_impossible_bounded) = S ((S (fom_index_impossible_bounded)) * x1)) /\ exists fom_beta_quotient_impossible_bounded_entry. x = fom_beta_quotient_impossible_bounded_entry * S ((S (fom_index_impossible_bounded)) * x1) + (fom_value_impossible_bounded))) /\ (exists fom_gap_impossible_bounded_value_bound. fom_gap_impossible_bounded_value_bound + S (fom_value_impossible_bounded) = l))
  35. 0035exact hbounded
  36. 0036have hbounded_small : BoundedPrefix(x,x1,S l)
    Exact native replay linehave hbounded_small : forall fp_i_impossible_small_bounded. (exists fp_gap_impossible_small_bounded_index. fp_gap_impossible_small_bounded_index + S fp_i_impossible_small_bounded = S l) -> exists fp_value_impossible_small_bounded. ((((exists ff_h_impossible_small_bounded_entry. ff_h_impossible_small_bounded_entry + S (fp_value_impossible_small_bounded) = S ((S (fp_i_impossible_small_bounded)) * x1)) /\ exists ff_q_impossible_small_bounded_entry. x = ff_q_impossible_small_bounded_entry * S ((S (fp_i_impossible_small_bounded)) * x1) + (fp_value_impossible_small_bounded))) /\ (exists fp_gap_impossible_small_bounded_value. fp_gap_impossible_small_bounded_value + S fp_value_impossible_small_bounded = S l))
  37. 0037intro i
  38. 0038intro hi
  39. 0039have hin : Lt(i,n)
    Exact native replay linehave hin : exists h. h + S i = n
  40. 0040specialize le_trans (S i)
  41. 0041specialize le_trans (S l)
  42. 0042specialize le_trans n
  43. 0043apply le_trans
  44. 0044exact hi
  45. 0045exact hln
  46. 0046specialize hbounded_all i
  47. 0047have hentry : ∃ v. BetaAt(x,x1,i,v) ∧ Lt(v,l)
    Exact native replay linehave hentry : exists v. (((exists h. h + S v = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + v) /\ exists h. h + S v = l)
  48. 0048apply hbounded_all
  49. 0049exact hin
  50. 0050cases hentry
  51. 0051cases hentry_witness
  52. 0052exists x2
  53. 0053split
  54. 0054exact hentry_witness_left
  55. 0055specialize le_succ (S x2)
  56. 0056specialize le_succ l
  57. 0057apply le_succ
  58. 0058exact hentry_witness_right
  59. 0059have hinjective_small : InjectivePrefix(x,x1,S l)
    Exact native replay linehave hinjective_small : forall fp_i_impossible_small_injective fp_j_impossible_small_injective fp_value_impossible_small_injective. (exists fp_gap_impossible_small_injective_i. fp_gap_impossible_small_injective_i + S fp_i_impossible_small_injective = S l) -> (exists fp_gap_impossible_small_injective_j. fp_gap_impossible_small_injective_j + S fp_j_impossible_small_injective = S l) -> (((exists ff_h_impossible_small_injective_left. ff_h_impossible_small_injective_left + S (fp_value_impossible_small_injective) = S ((S (fp_i_impossible_small_injective)) * x1)) /\ exists ff_q_impossible_small_injective_left. x = ff_q_impossible_small_injective_left * S ((S (fp_i_impossible_small_injective)) * x1) + (fp_value_impossible_small_injective))) -> (((exists ff_h_impossible_small_injective_right. ff_h_impossible_small_injective_right + S (fp_value_impossible_small_injective) = S ((S (fp_j_impossible_small_injective)) * x1)) /\ exists ff_q_impossible_small_injective_right. x = ff_q_impossible_small_injective_right * S ((S (fp_j_impossible_small_injective)) * x1) + (fp_value_impossible_small_injective))) -> fp_i_impossible_small_injective = fp_j_impossible_small_injective
  60. 0060intro i
  61. 0061intro j
  62. 0062intro v
  63. 0063intro hi
  64. 0064intro hj
  65. 0065intro hvi
  66. 0066intro hvj
  67. 0067specialize hinjective i
  68. 0068specialize hinjective j
  69. 0069specialize hinjective v
  70. 0070apply hinjective
  71. 0071specialize le_trans (S i)
  72. 0072specialize le_trans (S l)
  73. 0073specialize le_trans n
  74. 0074apply le_trans
  75. 0075exact hi
  76. 0076exact hln
  77. 0077specialize le_trans (S j)
  78. 0078specialize le_trans (S l)
  79. 0079specialize le_trans n
  80. 0080apply le_trans
  81. 0081exact hj
  82. 0082exact hln
  83. 0083exact hvi
  84. 0084exact hvj
  85. 0085have hsurjective : SurjectivePrefix(x,x1,S l)
    Exact native replay linehave hsurjective : forall fp_value_impossible_small_surjective. (exists fp_gap_impossible_small_surjective_value. fp_gap_impossible_small_surjective_value + S fp_value_impossible_small_surjective = S l) -> exists fp_i_impossible_small_surjective. ((exists fp_gap_impossible_small_surjective_index. fp_gap_impossible_small_surjective_index + S fp_i_impossible_small_surjective = S l) /\ (((exists ff_h_impossible_small_surjective_entry. ff_h_impossible_small_surjective_entry + S (fp_value_impossible_small_surjective) = S ((S (fp_i_impossible_small_surjective)) * x1)) /\ exists ff_q_impossible_small_surjective_entry. x = ff_q_impossible_small_surjective_entry * S ((S (fp_i_impossible_small_surjective)) * x1) + (fp_value_impossible_small_surjective))))
  86. 0086specialize finite_bounded_injective_surjective (S l)
  87. 0087specialize finite_bounded_injective_surjective x
  88. 0088specialize finite_bounded_injective_surjective x1
  89. 0089apply finite_bounded_injective_surjective
  90. 0090exact hbounded_small
  91. 0091exact hinjective_small
  92. 0092specialize hsurjective l
  93. 0093have hoccurs : ContainsPrefix(x,x1,S l,l)
    Exact native replay linehave hoccurs : exists i. ((exists h. h + S i = S l) /\ (((exists ff_h_impossible_last_entry. ff_h_impossible_last_entry + S (l) = S ((S (i)) * x1)) /\ exists ff_q_impossible_last_entry. x = ff_q_impossible_last_entry * S ((S (i)) * x1) + (l))))
  94. 0094apply hsurjective
  95. 0095specialize le_refl (S l)
  96. 0096exact le_refl
  97. 0097cases hoccurs
  98. 0098cases hoccurs_witness
  99. 0099have hindex_n : Lt(x2,n)
    Exact native replay linehave hindex_n : exists h. h + S x2 = n
  100. 0100specialize le_trans (S x2)
  101. 0101specialize le_trans (S l)
  102. 0102specialize le_trans n
  103. 0103apply le_trans
  104. 0104exact hoccurs_witness_left
  105. 0105exact hln
  106. 0106specialize hbounded x2
  107. 0107have hstored : ∃ v. BetaAt(x,x1,x2,v) ∧ Lt(v,l)
    Exact native replay linehave hstored : exists v. ((((exists ff_h_impossible_stored_entry. ff_h_impossible_stored_entry + S (v) = S ((S (x2)) * x1)) /\ exists ff_q_impossible_stored_entry. x = ff_q_impossible_stored_entry * S ((S (x2)) * x1) + (v))) /\ exists h. h + S v = l)
  108. 0108apply hbounded
  109. 0109exact hindex_n
  110. 0110cases hstored
  111. 0111cases hstored_witness
  112. 0112have hlv : l = x3
  113. 0113specialize beta_at_unique x
  114. 0114specialize beta_at_unique x1
  115. 0115specialize beta_at_unique x2
  116. 0116specialize beta_at_unique l
  117. 0117specialize beta_at_unique x3
  118. 0118apply beta_at_unique
  119. 0119exact hoccurs_witness_right
  120. 0120exact hstored_witness_left
  121. 0121rewrite <- hlv at hstored_witness_right
  122. 0122specialize lt_irrefl_expanded l
  123. 0123apply lt_irrefl_expanded
  124. 0124exact hstored_witness_right