Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

	step type	requirements	statement
0	instantiation	1, 2, 3	⊢
	: , : , :
1	reference	574	⊢
2	instantiation	574, 4, 5	⊢
	: , : , :
3	instantiation	151, 373, 11, 6, 7	⊢
	: , : , : , :
4	instantiation	574, 8, 9	⊢
	: , : , :
5	instantiation	151, 373, 10, 11, 12	⊢
	: , : , : , :
6	instantiation	13, 373	⊢
	: , :
7	instantiation	297, 647, 232, 233, 234, 235*	⊢
	: , : , : , : , : , :
8	instantiation	14, 335, 15, 556, 16, 367, 17, 18, 19, 211, 20, 21, 22, 23, 24, 25, 26, 178, 89, 593, 27, 28, 29, 457, 30, 31*, 32*, 33*	⊢
	: , : , : , : , : , :
9	instantiation	151, 373, 34, 35, 36	⊢
	: , : , : , :
10	instantiation	505, 37, 555, 265	⊢
	: , : , : , :
11	instantiation	505, 38, 555, 265	⊢
	: , : , : , :
12	instantiation	201, 202, 203, 345*	⊢
	: , : , : , :
13	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
14	theorem		⊢
	proveit.physics.quantum.circuits.output_consolidation
15	instantiation	505, 39, 55, 50	⊢
	: , : , : , :
16	instantiation	262, 634, 645, 556, 197	⊢
	: , : , :
17	instantiation	505, 40, 55, 50	⊢
	: , : , : , :
18	instantiation	313, 41, 121	⊢
	: , : , :
19	modus ponens	42, 43	⊢
20	instantiation	505, 44, 45, 46	⊢
	: , : , : , :
21	instantiation	515, 47	⊢
	: , :
22	instantiation	515, 48	⊢
	: , :
23	instantiation	505, 49, 55, 50	⊢
	: , : , : , :
24	instantiation	515, 51	⊢
	: , :
25	instantiation	561, 52, 53	⊢
	: , : , :
26	instantiation	505, 54, 55, 56	⊢
	: , : , : , :
27	modus ponens	57, 58	⊢
28	instantiation	292, 373, 318	⊢
	: , :
29	instantiation	59, 640, 288, 652, 60, 434, 61, 62	⊢
	: , : , : , : , : , :
30	instantiation	561, 63, 64	,  ⊢
	: , : , :
31	instantiation	561, 65, 66	⊢
	: , : , :
32	instantiation	561, 67, 68	⊢
	: , : , :
33	instantiation	561, 69, 70	,  ⊢
	: , : , :
34	instantiation	505, 71, 555, 265	⊢
	: , : , : , :
35	instantiation	505, 72, 555, 265	⊢
	: , : , : , :
36	instantiation	201, 202, 203	⊢
	: , : , : , :
37	instantiation	255, 558, 73, 257, 258, 259, 288, 260*	⊢
	: , : , : , :
38	instantiation	574, 74, 320	⊢
	: , : , :
39	instantiation	255, 92, 75, 94, 95, 259, 288, 96*	⊢
	: , : , : , :
40	instantiation	255, 92, 76, 94, 95, 259, 288, 96*	⊢
	: , : , : , :
41	instantiation	313, 77, 78	⊢
	: , : , :
42	instantiation	322, 634, 645, 197	⊢
	: , : , : , :
43	generalization	79	⊢
44	instantiation	255, 92, 80, 81, 95, 259, 369, 82*	⊢
	: , : , : , :
45	instantiation	585, 616, 566	⊢
	: , :
46	instantiation	515, 83	⊢
	: , :
47	instantiation	127, 88, 457	⊢
	: , : , :
48	instantiation	151, 373, 134, 84, 85	⊢
	: , : , : , :
49	instantiation	255, 92, 86, 94, 95, 259, 288, 96*	⊢
	: , : , : , :
50	instantiation	515, 87	⊢
	: , :
51	instantiation	176, 88, 89	⊢
	: , : , :
52	instantiation	515, 90	⊢
	: , :
53	instantiation	515, 91	⊢
	: , :
54	instantiation	255, 92, 93, 94, 95, 259, 288, 96*	⊢
	: , : , : , :
55	instantiation	573	⊢
	:
56	instantiation	515, 97	⊢
	: , :
57	instantiation	322, 644, 645, 323	⊢
	: , : , : , :
58	generalization	98	⊢
59	theorem		⊢
	proveit.logic.booleans.conjunction.disassociate
60	instantiation	608	⊢
	: , :
61	instantiation	505, 99, 388, 100	⊢
	: , : , : , :
62	instantiation	101, 102, 103, 104, 419, 105, 106	⊢
	: , :
63	instantiation	503, 107	,  ⊢
	: , : , :
64	instantiation	561, 108, 109	,  ⊢
	: , : , :
65	instantiation	503, 110	⊢
	: , : , :
66	instantiation	515, 111	⊢
	: , :
67	instantiation	503, 112	⊢
	: , : , :
68	instantiation	114, 556	⊢
	: , :
69	instantiation	503, 113	,  ⊢
	: , : , :
70	instantiation	114, 115	,  ⊢
	: , :
71	instantiation	255, 558, 116, 257, 258, 259, 288, 260*	⊢
	: , : , : , :
72	instantiation	574, 117, 320	⊢
	: , : , :
73	instantiation	608	⊢
	: , :
