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, 146, 240, 4, 56, 72, 5*, 6*	⊢
	: , : , : , : , : , :
2	theorem		⊢
	proveit.physics.quantum.QPE._Psi_output
3	theorem		⊢
	proveit.physics.quantum.circuits.concat_onto_ideal_expt
4	instantiation	360, 7, 8	⊢
	: , : , :
5	instantiation	338, 9, 10	⊢
	: , : , :
6	instantiation	338, 11, 12	⊢
	: , : , :
7	instantiation	13, 146, 14, 25, 27, 15*	⊢
	: , : , :
8	instantiation	16, 146, 17, 18, 19, 74, 75, 76	⊢
	: , : , : , :
9	instantiation	351, 20	⊢
	: , : , :
10	instantiation	292, 21	⊢
	: , :
11	instantiation	351, 22	⊢
	: , : , :
12	instantiation	292, 23	⊢
	: , :
13	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp
14	instantiation	342	⊢
	: , :
15	instantiation	24, 330, 376, 362	⊢
	: , : , :
16	theorem		⊢
	proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
17	instantiation	342	⊢
	: , :
18	instantiation	26, 25	⊢
	:
19	instantiation	26, 27	⊢
	:
20	instantiation	30, 272, 28	⊢
	: , : , :
21	instantiation	32, 29	⊢
	: , :
22	instantiation	30, 272, 31	⊢
	: , : , :
23	instantiation	32, 33	⊢
	: , :
24	theorem		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
25	instantiation	34, 374, 175	⊢
	: , :
26	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
27	instantiation	34, 374, 177	⊢
	: , :
28	modus ponens	35, 36	⊢
29	modus ponens	37, 38	⊢
30	theorem		⊢
	proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
31	modus ponens	39, 40	⊢
32	theorem		⊢
	proveit.physics.quantum.circuits.prob_eq_via_equiv
33	modus ponens	41, 42	⊢
34	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
35	instantiation	58, 173, 43, 44, 45, 46, 47, 48, 49, 50	⊢
	: , : , : , :
36	instantiation	65, 173, 51, 52, 53, 54, 55	⊢
	: , : , :
37	instantiation	71, 374, 379, 320, 56, 321	⊢
	: , : , : , : , : , : , : , :
38	instantiation	57, 146, 299, 376, 362, 74, 75, 76, 77, 78, 149, 79, 80, 81, 163, 320, 175, 179, 82, 160*	⊢
	: , : , : , : , : , :
39	instantiation	58, 173, 240, 59, 60, 61, 62, 63, 64	⊢
	: , : , : , :
40	instantiation	65, 173, 66, 67, 68, 69, 70	⊢
	: , : , :
41	instantiation	71, 320, 379, 374, 321, 72	⊢
	: , : , : , : , : , : , : , :
42	instantiation	73, 146, 299, 376, 362, 74, 75, 76, 77, 78, 149, 79, 80, 81, 163, 320, 175, 179, 82, 160*	⊢
	: , : , : , : , : , :
43	instantiation	273, 83, 84	⊢
	: , :
44	instantiation	338, 85, 86	⊢
	: , : , :
45	instantiation	268, 87, 96, 97	⊢
	: , : , : , :
46	instantiation	268, 88, 96, 97	⊢
	: , : , : , :
47	instantiation	268, 89, 118, 102	⊢
	: , : , : , :
48	instantiation	268, 90, 118, 102	⊢
	: , : , : , :
49	instantiation	268, 91, 118, 102	⊢
	: , : , : , :
50	instantiation	268, 92, 118, 102	⊢
	: , : , : , :
51	instantiation	335	⊢
	: , : , :
52	instantiation	335	⊢
	: , : , :
53	instantiation	344	⊢
	:
54	instantiation	344	⊢
	:
55	instantiation	292, 93	⊢
	: , :
56	instantiation	342	⊢
	: , :
57	theorem		⊢
	proveit.physics.quantum.circuits.output_consolidation
58	theorem		⊢
	proveit.physics.quantum.circuits.qcircuit_eq
59	instantiation	268, 94, 96, 97	⊢
	: , : , : , :
60	instantiation	268, 95, 96, 97	⊢
	: , : , : , :
61	instantiation	268, 98, 118, 102	⊢
	: , : , : , :
62	instantiation	268, 99, 118, 102	⊢
	: , : , : , :
63	instantiation	268, 100, 118, 102	⊢
	: , : , : , :
64	instantiation	268, 101, 118, 102	⊢
	: , : , : , :
