Proof of proveit.physics.quantum.QPE._Psi_output theorem¶

In [1]:

import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import m, n, s, t, U
from proveit.numbers import zero
from proveit.physics.quantum import var_ket_psi, Ket
from proveit.physics.quantum.circuits import Qcircuit, unitary_gate_operation
from proveit.physics.quantum.QFT import InverseFourierTransform, invFT_is_unitary
from proveit.physics.quantum.QPE import (
    _s, _t, _U, _ket_u, _psi__t_ket, _psi_t_ket_is_normalized_vec,
    _s_in_nat_pos, _t_in_natural_pos, _unitary_U, _u_ket_register, QPE_def, 
    _Psi_def, _psi_t_output)

In [2]:

%proving _Psi_output

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

(see dependencies)

In [3]:

QPE_def

⊢

In [4]:

QPE_def_inst = QPE_def.instantiate({s:_s, t:_t, U:_U})

QPE_def_inst: ⊢

In [5]:

invFT_is_unitary.instantiate({n:_t})

⊢

In [6]:

_psi_t_ket_is_normalized_vec.instantiate({t:_t})

⊢

In [7]:

unitary_gate_operation

⊢

In [8]:

qcircuit_prob1 = unitary_gate_operation.instantiate(
    {m:_t, U:InverseFourierTransform(_t), var_ket_psi:_psi__t_ket})

qcircuit_prob1: ⊢

In [9]:

_Psi_def

⊢

In [10]:

_Psi_output

In [11]:

qcircuit_prob2 = _Psi_def.sub_left_side_into(qcircuit_prob1)

qcircuit_prob2: ⊢

In [12]:

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

qcircuit_prob3: ⊢

In [13]:

psi_to_out = _psi_t_output.instantiate({t:_t})

psi_to_out: ⊢

In [14]:

qcircuit_prob4 = Qcircuit.concatenation(psi_to_out, qcircuit_prob3)

qcircuit_prob4: ⊢

In [15]:

QPE_def_inst

⊢

In [16]:

QPE_def_inst.sub_left_side_into(qcircuit_prob4)

⊢

_Psi_output has been proven.  Now simply execute "%qed".

In [17]:

%qed

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

Out[17]:

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