74	instantiation	368, 369	⊢
	: , : , :
75	instantiation	598	⊢
	: , : , :
76	instantiation	598	⊢
	: , : , :
77	instantiation	461, 462, 376, 118	⊢
	: , : , : , :
78	instantiation	503, 119	⊢
	: , : , :
79	instantiation	313, 120, 121	,  ⊢
	: , : , :
80	instantiation	598	⊢
	: , : , :
81	instantiation	598	⊢
	: , : , :
82	instantiation	561, 122, 123	⊢
	: , : , :
83	instantiation	574, 124, 125	⊢
	: , : , :
84	instantiation	505, 126, 555, 265	⊢
	: , : , : , :
85	instantiation	127, 202, 304, 345*	⊢
	: , : , :
86	instantiation	598	⊢
	: , : , :
87	instantiation	372, 282	⊢
	: , :
88	instantiation	348, 128, 129	⊢
	:
89	instantiation	561, 130, 131	⊢
	: , : , :
90	instantiation	151, 373, 135, 132, 133	⊢
	: , : , : , :
91	instantiation	151, 373, 134, 135, 136	⊢
	: , : , : , :
92	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
93	instantiation	598	⊢
	: , : , :
94	instantiation	598	⊢
	: , : , :
95	instantiation	598	⊢
	: , : , :
96	instantiation	561, 137, 138	⊢
	: , : , :
97	instantiation	574, 139, 140	⊢
	: , : , :
98	instantiation	348, 141, 142	,  ⊢
	:
99	instantiation	574, 143, 434	⊢
	: , : , :
100	instantiation	515, 144	⊢
	: , :
101	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_all
102	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
103	instantiation	145	⊢
	: , : , : , :
104	instantiation	573	⊢
	:
105	modus ponens	146, 147	⊢
106	instantiation	573	⊢
	:
107	instantiation	509, 652, 593, 594, 150, 550, 566	,  ⊢
	: , : , : , : , : , : , :
108	instantiation	547, 593, 578, 652, 594, 148, 150, 566, 550, 586	,  ⊢
	: , : , : , : , : , :
109	instantiation	518, 640, 593, 149, 594, 150, 566, 586	,  ⊢
	: , : , : , : , : , : , : , :
110	instantiation	151, 373, 152, 209, 153	⊢
	: , : , : , :
111	instantiation	503, 154, 155*	⊢
	: , : , :
112	instantiation	503, 457	⊢
	: , : , :
113	instantiation	503, 253	,  ⊢
	: , : , :
114	theorem		⊢
	proveit.physics.quantum.circuits.unary_multi_output_reduction
115	instantiation	156, 157, 158	,  ⊢
	:
116	instantiation	608	⊢
	: , :
117	instantiation	368, 369	⊢
	: , : , :
118	instantiation	423, 462, 424, 159	⊢
	: , : , : , :
119	instantiation	503, 160	⊢
	: , : , :
120	instantiation	461, 462, 376, 161	,  ⊢
	: , : , : , :
121	instantiation	503, 162	⊢
	: , : , :
122	instantiation	361, 578, 163, 164, 364, 320	⊢
	: , : , : , :
123	instantiation	561, 165, 166	⊢
	: , : , :
124	instantiation	368, 167	⊢
	: , : , :
125	instantiation	561, 168, 169	⊢
	: , : , :
126	instantiation	255, 558, 170, 257, 258, 259, 288, 260*	⊢
	: , : , : , :
127	theorem		⊢
	proveit.core_expr_types.tuples.partition_front
128	instantiation	646, 171, 172	⊢
	: , :
129	instantiation	400, 173	⊢
	: , :
130	instantiation	547, 593, 640, 652, 594, 285, 566, 586, 550	⊢
	: , : , : , : , : , :
131	instantiation	174, 586, 566, 521	⊢
	: , : , :
132	instantiation	505, 175, 555, 265	⊢
	: , : , : , :
133	instantiation	176, 177, 178, 179*	⊢
	: , : , :
134	instantiation	503, 180	⊢
	: , : , :
135	instantiation	503, 181	⊢
	: , : , :
136	instantiation	297, 614, 232, 182, 183, 184*	⊢
	: , : , : , : , : , :
137	instantiation	361, 578, 185, 186, 364, 434	⊢
	: , : , : , :
138	instantiation	561, 187, 188	⊢
	: , : , :
139	instantiation	368, 189	⊢
	: , : , :
140	instantiation	561, 190, 191	⊢
	: , : , :
141	instantiation	646, 639, 650	,  ⊢
	: , :
142	instantiation	524, 570, 446, 192, 193, 194*, 195*	,  ⊢
	: , : , :
143	instantiation	368, 288	⊢
	: , : , :
144	instantiation	372, 196	⊢
	: , :
145	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
146	instantiation	322, 634, 645, 197	⊢
	: , : , : , :
147	generalization	198	⊢
148	instantiation	598	⊢
	: , : , :
149	instantiation	608	⊢
	: , :
150	instantiation	653, 632, 199	,  ⊢
	: , : , :
151	theorem		⊢
	proveit.core_expr_types.operations.operands_substitution_via_tuple
152	instantiation	505, 200, 555, 265	⊢
	: , : , : , :
153	instantiation	201, 202, 203	⊢
	: , : , : , :
154	instantiation	204, 655	⊢
	:
