finite_prefix_choose_unused_nonendpoint

Proof neighborhood

Direct dependencies

Direct dependents

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 l
4. 0004intro n
5. 0005intro r
6. 0006intro hnr
7. 0007intro hshort
8. 0008have haugmented : exists z d. (((((exists wpo_beta_height_choose_augmented_trace_first. wpo_beta_height_choose_augmented_trace_first + S (0) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_choose_augmented_trace_first. z = wpo_beta_quotient_choose_augmented_trace_first * S ((S (l)) * d) + (0))) /\ ((((exists wpo_beta_height_choose_augmented_trace_second. wpo_beta_height_choose_augmented_trace_second + S (r) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_choose_augmented_trace_second. z = wpo_beta_quotient_choose_augmented_trace_second * S ((S (S (l))) * d) + (r))) /\ (forall wpo_old_index_choose_augmented_trace wpo_old_value_choose_augmented_trace. (exists wpo_gap_choose_augmented_trace_old_bound. wpo_gap_choose_augmented_trace_old_bound + S (wpo_old_index_choose_augmented_trace) = l) -> (((exists wpo_beta_height_choose_augmented_trace_old_entry. wpo_beta_height_choose_augmented_trace_old_entry + S (wpo_old_value_choose_augmented_trace) = S ((S (wpo_old_index_choose_augmented_trace)) * c)) /\ exists wpo_beta_quotient_choose_augmented_trace_old_entry. b = wpo_beta_quotient_choose_augmented_trace_old_entry * S ((S (wpo_old_index_choose_augmented_trace)) * c) + (wpo_old_value_choose_augmented_trace))) -> (((exists wpo_beta_height_choose_augmented_trace_new_entry. wpo_beta_height_choose_augmented_trace_new_entry + S (wpo_old_value_choose_augmented_trace) = S ((S (wpo_old_index_choose_augmented_trace)) * d)) /\ exists wpo_beta_quotient_choose_augmented_trace_new_entry. z = wpo_beta_quotient_choose_augmented_trace_new_entry * S ((S (wpo_old_index_choose_augmented_trace)) * d) + (wpo_old_value_choose_augmented_trace)))))))
9. 0009specialize beta_prefix_append_two_exists b
10. 0010specialize beta_prefix_append_two_exists c
11. 0011specialize beta_prefix_append_two_exists l
12. 0012specialize beta_prefix_append_two_exists 0
13. 0013specialize beta_prefix_append_two_exists r
14. 0014exact beta_prefix_append_two_exists
15. 0015cases haugmented
16. 0016cases haugmented_witness
17. 0017have homitted : exists wpo_value_choose_augmented_omit. ((exists wpo_gap_choose_augmented_omit_value_bound. wpo_gap_choose_augmented_omit_value_bound + S (wpo_value_choose_augmented_omit) = n) /\ (~(exists wpo_index_choose_augmented_omit_omitted_contains. ((exists wpo_gap_choose_augmented_omit_omitted_contains_bound. wpo_gap_choose_augmented_omit_omitted_contains_bound + S (wpo_index_choose_augmented_omit_omitted_contains) = S (S l)) /\ (((exists wpo_beta_height_choose_augmented_omit_omitted_contains_entry. wpo_beta_height_choose_augmented_omit_omitted_contains_entry + S (wpo_value_choose_augmented_omit) = S ((S (wpo_index_choose_augmented_omit_omitted_contains)) * x1)) /\ exists wpo_beta_quotient_choose_augmented_omit_omitted_contains_entry. x = wpo_beta_quotient_choose_augmented_omit_omitted_contains_entry * S ((S (wpo_index_choose_augmented_omit_omitted_contains)) * x1) + (wpo_value_choose_augmented_omit)))))))
18. 0018specialize finite_short_prefix_omits x
19. 0019specialize finite_short_prefix_omits x1
20. 0020specialize finite_short_prefix_omits (S (S l))
21. 0021specialize finite_short_prefix_omits n
22. 0022apply finite_short_prefix_omits
23. 0023exact hshort
24. 0024cases homitted
25. 0025cases homitted_witness
26. 0026cases haugmented_witness_witness
27. 0027cases haugmented_witness_witness_right
28. 0028exists x2
29. 0029split
30. 0030exact homitted_witness_left
31. 0031split
32. 0032split
33. 0033intro hxzero
34. 0034apply homitted_witness_right
35. 0035exists l
36. 0036split
37. 0037specialize le_succ (S l)
38. 0038specialize le_succ (S l)
39. 0039apply le_succ
40. 0040specialize le_refl (S l)
41. 0041exact le_refl
42. 0042rewrite hxzero
43. 0043rewrite hxzero
44. 0044exact haugmented_witness_witness_left
45. 0045intro hxlast
46. 0046have hxr : x2 = r
47. 0047specialize succ_injective x2
48. 0048specialize succ_injective r
49. 0049apply succ_injective
50. 0050trans n
51. 0051exact hxlast
52. 0052exact hnr
53. 0053apply homitted_witness_right
54. 0054exists (S l)
55. 0055split
56. 0056specialize le_refl (S (S l))
57. 0057exact le_refl
58. 0058rewrite hxr
59. 0059rewrite hxr
60. 0060exact haugmented_witness_witness_right_left
61. 0061have hold_omit : ~(exists wpo_index_choose_old_omit_y_contains. ((exists wpo_gap_choose_old_omit_y_contains_bound. wpo_gap_choose_old_omit_y_contains_bound + S (wpo_index_choose_old_omit_y_contains) = l) /\ (((exists wpo_beta_height_choose_old_omit_y_contains_entry. wpo_beta_height_choose_old_omit_y_contains_entry + S (x2) = S ((S (wpo_index_choose_old_omit_y_contains)) * c)) /\ exists wpo_beta_quotient_choose_old_omit_y_contains_entry. b = wpo_beta_quotient_choose_old_omit_y_contains_entry * S ((S (wpo_index_choose_old_omit_y_contains)) * c) + (x2)))))
62. 0062intro hold_contains
63. 0063cases hold_contains
64. 0064cases hold_contains_witness
65. 0065have hlift : exists h. h + S x3 = S l
66. 0066specialize le_succ (S x3)
67. 0067specialize le_succ l
68. 0068apply le_succ
69. 0069exact hold_contains_witness_left
70. 0070have hlift2 : exists h. h + S x3 = S (S l)
71. 0071specialize le_succ (S x3)
72. 0072specialize le_succ (S l)
73. 0073apply le_succ
74. 0074exact hlift
75. 0075have hnew_entry : ((exists h. h + S x2 = S ((S x3) * x1)) /\ exists q. x = q * S ((S x3) * x1) + x2)
76. 0076specialize haugmented_witness_witness_right_right x3
77. 0077specialize haugmented_witness_witness_right_right x2
78. 0078apply haugmented_witness_witness_right_right
79. 0079exact hold_contains_witness_left
80. 0080exact hold_contains_witness_right
81. 0081apply homitted_witness_right
82. 0082exists x3
83. 0083split
84. 0084exact hlift2
85. 0085exact hnew_entry
86. 0086exact hold_omit