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, 58, 105, 4, 5, 6, 7, 8, 9	⊢
	: , : , : , :
2	instantiation	10, 58, 11, 12, 13, 14, 15	⊢
	: , : , :
3	theorem		⊢
	proveit.physics.quantum.circuits.qcircuit_eq
4	instantiation	122, 16, 18, 19	⊢
	: , : , : , :
5	instantiation	122, 17, 18, 19	⊢
	: , : , : , :
6	instantiation	122, 20, 24, 25	⊢
	: , : , : , :
7	instantiation	122, 21, 24, 25	⊢
	: , : , : , :
8	instantiation	122, 22, 24, 25	⊢
	: , : , : , :
9	instantiation	122, 23, 24, 25	⊢
	: , : , : , :
10	theorem		⊢
	proveit.core_expr_types.expr_arrays.varray_eq_via_elem_eq
11	instantiation	174	⊢
	: , : , :
12	instantiation	174	⊢
	: , : , :
13	instantiation	139, 26	⊢
	: , :
14	instantiation	184	⊢
	:
15	instantiation	184	⊢
	:
16	instantiation	42, 27, 28, 29, 72, 30, 47, 41, 31*	⊢
	: , : , : , :
17	instantiation	42, 32, 33, 34, 35, 47, 48, 41, 36*	⊢
	: , : , : , :
18	instantiation	139, 37	⊢
	: , :
19	instantiation	139, 38	⊢
	: , :
20	instantiation	63, 64	⊢
	: , :
21	instantiation	42, 43, 39, 158, 146, 47, 41, 80*, 149*	⊢
	: , : , : , :
22	instantiation	42, 43, 40, 158, 146, 47, 41, 80*, 149*	⊢
	: , : , : , :
23	instantiation	42, 43, 44, 45, 46, 47, 48, 80*, 81*	⊢
	: , : , : , :
24	instantiation	184	⊢
	:
25	instantiation	139, 49	⊢
	: , :
26	instantiation	50, 51, 52, 53	⊢
	: , : , : , : , :
27	theorem		⊢
	proveit.numbers.numerals.decimals.posnat5
28	instantiation	91	⊢
	: , : , : , : , :
29	instantiation	91	⊢
	: , : , : , : , :
30	instantiation	61, 64, 73	⊢
	: , : , :
31	instantiation	177, 54, 55	⊢
	: , : , :
32	theorem		⊢
	proveit.numbers.numerals.decimals.posnat6
33	instantiation	99	⊢
	: , : , : , : , : , :
34	instantiation	99	⊢
	: , : , : , : , : , :
35	instantiation	99	⊢
	: , : , : , : , : , :
36	instantiation	177, 56, 75	⊢
	: , : , :
37	instantiation	154, 214, 164, 163, 146, 165, 138, 172, 176	⊢
	: , : , : , : , : , :
38	instantiation	57, 58, 59, 64	⊢
	: , : , :
39	instantiation	181	⊢
	: , :
40	instantiation	181	⊢
	: , :
41	instantiation	61, 62, 149	⊢
	: , : , :
42	theorem		⊢
	proveit.core_expr_types.tuples.general_len
43	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
44	instantiation	181	⊢
	: , :
45	instantiation	181	⊢
	: , :
46	instantiation	181	⊢
	: , :
47	instantiation	61, 60, 80	⊢
	: , : , :
48	instantiation	61, 62, 81	⊢
	: , : , :
49	instantiation	63, 64	⊢
	: , :
50	theorem		⊢
	proveit.core_expr_types.tuples.merge
51	instantiation	67, 65, 66	⊢
	:
52	instantiation	67, 68, 69	⊢
	:
53	instantiation	184	⊢
	:
54	instantiation	76, 70, 71, 72, 73, 80, 149	⊢
	: , : , : , :
55	instantiation	177, 74, 75	⊢
	: , : , :
56	instantiation	76, 77, 78, 79, 80, 81, 149	⊢
	: , : , : , :