155	instantiation	205, 593, 369, 652, 594, 320, 206, 207, 208, 209, 210, 211	⊢
	: , : , : , : , : , : , : , : , : , :
156	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
157	instantiation	646, 624, 650	,  ⊢
	: , :
158	instantiation	212, 379, 544, 213, 214, 215*, 216*	,  ⊢
	: , : , :
159	instantiation	461, 462, 217, 464	⊢
	: , : , : , :
160	instantiation	503, 218	⊢
	: , : , :
161	instantiation	423, 462, 424, 219	,  ⊢
	: , : , : , :
162	instantiation	220, 616	⊢
	:
163	instantiation	598	⊢
	: , : , :
164	instantiation	598	⊢
	: , : , :
165	instantiation	509, 652, 593, 594, 586, 566	⊢
	: , : , : , : , : , : , :
166	instantiation	541, 593, 640, 652, 594, 510, 586, 566, 584*	⊢
	: , : , : , : , : , :
167	instantiation	653, 415, 221	⊢
	: , : , :
168	instantiation	503, 387	⊢
	: , : , :
169	instantiation	505, 222, 223, 224	⊢
	: , : , : , :
170	instantiation	608	⊢
	: , :
171	instantiation	653, 654, 335	⊢
	: , : , :
172	instantiation	600, 225, 337	⊢
	: , : , :
173	instantiation	476, 226	⊢
	: , :
174	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
175	instantiation	227, 228, 229*	⊢
	: , : , : , :
176	theorem		⊢
	proveit.core_expr_types.tuples.partition_back
177	instantiation	348, 230, 231	⊢
	:
178	instantiation	485, 538, 586, 457	⊢
	: , : , :
179	instantiation	545, 586, 566, 521	⊢
	: , : , :
180	instantiation	297, 647, 232, 233, 234, 235*	⊢
	: , : , : , : , : , :
181	instantiation	561, 236, 237	⊢
	: , : , :
182	instantiation	515, 238	⊢
	: , :
183	instantiation	515, 239	⊢
	: , :
184	instantiation	547, 593, 640, 652, 594, 240, 241, 550, 566	,  ⊢
	: , : , : , : , : , :
185	instantiation	598	⊢
	: , : , :
186	instantiation	598	⊢
	: , : , :
187	instantiation	547, 652, 640, 549, 586, 566, 550	⊢
	: , : , : , : , : , :
188	instantiation	519, 593, 652, 594, 586, 566, 521	⊢
	: , : , : , : , : , : , : , :
189	instantiation	409, 578, 242, 373, 283, 652	⊢
	: , :
190	instantiation	503, 387	⊢
	: , : , :
191	instantiation	539, 652, 566, 586	⊢
	: , : , : , :
192	instantiation	426, 633, 620	,  ⊢
	: , :
193	instantiation	243, 446, 633, 620, 244, 245	,  ⊢
	: , : , :
194	instantiation	505, 246, 247, 248	⊢
	: , : , : , :
195	instantiation	505, 249, 250, 251	,  ⊢
	: , : , : , :
196	instantiation	348, 602, 252	⊢
	:
197	instantiation	524, 446, 620, 582, 525, 342*, 375*	⊢
	: , : , :
198	instantiation	515, 253	,  ⊢
	: , :
199	instantiation	653, 635, 254	,  ⊢
	: , : , :
200	instantiation	255, 558, 256, 257, 258, 259, 288, 260*	⊢
	: , : , : , :
201	theorem		⊢
	proveit.core_expr_types.tuples.merge_front
202	instantiation	292, 593, 411	⊢
	: , :
203	instantiation	515, 304	⊢
	: , :
204	axiom		⊢
	proveit.physics.quantum.QPE._psi_t_def
205	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_disassociation
206	instantiation	505, 261, 555, 265	⊢
	: , : , : , :
207	instantiation	262, 644, 645, 462, 323	⊢
	: , : , :
208	instantiation	498, 263	⊢
	:
209	instantiation	505, 264, 555, 265	⊢
	: , : , : , :
210	modus ponens	266, 267	⊢
211	axiom		⊢
	proveit.physics.quantum.QPE._u_ket_register
212	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
213	instantiation	653, 635, 268	,  ⊢
	: , : , :
214	instantiation	269, 544, 599, 625, 270, 271	,  ⊢
	: , : , :
215	instantiation	505, 272, 273, 274	⊢
	: , : , : , :
216	instantiation	505, 275, 276, 277	,  ⊢
	: , : , : , :
217	instantiation	615, 499, 278	⊢
	: , :
218	instantiation	503, 279	⊢
	: , : , :
219	instantiation	461, 462, 280, 464	,  ⊢
	: , : , : , :
220	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
221	instantiation	394, 640, 593, 281, 594, 282, 283, 652, 395	⊢
	: , : , : , : , :
222	instantiation	547, 593, 640, 594, 285, 284, 566, 586, 538	⊢
	: , : , : , : , : , :
223	instantiation	539, 640, 652, 285, 566, 586	⊢
	: , : , : , :
224	instantiation	541, 652, 640, 593, 510, 594, 566, 586, 584*	⊢
	: , : , : , : , : , :
225	instantiation	612, 286	⊢
	: , :
226	instantiation	512, 335	⊢
	:
227	theorem		⊢
	proveit.core_expr_types.tuples.extended_range_len
228	instantiation	287, 288	⊢
	: , : , :
