eisenstein_initial_segment_bit_count_functional

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 q
2. 0002intro b
3. 0003intro c
4. 0004induction k
5. 0005intro n
6. 0006intro hprefix
7. 0007intro hqk
8. 0008intro hcount
9. 0009have hq0 : q = 0
10. 0010specialize le_zero q
11. 0011apply le_zero
12. 0012exact hqk
13. 0013have hn0 : n = 0
14. 0014specialize bit_count_zero b
15. 0015specialize bit_count_zero c
16. 0016specialize bit_count_zero 0
17. 0017specialize bit_count_zero n
18. 0018apply bit_count_zero
19. 0019refl
20. 0020exact hcount
21. 0021trans 0
22. 0022exact hn0
23. 0023symm
24. 0024exact hq0
25. 0025intro n
26. 0026intro hprefix
27. 0027intro hqk
28. 0028intro hcount
29. 0029have hsplit : q = S k \/ exists gap. gap + S q = S k
30. 0030specialize le_eq_or_lt q
31. 0031specialize le_eq_or_lt (S k)
32. 0032apply le_eq_or_lt
33. 0033exact hqk
34. 0034cases hsplit
35. 0035have hallone : forall eis_one_index_initial_segment_functional_all_one. (exists eis_lt_gap_initial_segment_functional_all_one_bound. eis_lt_gap_initial_segment_functional_all_one_bound + S (eis_one_index_initial_segment_functional_all_one) = S k) -> (((exists ff_h_eis_initial_segment_functional_all_one_decoded. ff_h_eis_initial_segment_functional_all_one_decoded + S (1) = S ((S (eis_one_index_initial_segment_functional_all_one)) * c)) /\ exists ff_q_eis_initial_segment_functional_all_one_decoded. b = ff_q_eis_initial_segment_functional_all_one_decoded * S ((S (eis_one_index_initial_segment_functional_all_one)) * c) + (1)))
36. 0036intro j
37. 0037intro hj
38. 0038have hstored : exists bit. ((((exists ff_h_initial_segment_functional_stored. ff_h_initial_segment_functional_stored + S (bit) = S ((S (j)) * c)) /\ exists ff_q_initial_segment_functional_stored. b = ff_q_initial_segment_functional_stored * S ((S (j)) * c) + (bit))) /\ (((bit = 1 /\ (exists eis_le_gap_initial_segment_functional_stored_choice_inside. eis_le_gap_initial_segment_functional_stored_choice_inside + (S j) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_functional_stored_choice_outside. eis_lt_gap_initial_segment_functional_stored_choice_outside + S (q) = S j)))))
39. 0039specialize hprefix j
40. 0040apply hprefix
41. 0041exact hj
42. 0042cases hstored
43. 0043cases hstored_witness
44. 0044cases hstored_witness_right
45. 0045cases hstored_witness_right_left
46. 0046have hbit_one : x = 1
47. 0047exact hstored_witness_right_left_left
48. 0048rewrite hbit_one at hstored_witness_left
49. 0049rewrite hbit_one at hstored_witness_left
50. 0050exact hstored_witness_left
51. 0051cases hstored_witness_right_right
52. 0052exfalso
53. 0053rewrite hsplit_left at hstored_witness_right_right_right
54. 0054specialize lt_not_le (S k)
55. 0055specialize lt_not_le (S j)
56. 0056apply lt_not_le
57. 0057exact hstored_witness_right_right_right
58. 0058exact hj
59. 0059have hn : n = S k
60. 0060specialize beta_all_one_bit_count_exact b
61. 0061specialize beta_all_one_bit_count_exact c
62. 0062specialize beta_all_one_bit_count_exact (S k)
63. 0063specialize beta_all_one_bit_count_exact n
64. 0064apply beta_all_one_bit_count_exact
65. 0065exact hallone
66. 0066exact hcount
67. 0067trans S k
68. 0068exact hn
69. 0069symm
70. 0070exact hsplit_left
71. 0071have hqk_previous : exists gap. gap + q = k
72. 0072specialize le_of_succ_le_succ q
73. 0073specialize le_of_succ_le_succ k
74. 0074apply le_of_succ_le_succ
75. 0075exact hsplit_right
76. 0076have hprevious : forall eis_index_initial_segment_functional_previous. (exists eis_lt_gap_initial_segment_functional_previous_bound. eis_lt_gap_initial_segment_functional_previous_bound + S (eis_index_initial_segment_functional_previous) = k) -> exists eis_bit_initial_segment_functional_previous. ((((exists ff_h_eis_initial_segment_functional_previous_decoded. ff_h_eis_initial_segment_functional_previous_decoded + S (eis_bit_initial_segment_functional_previous) = S ((S (eis_index_initial_segment_functional_previous)) * c)) /\ exists ff_q_eis_initial_segment_functional_previous_decoded. b = ff_q_eis_initial_segment_functional_previous_decoded * S ((S (eis_index_initial_segment_functional_previous)) * c) + (eis_bit_initial_segment_functional_previous))) /\ (((eis_bit_initial_segment_functional_previous = 1 /\ (exists eis_le_gap_initial_segment_functional_previous_choice_inside. eis_le_gap_initial_segment_functional_previous_choice_inside + (S eis_index_initial_segment_functional_previous) = q)) \/ (eis_bit_initial_segment_functional_previous = 0 /\ (exists eis_lt_gap_initial_segment_functional_previous_choice_outside. eis_lt_gap_initial_segment_functional_previous_choice_outside + S (q) = S eis_index_initial_segment_functional_previous)))))
77. 0077intro j
78. 0078intro hj
79. 0079specialize hprefix j
80. 0080apply hprefix
81. 0081specialize le_succ (S j)
82. 0082specialize le_succ k
83. 0083apply le_succ
84. 0084exact hj
85. 0085have hdecomp : exists a r. (((exists ff_h_initial_segment_functional_last. ff_h_initial_segment_functional_last + S (a) = S ((S (k)) * c)) /\ exists ff_q_initial_segment_functional_last. b = ff_q_initial_segment_functional_last * S ((S (k)) * c) + (a))) /\ ((((exists ff_u_initial_segment_functional_prefix_count_sum ff_v_initial_segment_functional_prefix_count_sum. ((((exists ff_h_initial_segment_functional_prefix_count_sum_start. ff_h_initial_segment_functional_prefix_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_start. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_start * S ((S (0)) * ff_v_initial_segment_functional_prefix_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_terminal. ff_h_initial_segment_functional_prefix_count_sum_terminal + S (r) = S ((S (k)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_terminal. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_functional_prefix_count_sum) + (r))) /\ forall ff_i_initial_segment_functional_prefix_count_sum. (exists ff_lt_initial_segment_functional_prefix_count_sum_bound. ff_lt_initial_segment_functional_prefix_count_sum_bound + S ff_i_initial_segment_functional_prefix_count_sum = k) -> exists ff_a_initial_segment_functional_prefix_count_sum ff_r_initial_segment_functional_prefix_count_sum ff_s_initial_segment_functional_prefix_count_sum. ((((exists ff_h_initial_segment_functional_prefix_count_sum_summand. ff_h_initial_segment_functional_prefix_count_sum_summand + S (ff_a_initial_segment_functional_prefix_count_sum) = S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * c)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_summand. b = ff_q_initial_segment_functional_prefix_count_sum_summand * S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * c) + (ff_a_initial_segment_functional_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_partial. ff_h_initial_segment_functional_prefix_count_sum_partial + S (ff_r_initial_segment_functional_prefix_count_sum) = S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_partial. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_partial * S ((S (ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum) + (ff_r_initial_segment_functional_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_functional_prefix_count_sum_successor. ff_h_initial_segment_functional_prefix_count_sum_successor + S (ff_s_initial_segment_functional_prefix_count_sum) = S ((S (S ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum)) /\ exists ff_q_initial_segment_functional_prefix_count_sum_successor. ff_u_initial_segment_functional_prefix_count_sum = ff_q_initial_segment_functional_prefix_count_sum_successor * S ((S (S ff_i_initial_segment_functional_prefix_count_sum)) * ff_v_initial_segment_functional_prefix_count_sum) + (ff_s_initial_segment_functional_prefix_count_sum))) /\ ff_s_initial_segment_functional_prefix_count_sum = ff_r_initial_segment_functional_prefix_count_sum + ff_a_initial_segment_functional_prefix_count_sum)))))) /\ (forall ff_i_initial_segment_functional_prefix_count_bits. (exists ff_lt_initial_segment_functional_prefix_count_bits_bound. ff_lt_initial_segment_functional_prefix_count_bits_bound + S ff_i_initial_segment_functional_prefix_count_bits = k) -> exists ff_bit_initial_segment_functional_prefix_count_bits. ((((exists ff_h_initial_segment_functional_prefix_count_bits_decoded. ff_h_initial_segment_functional_prefix_count_bits_decoded + S (ff_bit_initial_segment_functional_prefix_count_bits) = S ((S (ff_i_initial_segment_functional_prefix_count_bits)) * c)) /\ exists ff_q_initial_segment_functional_prefix_count_bits_decoded. b = ff_q_initial_segment_functional_prefix_count_bits_decoded * S ((S (ff_i_initial_segment_functional_prefix_count_bits)) * c) + (ff_bit_initial_segment_functional_prefix_count_bits))) /\ (ff_bit_initial_segment_functional_prefix_count_bits = 0 \/ ff_bit_initial_segment_functional_prefix_count_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
86. 0086specialize bit_count_succ_decompose b
87. 0087specialize bit_count_succ_decompose c
88. 0088specialize bit_count_succ_decompose k
89. 0089specialize bit_count_succ_decompose (S k)
90. 0090specialize bit_count_succ_decompose n
91. 0091apply bit_count_succ_decompose
92. 0092refl
93. 0093exact hcount
94. 0094cases hdecomp
95. 0095cases hdecomp_witness
96. 0096cases hdecomp_witness_witness
97. 0097cases hdecomp_witness_witness_right
98. 0098cases hdecomp_witness_witness_right_right
99. 0099have hlast_choice : ((x = 1 /\ (exists eis_le_gap_initial_segment_functional_last_choice_inside. eis_le_gap_initial_segment_functional_last_choice_inside + (S k) = q)) \/ (x = 0 /\ (exists eis_lt_gap_initial_segment_functional_last_choice_outside. eis_lt_gap_initial_segment_functional_last_choice_outside + S (q) = S k)))
100. 0100specialize eisenstein_initial_segment_decoded_choice q
101. 0101specialize eisenstein_initial_segment_decoded_choice b
102. 0102specialize eisenstein_initial_segment_decoded_choice c
103. 0103specialize eisenstein_initial_segment_decoded_choice (S k)
104. 0104specialize eisenstein_initial_segment_decoded_choice k
105. 0105specialize eisenstein_initial_segment_decoded_choice x
106. 0106apply eisenstein_initial_segment_decoded_choice
107. 0107exact hprefix
108. 0108specialize le_refl (S k)
109. 0109exact le_refl
110. 0110exact hdecomp_witness_witness_left
111. 0111cases hlast_choice
112. 0112cases hlast_choice_left
113. 0113exfalso
114. 0114specialize lt_not_le q
115. 0115specialize lt_not_le (S k)
116. 0116apply lt_not_le
117. 0117exact hsplit_right
118. 0118exact hlast_choice_left_right
119. 0119cases hlast_choice_right
120. 0120have hrq : x1 = q
121. 0121specialize IH x1
122. 0122apply IH
123. 0123exact hprevious
124. 0124exact hqk_previous
125. 0125exact hdecomp_witness_witness_right_left
126. 0126rewrite hdecomp_witness_witness_right_right_right
127. 0127rewrite hrq
128. 0128rewrite hlast_choice_right_left
129. 0129apply PA3