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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, e, l, x, y, defaults
from proveit.logic import Iff, InSet, Or, SubsetEq, Union
from proveit.numbers import zero, Add, subtract, greater_eq, Less, Neg, NaturalPos
from proveit.numbers.ordering import less_or_greater_eq
from proveit.physics.quantum.QPE import (
    _full_domain, _modabs_in_full_domain_simp, _neg_domain, _pos_domain)
from proveit.physics.quantum.QPE import (
    _two_pow_t, _two_pow_t__minus_one, _t_in_natural_pos, _two_pow_t_minus_one_is_nat_pos)

%proving _fail_sum_prob_conds_equiv_lemma

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

defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions()

defaults.assumptions:

We want to derive the logical equivalence (if and only if) between the following conditions:

lhs_condition = _fail_sum_prob_conds_equiv_lemma.instance_expr.instance_expr.lhs

lhs_condition:

rhs_condition = _fail_sum_prob_conds_equiv_lemma.instance_expr.instance_expr.rhs

rhs_condition:

(1) $\text{lhs} \Rightarrow \text{rhs}$. This direction is straightforward using the fact that $\{-2^{t-1}+1~\ldotp \ldotp~-(e+1)\} \cup \{e + 1~\ldotp \ldotp~2^{t-1}\} \subseteq \{-2^{t-1}+1~\ldotp \ldotp~2^{t-2}\}$.

SubsetEq(Union(_neg_domain, _pos_domain), _full_domain).prove()

 ⊢  

rhs_condition.prove(assumptions=defaults.assumptions + (lhs_condition,))

,  ⊢  

(2) $\text{lhs} \Leftarrow \text{rhs}$.

Going from rhs to lhs requires us to consider the non-negative/negative cases separately.

2(a): $\text{lhs} \Leftarrow \text{rhs}$. The NON-NEGATIVE case.

# update our default assumptions
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition, greater_eq(l, zero)]

defaults.assumptions:

_modabs_in_full_domain_simp

 ⊢  

_modabs_in_full_domain_simp.instantiate().sub_right_side_into(rhs_condition.operands[1])

,  ⊢  

InSet(subtract(l, e), NaturalPos).prove()

, ,  ⊢  

lhs_condition.prove()

, ,  ⊢  

2(b): $\text{lhs} \Leftarrow \text{rhs}$. The NEGATIVE case.

# update our default assumptions
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition, Less(l, zero)]

defaults.assumptions:

_modabs_in_full_domain_simp.instantiate().sub_right_side_into(rhs_condition.operands[1])

,  ⊢  

InSet(Neg(Add(e, l)), NaturalPos).prove()

, ,  ⊢  

lhs_condition.prove()

, ,  ⊢  

Since either $l \geq 0$ or $l < 0$ but we can derive lhs_condition either way, then lhs_condition must be true (under these assumptions).

# update our default assumptions (removing the specifics about ell being negative or non-negative)
defaults.assumptions = _fail_sum_prob_conds_equiv_lemma.all_conditions() + [rhs_condition]

defaults.assumptions:

less_or_greater_eq

 ⊢  

less_or_greater_eq.instantiate({x:l, y:zero})

 ⊢  

Or(Less(l, zero), greater_eq(l, zero)).derive_via_dilemma(lhs_condition)

,  ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	⊢
	: , :
2	theorem		⊢
	proveit.logic.booleans.implication.iff_intro
3	deduction	5	⊢
4	deduction	6	⊢
5	instantiation	85, 7, 8	,  ⊢
	: , :
6	instantiation	9, 10, 11, 26, 12, 13	,  ⊢
	: , : , :
7	instantiation	365, 14, 15	,  ⊢
	: , : , :
8	instantiation	283, 24	⊢
	: , :
9	theorem		⊢
	proveit.logic.booleans.disjunction.singular_constructive_dilemma
10	instantiation	16, 18	⊢
	: , :
11	instantiation	17, 18	⊢
	: , :
12	deduction	19	,  ⊢
13	deduction	20	,  ⊢
14	instantiation	21, 394, 35, 22, 23	⊢
	: , : , :