229	instantiation	561, 289, 290	⊢
	: , : , :
230	instantiation	646, 648, 399	⊢
	: , :
231	instantiation	400, 291	⊢
	: , :
232	instantiation	292, 293, 411	⊢
	: , :
233	instantiation	515, 294	⊢
	: , :
234	instantiation	515, 295	⊢
	: , :
235	instantiation	561, 296, 490	,  ⊢
	: , : , :
236	instantiation	297, 644, 298, 299, 300	⊢
	: , : , : , : , : , :
237	modus ponens	301, 302	⊢
238	instantiation	561, 303, 304	⊢
	: , : , :
239	instantiation	561, 305, 457	⊢
	: , : , :
240	instantiation	608	⊢
	: , :
241	instantiation	653, 632, 306	,  ⊢
	: , : , :
242	instantiation	598	⊢
	: , : , :
243	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right
244	instantiation	326, 644, 645, 642	,  ⊢
	: , : , :
245	instantiation	307, 652	⊢
	:
246	instantiation	547, 593, 640, 652, 594, 493, 553, 586, 546	⊢
	: , : , : , : , : , :
247	instantiation	547, 640, 593, 493, 549, 594, 553, 586, 566, 550	⊢
	: , : , : , : , : , :
248	instantiation	561, 308, 328	⊢
	: , : , :
249	instantiation	547, 593, 640, 652, 594, 309, 627, 586, 546	,  ⊢
	: , : , : , : , : , :
250	instantiation	547, 640, 593, 309, 549, 594, 627, 586, 566, 550	,  ⊢
	: , : , : , : , : , :
251	instantiation	519, 652, 593, 594, 627, 586, 566, 521	,  ⊢
	: , : , : , : , : , : , : , :
252	instantiation	400, 525	⊢
	: , :
253	instantiation	561, 310, 311	,  ⊢
	: , : , :
254	instantiation	653, 638, 312	,  ⊢
	: , : , :
255	theorem		⊢
	proveit.core_expr_types.tuples.general_len
256	instantiation	608	⊢
	: , :
257	instantiation	608	⊢
	: , :
258	instantiation	608	⊢
	: , :
259	instantiation	313, 652, 364	⊢
	: , : , :
260	instantiation	561, 314, 315	⊢
	: , : , :
261	instantiation	574, 316, 320	⊢
	: , : , :
262	theorem		⊢
	proveit.logic.booleans.conjunction.redundant_conjunction_general
263	instantiation	317, 640, 318	⊢
	: , :
264	instantiation	574, 319, 320	⊢
	: , : , :
265	instantiation	515, 321	⊢
	: , :
266	instantiation	322, 644, 645, 323	⊢
	: , : , : , :
267	generalization	324	⊢
268	instantiation	653, 638, 325	,  ⊢
	: , : , :
269	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
270	instantiation	326, 634, 645, 630	,  ⊢
	: , : , :
271	instantiation	512, 558	⊢
	:
272	instantiation	547, 593, 640, 652, 594, 548, 553, 616, 329	⊢
	: , : , : , : , : , :
273	instantiation	547, 640, 593, 548, 537, 594, 553, 616, 566, 587	⊢
	: , : , : , : , : , :
274	instantiation	561, 327, 328	⊢
	: , : , :
275	instantiation	547, 593, 640, 652, 594, 330, 581, 616, 329	,  ⊢
	: , : , : , : , : , :
276	instantiation	547, 640, 593, 330, 537, 594, 581, 616, 566, 587	,  ⊢
	: , : , : , : , : , :
277	instantiation	519, 652, 593, 594, 581, 616, 566, 481	,  ⊢
	: , : , : , : , : , : , : , :
278	instantiation	574, 331, 332	⊢
	: , : , :
279	instantiation	503, 333	⊢
	: , : , :
280	instantiation	615, 499, 334	,  ⊢
	: , :
281	instantiation	608	⊢
	: , :
282	instantiation	653, 415, 335	⊢
	: , : , :
283	instantiation	600, 336, 337	⊢
	: , : , :
284	instantiation	608	⊢
	: , :
285	instantiation	608	⊢
	: , :
286	theorem		⊢
	proveit.numbers.number_sets.integers.zero_set_within_int
287	theorem		⊢
	proveit.core_expr_types.tuples.range_len_is_nat
288	instantiation	574, 411, 338	⊢
	: , : , :
289	instantiation	503, 504	⊢
	: , : , :
290	instantiation	505, 339, 340, 341	⊢
	: , : , : , :
291	instantiation	524, 446, 620, 582, 525, 342*, 418*	⊢
	: , : , :
292	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
293	instantiation	653, 415, 343	⊢
	: , : , :
294	instantiation	561, 344, 345	⊢
	: , : , :
295	instantiation	561, 346, 347	⊢
	: , : , :
296	instantiation	547, 593, 640, 652, 594, 520, 523, 553, 566	,  ⊢
	: , : , : , : , : , :
297	theorem		⊢
	proveit.core_expr_types.tuples.shift_equivalence
298	instantiation	348, 349, 350	⊢
	:
299	instantiation	515, 351	⊢
	: , :
300	instantiation	515, 352	⊢
	: , :
301	instantiation	353, 648, 650	⊢
	: , : , : , : , :
302	generalization	354	⊢
303	instantiation	503, 357	⊢
	: , : , :
