PA00AT · theorem

beta_prefix_append_two_orbit_closed

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

Appending both directions of a decoded two-cycle preserves orbit closure of the used prefix.

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

∀ u. ∀ v. ∀ b. ∀ c. ∀ z. ∀ d. ∀ l. ∀ a. ∀ e. BetaAt(z,d,l,a) ∧ (BetaAt(z,d,S l,e) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))) → (∀ x. ∀ y. ∀ n. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,y,n) → ContainsPrefix(b,c,l,n)) → BetaAt(u,v,a,e) → BetaAt(u,v,e,a) → ∀ x. ∀ y. ∀ n. Lt(x,S S l) → BetaAt(z,d,x,y) → BetaAt(u,v,y,n) → ContainsPrefix(z,d,S S l,n)

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 PD0013 BetaAt PD0027 ContainsPrefix

15 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0027 ContainsPrefix

13 occurrences

Exact expanded native-PA statement
forall u v b c z d l a e. (((((exists wpo_beta_height_closure_trace_first. wpo_beta_height_closure_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_closure_trace_first. z = wpo_beta_quotient_closure_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_closure_trace_second. wpo_beta_height_closure_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_closure_trace_second. z = wpo_beta_quotient_closure_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_closure_trace wpo_old_value_closure_trace. (exists wpo_gap_closure_trace_old_bound. wpo_gap_closure_trace_old_bound + S (wpo_old_index_closure_trace) = l) -> (((exists wpo_beta_height_closure_trace_old_entry. wpo_beta_height_closure_trace_old_entry + S (wpo_old_value_closure_trace) = S ((S (wpo_old_index_closure_trace)) * c)) /\ exists wpo_beta_quotient_closure_trace_old_entry. b = wpo_beta_quotient_closure_trace_old_entry * S ((S (wpo_old_index_closure_trace)) * c) + (wpo_old_value_closure_trace))) -> (((exists wpo_beta_height_closure_trace_new_entry. wpo_beta_height_closure_trace_new_entry + S (wpo_old_value_closure_trace) = S ((S (wpo_old_index_closure_trace)) * d)) /\ exists wpo_beta_quotient_closure_trace_new_entry. z = wpo_beta_quotient_closure_trace_new_entry * S ((S (wpo_old_index_closure_trace)) * d) + (wpo_old_value_closure_trace))))))) -> (forall wpo_position_closure_before wpo_source_closure_before wpo_mate_closure_before. (exists wpo_gap_closure_before_position_bound. wpo_gap_closure_before_position_bound + S (wpo_position_closure_before) = l) -> (((exists wpo_beta_height_closure_before_source_entry. wpo_beta_height_closure_before_source_entry + S (wpo_source_closure_before) = S ((S (wpo_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_source_entry. b = wpo_beta_quotient_closure_before_source_entry * S ((S (wpo_position_closure_before)) * c) + (wpo_source_closure_before))) -> (((exists wpo_beta_height_closure_before_inverse_entry. wpo_beta_height_closure_before_inverse_entry + S (wpo_mate_closure_before) = S ((S (wpo_source_closure_before)) * v)) /\ exists wpo_beta_quotient_closure_before_inverse_entry. u = wpo_beta_quotient_closure_before_inverse_entry * S ((S (wpo_source_closure_before)) * v) + (wpo_mate_closure_before))) -> exists wpo_mate_position_closure_before. ((exists wpo_gap_closure_before_mate_bound. wpo_gap_closure_before_mate_bound + S (wpo_mate_position_closure_before) = l) /\ (((exists wpo_beta_height_closure_before_mate_entry. wpo_beta_height_closure_before_mate_entry + S (wpo_mate_closure_before) = S ((S (wpo_mate_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_mate_entry. b = wpo_beta_quotient_closure_before_mate_entry * S ((S (wpo_mate_position_closure_before)) * c) + (wpo_mate_closure_before))))) -> (((exists wpo_beta_height_closure_forward. wpo_beta_height_closure_forward + S (e) = S ((S (a)) * v)) /\ exists wpo_beta_quotient_closure_forward. u = wpo_beta_quotient_closure_forward * S ((S (a)) * v) + (e))) -> (((exists wpo_beta_height_closure_back. wpo_beta_height_closure_back + S (a) = S ((S (e)) * v)) /\ exists wpo_beta_quotient_closure_back. u = wpo_beta_quotient_closure_back * S ((S (e)) * v) + (a))) -> (forall wpo_position_closure_after wpo_source_closure_after wpo_mate_closure_after. (exists wpo_gap_closure_after_position_bound. wpo_gap_closure_after_position_bound + S (wpo_position_closure_after) = S (S l)) -> (((exists wpo_beta_height_closure_after_source_entry. wpo_beta_height_closure_after_source_entry + S (wpo_source_closure_after) = S ((S (wpo_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_source_entry. z = wpo_beta_quotient_closure_after_source_entry * S ((S (wpo_position_closure_after)) * d) + (wpo_source_closure_after))) -> (((exists wpo_beta_height_closure_after_inverse_entry. wpo_beta_height_closure_after_inverse_entry + S (wpo_mate_closure_after) = S ((S (wpo_source_closure_after)) * v)) /\ exists wpo_beta_quotient_closure_after_inverse_entry. u = wpo_beta_quotient_closure_after_inverse_entry * S ((S (wpo_source_closure_after)) * v) + (wpo_mate_closure_after))) -> exists wpo_mate_position_closure_after. ((exists wpo_gap_closure_after_mate_bound. wpo_gap_closure_after_mate_bound + S (wpo_mate_position_closure_after) = S (S l)) /\ (((exists wpo_beta_height_closure_after_mate_entry. wpo_beta_height_closure_after_mate_entry + S (wpo_mate_closure_after) = S ((S (wpo_mate_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_mate_entry. z = wpo_beta_quotient_closure_after_mate_entry * S ((S (wpo_mate_position_closure_after)) * d) + (wpo_mate_closure_after)))))

Proof neighborhood

Direct theorem prerequisites

PA009L beta_prefix_append_two_reflect PA002F beta_at_unique PA001A le_refl PA002O le_succ

Direct theorem dependents

PA00AV prime_pair_order_choose_append

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

109 script commands · 30 reading checkpoints · 7 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 prefix append two reflectbeta at uniquele reflle succ
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro z
  6. L6
    intro d
  7. L7
    intro l
  8. L8
    intro a
  9. L9
    intro e
  10. L10
    intro htrace
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hclosed
  2. L12
    intro hforward
  3. L13
    intro hback
03Establish htrace_partsL14–15

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

  1. L14
    have htrace_parts : BetaAt(z,d,l,a) ∧ (BetaAt(z,d,S l,e) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y)))Definitions: BetaAt(z,d,l,a)BetaAt(z,d,S l,e)Lt(x,l)BetaAt(b,c,x,y)BetaAt(z,d,x,y)Original native command in the exact edition
  2. L15
    exact htrace
04Separate the logical casesL16–17

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

  1. L16
    cases htrace_parts
  2. L17
    cases htrace_parts_right
05Fix variables and assumptionsL18–23

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

  1. L18
    intro q
  2. L19
    intro s
  3. L20
    intro m
  4. L21
    intro hq
  5. L22
    intro hsource
  6. L23
    intro hinverse
06Establish hreflect_allL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix append two reflect.

  1. L24
    have hreflect_all : ∀ q. ∀ s. Lt(q,S S l) → BetaAt(z,d,q,s) → q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))Definitions: Lt(q,S S l)BetaAt(z,d,q,s)Lt(q,l)BetaAt(b,c,q,s)Original native command in the exact edition
  2. L25
    specialize beta_prefix_append_two_reflect b
  3. L26
    specialize beta_prefix_append_two_reflect c
  4. L27
    specialize beta_prefix_append_two_reflect z
  5. L28
    specialize beta_prefix_append_two_reflect d
  6. L29
    specialize beta_prefix_append_two_reflect l
  7. L30
    specialize beta_prefix_append_two_reflect a
  8. L31
    specialize beta_prefix_append_two_reflect e
  9. L32
    apply beta_prefix_append_two_reflect
  10. L33
    exact htrace
07Establish hreflectL34–39

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

  1. L34
    have hreflect : q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))Definitions: Lt(q,l)BetaAt(b,c,q,s)Original native command in the exact edition
  2. L35
    specialize hreflect_all q
  3. L36
    specialize hreflect_all s
  4. L37
    apply hreflect_all
  5. L38
    exact hq
  6. L39
    exact hsource
08Separate the logical casesL40–41

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

  1. L40
    cases hreflect
  2. L41
    cases hreflect_left
09Establish hmate_firstL42–51

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

  1. L42
    have hmate_first : m = a
  2. L43
    specialize beta_at_unique u
  3. L44
    specialize beta_at_unique v
  4. L45
    specialize beta_at_unique e
  5. L46
    specialize beta_at_unique m
  6. L47
    specialize beta_at_unique a
  7. L48
    apply beta_at_unique
  8. L49
    rewrite hreflect_left_right at hinverse
  9. L50
    rewrite hreflect_left_right at hinverse
  10. L51
    exact hinverse
10Use earlier factsL52–52

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

  1. L52
    exact hback
11Construct an explicit witnessL53–53

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

  1. L53
    exists l
12Separate the logical casesL54–54

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

  1. L54
    split
13Use earlier factsL55–59

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

  1. L55
    specialize le_succ (S l)
  2. L56
    specialize le_succ (S l)
  3. L57
    apply le_succ
  4. L58
    specialize le_refl (S l)
  5. L59
    exact le_refl
14Calculate and transport equalitiesL60–61

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

  1. L60
    rewrite hmate_first
  2. L61
    rewrite hmate_first
15Use earlier factsL62–62

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

  1. L62
    exact htrace_parts_left
16Separate the logical casesL63–64

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

  1. L63
    cases hreflect_right
  2. L64
    cases hreflect_right_left
17Establish hmate_secondL65–74

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

  1. L65
    have hmate_second : m = e
  2. L66
    specialize beta_at_unique u
  3. L67
    specialize beta_at_unique v
  4. L68
    specialize beta_at_unique a
  5. L69
    specialize beta_at_unique m
  6. L70
    specialize beta_at_unique e
  7. L71
    apply beta_at_unique
  8. L72
    rewrite hreflect_right_left_right at hinverse
  9. L73
    rewrite hreflect_right_left_right at hinverse
  10. L74
    exact hinverse
18Use earlier factsL75–75

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

  1. L75
    exact hforward
19Construct an explicit witnessL76–76

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

  1. L76
    exists (S l)
20Separate the logical casesL77–77

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

  1. L77
    split
21Use earlier factsL78–79

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

  1. L78
    specialize le_refl (S (S l))
  2. L79
    exact le_refl
22Calculate and transport equalitiesL80–81

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

  1. L80
    rewrite hmate_second
  2. L81
    rewrite hmate_second
23Use earlier factsL82–82

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

  1. L82
    exact htrace_parts_right_left
24Separate the logical casesL83–83

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

  1. L83
    cases hreflect_right_right
25Establish hold_occurrenceL84–91

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

  1. L84
    have hold_occurrence : ContainsPrefix(b,c,l,m)Definitions: ContainsPrefix(b,c,l,m)Original native command in the exact edition
  2. L85
    specialize hclosed q
  3. L86
    specialize hclosed s
  4. L87
    specialize hclosed m
  5. L88
    apply hclosed
  6. L89
    exact hreflect_right_right_left
  7. L90
    exact hreflect_right_right_right
  8. L91
    exact hinverse
26Separate the logical casesL92–93

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

  1. L92
    cases hold_occurrence
  2. L93
    cases hold_occurrence_witness
27Construct an explicit witnessL94–94

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

  1. L94
    exists x
28Separate the logical casesL95–95

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

  1. L95
    split
29Establish hliftL96–105

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

  1. L96
  2. L97
    specialize le_succ (S x)
  3. L98
    specialize le_succ l
  4. L99
    apply le_succ
  5. L100
    exact hold_occurrence_witness_left
  6. L101
    specialize le_succ (S x)
  7. L102
    specialize le_succ (S l)
  8. L103
    apply le_succ
  9. L104
    exact hlift
  10. L105
    specialize htrace_parts_right_right x
30Use earlier factsL106–109

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

  1. L106
    specialize htrace_parts_right_right m
  2. L107
    apply htrace_parts_right_right
  3. L108
    exact hold_occurrence_witness_left
  4. L109
    exact hold_occurrence_witness_right

Library-wide reading audit

Original defined command ledger · 109 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro l
  8. 0008intro a
  9. 0009intro e
  10. 0010intro htrace
  11. 0011intro hclosed
  12. 0012intro hforward
  13. 0013intro hback
  14. 0014have htrace_parts : BetaAt(z,d,l,a) ∧ (BetaAt(z,d,S l,e) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y)))
    Exact native replay linehave htrace_parts : ((((exists wpo_beta_height_closure_trace_first. wpo_beta_height_closure_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_closure_trace_first. z = wpo_beta_quotient_closure_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_closure_trace_second. wpo_beta_height_closure_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_closure_trace_second. z = wpo_beta_quotient_closure_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_closure_trace wpo_old_value_closure_trace. (exists wpo_gap_closure_trace_old_bound. wpo_gap_closure_trace_old_bound + S (wpo_old_index_closure_trace) = l) -> (((exists wpo_beta_height_closure_trace_old_entry. wpo_beta_height_closure_trace_old_entry + S (wpo_old_value_closure_trace) = S ((S (wpo_old_index_closure_trace)) * c)) /\ exists wpo_beta_quotient_closure_trace_old_entry. b = wpo_beta_quotient_closure_trace_old_entry * S ((S (wpo_old_index_closure_trace)) * c) + (wpo_old_value_closure_trace))) -> (((exists wpo_beta_height_closure_trace_new_entry. wpo_beta_height_closure_trace_new_entry + S (wpo_old_value_closure_trace) = S ((S (wpo_old_index_closure_trace)) * d)) /\ exists wpo_beta_quotient_closure_trace_new_entry. z = wpo_beta_quotient_closure_trace_new_entry * S ((S (wpo_old_index_closure_trace)) * d) + (wpo_old_value_closure_trace))))))
  15. 0015exact htrace
  16. 0016cases htrace_parts
  17. 0017cases htrace_parts_right
  18. 0018intro q
  19. 0019intro s
  20. 0020intro m
  21. 0021intro hq
  22. 0022intro hsource
  23. 0023intro hinverse
  24. 0024have hreflect_all : ∀ q. ∀ s. Lt(q,S S l) → BetaAt(z,d,q,s) → q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))
    Exact native replay linehave hreflect_all : forall q s. (exists wpo_gap_closure_reflection_bound. wpo_gap_closure_reflection_bound + S (q) = S (S l)) -> (((exists wpo_beta_height_closure_reflection_entry. wpo_beta_height_closure_reflection_entry + S (s) = S ((S (q)) * d)) /\ exists wpo_beta_quotient_closure_reflection_entry. z = wpo_beta_quotient_closure_reflection_entry * S ((S (q)) * d) + (s))) -> (((q = S (l) /\ s = e) \/ ((q = l /\ s = a) \/ ((exists wpo_gap_closure_reflection_old_bound. wpo_gap_closure_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_closure_reflection_old_entry. wpo_beta_height_closure_reflection_old_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_closure_reflection_old_entry. b = wpo_beta_quotient_closure_reflection_old_entry * S ((S (q)) * c) + (s)))))))
  25. 0025specialize beta_prefix_append_two_reflect b
  26. 0026specialize beta_prefix_append_two_reflect c
  27. 0027specialize beta_prefix_append_two_reflect z
  28. 0028specialize beta_prefix_append_two_reflect d
  29. 0029specialize beta_prefix_append_two_reflect l
  30. 0030specialize beta_prefix_append_two_reflect a
  31. 0031specialize beta_prefix_append_two_reflect e
  32. 0032apply beta_prefix_append_two_reflect
  33. 0033exact htrace
  34. 0034have hreflect : q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))
    Exact native replay linehave hreflect : ((q = S (l) /\ s = e) \/ ((q = l /\ s = a) \/ ((exists wpo_gap_closure_reflection_old_bound. wpo_gap_closure_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_closure_reflection_old_entry. wpo_beta_height_closure_reflection_old_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_closure_reflection_old_entry. b = wpo_beta_quotient_closure_reflection_old_entry * S ((S (q)) * c) + (s))))))
  35. 0035specialize hreflect_all q
  36. 0036specialize hreflect_all s
  37. 0037apply hreflect_all
  38. 0038exact hq
  39. 0039exact hsource
  40. 0040cases hreflect
  41. 0041cases hreflect_left
  42. 0042have hmate_first : m = a
  43. 0043specialize beta_at_unique u
  44. 0044specialize beta_at_unique v
  45. 0045specialize beta_at_unique e
  46. 0046specialize beta_at_unique m
  47. 0047specialize beta_at_unique a
  48. 0048apply beta_at_unique
  49. 0049rewrite hreflect_left_right at hinverse
  50. 0050rewrite hreflect_left_right at hinverse
  51. 0051exact hinverse
  52. 0052exact hback
  53. 0053exists l
  54. 0054split
  55. 0055specialize le_succ (S l)
  56. 0056specialize le_succ (S l)
  57. 0057apply le_succ
  58. 0058specialize le_refl (S l)
  59. 0059exact le_refl
  60. 0060rewrite hmate_first
  61. 0061rewrite hmate_first
  62. 0062exact htrace_parts_left
  63. 0063cases hreflect_right
  64. 0064cases hreflect_right_left
  65. 0065have hmate_second : m = e
  66. 0066specialize beta_at_unique u
  67. 0067specialize beta_at_unique v
  68. 0068specialize beta_at_unique a
  69. 0069specialize beta_at_unique m
  70. 0070specialize beta_at_unique e
  71. 0071apply beta_at_unique
  72. 0072rewrite hreflect_right_left_right at hinverse
  73. 0073rewrite hreflect_right_left_right at hinverse
  74. 0074exact hinverse
  75. 0075exact hforward
  76. 0076exists (S l)
  77. 0077split
  78. 0078specialize le_refl (S (S l))
  79. 0079exact le_refl
  80. 0080rewrite hmate_second
  81. 0081rewrite hmate_second
  82. 0082exact htrace_parts_right_left
  83. 0083cases hreflect_right_right
  84. 0084have hold_occurrence : ContainsPrefix(b,c,l,m)
    Exact native replay linehave hold_occurrence : exists wpo_index_closure_old_occurrence. ((exists wpo_gap_closure_old_occurrence_bound. wpo_gap_closure_old_occurrence_bound + S (wpo_index_closure_old_occurrence) = l) /\ (((exists wpo_beta_height_closure_old_occurrence_entry. wpo_beta_height_closure_old_occurrence_entry + S (m) = S ((S (wpo_index_closure_old_occurrence)) * c)) /\ exists wpo_beta_quotient_closure_old_occurrence_entry. b = wpo_beta_quotient_closure_old_occurrence_entry * S ((S (wpo_index_closure_old_occurrence)) * c) + (m))))
  85. 0085specialize hclosed q
  86. 0086specialize hclosed s
  87. 0087specialize hclosed m
  88. 0088apply hclosed
  89. 0089exact hreflect_right_right_left
  90. 0090exact hreflect_right_right_right
  91. 0091exact hinverse
  92. 0092cases hold_occurrence
  93. 0093cases hold_occurrence_witness
  94. 0094exists x
  95. 0095split
  96. 0096have hlift : Lt(x,S l)
    Exact native replay linehave hlift : exists h. h + S x = S l
  97. 0097specialize le_succ (S x)
  98. 0098specialize le_succ l
  99. 0099apply le_succ
  100. 0100exact hold_occurrence_witness_left
  101. 0101specialize le_succ (S x)
  102. 0102specialize le_succ (S l)
  103. 0103apply le_succ
  104. 0104exact hlift
  105. 0105specialize htrace_parts_right_right x
  106. 0106specialize htrace_parts_right_right m
  107. 0107apply htrace_parts_right_right
  108. 0108exact hold_occurrence_witness_left
  109. 0109exact hold_occurrence_witness_right