15	instantiation	378, 24	⊢
	: , :
16	axiom		⊢
	proveit.logic.booleans.disjunction.left_in_bool
17	axiom		⊢
	proveit.logic.booleans.disjunction.right_in_bool
18	instantiation	25, 26	⊢
	:
19	instantiation	85, 27, 260	, ,  ⊢
	: , :
20	instantiation	85, 28, 260	, ,  ⊢
	: , :
21	conjecture		⊢
	proveit.logic.sets.unification.union_inclusion
22	instantiation	30, 377, 83, 404, 29	⊢
	: , : , : , :
23	instantiation	30, 377, 113, 404, 31	⊢
	: , : , : , :
24	assumption		⊢
25	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
26	instantiation	32, 328, 132	⊢
	: , :
27	instantiation	34, 394, 35, 33	, ,  ⊢
	: , : , :
28	instantiation	34, 394, 35, 36	, ,  ⊢
	: , : , :
29	instantiation	40, 319, 37, 38, 52, 39	⊢
	: , :
30	conjecture		⊢
	proveit.numbers.number_sets.integers.interval_subset_eq
31	instantiation	40, 319, 41, 42, 43, 44	⊢
	: , :
32	conjecture		⊢
	proveit.numbers.ordering.less_or_greater_eq
33	instantiation	110, 45, 46	, ,  ⊢
	: , :
34	conjecture		⊢
	proveit.logic.sets.unification.membership_folding
35	instantiation	323	⊢
	: , :
36	instantiation	114, 47, 48	, ,  ⊢
	: , :
37	instantiation	335	⊢
	: , : , :
38	instantiation	57, 154, 49	⊢
	: , :
39	instantiation	325, 50	⊢
	: , :
40	conjecture		⊢
	proveit.logic.booleans.conjunction.and_if_all
41	instantiation	335	⊢
	: , : , :
42	instantiation	51, 52, 53	⊢
	: , : , :
43	instantiation	131, 384, 351, 54, 55, 56*	⊢
	: , : , :
44	instantiation	57, 151, 58	⊢
	: , :
45	instantiation	63, 377, 83, 352, 59	, ,  ⊢
	: , : , :
46	instantiation	61, 60	, ,  ⊢
	: , :
47	instantiation	61, 62	, ,  ⊢
	: , :
48	instantiation	63, 113, 404, 352, 64	, ,  ⊢
	: , : , :
49	instantiation	303	⊢
	:
50	instantiation	149, 156, 65	⊢
	: , : , :
51	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
52	instantiation	131, 66, 351, 75, 76, 67*, 68*	⊢
	: , : , :
53	instantiation	131, 172, 69, 70, 71, 72*, 73*	⊢
	: , : , :
54	instantiation	327, 75, 384	⊢
	: , :
55	instantiation	74, 351, 75, 384, 76, 77	⊢
	: , : , :
56	instantiation	314, 78, 277, 79	⊢
	: , : , : , :
57	conjecture		⊢
	proveit.numbers.ordering.relax_equal_to_less_eq
58	instantiation	303	⊢
	:
59	instantiation	85, 155, 80	, ,  ⊢
	: , :
60	instantiation	82, 113, 404, 352, 81	, ,  ⊢
	: , : , :
61	theorem		⊢
	proveit.logic.sets.membership.unfold_not_in_set
62	instantiation	82, 377, 83, 352, 84	, ,  ⊢
	: , : , :
63	conjecture		⊢
	proveit.numbers.number_sets.integers.in_interval
64	instantiation	85, 86, 152	, ,  ⊢
	: , :
65	instantiation	187, 409	⊢
	:
66	instantiation	87, 319, 88, 89, 384, 206	⊢
	: , :
67	instantiation	314, 90, 91, 92	⊢
	: , : , : , :
68	instantiation	331, 93	⊢
	: , :
69	instantiation	229, 397, 132	⊢
	: , :
70	instantiation	327, 207, 397	⊢
	: , :
71	instantiation	94, 95, 96, 411, 97, 98	⊢
	: , : , :