304	instantiation	561, 355, 356	⊢
	: , : , :
305	instantiation	503, 357	⊢
	: , : , :
306	instantiation	653, 635, 358	,  ⊢
	: , : , :
307	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
308	instantiation	519, 652, 593, 594, 553, 586, 566, 521	⊢
	: , : , : , : , : , : , : , :
309	instantiation	608	⊢
	: , :
310	instantiation	547, 593, 578, 652, 594, 359, 581, 550, 566, 586	,  ⊢
	: , : , : , : , : , :
311	instantiation	518, 652, 593, 594, 581, 586, 566	,  ⊢
	: , : , : , : , : , : , : , :
312	instantiation	653, 629, 360	,  ⊢
	: , : , :
313	theorem		⊢
	proveit.logic.equality.sub_left_side_into
314	instantiation	361, 640, 362, 363, 364, 434	⊢
	: , : , : , :
315	instantiation	561, 365, 366	⊢
	: , : , :
316	instantiation	368, 369	⊢
	: , : , :
317	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
318	instantiation	653, 415, 367	⊢
	: , : , :
319	instantiation	368, 369	⊢
	: , : , :
320	instantiation	561, 370, 371	⊢
	: , : , :
321	instantiation	372, 373	⊢
	: , :
322	theorem		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
323	instantiation	524, 446, 619, 582, 440, 374*, 375*	⊢
	: , : , :
324	instantiation	461, 462, 376, 377	,  ⊢
	: , : , : , :
325	instantiation	646, 624, 637	,  ⊢
	: , :
326	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
327	instantiation	519, 652, 593, 594, 553, 616, 566, 481	⊢
	: , : , : , : , : , : , : , :
328	instantiation	378, 566, 555	⊢
	: , :
329	instantiation	653, 632, 379	⊢
	: , : , :
330	instantiation	608	⊢
	: , :
331	instantiation	605, 577, 380	⊢
	: , :
332	instantiation	561, 381, 382	⊢
	: , : , :
333	instantiation	503, 443	⊢
	: , : , :
334	instantiation	574, 383, 384	,  ⊢
	: , : , :
335	instantiation	475, 655, 556	⊢
	: , :
336	instantiation	612, 385	⊢
	: , :
337	instantiation	386, 387	⊢
	: , :
338	instantiation	505, 443, 388, 389	⊢
	: , : , : , :
339	instantiation	547, 652, 640, 537, 538, 566, 587, 616	⊢
	: , : , : , : , : , :
340	instantiation	539, 593, 578, 594, 390, 566, 587, 616	⊢
	: , : , : , :
341	instantiation	522, 616, 566, 481	⊢
	: , : , :
342	instantiation	505, 391, 392, 393	⊢
	: , : , : , :
343	instantiation	394, 652, 593, 594, 395	⊢
	: , : , : , : , :
344	instantiation	503, 536	⊢
	: , : , :
345	instantiation	561, 396, 397	⊢
	: , : , :
346	instantiation	503, 536	⊢
	: , : , :
347	instantiation	494, 566	⊢
	:
348	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
349	instantiation	646, 398, 399	⊢
	: , :
350	instantiation	400, 401	⊢
	: , :
351	instantiation	561, 402, 403	⊢
	: , : , :
352	instantiation	485, 566, 404, 586, 418	⊢
	: , : , :
353	theorem		⊢
	proveit.core_expr_types.tuples.range_fn_transformation
354	instantiation	561, 405, 406	,  ⊢
	: , : , :
355	instantiation	547, 593, 640, 652, 594, 493, 553, 586	⊢
	: , : , : , : , : , :
356	instantiation	541, 652, 640, 593, 510, 594, 553, 586, 584*	⊢
	: , : , : , : , : , :
357	instantiation	565, 586	⊢
	:
358	instantiation	653, 638, 407	,  ⊢
	: , : , :
359	instantiation	598	⊢
	: , : , :
360	assumption		⊢
361	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
362	instantiation	608	⊢
	: , :
363	instantiation	608	⊢
	: , :
364	instantiation	545, 586, 521	⊢
	: , : , :
365	instantiation	547, 652, 640, 593, 549, 594, 586, 566, 550	⊢
	: , : , : , : , : , :
366	instantiation	408, 586, 566, 521	⊢
	: , : , :
367	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
368	theorem		⊢
	proveit.core_expr_types.tuples.range_len
369	instantiation	409, 578, 410, 593, 411, 652	⊢
	: , :
370	instantiation	503, 443	⊢
	: , : , :
371	instantiation	505, 412, 413, 414	⊢
	: , : , : , :
372	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
373	instantiation	653, 415, 655	⊢
	: , : , :
374	instantiation	561, 416, 417	⊢
	: , : , :
375	instantiation	505, 418, 521, 419	⊢
	: , : , : , :
376	instantiation	420, 586, 421, 422	⊢
	: , :
377	instantiation	423, 462, 424, 425	,  ⊢
	: , : , : , :
378	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_reverse
379	instantiation	426, 582, 427	⊢
	: , :
380	instantiation	574, 428, 429	⊢
	: , : , :
381	instantiation	592, 652, 578, 593, 430, 594, 577, 606, 501, 596	⊢
	: , : , : , : , : , :
382	instantiation	592, 593, 640, 578, 594, 579, 430, 616, 597, 606, 501, 596	⊢
	: , : , : , : , : , :