65	theorem		⊢
	proveit.core_expr_types.expr_arrays.varray_eq_via_elem_eq
66	instantiation	335	⊢
	: , : , :
67	instantiation	335	⊢
	: , : , :
68	instantiation	292, 103	⊢
	: , :
69	instantiation	344	⊢
	:
70	instantiation	344	⊢
	:
71	theorem		⊢
	proveit.physics.quantum.circuits.circuit_equiv_temporal_sub
72	instantiation	342	⊢
	: , :
73	theorem		⊢
	proveit.physics.quantum.circuits.input_consolidation
74	instantiation	342	⊢
	: , :
75	instantiation	104, 105	⊢
	: , :
76	axiom		⊢
	proveit.physics.quantum.QPE._u_ket_register
77	instantiation	268, 106, 107, 108	⊢
	: , : , : , :
78	instantiation	292, 109	⊢
	: , :
79	instantiation	292, 110	⊢
	: , :
80	instantiation	268, 111, 112, 113	⊢
	: , : , : , :
81	instantiation	189, 256, 332, 160	⊢
	: , : , :
82	instantiation	114, 359, 115, 116, 117, 118	⊢
	: , :
83	instantiation	176, 376, 207	⊢
	: , : , :
84	instantiation	176, 362, 302	⊢
	: , : , :
85	instantiation	351, 207	⊢
	: , : , :
86	instantiation	351, 302	⊢
	: , : , :
87	instantiation	145, 130, 119, 120, 121, 150, 144, 151, 133, 122*	⊢
	: , : , : , :
88	instantiation	145, 135, 123, 124, 125, 150, 144, 151, 126*	⊢
	: , : , : , :
89	instantiation	145, 146, 127, 315, 299, 150, 144, 207*, 302*	⊢
	: , : , : , :
90	instantiation	145, 146, 128, 148, 149, 150, 151, 207*, 208*	⊢
	: , : , : , :
91	instantiation	178, 179	⊢
	: , :
92	instantiation	145, 146, 129, 148, 149, 150, 151, 207*, 208*	⊢
	: , : , : , :
93	instantiation	153, 154, 155, 156	⊢
	: , : , : , : , :
94	instantiation	145, 130, 131, 132, 199, 133, 150, 144, 134*	⊢
	: , : , : , :
95	instantiation	145, 135, 136, 137, 138, 150, 151, 144, 139*	⊢
	: , : , : , :
96	instantiation	292, 140	⊢
	: , :
97	instantiation	292, 141	⊢
	: , :
98	instantiation	178, 179	⊢
	: , :
99	instantiation	145, 146, 142, 315, 299, 150, 144, 207*, 302*	⊢
	: , : , : , :
100	instantiation	145, 146, 143, 315, 299, 150, 144, 207*, 302*	⊢
	: , : , : , :
101	instantiation	145, 146, 147, 148, 149, 150, 151, 207*, 208*	⊢
	: , : , : , :
102	instantiation	292, 152	⊢
	: , :
103	instantiation	153, 154, 155, 156	⊢
	: , : , : , : , :
104	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
105	theorem		⊢
	proveit.physics.quantum.QPE._Psi_ket_is_normalized_vec
106	instantiation	157	⊢
	: , : , :
107	instantiation	344	⊢
	:
108	instantiation	292, 158	⊢
	: , :
109	instantiation	159, 162, 160	⊢
	: , : , :
110	instantiation	161, 162, 163	⊢
	: , : , :
111	instantiation	164	⊢
	: , :
112	instantiation	344	⊢
	:
113	instantiation	292, 165	⊢
	: , :
114	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_all
115	instantiation	335	⊢
	: , : , :
116	instantiation	344	⊢
	:
117	instantiation	292, 245	⊢
	: , :
118	instantiation	344	⊢
	:
119	instantiation	226	⊢
	: , : , : , : , :
120	instantiation	226	⊢
	: , : , : , : , :
121	instantiation	226	⊢
	: , : , : , : , :
122	instantiation	338, 166, 167	⊢
	: , : , :
123	instantiation	234	⊢
	: , : , : , : , : , :
124	instantiation	234	⊢
	: , : , : , : , : , :
125	instantiation	234	⊢
	: , : , : , : , : , :
126	instantiation	338, 168, 202	⊢
	: , : , :
127	instantiation	342	⊢
	: , :
128	instantiation	342	⊢
	: , :
129	instantiation	342	⊢
	: , :
130	theorem		⊢
	proveit.numbers.numerals.decimals.posnat5
131	instantiation	226	⊢
	: , : , : , : , :