72	instantiation	331, 99	⊢
	: , :
73	instantiation	314, 100, 101, 102	⊢
	: , : , : , :
74	conjecture		⊢
	proveit.numbers.ordering.less_eq_add_right
75	instantiation	412, 401, 103	⊢
	: , : , :
76	instantiation	188, 400, 399, 391	⊢
	: , : , :
77	instantiation	166, 406	⊢
	:
78	instantiation	272, 104, 105	⊢
	: , : , :
79	instantiation	331, 297	⊢
	: , :
80	instantiation	131, 309, 384, 106, 107, 108*, 109*	, ,  ⊢
	: , : , :
81	instantiation	110, 111, 112	, ,  ⊢
	: , :
82	conjecture		⊢
	proveit.numbers.number_sets.integers.int_not_in_interval
83	instantiation	410, 113	⊢
	:
84	instantiation	114, 115, 116	, ,  ⊢
	: , :
85	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
86	instantiation	131, 351, 384, 117, 118, 119*, 120*	, ,  ⊢
	: , : , :
87	conjecture		⊢
	proveit.numbers.addition.add_real_closure
88	instantiation	335	⊢
	: , : , :
89	instantiation	412, 401, 121	⊢
	: , : , :
90	instantiation	272, 122, 123	⊢
	: , : , :
91	instantiation	303	⊢
	:
92	instantiation	331, 124	⊢
	: , :
93	instantiation	314, 184, 125, 126	⊢
	: , : , : , :
94	conjecture		⊢
	proveit.numbers.ordering.less_add_right_weak_int
95	instantiation	412, 413, 127	⊢
	: , : , :
96	instantiation	412, 413, 128	⊢
	: , : , :
97	instantiation	129, 397, 132, 351, 294, 130	⊢
	: , : , :
98	instantiation	131, 344, 132, 203, 133, 134*, 135*	⊢
	: , : , :
99	instantiation	314, 184, 185, 136	⊢
	: , : , : , :
100	instantiation	299, 300, 414, 406, 302, 138, 175, 387, 137	⊢
	: , : , : , : , : , :
101	instantiation	299, 414, 300, 138, 254, 302, 175, 387, 322, 342	⊢
	: , : , : , : , : , :
102	instantiation	314, 139, 140, 141	⊢
	: , : , : , :
103	instantiation	412, 407, 399	⊢
	: , : , :
104	instantiation	333, 142	⊢
	: , : , :
105	instantiation	272, 143, 144	⊢
	: , : , :
106	instantiation	365, 366, 145	, ,  ⊢
	: , : , :
107	instantiation	157, 145	, ,  ⊢
	:
108	instantiation	272, 146, 147	⊢
	: , : , :
109	instantiation	331, 148	,  ⊢
	: , :
110	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_only_left
111	instantiation	149, 326, 150	,  ⊢
	: , : , :
112	instantiation	153, 328, 151, 152	⊢
	: , :
113	instantiation	403, 376, 400	⊢
	: , :
114	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_only_right
115	instantiation	153, 154, 328, 155	⊢
	: , :
116	instantiation	311, 156, 296	,  ⊢
	: , : , :
117	instantiation	327, 328, 206	,  ⊢
	: , :
118	instantiation	157, 158	, ,  ⊢
	:
119	instantiation	340, 370, 337	⊢
	: , :
120	instantiation	272, 159, 160	,  ⊢
	: , : , :
121	instantiation	412, 407, 392	⊢
	: , : , :
122	instantiation	333, 244	⊢
	: , : , :
123	instantiation	272, 161, 162	⊢
	: , : , :
124	instantiation	333, 271	⊢
	: , : , :
125	instantiation	340, 322, 342	⊢
	: , :
126	instantiation	331, 163	⊢
	: , :
127	instantiation	164, 414, 300	⊢
	: , :
128	instantiation	164, 414, 165	⊢
	: , :
129	conjecture		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
130	instantiation	187, 394	⊢
	:
131	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
132	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
133	instantiation	166, 319	⊢
	:
134	instantiation	278, 167, 168	⊢
	: , : , :
135	instantiation	282, 387, 370, 169, 170	⊢
	: , : , :
136	instantiation	331, 171	⊢
	: , :
137	instantiation	412, 396, 172	⊢
	: , : , :
138	instantiation	323	⊢
	: , :
139	instantiation	173, 406, 175, 387, 322, 342	⊢
	: , : , : , : , : , : , :
140	instantiation	247, 300, 414, 302, 174, 257, 175, 322, 387, 342, 176*	⊢
	: , : , : , : , : , :
141	instantiation	247, 406, 414, 300, 257, 302, 337, 387, 342, 258*	⊢
	: , : , : , : , : , :
142	instantiation	272, 177, 178	⊢
	: , : , :
143	instantiation	299, 300, 414, 406, 302, 179, 336, 342, 370	⊢
	: , : , : , : , : , :
144	instantiation	195, 370, 336, 183	⊢
	: , : , :
145	instantiation	180, 181	, ,  ⊢
	:
146	instantiation	299, 406, 414, 300, 289, 302, 370, 292, 342	⊢
	: , : , : , : , : , :
147	instantiation	182, 370, 292, 183	⊢
	: , : , :
148	instantiation	314, 184, 185, 186	,  ⊢
	: , : , : , :
149	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
150	instantiation	187, 217	⊢
	:
151	instantiation	365, 366, 409	⊢
	: , : , :
152	instantiation	188, 377, 404, 364	⊢
	: , : , :
153	conjecture		⊢
	proveit.numbers.ordering.not_less_from_less_eq
154	instantiation	412, 401, 189	⊢
	: , : , :
155	instantiation	329, 377, 404, 364	⊢
	: , : , :
156	instantiation	190, 191	⊢
	:
157	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
158	instantiation	293, 192, 193	, ,  ⊢
	:
159	instantiation	299, 300, 414, 406, 302, 194, 292, 322, 337	,  ⊢
	: , : , : , : , : , :
160	instantiation	195, 337, 292, 197	,  ⊢
	: , : , :
161	instantiation	299, 406, 319, 300, 320, 302, 337, 321, 370, 322	⊢
	: , : , : , : , : , :
162	instantiation	275, 300, 414, 302, 196, 337, 321, 370, 197	⊢
	: , : , : , : , : , : , : , :
163	instantiation	272, 198, 199	⊢
	: , : , :
164	conjecture		⊢
	proveit.numbers.multiplication.mult_nat_closure_bin
165	instantiation	200, 376, 201	⊢
	:
166	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
167	instantiation	202, 342	⊢
	:
168	instantiation	340, 342, 252	⊢
	: , :
169	instantiation	412, 396, 203	⊢
	: , : , :
170	conjecture		⊢
	proveit.numbers.numerals.decimals.add_2_1
171	instantiation	272, 204, 205	⊢
	: , : , :
172	instantiation	327, 206, 344	⊢
	: , :
173	conjecture		⊢
	proveit.numbers.addition.leftward_commutation
174	instantiation	323	⊢
	: , :
175	instantiation	412, 396, 207	⊢
	: , : , :
176	instantiation	272, 208, 209, 210*	⊢
	: , : , :
177	instantiation	333, 243	⊢
	: , : , :
178	instantiation	272, 211, 212	⊢
	: , : , :
179	instantiation	323	⊢
	: , :
180	conjecture		⊢
	proveit.numbers.negation.nat_pos_closure
181	instantiation	213, 214, 215	, ,  ⊢
	:
182	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
183	instantiation	303	⊢
	:
184	instantiation	286, 337, 370	⊢
	: , :
185	instantiation	303	⊢
	:
186	instantiation	331, 216	,  ⊢
	: , :
187	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
188	conjecture		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
189	instantiation	412, 407, 377	⊢
	: , : , :
190	conjecture		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
191	instantiation	268, 217	⊢
	:
192	instantiation	403, 352, 218	,  ⊢
	: , :
193	instantiation	219, 220	,  ⊢
	: , :
194	instantiation	323	⊢
	: , :