383	instantiation	605, 577, 431	,  ⊢
	: , :
384	instantiation	561, 432, 433	,  ⊢
	: , : , :
385	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.zero_set_within_nat
386	theorem		⊢
	proveit.logic.sets.enumeration.fold_singleton
387	theorem		⊢
	proveit.numbers.negation.negated_zero
388	instantiation	573	⊢
	:
389	instantiation	515, 434	⊢
	: , :
390	instantiation	598	⊢
	: , : , :
391	instantiation	561, 435, 436	⊢
	: , : , :
392	instantiation	485, 511, 566, 616, 437	⊢
	: , : , :
393	instantiation	573	⊢
	:
394	theorem		⊢
	proveit.numbers.addition.add_nat_pos_from_nonneg
395	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
396	instantiation	547, 593, 640, 652, 594, 493, 553, 586, 566	⊢
	: , : , : , : , : , :
397	instantiation	438, 566, 586, 555	⊢
	: , : , :
398	instantiation	653, 654, 439	⊢
	: , : , :
399	instantiation	649, 634	⊢
	:
400	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
401	instantiation	524, 544, 619, 582, 440, 441*, 442*	⊢
	: , : , :
402	instantiation	503, 443	⊢
	: , : , :
403	instantiation	561, 444, 445	⊢
	: , : , :
404	instantiation	653, 632, 446	⊢
	: , : , :
405	instantiation	503, 447	,  ⊢
	: , : , :
406	instantiation	561, 448, 449	,  ⊢
	: , : , :
407	instantiation	653, 450, 451	,  ⊢
	: , : , :
408	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
409	theorem		⊢
	proveit.numbers.addition.add_nat_closure
410	instantiation	598	⊢
	: , : , :
411	instantiation	452, 453	⊢
	:
412	instantiation	547, 652, 640, 549, 538, 566, 550, 586	⊢
	: , : , : , : , : , :
413	instantiation	539, 593, 578, 594, 454, 566, 550, 586	⊢
	: , : , : , :
414	instantiation	522, 586, 566, 521	⊢
	: , : , :
415	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
416	instantiation	547, 652, 640, 593, 493, 594, 538, 553, 586	⊢
	: , : , : , : , : , :
417	instantiation	539, 593, 640, 594, 493, 553, 586	⊢
	: , : , : , :
418	instantiation	561, 455, 456	⊢
	: , : , :
419	instantiation	515, 457	⊢
	: , :
420	theorem		⊢
	proveit.numbers.division.div_complex_closure
421	instantiation	458, 616	⊢
	:
422	instantiation	459, 497, 460	⊢
	: , :
423	theorem		⊢
	proveit.linear_algebra.addition.binary_closure
424	theorem		⊢
	proveit.physics.quantum.algebra.ket_zero_in_qubit_space
425	instantiation	461, 462, 463, 464	,  ⊢
	: , : , : , :
426	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
427	instantiation	465, 625	⊢
	:
428	instantiation	605, 466, 596	⊢
	: , :
429	instantiation	592, 593, 640, 652, 594, 467, 606, 501, 596	⊢
	: , : , : , : , : , :
430	instantiation	598	⊢
	: , : , :
431	instantiation	574, 468, 469	,  ⊢
	: , : , :
432	instantiation	592, 652, 578, 593, 580, 594, 577, 606, 534, 596	,  ⊢
	: , : , : , : , : , :
433	instantiation	592, 593, 640, 578, 594, 579, 580, 616, 597, 606, 534, 596	,  ⊢
	: , : , : , : , : , :
434	instantiation	561, 470, 471	⊢
	: , : , :
435	instantiation	547, 652, 640, 593, 493, 594, 586, 553	⊢
	: , : , : , : , : , :
436	instantiation	561, 472, 473	⊢
	: , : , :
437	instantiation	574, 480, 474	⊢
	: , : , :
438	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_31
439	instantiation	475, 556	⊢
	: , :
440	instantiation	476, 477	⊢
	: , :
441	instantiation	561, 478, 479	⊢
	: , : , :
442	instantiation	505, 480, 481, 482	⊢
	: , : , : , :
443	instantiation	535, 553, 586, 536*	⊢
	: , :
444	instantiation	561, 483, 484	⊢
	: , : , :
445	instantiation	485, 586, 616, 584	⊢
	: , : , :
446	instantiation	653, 635, 486	⊢
	: , : , :
447	instantiation	547, 652, 640, 593, 493, 594, 523, 553, 586	,  ⊢
	: , : , : , : , : , :
448	instantiation	547, 593, 578, 640, 594, 487, 488, 523, 553, 586, 550, 566	,  ⊢
	: , : , : , : , : , :
449	instantiation	561, 489, 490	,  ⊢
	: , : , :
450	instantiation	643, 634, 648	⊢
	: , :
451	assumption		⊢
452	theorem		⊢
	proveit.numbers.negation.nat_closure
453	instantiation	491, 644, 492	⊢
	:
454	instantiation	598	⊢
	: , : , :
455	instantiation	547, 652, 640, 593, 493, 594, 566, 553, 586	⊢
	: , : , : , : , : , :
456	instantiation	545, 566, 586, 555	⊢
	: , : , :
457	instantiation	494, 586	⊢
	:
458	theorem		⊢
	proveit.numbers.exponentiation.sqrt_complex_closure