132	instantiation	226	⊢
	: , : , : , : , :
133	instantiation	176, 179, 200	⊢
	: , : , :
134	instantiation	338, 169, 170	⊢
	: , : , :
135	theorem		⊢
	proveit.numbers.numerals.decimals.posnat6
136	instantiation	234	⊢
	: , : , : , : , : , :
137	instantiation	234	⊢
	: , : , : , : , : , :
138	instantiation	234	⊢
	: , : , : , : , : , :
139	instantiation	338, 171, 202	⊢
	: , : , :
140	instantiation	311, 379, 374, 320, 299, 321, 291, 333, 337	⊢
	: , : , : , : , : , :
141	instantiation	172, 173, 174, 179	⊢
	: , : , :
142	instantiation	342	⊢
	: , :
143	instantiation	342	⊢
	: , :
144	instantiation	176, 177, 302	⊢
	: , : , :
145	theorem		⊢
	proveit.core_expr_types.tuples.general_len
146	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
147	instantiation	342	⊢
	: , :
148	instantiation	342	⊢
	: , :
149	instantiation	342	⊢
	: , :
150	instantiation	176, 175, 207	⊢
	: , : , :
151	instantiation	176, 177, 208	⊢
	: , : , :
152	instantiation	178, 179	⊢
	: , :
153	theorem		⊢
	proveit.core_expr_types.tuples.merge
154	instantiation	186, 180, 181	⊢
	:
155	instantiation	186, 182, 183	⊢
	:
156	instantiation	344	⊢
	:
157	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3
158	instantiation	190, 184, 185	⊢
	: , : , :
159	theorem		⊢
	proveit.core_expr_types.tuples.partition_front
160	instantiation	276, 332	⊢
	:
161	theorem		⊢
	proveit.core_expr_types.tuples.partition_back
162	instantiation	186, 187, 188	⊢
	:
163	instantiation	189, 332, 330, 352	⊢
	: , : , :
164	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2
165	instantiation	190, 191, 192	⊢
	: , : , :
166	instantiation	203, 197, 193, 194, 207, 302, 208, 200	⊢
	: , : , : , :
167	instantiation	338, 195, 202	⊢
	: , : , :
168	instantiation	203, 204, 196, 206, 207, 302, 208	⊢
	: , : , : , :
169	instantiation	203, 197, 198, 199, 200, 207, 302	⊢
	: , : , : , :
170	instantiation	338, 201, 202	⊢
	: , : , :
171	instantiation	203, 204, 205, 206, 207, 208, 302	⊢
	: , : , : , :
172	theorem		⊢
	proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1
173	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
174	instantiation	209, 359	⊢
	: , :
175	instantiation	377, 247, 376	⊢
	: , : , :
176	theorem		⊢
	proveit.logic.equality.sub_left_side_into
177	instantiation	377, 247, 362	⊢
	: , : , :
178	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
179	instantiation	377, 247, 240	⊢
	: , : , :
180	instantiation	218, 210, 365	⊢
	: , :
181	instantiation	220, 211	⊢
	: , :
182	instantiation	218, 212, 213	⊢
	: , :
183	instantiation	220, 214	⊢
	: , :
184	instantiation	222, 215	⊢
	: , : , :
185	instantiation	338, 216, 217	⊢
	: , : , :
186	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
187	instantiation	218, 366, 219	⊢
	: , :
188	instantiation	220, 221	⊢
	: , :
189	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
190	theorem		⊢
	proveit.logic.equality.sub_right_side_into
191	instantiation	222, 223	⊢
	: , : , :
192	instantiation	338, 224, 225	⊢
	: , : , :
193	instantiation	226	⊢
	: , : , : , : , :
194	instantiation	226	⊢
	: , : , : , : , :
195	instantiation	298, 229, 374, 320, 230, 299, 321, 333, 337	⊢
	: , : , : , : , : , :
196	instantiation	234	⊢
	: , : , : , : , : , :
197	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
198	instantiation	226	⊢
	: , : , : , : , :
199	instantiation	226	⊢
	: , : , : , : , :
200	instantiation	338, 227, 228	⊢
	: , : , :
201	instantiation	298, 320, 374, 229, 321, 299, 230, 333, 337	⊢
	: , : , : , : , : , :
202	instantiation	268, 231, 232, 233	⊢
	: , : , : , :
203	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
204	theorem		⊢
	proveit.numbers.numerals.decimals.nat6
205	instantiation	234	⊢
	: , : , : , : , : , :
206	instantiation	234	⊢
	: , : , : , : , : , :