195	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
196	instantiation	323	⊢
	: , :
197	instantiation	303	⊢
	:
198	instantiation	272, 221, 222	⊢
	: , : , :
199	instantiation	272, 223, 224	⊢
	: , : , :
200	conjecture		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
201	instantiation	325, 294	⊢
	: , :
202	conjecture		⊢
	proveit.numbers.addition.elim_zero_right
203	instantiation	412, 401, 225	⊢
	: , : , :
204	instantiation	333, 226	⊢
	: , : , :
205	instantiation	272, 227, 228	⊢
	: , : , :
206	instantiation	355, 351	⊢
	:
207	instantiation	229, 397, 351	⊢
	: , :
208	instantiation	333, 230	⊢
	: , : , :
209	instantiation	331, 231	⊢
	: , :
210	instantiation	272, 232, 233	⊢
	: , : , :
211	instantiation	299, 300, 414, 406, 302, 301, 336, 306, 370	⊢
	: , : , : , : , : , :
212	instantiation	247, 406, 414, 300, 248, 302, 336, 306, 370, 249*	⊢
	: , : , : , : , : , :
213	conjecture		⊢
	proveit.numbers.number_sets.integers.neg_int_is_int_neg
214	instantiation	403, 376, 352	,  ⊢
	: , :
215	instantiation	234, 328, 351, 310, 235, 236*	, ,  ⊢
	: , : , :
216	instantiation	272, 237, 238	,  ⊢
	: , : , :
217	instantiation	239, 269, 347	⊢
	: , :
218	instantiation	412, 240, 241	⊢
	: , : , :
219	conjecture		⊢
	proveit.numbers.addition.subtraction.pos_difference
220	instantiation	278, 260, 242	,  ⊢
	: , : , :
221	instantiation	333, 243	⊢
	: , : , :
222	instantiation	333, 244	⊢
	: , : , :
223	instantiation	272, 245, 246	⊢
	: , : , :
224	instantiation	247, 300, 414, 406, 302, 248, 306, 370, 322, 249*	⊢
	: , : , : , : , : , :
225	instantiation	412, 407, 250	⊢
	: , : , :
226	instantiation	251, 387	⊢
	:
227	instantiation	299, 406, 414, 300, 254, 302, 252, 322, 342	⊢
	: , : , : , : , : , :
228	instantiation	253, 300, 414, 302, 254, 322, 342	⊢
	: , : , : , :
229	conjecture		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
230	instantiation	331, 255	⊢
	: , :
231	instantiation	256, 300, 414, 406, 302, 257, 387, 342, 337	⊢
	: , : , : , : , : , :
232	instantiation	333, 258	⊢
	: , : , :
233	instantiation	259, 337	⊢
	:
234	conjecture		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
235	instantiation	278, 260, 261	,  ⊢
	: , : , :
236	instantiation	262, 292, 263	⊢
	: , :
237	instantiation	333, 264	,  ⊢
	: , : , :
238	instantiation	314, 265, 266, 267	,  ⊢
	: , : , : , :
239	conjecture		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
240	conjecture		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
241	instantiation	268, 269	⊢
	:
242	instantiation	284, 364, 270*	,  ⊢
	:
243	instantiation	333, 297	⊢
	: , : , :
244	instantiation	333, 271	⊢
	: , : , :
245	instantiation	272, 273, 274	⊢
	: , : , :
246	instantiation	275, 300, 406, 414, 302, 276, 336, 306, 370, 322, 277	⊢
	: , : , : , : , : , : , : , :
247	conjecture		⊢
	proveit.numbers.addition.association
248	instantiation	323	⊢
	: , :
249	instantiation	278, 279, 280	⊢
	: , : , :
250	instantiation	412, 413, 319	⊢
	: , : , :
251	conjecture		⊢
	proveit.numbers.multiplication.mult_zero_right
252	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
253	conjecture		⊢
	proveit.numbers.addition.elim_zero_any
254	instantiation	323	⊢
	: , :
255	instantiation	281, 337	⊢
	:
256	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_sum
257	instantiation	323	⊢
	: , :
