PA009M · theorem

beta_prefix_append_two_scaled_orbit_closed

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

Appending both zero-based sources preserves closure under actual-mate entries S j.

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. ∀ i. ∀ j. BetaAt(z,d,l,i) ∧ (BetaAt(z,d,S l,j) ∧ (∀ 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,S n) → ContainsPrefix(b,c,l,n)) → BetaAt(u,v,i,S j) → BetaAt(u,v,j,S i) → ∀ x. ∀ y. ∀ n. Lt(x,S S l) → BetaAt(z,d,x,y) → BetaAt(u,v,y,S 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 i j. (((((exists wpo_beta_height_closure_trace_first. wpo_beta_height_closure_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_closure_trace_first. z = wpo_beta_quotient_closure_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_closure_trace_second. wpo_beta_height_closure_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_closure_trace_second. z = wpo_beta_quotient_closure_trace_second * S ((S (S (l))) * d) + (j))) /\ (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 espo_position_closure_before espo_source_closure_before espo_mate_closure_before. (exists wpo_gap_closure_before_position_bound. wpo_gap_closure_before_position_bound + S (espo_position_closure_before) = l) -> (((exists wpo_beta_height_closure_before_source_entry. wpo_beta_height_closure_before_source_entry + S (espo_source_closure_before) = S ((S (espo_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_source_entry. b = wpo_beta_quotient_closure_before_source_entry * S ((S (espo_position_closure_before)) * c) + (espo_source_closure_before))) -> (((exists wpo_beta_height_closure_before_scaled_entry. wpo_beta_height_closure_before_scaled_entry + S (S espo_mate_closure_before) = S ((S (espo_source_closure_before)) * v)) /\ exists wpo_beta_quotient_closure_before_scaled_entry. u = wpo_beta_quotient_closure_before_scaled_entry * S ((S (espo_source_closure_before)) * v) + (S espo_mate_closure_before))) -> exists espo_mate_position_closure_before. ((exists wpo_gap_closure_before_mate_bound. wpo_gap_closure_before_mate_bound + S (espo_mate_position_closure_before) = l) /\ (((exists wpo_beta_height_closure_before_mate_entry. wpo_beta_height_closure_before_mate_entry + S (espo_mate_closure_before) = S ((S (espo_mate_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_mate_entry. b = wpo_beta_quotient_closure_before_mate_entry * S ((S (espo_mate_position_closure_before)) * c) + (espo_mate_closure_before))))) -> (((exists wpo_beta_height_closure_forward. wpo_beta_height_closure_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_closure_forward. u = wpo_beta_quotient_closure_forward * S ((S (i)) * v) + (S j))) -> (((exists wpo_beta_height_closure_back. wpo_beta_height_closure_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_closure_back. u = wpo_beta_quotient_closure_back * S ((S (j)) * v) + (S i))) -> (forall espo_position_closure_after espo_source_closure_after espo_mate_closure_after. (exists wpo_gap_closure_after_position_bound. wpo_gap_closure_after_position_bound + S (espo_position_closure_after) = S (S l)) -> (((exists wpo_beta_height_closure_after_source_entry. wpo_beta_height_closure_after_source_entry + S (espo_source_closure_after) = S ((S (espo_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_source_entry. z = wpo_beta_quotient_closure_after_source_entry * S ((S (espo_position_closure_after)) * d) + (espo_source_closure_after))) -> (((exists wpo_beta_height_closure_after_scaled_entry. wpo_beta_height_closure_after_scaled_entry + S (S espo_mate_closure_after) = S ((S (espo_source_closure_after)) * v)) /\ exists wpo_beta_quotient_closure_after_scaled_entry. u = wpo_beta_quotient_closure_after_scaled_entry * S ((S (espo_source_closure_after)) * v) + (S espo_mate_closure_after))) -> exists espo_mate_position_closure_after. ((exists wpo_gap_closure_after_mate_bound. wpo_gap_closure_after_mate_bound + S (espo_mate_position_closure_after) = S (S l)) /\ (((exists wpo_beta_height_closure_after_mate_entry. wpo_beta_height_closure_after_mate_entry + S (espo_mate_closure_after) = S ((S (espo_mate_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_mate_entry. z = wpo_beta_quotient_closure_after_mate_entry * S ((S (espo_mate_position_closure_after)) * d) + (espo_mate_closure_after)))))

Proof neighborhood

Direct theorem prerequisites

PA009L beta_prefix_append_two_reflect PA002F beta_at_unique PA003V succ_injective PA001A le_refl PA002O le_succ

Direct theorem dependents

PA009O scaled_inverse_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

119 script commands · 32 reading checkpoints · 9 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 (5)
beta prefix append two reflectbeta at uniquesucc injectivele 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 i
  9. L9
    intro j
  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,i) ∧ (BetaAt(z,d,S l,j) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y)))Definitions: BetaAt(z,d,l,i)BetaAt(z,d,S l,j)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 hscaled
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 = j ∨ (q = l ∧ s = i ∨ 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 i
  8. L31
    specialize beta_prefix_append_two_reflect j
  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 = j ∨ (q = l ∧ s = i ∨ 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_succL42–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_succ : S m = S i
  2. L43
    specialize beta_at_unique u
  3. L44
    specialize beta_at_unique v
  4. L45
    specialize beta_at_unique j
  5. L46
    specialize beta_at_unique (S m)
  6. L47
    specialize beta_at_unique (S i)
  7. L48
    apply beta_at_unique
  8. L49
    rewrite hreflect_left_right at hscaled
  9. L50
    rewrite hreflect_left_right at hscaled
  10. L51
    exact hscaled
10Use earlier factsL52–52

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

  1. L52
    exact hback
11Establish hmateL53–57

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

  1. L53
    have hmate : m = i
  2. L54
    specialize succ_injective m
  3. L55
    specialize succ_injective i
  4. L56
    apply succ_injective
  5. L57
    exact hmate_succ
12Construct an explicit witnessL58–58

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

  1. L58
    exists l
13Separate the logical casesL59–59

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

  1. L59
    split
14Use earlier factsL60–64

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

  1. L60
    specialize le_succ (S l)
  2. L61
    specialize le_succ (S l)
  3. L62
    apply le_succ
  4. L63
    specialize le_refl (S l)
  5. L64
    exact le_refl
15Calculate and transport equalitiesL65–66

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

  1. L65
    rewrite hmate
  2. L66
    rewrite hmate
16Use earlier factsL67–67

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

  1. L67
    exact htrace_parts_left
17Separate the logical casesL68–69

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

  1. L68
    cases hreflect_right
  2. L69
    cases hreflect_right_left
18Establish hmate_succ_secondL70–79

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

  1. L70
    have hmate_succ_second : S m = S j
  2. L71
    specialize beta_at_unique u
  3. L72
    specialize beta_at_unique v
  4. L73
    specialize beta_at_unique i
  5. L74
    specialize beta_at_unique (S m)
  6. L75
    specialize beta_at_unique (S j)
  7. L76
    apply beta_at_unique
  8. L77
    rewrite hreflect_right_left_right at hscaled
  9. L78
    rewrite hreflect_right_left_right at hscaled
  10. L79
    exact hscaled
19Use earlier factsL80–80

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

  1. L80
    exact hforward
20Establish hmate_secondL81–85

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

  1. L81
    have hmate_second : m = j
  2. L82
    specialize succ_injective m
  3. L83
    specialize succ_injective j
  4. L84
    apply succ_injective
  5. L85
    exact hmate_succ_second
21Construct an explicit witnessL86–86

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

  1. L86
    exists (S l)
22Separate the logical casesL87–87

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

  1. L87
    split
23Use earlier factsL88–89

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

  1. L88
    specialize le_refl (S (S l))
  2. L89
    exact le_refl
24Calculate and transport equalitiesL90–91

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

  1. L90
    rewrite hmate_second
  2. L91
    rewrite hmate_second
25Use earlier factsL92–92

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

  1. L92
    exact htrace_parts_right_left
26Separate the logical casesL93–93

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

  1. L93
    cases hreflect_right_right
27Establish hold_occurrenceL94–101

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

  1. L94
    have hold_occurrence : ContainsPrefix(b,c,l,m)Definitions: ContainsPrefix(b,c,l,m)Original native command in the exact edition
  2. L95
    specialize hclosed q
  3. L96
    specialize hclosed s
  4. L97
    specialize hclosed m
  5. L98
    apply hclosed
  6. L99
    exact hreflect_right_right_left
  7. L100
    exact hreflect_right_right_right
  8. L101
    exact hscaled
28Separate the logical casesL102–103

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

  1. L102
    cases hold_occurrence
  2. L103
    cases hold_occurrence_witness
29Construct an explicit witnessL104–104

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

  1. L104
    exists x
30Separate the logical casesL105–105

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

  1. L105
    split
31Establish hliftL106–115

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

  1. L106
  2. L107
    specialize le_succ (S x)
  3. L108
    specialize le_succ l
  4. L109
    apply le_succ
  5. L110
    exact hold_occurrence_witness_left
  6. L111
    specialize le_succ (S x)
  7. L112
    specialize le_succ (S l)
  8. L113
    apply le_succ
  9. L114
    exact hlift
  10. L115
    specialize htrace_parts_right_right x
32Use earlier factsL116–119

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

  1. L116
    specialize htrace_parts_right_right m
  2. L117
    apply htrace_parts_right_right
  3. L118
    exact hold_occurrence_witness_left
  4. L119
    exact hold_occurrence_witness_right

Library-wide reading audit

Original defined command ledger · 119 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro l
  8. 0008intro i
  9. 0009intro j
  10. 0010intro htrace
  11. 0011intro hclosed
  12. 0012intro hforward
  13. 0013intro hback
  14. 0014have htrace_parts : BetaAt(z,d,l,i) ∧ (BetaAt(z,d,S l,j) ∧ (∀ 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 (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_closure_trace_first. z = wpo_beta_quotient_closure_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_closure_trace_second. wpo_beta_height_closure_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_closure_trace_second. z = wpo_beta_quotient_closure_trace_second * S ((S (S (l))) * d) + (j))) /\ (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 hscaled
  24. 0024have hreflect_all : ∀ q. ∀ s. Lt(q,S S l) → BetaAt(z,d,q,s) → q = S l ∧ s = j ∨ (q = l ∧ s = i ∨ 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 = j) \/ ((q = l /\ s = i) \/ ((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 i
  31. 0031specialize beta_prefix_append_two_reflect j
  32. 0032apply beta_prefix_append_two_reflect
  33. 0033exact htrace
  34. 0034have hreflect : q = S l ∧ s = j ∨ (q = l ∧ s = i ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))
    Exact native replay linehave hreflect : ((q = S (l) /\ s = j) \/ ((q = l /\ s = i) \/ ((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_succ : S m = S i
  43. 0043specialize beta_at_unique u
  44. 0044specialize beta_at_unique v
  45. 0045specialize beta_at_unique j
  46. 0046specialize beta_at_unique (S m)
  47. 0047specialize beta_at_unique (S i)
  48. 0048apply beta_at_unique
  49. 0049rewrite hreflect_left_right at hscaled
  50. 0050rewrite hreflect_left_right at hscaled
  51. 0051exact hscaled
  52. 0052exact hback
  53. 0053have hmate : m = i
  54. 0054specialize succ_injective m
  55. 0055specialize succ_injective i
  56. 0056apply succ_injective
  57. 0057exact hmate_succ
  58. 0058exists l
  59. 0059split
  60. 0060specialize le_succ (S l)
  61. 0061specialize le_succ (S l)
  62. 0062apply le_succ
  63. 0063specialize le_refl (S l)
  64. 0064exact le_refl
  65. 0065rewrite hmate
  66. 0066rewrite hmate
  67. 0067exact htrace_parts_left
  68. 0068cases hreflect_right
  69. 0069cases hreflect_right_left
  70. 0070have hmate_succ_second : S m = S j
  71. 0071specialize beta_at_unique u
  72. 0072specialize beta_at_unique v
  73. 0073specialize beta_at_unique i
  74. 0074specialize beta_at_unique (S m)
  75. 0075specialize beta_at_unique (S j)
  76. 0076apply beta_at_unique
  77. 0077rewrite hreflect_right_left_right at hscaled
  78. 0078rewrite hreflect_right_left_right at hscaled
  79. 0079exact hscaled
  80. 0080exact hforward
  81. 0081have hmate_second : m = j
  82. 0082specialize succ_injective m
  83. 0083specialize succ_injective j
  84. 0084apply succ_injective
  85. 0085exact hmate_succ_second
  86. 0086exists (S l)
  87. 0087split
  88. 0088specialize le_refl (S (S l))
  89. 0089exact le_refl
  90. 0090rewrite hmate_second
  91. 0091rewrite hmate_second
  92. 0092exact htrace_parts_right_left
  93. 0093cases hreflect_right_right
  94. 0094have 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))))
  95. 0095specialize hclosed q
  96. 0096specialize hclosed s
  97. 0097specialize hclosed m
  98. 0098apply hclosed
  99. 0099exact hreflect_right_right_left
  100. 0100exact hreflect_right_right_right
  101. 0101exact hscaled
  102. 0102cases hold_occurrence
  103. 0103cases hold_occurrence_witness
  104. 0104exists x
  105. 0105split
  106. 0106have hlift : Lt(x,S l)
    Exact native replay linehave hlift : exists h. h + S x = S l
  107. 0107specialize le_succ (S x)
  108. 0108specialize le_succ l
  109. 0109apply le_succ
  110. 0110exact hold_occurrence_witness_left
  111. 0111specialize le_succ (S x)
  112. 0112specialize le_succ (S l)
  113. 0113apply le_succ
  114. 0114exact hlift
  115. 0115specialize htrace_parts_right_right x
  116. 0116specialize htrace_parts_right_right m
  117. 0117apply htrace_parts_right_right
  118. 0118exact hold_occurrence_witness_left
  119. 0119exact hold_occurrence_witness_right