beta_sign_factor_product_power

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 sb
2. 0002intro sc
3. 0003intro fb
4. 0004intro fc
5. 0005intro r
6. 0006induction l
7. 0007intro e
8. 0008intro F
9. 0009intro R
10. 0010intro hcount
11. 0011intro hsigns
12. 0012intro hproduct
13. 0013intro hpower
14. 0014have he0 : e = 0
15. 0015specialize bit_count_zero sb
16. 0016specialize bit_count_zero sc
17. 0017specialize bit_count_zero 0
18. 0018specialize bit_count_zero e
19. 0019apply bit_count_zero
20. 0020refl
21. 0021exact hcount
22. 0022have hF1 : F = 1
23. 0023specialize beta_product_zero fb
24. 0024specialize beta_product_zero fc
25. 0025specialize beta_product_zero F
26. 0026apply beta_product_zero
27. 0027exact hproduct
28. 0028have hR1 : R = 1
29. 0029specialize pow_zero r
30. 0030specialize pow_zero e
31. 0031specialize pow_zero R
32. 0032apply pow_zero
33. 0033exact he0
34. 0034exact hpower
35. 0035trans 1
36. 0036exact hF1
37. 0037symm
38. 0038exact hR1
39. 0039intro e
40. 0040intro F
41. 0041intro R
42. 0042intro hcount
43. 0043intro hsigns
44. 0044intro hproduct
45. 0045intro hpower
46. 0046have hcount_decomp : exists a k. (((exists ff_h_sign_product_last_bit. ff_h_sign_product_last_bit + S (a) = S ((S (l)) * sc)) /\ exists ff_q_sign_product_last_bit. sb = ff_q_sign_product_last_bit * S ((S (l)) * sc) + (a))) /\ ((((exists ff_u_sign_product_prefix_count_sum ff_v_sign_product_prefix_count_sum. ((((exists ff_h_sign_product_prefix_count_sum_start. ff_h_sign_product_prefix_count_sum_start + S (0) = S ((S (0)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_start. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_start * S ((S (0)) * ff_v_sign_product_prefix_count_sum) + (0))) /\ ((((exists ff_h_sign_product_prefix_count_sum_terminal. ff_h_sign_product_prefix_count_sum_terminal + S (k) = S ((S (l)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_terminal. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_terminal * S ((S (l)) * ff_v_sign_product_prefix_count_sum) + (k))) /\ forall ff_i_sign_product_prefix_count_sum. (exists ff_lt_sign_product_prefix_count_sum_bound. ff_lt_sign_product_prefix_count_sum_bound + S ff_i_sign_product_prefix_count_sum = l) -> exists ff_a_sign_product_prefix_count_sum ff_r_sign_product_prefix_count_sum ff_s_sign_product_prefix_count_sum. ((((exists ff_h_sign_product_prefix_count_sum_summand. ff_h_sign_product_prefix_count_sum_summand + S (ff_a_sign_product_prefix_count_sum) = S ((S (ff_i_sign_product_prefix_count_sum)) * sc)) /\ exists ff_q_sign_product_prefix_count_sum_summand. sb = ff_q_sign_product_prefix_count_sum_summand * S ((S (ff_i_sign_product_prefix_count_sum)) * sc) + (ff_a_sign_product_prefix_count_sum))) /\ ((((exists ff_h_sign_product_prefix_count_sum_partial. ff_h_sign_product_prefix_count_sum_partial + S (ff_r_sign_product_prefix_count_sum) = S ((S (ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_partial. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_partial * S ((S (ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum) + (ff_r_sign_product_prefix_count_sum))) /\ ((((exists ff_h_sign_product_prefix_count_sum_successor. ff_h_sign_product_prefix_count_sum_successor + S (ff_s_sign_product_prefix_count_sum) = S ((S (S ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum)) /\ exists ff_q_sign_product_prefix_count_sum_successor. ff_u_sign_product_prefix_count_sum = ff_q_sign_product_prefix_count_sum_successor * S ((S (S ff_i_sign_product_prefix_count_sum)) * ff_v_sign_product_prefix_count_sum) + (ff_s_sign_product_prefix_count_sum))) /\ ff_s_sign_product_prefix_count_sum = ff_r_sign_product_prefix_count_sum + ff_a_sign_product_prefix_count_sum)))))) /\ (forall ff_i_sign_product_prefix_count_bits. (exists ff_lt_sign_product_prefix_count_bits_bound. ff_lt_sign_product_prefix_count_bits_bound + S ff_i_sign_product_prefix_count_bits = l) -> exists ff_bit_sign_product_prefix_count_bits. ((((exists ff_h_sign_product_prefix_count_bits_decoded. ff_h_sign_product_prefix_count_bits_decoded + S (ff_bit_sign_product_prefix_count_bits) = S ((S (ff_i_sign_product_prefix_count_bits)) * sc)) /\ exists ff_q_sign_product_prefix_count_bits_decoded. sb = ff_q_sign_product_prefix_count_bits_decoded * S ((S (ff_i_sign_product_prefix_count_bits)) * sc) + (ff_bit_sign_product_prefix_count_bits))) /\ (ff_bit_sign_product_prefix_count_bits = 0 \/ ff_bit_sign_product_prefix_count_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ e = k + a))
47. 0047specialize bit_count_succ_decompose sb
48. 0048specialize bit_count_succ_decompose sc
49. 0049specialize bit_count_succ_decompose l
50. 0050specialize bit_count_succ_decompose (S l)
51. 0051specialize bit_count_succ_decompose e
52. 0052apply bit_count_succ_decompose
53. 0053refl
54. 0054exact hcount
55. 0055cases hcount_decomp
56. 0056cases hcount_decomp_witness
57. 0057cases hcount_decomp_witness_witness
58. 0058cases hcount_decomp_witness_witness_right
59. 0059cases hcount_decomp_witness_witness_right_right
60. 0060have hproduct_decomp : exists f G. (((exists ff_h_sign_product_last_factor. ff_h_sign_product_last_factor + S (f) = S ((S (l)) * fc)) /\ exists ff_q_sign_product_last_factor. fb = ff_q_sign_product_last_factor * S ((S (l)) * fc) + (f))) /\ ((exists ff_u_sign_product_prefix_product ff_v_sign_product_prefix_product. ((((exists ff_h_sign_product_prefix_product_start. ff_h_sign_product_prefix_product_start + S (1) = S ((S (0)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_start. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_start * S ((S (0)) * ff_v_sign_product_prefix_product) + (1))) /\ ((((exists ff_h_sign_product_prefix_product_terminal. ff_h_sign_product_prefix_product_terminal + S (G) = S ((S (l)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_terminal. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_terminal * S ((S (l)) * ff_v_sign_product_prefix_product) + (G))) /\ forall ff_i_sign_product_prefix_product. (exists ff_lt_sign_product_prefix_product_bound. ff_lt_sign_product_prefix_product_bound + S ff_i_sign_product_prefix_product = l) -> exists ff_p_sign_product_prefix_product ff_r_sign_product_prefix_product ff_s_sign_product_prefix_product. ((((exists ff_h_sign_product_prefix_product_factor. ff_h_sign_product_prefix_product_factor + S (ff_p_sign_product_prefix_product) = S ((S (ff_i_sign_product_prefix_product)) * fc)) /\ exists ff_q_sign_product_prefix_product_factor. fb = ff_q_sign_product_prefix_product_factor * S ((S (ff_i_sign_product_prefix_product)) * fc) + (ff_p_sign_product_prefix_product))) /\ ((((exists ff_h_sign_product_prefix_product_partial. ff_h_sign_product_prefix_product_partial + S (ff_r_sign_product_prefix_product) = S ((S (ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_partial. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_partial * S ((S (ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product) + (ff_r_sign_product_prefix_product))) /\ ((((exists ff_h_sign_product_prefix_product_successor. ff_h_sign_product_prefix_product_successor + S (ff_s_sign_product_prefix_product) = S ((S (S ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product)) /\ exists ff_q_sign_product_prefix_product_successor. ff_u_sign_product_prefix_product = ff_q_sign_product_prefix_product_successor * S ((S (S ff_i_sign_product_prefix_product)) * ff_v_sign_product_prefix_product) + (ff_s_sign_product_prefix_product))) /\ ff_s_sign_product_prefix_product = ff_r_sign_product_prefix_product * ff_p_sign_product_prefix_product)))))) /\ F = G * f)
61. 0061specialize beta_product_succ_decompose fb
62. 0062specialize beta_product_succ_decompose fc
63. 0063specialize beta_product_succ_decompose l
64. 0064specialize beta_product_succ_decompose F
65. 0065apply beta_product_succ_decompose
66. 0066exact hproduct
67. 0067cases hproduct_decomp
68. 0068cases hproduct_decomp_witness
69. 0069cases hproduct_decomp_witness_witness
70. 0070cases hproduct_decomp_witness_witness_right
71. 0071have hprefix_signs : forall gspf_index_sign_product_restricted_signs gspf_bit_sign_product_restricted_signs. (exists gsp_lt_gap_sign_product_restricted_signs_bound. gsp_lt_gap_sign_product_restricted_signs_bound + S gspf_index_sign_product_restricted_signs = l) -> (((exists ff_h_gspf_sign_product_restricted_signs_bit. ff_h_gspf_sign_product_restricted_signs_bit + S (gspf_bit_sign_product_restricted_signs) = S ((S (gspf_index_sign_product_restricted_signs)) * sc)) /\ exists ff_q_gspf_sign_product_restricted_signs_bit. sb = ff_q_gspf_sign_product_restricted_signs_bit * S ((S (gspf_index_sign_product_restricted_signs)) * sc) + (gspf_bit_sign_product_restricted_signs))) -> (((gspf_bit_sign_product_restricted_signs = 0) /\ (((exists gsp_beta_height_gspf_sign_product_restricted_signs_one. gsp_beta_height_gspf_sign_product_restricted_signs_one + S (1) = S ((S (gspf_index_sign_product_restricted_signs)) * fc)) /\ exists gsp_beta_quotient_gspf_sign_product_restricted_signs_one. fb = gsp_beta_quotient_gspf_sign_product_restricted_signs_one * S ((S (gspf_index_sign_product_restricted_signs)) * fc) + (1)))) \/ ((gspf_bit_sign_product_restricted_signs = 1) /\ (((exists ff_h_gspf_sign_product_restricted_signs_predecessor. ff_h_gspf_sign_product_restricted_signs_predecessor + S (r) = S ((S (gspf_index_sign_product_restricted_signs)) * fc)) /\ exists ff_q_gspf_sign_product_restricted_signs_predecessor. fb = ff_q_gspf_sign_product_restricted_signs_predecessor * S ((S (gspf_index_sign_product_restricted_signs)) * fc) + (r)))))
72. 0072specialize beta_sign_factor_prefix_drop_last sb
73. 0073specialize beta_sign_factor_prefix_drop_last sc
74. 0074specialize beta_sign_factor_prefix_drop_last fb
75. 0075specialize beta_sign_factor_prefix_drop_last fc
76. 0076specialize beta_sign_factor_prefix_drop_last r
77. 0077specialize beta_sign_factor_prefix_drop_last l
78. 0078apply beta_sign_factor_prefix_drop_last
79. 0079exact hsigns
80. 0080have hlast_case : ((x = 0) /\ (((exists gsp_beta_height_sign_product_last_one. gsp_beta_height_sign_product_last_one + S (1) = S ((S (l)) * fc)) /\ exists gsp_beta_quotient_sign_product_last_one. fb = gsp_beta_quotient_sign_product_last_one * S ((S (l)) * fc) + (1)))) \/ ((x = 1) /\ (((exists ff_h_sign_product_last_predecessor. ff_h_sign_product_last_predecessor + S (r) = S ((S (l)) * fc)) /\ exists ff_q_sign_product_last_predecessor. fb = ff_q_sign_product_last_predecessor * S ((S (l)) * fc) + (r))))
81. 0081specialize hsigns l
82. 0082specialize hsigns x
83. 0083apply hsigns
84. 0084specialize le_refl (S l)
85. 0085exact le_refl
86. 0086exact hcount_decomp_witness_witness_left
87. 0087cases hlast_case
88. 0088cases hlast_case_left
89. 0089have hfactor_one : x2 = 1
90. 0090specialize beta_at_unique fb
91. 0091specialize beta_at_unique fc
92. 0092specialize beta_at_unique l
93. 0093specialize beta_at_unique x2
94. 0094specialize beta_at_unique 1
95. 0095apply beta_at_unique
96. 0096exact hproduct_decomp_witness_witness_left
97. 0097exact hlast_case_left_right
98. 0098have heqk : e = x1
99. 0099trans x1 + x
100. 0100exact hcount_decomp_witness_witness_right_right_right
101. 0101rewrite hlast_case_left_left
102. 0102apply PA3
103. 0103rewrite heqk at hpower
104. 0104rewrite heqk at hpower
105. 0105rewrite heqk at hpower
106. 0106rewrite heqk at hpower
107. 0107have hprefix_equal : x3 = R
108. 0108specialize IH x1
109. 0109specialize IH x3
110. 0110specialize IH R
111. 0111apply IH
112. 0112exact hcount_decomp_witness_witness_right_left
113. 0113exact hprefix_signs
114. 0114exact hproduct_decomp_witness_witness_right_left
115. 0115exact hpower
116. 0116rewrite hproduct_decomp_witness_witness_right_right
117. 0117rewrite hfactor_one
118. 0118specialize mul_one x3
119. 0119rewrite mul_one
120. 0120exact hprefix_equal
121. 0121cases hlast_case_right
122. 0122have hfactor_r : x2 = r
123. 0123specialize beta_at_unique fb
124. 0124specialize beta_at_unique fc
125. 0125specialize beta_at_unique l
126. 0126specialize beta_at_unique x2
127. 0127specialize beta_at_unique r
128. 0128apply beta_at_unique
129. 0129exact hproduct_decomp_witness_witness_left
130. 0130exact hlast_case_right_right
131. 0131have hsum : e = x1 + 1
132. 0132trans x1 + x
133. 0133exact hcount_decomp_witness_witness_right_right_right
134. 0134congr
135. 0135refl
136. 0136exact hlast_case_right_left
137. 0137have hsucc : x1 + 1 = S x1
138. 0138trans S (x1 + 0)
139. 0139apply PA4
140. 0140congr
141. 0141apply PA3
142. 0142have heqsucc : e = S x1
143. 0143trans x1 + 1
144. 0144exact hsum
145. 0145exact hsucc
146. 0146have hpower_decomp : exists W. (exists ff_b_sign_product_predecessor_power ff_c_sign_product_predecessor_power. ((forall ff_i_sign_product_predecessor_power_repeat. (exists ff_lt_sign_product_predecessor_power_repeat_bound. ff_lt_sign_product_predecessor_power_repeat_bound + S ff_i_sign_product_predecessor_power_repeat = x1) -> (((exists ff_h_sign_product_predecessor_power_repeat_decoded. ff_h_sign_product_predecessor_power_repeat_decoded + S (r) = S ((S (ff_i_sign_product_predecessor_power_repeat)) * ff_c_sign_product_predecessor_power)) /\ exists ff_q_sign_product_predecessor_power_repeat_decoded. ff_b_sign_product_predecessor_power = ff_q_sign_product_predecessor_power_repeat_decoded * S ((S (ff_i_sign_product_predecessor_power_repeat)) * ff_c_sign_product_predecessor_power) + (r)))) /\ (exists ff_u_sign_product_predecessor_power_product ff_v_sign_product_predecessor_power_product. ((((exists ff_h_sign_product_predecessor_power_product_start. ff_h_sign_product_predecessor_power_product_start + S (1) = S ((S (0)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_start. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_start * S ((S (0)) * ff_v_sign_product_predecessor_power_product) + (1))) /\ ((((exists ff_h_sign_product_predecessor_power_product_terminal. ff_h_sign_product_predecessor_power_product_terminal + S (W) = S ((S (x1)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_terminal. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_terminal * S ((S (x1)) * ff_v_sign_product_predecessor_power_product) + (W))) /\ forall ff_i_sign_product_predecessor_power_product. (exists ff_lt_sign_product_predecessor_power_product_bound. ff_lt_sign_product_predecessor_power_product_bound + S ff_i_sign_product_predecessor_power_product = x1) -> exists ff_p_sign_product_predecessor_power_product ff_r_sign_product_predecessor_power_product ff_s_sign_product_predecessor_power_product. ((((exists ff_h_sign_product_predecessor_power_product_factor. ff_h_sign_product_predecessor_power_product_factor + S (ff_p_sign_product_predecessor_power_product) = S ((S (ff_i_sign_product_predecessor_power_product)) * ff_c_sign_product_predecessor_power)) /\ exists ff_q_sign_product_predecessor_power_product_factor. ff_b_sign_product_predecessor_power = ff_q_sign_product_predecessor_power_product_factor * S ((S (ff_i_sign_product_predecessor_power_product)) * ff_c_sign_product_predecessor_power) + (ff_p_sign_product_predecessor_power_product))) /\ ((((exists ff_h_sign_product_predecessor_power_product_partial. ff_h_sign_product_predecessor_power_product_partial + S (ff_r_sign_product_predecessor_power_product) = S ((S (ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_partial. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_partial * S ((S (ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product) + (ff_r_sign_product_predecessor_power_product))) /\ ((((exists ff_h_sign_product_predecessor_power_product_successor. ff_h_sign_product_predecessor_power_product_successor + S (ff_s_sign_product_predecessor_power_product) = S ((S (S ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product)) /\ exists ff_q_sign_product_predecessor_power_product_successor. ff_u_sign_product_predecessor_power_product = ff_q_sign_product_predecessor_power_product_successor * S ((S (S ff_i_sign_product_predecessor_power_product)) * ff_v_sign_product_predecessor_power_product) + (ff_s_sign_product_predecessor_power_product))) /\ ff_s_sign_product_predecessor_power_product = ff_r_sign_product_predecessor_power_product * ff_p_sign_product_predecessor_power_product)))))))) /\ R = W * r
147. 0147specialize pow_successor_decompose r
148. 0148specialize pow_successor_decompose x1
149. 0149specialize pow_successor_decompose e
150. 0150specialize pow_successor_decompose R
151. 0151apply pow_successor_decompose
152. 0152exact heqsucc
153. 0153exact hpower
154. 0154cases hpower_decomp
155. 0155cases hpower_decomp_witness
156. 0156have hprefix_equal : x3 = x4
157. 0157specialize IH x1
158. 0158specialize IH x3
159. 0159specialize IH x4
160. 0160apply IH
161. 0161exact hcount_decomp_witness_witness_right_left
162. 0162exact hprefix_signs
163. 0163exact hproduct_decomp_witness_witness_right_left
164. 0164exact hpower_decomp_witness_left
165. 0165rewrite hproduct_decomp_witness_witness_right_right
166. 0166rewrite hfactor_r
167. 0167rewrite hprefix_equal
168. 0168symm
169. 0169exact hpower_decomp_witness_right