57	theorem		⊢
	proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1
58	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
59	instantiation	82, 196	⊢
	: , :
60	instantiation	212, 83, 211	⊢
	: , : , :
61	theorem		⊢
	proveit.logic.equality.sub_left_side_into
62	instantiation	212, 83, 199	⊢
	: , : , :
63	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
64	instantiation	212, 83, 105	⊢
	: , : , :
65	instantiation	86, 84, 202	⊢
	: , :
66	instantiation	89, 85	⊢
	: , :
67	theorem		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
68	instantiation	86, 87, 88	⊢
	: , :
69	instantiation	89, 90	⊢
	: , :
70	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
71	instantiation	91	⊢
	: , : , : , : , :
72	instantiation	91	⊢
	: , : , : , : , :
73	instantiation	177, 92, 93	⊢
	: , : , :
74	instantiation	145, 163, 164, 94, 165, 146, 95, 172, 176	⊢
	: , : , : , : , : , :
75	instantiation	122, 96, 97, 98	⊢
	: , : , : , :
76	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
77	theorem		⊢
	proveit.numbers.numerals.decimals.nat6
78	instantiation	99	⊢
	: , : , : , : , : , :
79	instantiation	99	⊢
	: , : , : , : , : , :
80	instantiation	169, 170, 172, 171	⊢
	: , : , :
81	instantiation	177, 100, 101	⊢
	: , : , :
82	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
83	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
84	instantiation	212, 104, 103	⊢
	: , : , :
85	instantiation	102, 103	⊢
	:
86	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
87	instantiation	212, 104, 105	⊢
	: , : , :
88	instantiation	212, 106, 207	⊢
	: , : , :
89	theorem		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
90	instantiation	107, 185, 108, 188, 109, 110*, 111*	⊢
	: , : , :
91	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
92	instantiation	145, 163, 164, 165, 146, 166, 172, 176, 167, 170	⊢
	: , : , : , : , : , :
93	instantiation	112, 164, 163, 146, 165, 172, 176, 170	⊢
	: , : , : , : , : , : , : , :
94	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
95	instantiation	113	⊢
	: , : , : , :
96	instantiation	177, 114, 115	⊢
	: , : , :
97	instantiation	157, 163, 196, 165, 116, 118, 172, 176, 117*	⊢
	: , : , : , : , : , :
98	instantiation	157, 214, 196, 163, 118, 165, 119, 176, 120*	⊢
	: , : , : , : , : , :
99	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_6_typical_eq
100	instantiation	189, 121	⊢
	: , : , :
101	instantiation	122, 123, 124, 125	⊢
	: , : , : , :
102	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
103	instantiation	127, 211, 126	⊢
	: , :
104	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
105	instantiation	127, 211, 199	⊢
	: , :
106	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
107	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
108	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
109	instantiation	128, 129	⊢
	: , :
110	instantiation	130, 172	⊢
	:
111	instantiation	139, 131	⊢
	: , :
112	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
113	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
114	instantiation	133, 214, 196, 132, 172, 176	⊢
	: , : , : , : , : , : , :
115	instantiation	133, 164, 214, 134, 135, 172, 176	⊢
	: , : , : , : , : , : , :
116	instantiation	174	⊢
	: , : , :
117	instantiation	139, 136, 141*	⊢
	: , :
118	instantiation	174	⊢
	: , : , :
119	instantiation	137, 138, 172	⊢
	: , :
120	instantiation	139, 140, 141*	⊢
	: , :
121	instantiation	142, 172, 170	⊢
	: , :
122	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
123	instantiation	145, 163, 164, 165, 146, 143, 172, 176, 144, 170	⊢
	: , : , : , : , : , :
124	instantiation	145, 164, 214, 146, 147, 172, 176, 161, 167, 170	⊢
	: , : , : , : , : , :
125	instantiation	177, 148, 149	⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
127	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
128	theorem		⊢
	proveit.numbers.ordering.relax_less
129	instantiation	150, 199	⊢
	:
130	theorem		⊢
	proveit.numbers.addition.elim_zero_left
131	instantiation	151, 172, 176	⊢
	: , :
132	instantiation	174	⊢
	: , : , :
133	theorem		⊢
	proveit.numbers.addition.leftward_commutation
134	instantiation	181	⊢
	: , :
135	instantiation	181	⊢
	: , :
136	instantiation	154, 163, 196, 214, 165, 155, 170, 172, 152*	⊢
	: , : , : , : , : , :
137	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
138	instantiation	212, 187, 153	⊢
	: , : , :
139	theorem		⊢
	proveit.logic.equality.equals_reversal
140	instantiation	154, 163, 196, 214, 165, 155, 170, 176, 156*	⊢
	: , : , : , : , : , :
141	instantiation	157, 163, 164, 214, 165, 158, 170, 159*	⊢
	: , : , : , : , : , :
142	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
143	instantiation	181	⊢
	: , :
144	instantiation	160, 161, 167	⊢
	: , :
145	theorem		⊢
	proveit.numbers.addition.disassociation
146	instantiation	181	⊢
	: , :
147	instantiation	181	⊢
	: , :
148	instantiation	162, 163, 214, 164, 165, 166, 172, 176, 167, 170, 168	⊢
	: , : , : , : , : , : , : , :
149	instantiation	169, 170, 176, 171	⊢
	: , : , :
150	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
151	theorem		⊢
	proveit.numbers.addition.commutation
152	instantiation	175, 172	⊢
	:
153	instantiation	212, 194, 173	⊢
	: , : , :
154	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
155	instantiation	174	⊢
	: , : , :
156	instantiation	175, 176	⊢
	:
157	theorem		⊢
	proveit.numbers.addition.association
158	instantiation	181	⊢
	: , :
159	instantiation	177, 178, 179	⊢
	: , : , :
160	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
161	instantiation	212, 187, 180	⊢
	: , : , :
162	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
163	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
164	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
165	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
166	instantiation	181	⊢
	: , :
167	instantiation	212, 187, 182	⊢
	: , : , :
168	instantiation	184	⊢
	:
169	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
170	instantiation	212, 187, 183	⊢
	: , : , :
171	instantiation	184	⊢
	:
172	instantiation	212, 187, 185	⊢
	: , : , :
173	instantiation	212, 203, 186	⊢
	: , : , :
174	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
175	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
176	instantiation	212, 187, 188	⊢
	: , : , :
177	axiom		⊢
	proveit.logic.equality.equals_transitivity
178	instantiation	189, 190	⊢
	: , : , :
179	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_1
180	instantiation	212, 191, 192	⊢
	: , : , :
181	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
182	instantiation	212, 194, 193	⊢
	: , : , :
183	instantiation	212, 194, 195	⊢
	: , : , :
184	axiom		⊢
	proveit.logic.equality.equals_reflexivity
185	instantiation	197, 198, 211	⊢
	: , : , :
186	instantiation	212, 213, 196	⊢
	: , : , :
187	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
188	instantiation	197, 198, 199	⊢
	: , : , :
189	axiom		⊢
	proveit.logic.equality.substitution
190	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
191	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_neg_within_real
192	instantiation	212, 200, 201	⊢
	: , : , :
193	instantiation	212, 203, 202	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
195	instantiation	212, 203, 209	⊢
	: , : , :
196	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
197	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
198	instantiation	204, 205	⊢
	: , :
199	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
200	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_neg_within_real_neg
201	instantiation	212, 206, 207	⊢
	: , : , :
202	instantiation	208, 209	⊢
	:
203	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
204	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
205	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
206	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.neg_int_within_rational_neg
207	instantiation	210, 211	⊢
	:
208	theorem		⊢
	proveit.numbers.negation.int_closure
209	instantiation	212, 213, 214	⊢
	: , : , :
210	theorem		⊢
	proveit.numbers.negation.int_neg_closure
211	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
212	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
213	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
214	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements