# Show the Proof¶

In [1]:
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

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