207	instantiation	325, 332, 333, 326	⊢
	: , : , :
208	instantiation	338, 235, 236	⊢
	: , : , :
209	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
210	instantiation	377, 239, 238	⊢
	: , : , :
211	instantiation	237, 238	⊢
	:
212	instantiation	377, 239, 240	⊢
	: , : , :
213	instantiation	377, 241, 371	⊢
	: , : , :
214	instantiation	242, 347, 243, 350, 244, 245*, 246*	⊢
	: , : , :
215	instantiation	377, 247, 248	⊢
	: , : , :
216	instantiation	351, 329	⊢
	: , : , :
217	instantiation	314, 320, 374, 379, 321, 249, 330, 256, 332, 250*	⊢
	: , : , : , : , : , :
218	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
219	instantiation	360, 251, 306	⊢
	: , : , :
220	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
221	instantiation	252, 374	⊢
	:
222	theorem		⊢
	proveit.core_expr_types.tuples.range_len
223	instantiation	253, 359, 254, 379, 280	⊢
	: , :
224	instantiation	351, 329	⊢
	: , : , :
225	instantiation	314, 320, 374, 379, 321, 255, 332, 256, 257*	⊢
	: , : , : , : , : , :
226	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
227	instantiation	298, 320, 374, 321, 299, 322, 333, 337, 323, 332	⊢
	: , : , : , : , : , :
228	instantiation	258, 374, 320, 299, 321, 333, 337, 332	⊢
	: , : , : , : , : , : , : , :
229	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
230	instantiation	259	⊢
	: , : , : , :
231	instantiation	338, 260, 261	⊢
	: , : , :
232	instantiation	314, 320, 359, 321, 262, 264, 333, 337, 263*	⊢
	: , : , : , : , : , :
233	instantiation	314, 379, 359, 320, 264, 321, 265, 337, 266*	⊢
	: , : , : , : , : , :
234	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_6_typical_eq
235	instantiation	351, 267	⊢
	: , : , :
236	instantiation	268, 269, 270, 271	⊢
	: , : , : , :
237	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
238	instantiation	273, 376, 272	⊢
	: , :
239	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
240	instantiation	273, 376, 362	⊢
	: , :
241	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
242	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
243	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
244	instantiation	274, 275	⊢
	: , :
245	instantiation	276, 333	⊢
	:
246	instantiation	292, 277	⊢
	: , :
247	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
248	instantiation	278, 374, 320, 279, 321, 280, 379, 281	⊢
	: , : , : , : , :
249	instantiation	342	⊢
	: , :
250	instantiation	338, 282, 340	⊢
	: , : , :
251	instantiation	368, 283	⊢
	: , :
252	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
253	theorem		⊢
	proveit.numbers.addition.add_nat_closure
254	instantiation	335	⊢
	: , : , :
255	instantiation	342	⊢
	: , :
256	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
257	instantiation	338, 284, 352	⊢
	: , : , :
258	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
259	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
260	instantiation	286, 379, 359, 285, 333, 337	⊢
	: , : , : , : , : , : , :
261	instantiation	286, 374, 379, 287, 288, 333, 337	⊢
	: , : , : , : , : , : , :
262	instantiation	335	⊢
	: , : , :
263	instantiation	292, 289, 294*	⊢
	: , :
264	instantiation	335	⊢
	: , : , :
265	instantiation	290, 291, 333	⊢
	: , :
266	instantiation	292, 293, 294*	⊢
	: , :
267	instantiation	295, 333, 332	⊢
	: , :
268	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
269	instantiation	298, 320, 374, 321, 299, 296, 333, 337, 297, 332	⊢
	: , : , : , : , : , :
270	instantiation	298, 374, 379, 299, 300, 333, 337, 318, 323, 332	⊢
	: , : , : , : , : , :
271	instantiation	338, 301, 302	⊢
	: , : , :
272	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
273	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
274	theorem		⊢
	proveit.numbers.ordering.relax_less
275	instantiation	303, 362	⊢
	:
276	theorem		⊢
	proveit.numbers.addition.elim_zero_left
277	instantiation	304, 333, 337	⊢
	: , :
278	theorem		⊢
	proveit.numbers.addition.add_nat_pos_from_nonneg
279	instantiation	342	⊢
	: , :
280	instantiation	360, 305, 306	⊢
	: , : , :
281	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
282	instantiation	351, 307	⊢
	: , : , :
283	theorem		⊢
	proveit.numbers.number_sets.integers.zero_set_within_int
284	instantiation	351, 308	⊢
	: , : , :
285	instantiation	335	⊢
	: , : , :