459	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
460	instantiation	495, 496, 497	⊢
	: , :
461	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
462	instantiation	498, 558	⊢
	:
463	instantiation	615, 499, 500	,  ⊢
	: , :
464	theorem		⊢
	proveit.physics.quantum.algebra.ket_one_in_qubit_space
465	theorem		⊢
	proveit.numbers.negation.real_closure
466	instantiation	605, 606, 501	⊢
	: , :
467	instantiation	608	⊢
	: , :
468	instantiation	605, 502, 596	,  ⊢
	: , :
469	instantiation	592, 593, 640, 652, 594, 595, 606, 534, 596	,  ⊢
	: , : , : , : , : , :
470	instantiation	503, 504	⊢
	: , : , :
471	instantiation	505, 506, 507, 508	⊢
	: , : , : , :
472	instantiation	509, 652, 593, 594, 586, 553	⊢
	: , : , : , : , : , : , :
473	instantiation	541, 593, 640, 652, 594, 510, 586, 553, 584*	⊢
	: , : , : , : , : , :
474	instantiation	585, 566, 511	⊢
	: , :
475	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
476	theorem		⊢
	proveit.numbers.ordering.relax_less
477	instantiation	512, 655	⊢
	:
478	instantiation	547, 652, 640, 593, 548, 594, 538, 553, 616	⊢
	: , : , : , : , : , :
479	instantiation	539, 593, 640, 594, 548, 553, 616	⊢
	: , : , : , :
480	instantiation	561, 513, 514	⊢
	: , : , :
481	instantiation	573	⊢
	:
482	instantiation	515, 584	⊢
	: , :
483	instantiation	561, 516, 517	⊢
	: , : , :
484	instantiation	518, 593, 652, 594, 566, 616, 550	⊢
	: , : , : , : , : , : , : , :
485	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
486	instantiation	653, 638, 644	⊢
	: , : , :
487	instantiation	598	⊢
	: , : , :
488	instantiation	608	⊢
	: , :
489	instantiation	519, 640, 593, 652, 520, 594, 523, 553, 586, 566, 521	,  ⊢
	: , : , : , : , : , : , : , :
490	instantiation	522, 566, 523, 555	,  ⊢
	: , : , :
491	theorem		⊢
	proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
492	instantiation	524, 572, 620, 582, 525, 526*, 527*	⊢
	: , : , :
493	instantiation	608	⊢
	: , :
494	theorem		⊢
	proveit.numbers.addition.elim_zero_left
495	theorem		⊢
	proveit.numbers.division.div_rational_nonzero_closure
496	instantiation	653, 529, 528	⊢
	: , : , :
497	instantiation	653, 529, 530	⊢
	: , : , :
498	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
499	instantiation	653, 632, 531	⊢
	: , : , :
500	instantiation	574, 532, 533	,  ⊢
	: , : , :
501	instantiation	615, 616, 546	⊢
	: , :
502	instantiation	605, 606, 534	,  ⊢
	: , :
503	axiom		⊢
	proveit.logic.equality.substitution
504	instantiation	535, 553, 616, 536*	⊢
	: , :
505	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
506	instantiation	547, 652, 640, 537, 538, 566, 587, 586	⊢
	: , : , : , : , : , :
507	instantiation	539, 593, 578, 594, 540, 566, 587, 586	⊢
	: , : , : , :
508	instantiation	541, 652, 640, 593, 542, 594, 566, 587, 586, 543*	⊢
	: , : , : , : , : , :
509	theorem		⊢
	proveit.numbers.addition.leftward_commutation
510	instantiation	608	⊢
	: , :
511	instantiation	653, 632, 544	⊢
	: , : , :
512	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
513	instantiation	547, 652, 640, 593, 548, 594, 566, 553, 616	⊢
	: , : , : , : , : , :
514	instantiation	545, 566, 616, 555	⊢
	: , : , :
515	theorem		⊢
	proveit.logic.equality.equals_reversal
516	instantiation	547, 593, 640, 652, 594, 548, 553, 616, 546	⊢
	: , : , : , : , : , :
517	instantiation	547, 640, 593, 548, 549, 594, 553, 616, 566, 550	⊢
	: , : , : , : , : , :
518	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
519	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
520	instantiation	608	⊢
	: , :
521	instantiation	573	⊢
	:
522	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
523	instantiation	653, 632, 551	,  ⊢
	: , : , :
524	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
525	instantiation	552, 655	⊢
	:
526	instantiation	585, 586, 553	⊢
	: , :
527	instantiation	554, 566, 555	⊢
	: , :
528	instantiation	653, 557, 556	⊢
	: , : , :
529	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
530	instantiation	653, 557, 558	⊢
	: , : , :
531	instantiation	653, 622, 559	⊢
	: , : , :
532	instantiation	605, 577, 560	,  ⊢
	: , :
533	instantiation	561, 562, 563	,  ⊢
	: , : , :
534	instantiation	615, 616, 564	,  ⊢
	: , :
535	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
536	instantiation	565, 566	⊢
	:
537	instantiation	608	⊢
	: , :
538	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
539	theorem		⊢
	proveit.numbers.addition.elim_zero_any
540	instantiation	598	⊢
	: , : , :
541	theorem		⊢
	proveit.numbers.addition.association
542	instantiation	608	⊢
	: , :
543	instantiation	574, 567, 568	⊢
	: , : , :
