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