286	theorem		⊢
	proveit.numbers.addition.leftward_commutation
287	instantiation	342	⊢
	: , :
288	instantiation	342	⊢
	: , :
289	instantiation	311, 320, 359, 379, 321, 312, 332, 333, 309*	⊢
	: , : , : , : , : , :
290	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
291	instantiation	377, 349, 310	⊢
	: , : , :
292	theorem		⊢
	proveit.logic.equality.equals_reversal
293	instantiation	311, 320, 359, 379, 321, 312, 332, 337, 313*	⊢
	: , : , : , : , : , :
294	instantiation	314, 320, 374, 379, 321, 315, 332, 316*	⊢
	: , : , : , : , : , :
295	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
296	instantiation	342	⊢
	: , :
297	instantiation	317, 318, 323	⊢
	: , :
298	theorem		⊢
	proveit.numbers.addition.disassociation
299	instantiation	342	⊢
	: , :
300	instantiation	342	⊢
	: , :
301	instantiation	319, 320, 379, 374, 321, 322, 333, 337, 323, 332, 324	⊢
	: , : , : , : , : , : , : , :
302	instantiation	325, 332, 337, 326	⊢
	: , : , :
303	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
304	theorem		⊢
	proveit.numbers.addition.commutation
305	instantiation	368, 327	⊢
	: , :
306	instantiation	328, 329	⊢
	: , :
307	instantiation	331, 330	⊢
	:
308	instantiation	331, 332	⊢
	:
309	instantiation	336, 333	⊢
	:
310	instantiation	377, 357, 334	⊢
	: , : , :
311	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
312	instantiation	335	⊢
	: , : , :
313	instantiation	336, 337	⊢
	:
314	theorem		⊢
	proveit.numbers.addition.association
315	instantiation	342	⊢
	: , :
316	instantiation	338, 339, 340	⊢
	: , : , :
317	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
318	instantiation	377, 349, 341	⊢
	: , : , :
319	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
320	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
321	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
322	instantiation	342	⊢
	: , :
323	instantiation	377, 349, 343	⊢
	: , : , :
324	instantiation	344	⊢
	:
325	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
326	instantiation	344	⊢
	:
327	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.zero_set_within_nat
328	theorem		⊢
	proveit.logic.sets.enumeration.fold_singleton
329	theorem		⊢
	proveit.numbers.negation.negated_zero
330	instantiation	377, 349, 345	⊢
	: , : , :
331	theorem		⊢
	proveit.numbers.addition.elim_zero_right
332	instantiation	377, 349, 346	⊢
	: , : , :
333	instantiation	377, 349, 347	⊢
	: , : , :
334	instantiation	377, 367, 348	⊢
	: , : , :
335	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
336	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
337	instantiation	377, 349, 350	⊢
	: , : , :
338	axiom		⊢
	proveit.logic.equality.equals_transitivity
339	instantiation	351, 352	⊢
	: , : , :
340	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_1
341	instantiation	377, 353, 354	⊢
	: , : , :
342	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
343	instantiation	377, 357, 355	⊢
	: , : , :
344	axiom		⊢
	proveit.logic.equality.equals_reflexivity
345	instantiation	377, 357, 356	⊢
	: , : , :
346	instantiation	377, 357, 358	⊢
	: , : , :
347	instantiation	360, 361, 376	⊢
	: , : , :
348	instantiation	377, 378, 359	⊢
	: , : , :
349	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
350	instantiation	360, 361, 362	⊢
	: , : , :
351	axiom		⊢
	proveit.logic.equality.substitution
352	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
353	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_neg_within_real
354	instantiation	377, 363, 364	⊢
	: , : , :
355	instantiation	377, 367, 365	⊢
	: , : , :
356	instantiation	377, 367, 366	⊢
	: , : , :
357	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
358	instantiation	377, 367, 373	⊢
	: , : , :
359	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
360	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
361	instantiation	368, 369	⊢
	: , :
362	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
363	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_neg_within_real_neg
364	instantiation	377, 370, 371	⊢
	: , : , :
365	instantiation	372, 373	⊢
	:
366	instantiation	377, 378, 374	⊢
	: , : , :
367	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
368	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
369	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
370	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.neg_int_within_rational_neg
371	instantiation	375, 376	⊢
	:
372	theorem		⊢
	proveit.numbers.negation.int_closure
373	instantiation	377, 378, 379	⊢
	: , : , :
374	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
375	theorem		⊢
	proveit.numbers.negation.int_neg_closure
376	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
377	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
378	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
379	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements