Proof of proveit.physics.quantum.QPE._outcome_prob theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import m, n, defaults
from proveit.physics.quantum import var_ket_psi
from proveit.physics.quantum.circuits import born_rule_on_register, Qcircuit
from proveit.physics.quantum.QPE import (
    _alpha_m_def, _ket_u, _Psi_ket, _Psi_ket_is_normalized_vec,
    _Psi_output, _psi_t_ket_is_normalized_vec,
    _s, _s_in_nat_pos, _t, _t_in_natural_pos, _u_ket_register)

%proving _outcome_prob

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_outcome_prob:
(see dependencies)

from proveit.numbers import Mult
Mult.change_simplification_directives(combine_all_exponents=True)

defaults.assumptions = _outcome_prob.conditions

defaults.assumptions:

_alpha_m_def

 ⊢  

alpha_m_replacement = _alpha_m_def.instantiate().derive_reversed()

alpha_m_replacement:  ⊢  

born_rule_on_register

 ⊢  

born_rule_prob = born_rule_on_register.instantiate({m:_t, n:m, var_ket_psi:_Psi_ket},
                                                   replacements=[alpha_m_replacement])

born_rule_prob:  ⊢  

qcircuit_prob2 = Qcircuit.trivial_expansion_below(born_rule_prob, _ket_u, _s)

qcircuit_prob2:  ⊢  

_Psi_output

 ⊢  

qcircuit_prob3 = Qcircuit.concatenation(_Psi_output, qcircuit_prob2)

qcircuit_prob3:  ⊢  

_outcome_prob may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.physics.quantum.QPE._outcome_prob has been proven.

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