PA009L

beta_prefix_append_two_reflect

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

Every entry of a two-appended prefix is the second append, the first append, or an old entry.

Exact expanded PA statement

forall b c z d l a e. (((((exists wpo_beta_height_reflect_trace_first. wpo_beta_height_reflect_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_reflect_trace_first. z = wpo_beta_quotient_reflect_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_reflect_trace_second. wpo_beta_height_reflect_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_reflect_trace_second. z = wpo_beta_quotient_reflect_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_reflect_trace wpo_old_value_reflect_trace. (exists wpo_gap_reflect_trace_old_bound. wpo_gap_reflect_trace_old_bound + S (wpo_old_index_reflect_trace) = l) -> (((exists wpo_beta_height_reflect_trace_old_entry. wpo_beta_height_reflect_trace_old_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * c)) /\ exists wpo_beta_quotient_reflect_trace_old_entry. b = wpo_beta_quotient_reflect_trace_old_entry * S ((S (wpo_old_index_reflect_trace)) * c) + (wpo_old_value_reflect_trace))) -> (((exists wpo_beta_height_reflect_trace_new_entry. wpo_beta_height_reflect_trace_new_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * d)) /\ exists wpo_beta_quotient_reflect_trace_new_entry. z = wpo_beta_quotient_reflect_trace_new_entry * S ((S (wpo_old_index_reflect_trace)) * d) + (wpo_old_value_reflect_trace))))))) -> forall i v. (exists wpo_gap_reflect_new_bound. wpo_gap_reflect_new_bound + S (i) = S (S l)) -> (((exists wpo_beta_height_reflect_new_entry. wpo_beta_height_reflect_new_entry + S (v) = S ((S (i)) * d)) /\ exists wpo_beta_quotient_reflect_new_entry. z = wpo_beta_quotient_reflect_new_entry * S ((S (i)) * d) + (v))) -> (((i = S (l) /\ v = e) \/ ((i = l /\ v = a) \/ ((exists wpo_gap_reflect_result_old_bound. wpo_gap_reflect_result_old_bound + S (i) = l) /\ (((exists wpo_beta_height_reflect_result_old_entry. wpo_beta_height_reflect_result_old_entry + S (v) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_reflect_result_old_entry. b = wpo_beta_quotient_reflect_result_old_entry * S ((S (i)) * c) + (v)))))))

Structural proof guide

Generated structural guide

Every entry of a two-appended prefix is the second append, the first append, or an old entry.

Use the direct prerequisites finite_lt_succ_eq_or_lt, beta_at_exists, beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (7), equality transport (6).

Referenced ingredients

PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique

Direct dependents

PA009M beta_prefix_append_two_scaled_orbit_closed PA009N beta_prefix_append_two_injective PA00AT beta_prefix_append_two_orbit_closed PA00AU beta_prefix_append_two_nonendpoint

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro l
  6. 0006intro a
  7. 0007intro e
  8. 0008intro htrace
  9. 0009cases htrace
  10. 0010cases htrace_right
  11. 0011intro i
  12. 0012intro v
  13. 0013intro hi
  14. 0014intro hentry
  15. 0015have htop : i = S l \/ exists h. h + S i = S l
  16. 0016specialize finite_lt_succ_eq_or_lt (S l)
  17. 0017specialize finite_lt_succ_eq_or_lt i
  18. 0018apply finite_lt_succ_eq_or_lt
  19. 0019exact hi
  20. 0020cases htop
  21. 0021left
  22. 0022split
  23. 0023exact htop_left
  24. 0024have hive : v = e
  25. 0025specialize beta_at_unique z
  26. 0026specialize beta_at_unique d
  27. 0027specialize beta_at_unique (S l)
  28. 0028specialize beta_at_unique v
  29. 0029specialize beta_at_unique e
  30. 0030apply beta_at_unique
  31. 0031rewrite htop_left at hentry
  32. 0032rewrite htop_left at hentry
  33. 0033exact hentry
  34. 0034exact htrace_right_left
  35. 0035exact hive
  36. 0036have hmiddle : i = l \/ exists h. h + S i = l
  37. 0037specialize finite_lt_succ_eq_or_lt l
  38. 0038specialize finite_lt_succ_eq_or_lt i
  39. 0039apply finite_lt_succ_eq_or_lt
  40. 0040exact htop_right
  41. 0041cases hmiddle
  42. 0042right
  43. 0043left
  44. 0044split
  45. 0045exact hmiddle_left
  46. 0046have hiva : v = a
  47. 0047specialize beta_at_unique z
  48. 0048specialize beta_at_unique d
  49. 0049specialize beta_at_unique l
  50. 0050specialize beta_at_unique v
  51. 0051specialize beta_at_unique a
  52. 0052apply beta_at_unique
  53. 0053rewrite hmiddle_left at hentry
  54. 0054rewrite hmiddle_left at hentry
  55. 0055exact hentry
  56. 0056exact htrace_left
  57. 0057exact hiva
  58. 0058have hold : exists w. (((exists wpo_beta_height_reflect_old_exists_entry. wpo_beta_height_reflect_old_exists_entry + S (w) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_reflect_old_exists_entry. b = wpo_beta_quotient_reflect_old_exists_entry * S ((S (i)) * c) + (w)))
  59. 0059specialize beta_at_exists b
  60. 0060specialize beta_at_exists c
  61. 0061specialize beta_at_exists i
  62. 0062exact beta_at_exists
  63. 0063cases hold
  64. 0064have hnew_old : ((exists h. h + S x = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + x)
  65. 0065specialize htrace_right_right i
  66. 0066specialize htrace_right_right x
  67. 0067apply htrace_right_right
  68. 0068exact hmiddle_right
  69. 0069exact hold_witness
  70. 0070have hivx : v = x
  71. 0071specialize beta_at_unique z
  72. 0072specialize beta_at_unique d
  73. 0073specialize beta_at_unique i
  74. 0074specialize beta_at_unique v
  75. 0075specialize beta_at_unique x
  76. 0076apply beta_at_unique
  77. 0077exact hentry
  78. 0078exact hnew_old
  79. 0079right
  80. 0080right
  81. 0081split
  82. 0082exact hmiddle_right
  83. 0083rewrite <- hivx at hold_witness
  84. 0084rewrite <- hivx at hold_witness
  85. 0085exact hold_witness