544	instantiation	653, 635, 569	⊢
	: , : , :
545	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
546	instantiation	653, 632, 570	⊢
	: , : , :
547	theorem		⊢
	proveit.numbers.addition.disassociation
548	instantiation	608	⊢
	: , :
549	instantiation	608	⊢
	: , :
550	instantiation	626, 586	⊢
	:
551	instantiation	653, 635, 571	,  ⊢
	: , : , :
552	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
553	instantiation	653, 632, 572	⊢
	: , : , :
554	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
555	instantiation	573	⊢
	:
556	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
557	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
558	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
559	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
560	instantiation	574, 575, 576	,  ⊢
	: , : , :
561	axiom		⊢
	proveit.logic.equality.equals_transitivity
562	instantiation	592, 652, 578, 593, 580, 594, 577, 606, 607, 596	,  ⊢
	: , : , : , : , : , :
563	instantiation	592, 593, 640, 578, 594, 579, 580, 616, 597, 606, 607, 596	,  ⊢
	: , : , : , : , : , :
564	instantiation	626, 581	,  ⊢
	:
565	theorem		⊢
	proveit.numbers.negation.double_negation
566	instantiation	653, 632, 582	⊢
	: , : , :
567	instantiation	583, 586, 616, 584	⊢
	: , : , :
568	instantiation	585, 586, 587	⊢
	: , :
569	instantiation	653, 638, 634	⊢
	: , : , :
570	instantiation	653, 635, 588	⊢
	: , : , :
571	instantiation	653, 638, 589	,  ⊢
	: , : , :
572	instantiation	653, 635, 590	⊢
	: , : , :
573	axiom		⊢
	proveit.logic.equality.equals_reflexivity
574	theorem		⊢
	proveit.logic.equality.sub_right_side_into
575	instantiation	605, 591, 596	,  ⊢
	: , :
576	instantiation	592, 593, 640, 652, 594, 595, 606, 607, 596	,  ⊢
	: , : , : , : , : , :
577	instantiation	605, 616, 597	⊢
	: , :
578	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
579	instantiation	608	⊢
	: , :
580	instantiation	598	⊢
	: , : , :
581	instantiation	653, 632, 599	,  ⊢
	: , : , :
582	instantiation	600, 601, 655	⊢
	: , : , :
583	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
584	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
585	theorem		⊢
	proveit.numbers.addition.commutation
586	instantiation	653, 632, 620	⊢
	: , : , :
587	instantiation	626, 616	⊢
	:
588	instantiation	653, 638, 602	⊢
	: , : , :
589	instantiation	653, 603, 604	,  ⊢
	: , : , :
590	instantiation	653, 638, 647	⊢
	: , : , :
591	instantiation	605, 606, 607	,  ⊢
	: , :
592	theorem		⊢
	proveit.numbers.multiplication.disassociation
593	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
594	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
595	instantiation	608	⊢
	: , :
596	instantiation	653, 632, 609	⊢
	: , : , :
597	instantiation	653, 632, 610	⊢
	: , : , :
598	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
599	instantiation	653, 635, 611	,  ⊢
	: , : , :
600	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
601	instantiation	612, 613	⊢
	: , :
602	instantiation	646, 650, 614	⊢
	: , :
603	instantiation	643, 648, 650	⊢
	: , :
604	assumption		⊢
605	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
606	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
607	instantiation	615, 616, 617	,  ⊢
	: , :
608	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
609	instantiation	618, 619, 620, 621	⊢
	: , : , :
610	instantiation	653, 622, 623	⊢
	: , : , :
611	instantiation	653, 638, 624	,  ⊢
	: , : , :
612	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
613	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
614	instantiation	649, 648	⊢
	:
615	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
616	instantiation	653, 632, 625	⊢
	: , : , :
617	instantiation	626, 627	,  ⊢
	:
618	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
619	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
620	instantiation	653, 635, 628	⊢
	: , : , :
621	axiom		⊢
	proveit.physics.quantum.QPE._phase_in_interval
622	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
623	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
624	instantiation	653, 629, 630	,  ⊢
	: , : , :
625	instantiation	653, 635, 631	⊢
	: , : , :
626	theorem		⊢
	proveit.numbers.negation.complex_closure
627	instantiation	653, 632, 633	,  ⊢
	: , : , :
628	instantiation	653, 638, 648	⊢
	: , : , :
629	instantiation	643, 634, 645	⊢
	: , :
630	assumption		⊢
631	instantiation	653, 638, 637	⊢
	: , : , :
632	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
633	instantiation	653, 635, 636	,  ⊢
	: , : , :
634	instantiation	646, 647, 637	⊢
	: , :
635	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
636	instantiation	653, 638, 639	,  ⊢
	: , : , :
637	instantiation	653, 651, 640	⊢
	: , : , :
638	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
639	instantiation	653, 641, 642	,  ⊢
	: , : , :
640	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
641	instantiation	643, 644, 645	⊢
	: , :
642	assumption		⊢
643	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
644	instantiation	646, 647, 648	⊢
	: , :
645	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
646	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
647	instantiation	649, 650	⊢
	:
648	instantiation	653, 651, 652	⊢
	: , : , :
649	theorem		⊢
	proveit.numbers.negation.int_closure
650	instantiation	653, 654, 655	⊢
	: , : , :
651	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
652	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
653	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
654	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
655	assumption		⊢
*equality replacement requirements