258	instantiation	282, 370, 387, 305	⊢
	: , : , :
259	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
260	instantiation	283, 379	⊢
	: , :
261	instantiation	284, 364, 285*	,  ⊢
	:
262	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_reverse
263	instantiation	303	⊢
	:
264	instantiation	286, 337, 292	,  ⊢
	: , :
265	instantiation	299, 300, 414, 406, 302, 288, 322, 290, 287	,  ⊢
	: , : , : , : , : , :
266	instantiation	299, 414, 300, 288, 289, 302, 322, 290, 292, 342	,  ⊢
	: , : , : , : , : , :
267	instantiation	291, 406, 300, 302, 322, 292, 342	,  ⊢
	: , : , : , : , : , : , : , :
268	conjecture		⊢
	proveit.numbers.negation.int_neg_closure
269	instantiation	293, 376, 294	⊢
	:
270	instantiation	295, 296	⊢
	:
271	instantiation	333, 297	⊢
	: , : , :
272	axiom		⊢
	proveit.logic.equality.equals_transitivity
273	instantiation	299, 300, 414, 406, 302, 301, 336, 306, 298	⊢
	: , : , : , : , : , :
274	instantiation	299, 414, 319, 300, 301, 320, 302, 336, 306, 321, 370, 322	⊢
	: , : , : , : , : , :
275	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
276	instantiation	323	⊢
	: , :
277	instantiation	303	⊢
	:
278	theorem		⊢
	proveit.logic.equality.sub_right_side_into
279	instantiation	304, 370, 387, 305	⊢
	: , : , :
280	instantiation	340, 370, 306	⊢
	: , :
281	conjecture		⊢
	proveit.numbers.negation.mult_neg_one_left
282	conjecture		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
283	theorem		⊢
	proveit.logic.booleans.conjunction.right_from_and
284	conjecture		⊢
	proveit.physics.quantum.QPE._modabs_in_full_domain_simp
285	instantiation	307, 308	⊢
	:
286	conjecture		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
287	instantiation	412, 396, 309	⊢
	: , : , :
288	instantiation	323	⊢
	: , :
289	instantiation	323	⊢
	: , :
290	instantiation	412, 396, 310	⊢
	: , : , :
291	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
292	instantiation	412, 396, 328	⊢
	: , : , :
293	conjecture		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
294	instantiation	311, 312, 313	⊢
	: , : , :
295	conjecture		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
296	assumption		⊢
297	instantiation	314, 315, 316, 317	⊢
	: , : , : , :
298	instantiation	318, 319, 320, 321, 370, 322	⊢
	: , :
299	conjecture		⊢
	proveit.numbers.addition.disassociation
300	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
301	instantiation	323	⊢
	: , :
302	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
303	axiom		⊢
	proveit.logic.equality.equals_reflexivity
304	conjecture		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
305	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_1
306	instantiation	412, 396, 324	⊢
	: , : , :
307	conjecture		⊢
	proveit.numbers.absolute_value.abs_neg_elim
308	instantiation	325, 326	⊢
	: , :
309	instantiation	327, 328, 344	⊢
	: , :
310	instantiation	355, 328	⊢
	:
311	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
312	conjecture		⊢
	proveit.numbers.numerals.decimals.less_0_1
313	instantiation	329, 400, 399, 391	⊢
	: , : , :
314	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
315	instantiation	333, 330	⊢
	: , : , :
316	instantiation	331, 332	⊢
	: , :
317	instantiation	333, 334	⊢
	: , : , :
318	conjecture		⊢
	proveit.numbers.addition.add_complex_closure
319	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
320	instantiation	335	⊢
	: , : , :
321	instantiation	354, 336	⊢
	:
322	instantiation	354, 337	⊢
	:
323	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
324	instantiation	412, 401, 338	⊢
	: , : , :
325	conjecture		⊢
	proveit.numbers.ordering.relax_less
326	assumption		⊢
327	conjecture		⊢
	proveit.numbers.addition.add_real_closure_bin
328	instantiation	412, 401, 339	⊢
	: , : , :
