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