finite_short_cover_impossible

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 hln
6. 0006intro hcover
7. 0007have 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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