329	conjecture		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
330	instantiation	340, 341, 342	⊢
	: , :
331	theorem		⊢
	proveit.logic.equality.equals_reversal
332	instantiation	343, 387, 344, 353, 372	⊢
	: , : , :
333	axiom		⊢
	proveit.logic.equality.substitution
334	instantiation	345, 346, 347	⊢
	: , :
335	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
336	instantiation	348, 349, 350	⊢
	: , :
337	instantiation	412, 396, 351	⊢
	: , : , :
338	instantiation	412, 407, 405	⊢
	: , : , :
339	instantiation	412, 407, 352	⊢
	: , : , :
340	conjecture		⊢
	proveit.numbers.addition.commutation
341	instantiation	412, 396, 353	⊢
	: , : , :
342	instantiation	354, 370	⊢
	:
343	conjecture		⊢
	proveit.numbers.exponentiation.product_of_real_powers
344	instantiation	355, 384	⊢
	:
345	conjecture		⊢
	proveit.numbers.exponentiation.neg_power_as_div
346	instantiation	412, 356, 357	⊢
	: , : , :
347	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
348	conjecture		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
349	instantiation	358, 370, 359, 360	⊢
	: , :
350	instantiation	412, 396, 361	⊢
	: , : , :
351	instantiation	412, 401, 362	⊢
	: , : , :
352	instantiation	412, 363, 364	⊢
	: , : , :
353	instantiation	365, 366, 389	⊢
	: , : , :
354	conjecture		⊢
	proveit.numbers.negation.complex_closure
355	conjecture		⊢
	proveit.numbers.negation.real_closure
356	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
357	instantiation	412, 367, 368	⊢
	: , : , :
358	conjecture		⊢
	proveit.numbers.division.div_complex_closure
359	instantiation	369, 387, 370	⊢
	: , :
360	instantiation	371, 372, 373	⊢
	: , : , :
361	instantiation	374, 397, 375	⊢
	: , :
362	instantiation	412, 407, 376	⊢
	: , : , :
363	instantiation	398, 377, 404	⊢
	: , :
364	instantiation	378, 379	⊢
	: , :
365	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
366	instantiation	380, 381	⊢
	: , :
367	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
368	instantiation	412, 382, 383	⊢
	: , : , :
369	conjecture		⊢
	proveit.numbers.exponentiation.exp_complex_closure
370	instantiation	412, 396, 384	⊢
	: , : , :
371	theorem		⊢
	proveit.logic.equality.sub_left_side_into
372	instantiation	385, 394	⊢
	:
373	instantiation	386, 387	⊢
	:
374	conjecture		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
375	instantiation	412, 388, 389	⊢
	: , : , :
376	instantiation	412, 390, 391	⊢
	: , : , :
377	instantiation	403, 392, 400	⊢
	: , :
378	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
379	assumption		⊢
380	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
381	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
382	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
383	instantiation	412, 393, 394	⊢
	: , : , :
384	instantiation	412, 401, 395	⊢
	: , : , :
385	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
386	conjecture		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
387	instantiation	412, 396, 397	⊢
	: , : , :
388	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
389	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
390	instantiation	398, 400, 399	⊢
	: , :
391	assumption		⊢
392	instantiation	410, 404	⊢
	:
393	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
394	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
395	instantiation	412, 407, 400	⊢
	: , : , :
396	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
397	instantiation	412, 401, 402	⊢
	: , : , :
398	conjecture		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
399	instantiation	403, 404, 405	⊢
	: , :
400	instantiation	412, 413, 406	⊢
	: , : , :
401	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
402	instantiation	412, 407, 411	⊢
	: , : , :
403	conjecture		⊢
	proveit.numbers.addition.add_int_closure_bin
404	instantiation	412, 408, 409	⊢
	: , : , :
405	instantiation	410, 411	⊢
	:
406	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
407	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
408	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
409	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
410	conjecture		⊢
	proveit.numbers.negation.int_closure
411	instantiation	412, 413, 414	⊢
	: , : , :
412	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
413	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
414	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements