These are archival webpages, generated on 2023-03-20 by Prove-It Beta Version 0.3, licensed under the GNU Public Licence by Sandia Corporation. See pyproveit.org for the lastest version.
logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults, Lambda
from proveit import a, b, c, e, f, l, m, x, y, A, B, C, N, Q, X, Omega
from proveit.logic import Or, Forall, InSet, Union, Disjoint
from proveit.logic.sets.functions.injections import subset_injection
from proveit.logic.sets.functions.bijections import bijection_transitivity
from proveit.numbers import (zero, one, Add, Neg, greater, Less)
from proveit.numbers.modular import interval_left_shift_bijection
from proveit.statistics import prob_of_disjoint_events_is_prob_sum
from proveit.physics.quantum import NumKet
from proveit.physics.quantum.QPE import (
    _t, _two_pow_t, _two_pow_t__minus_one,  _t_in_natural_pos,
    _two_pow_t_minus_one_is_nat_pos, _Omega,
    _b_floor, _best_floor_is_int, _best_floor_def,
    _alpha_m_def, _full_domain, _neg_domain, _pos_domain,
    _modabs_in_full_domain_simp, ModAdd, _sample_space_bijection,
    _Omega_is_sample_space, _outcome_prob, _fail_def,
    _fail_sum_prob_conds_equiv_lemma)
In [2]:
%proving _fail_sum
Under these presumptions, we begin our proof of
_fail_sum:
(see dependencies)
In [3]:
defaults.assumptions = _fail_sum.all_conditions()
defaults.assumptions:
In [4]:
e_in_domain = defaults.assumptions[0]
e_in_domain:
In [5]:
defaults.preserved_exprs = {e_in_domain.domain.upper_bound.operands[0]}
defaults.preserved_exprs:

Start with the $P_{\textrm{fail}}$ definition

In [6]:
fail_def_inst = _fail_def.instantiate()
fail_def_inst:  ⊢  

We will next translate from $m \in \{0~\ldotp \ldotp~2^{t} - 1\}$ to $b_f \oplus l$ with $l \in \{-2^{t-1} + 1 ~\ldotp \ldotp~2^{t-1}\}$

In [7]:
lower_bound = _neg_domain.lower_bound
lower_bound:
In [8]:
upper_bound = _pos_domain.upper_bound
upper_bound:
In [9]:
interval_left_shift_bijection
In [10]:
lambda_map_bijection = interval_left_shift_bijection.instantiate(
    {a:lower_bound, b:upper_bound, c:_b_floor, N:_two_pow_t, x:l})
lambda_map_bijection:  ⊢  

Use the $\oplus$ notation within kets (but not otherwise, for simplification purposed):

In [11]:
b_modadd_l__def = ModAdd(_b_floor, l).definition(assumptions=[InSet(l, _full_domain)])
b_modadd_l__def:  ⊢  
In [12]:
defaults.replacements = [b_modadd_l__def.derive_reversed().substitution(NumKet(b_modadd_l__def.rhs, _t))]
defaults.replacements:
In [13]:
transformed_fail_def = fail_def_inst.inner_expr().rhs.transform(
    lambda_map_bijection.element, lambda_map_bijection.domain.domain, _Omega)
transformed_fail_def:  ⊢  

Proceed to split the probability of this event into the sum of two disjoint possibilities

Our goal will be to apply the following theorem:

In [14]:
prob_of_disjoint_events_is_prob_sum

Prove the $|l|_{\textrm{mod}~2^t} > e$ condition for either the positive or negative domain for simplification purposes

In [15]:
condition = transformed_fail_def.rhs.non_domain_condition()
condition:
In [16]:
neg_domain_assumptions = [InSet(l, _neg_domain), *_fail_sum.all_conditions()]
neg_domain_assumptions:
In [17]:
pos_domain_assumptions = [InSet(l, _pos_domain), *_fail_sum.all_conditions()]
pos_domain_assumptions:
In [18]:
_modabs_in_full_domain_simp
In [19]:
absmod_posdomain_simp = _modabs_in_full_domain_simp.instantiate(
    assumptions=pos_domain_assumptions)
absmod_posdomain_simp: ,  ⊢  
In [20]:
absmod_negdomain_simp = _modabs_in_full_domain_simp.instantiate(
    assumptions=neg_domain_assumptions)
absmod_negdomain_simp: ,  ⊢  
In [21]:
pos_cond_eval = absmod_posdomain_simp.sub_left_side_into(
    greater(l, e), assumptions=pos_domain_assumptions).evaluation()
pos_cond_eval: ,  ⊢  
In [22]:
neg_cond_eval = absmod_negdomain_simp.sub_left_side_into(
    greater(Neg(l), e), assumptions=neg_domain_assumptions).evaluation()
neg_cond_eval: ,  ⊢  

Prove the proper injective mapping condition then apply prob_of_disjoint_events_is_prob_sum

In [23]:
circuit_map = Lambda(l, transformed_fail_def.rhs.instance_expr)
circuit_map:
In [24]:
lambda_map_bijection
In [25]:
_sample_space_bijection
In [26]:
trans_bijection = lambda_map_bijection.apply_transitivity(_sample_space_bijection)
trans_bijection:  ⊢  
In [27]:
prob_eq_sum1 = prob_of_disjoint_events_is_prob_sum.instantiate(
    {Omega:_Omega, A:_neg_domain, B:_pos_domain, C:Union(_neg_domain, _pos_domain), 
     X:_full_domain, f:circuit_map, Q:Lambda(l, condition), x:l},
    replacements=[pos_cond_eval, neg_cond_eval]).with_wrap_after_operator()
prob_eq_sum1:  ⊢  

Compute the event probabilities in terms of summing outcome probabilities

In [28]:
outcome_prob_pos = _outcome_prob.instantiate({m:ModAdd(_b_floor, l)}, assumptions=pos_domain_assumptions)
outcome_prob_pos: ,  ⊢  
In [29]:
outcome_prob_neg = _outcome_prob.instantiate({m:ModAdd(_b_floor, l)}, assumptions=neg_domain_assumptions)
outcome_prob_neg: ,  ⊢  
In [30]:
subset_injection
In [31]:
subset_injection.instantiate({A:_pos_domain, B:_full_domain, C:_Omega, f:trans_bijection.element})
In [32]:
subset_injection.instantiate({A:_neg_domain, B:_full_domain, C:_Omega, f:trans_bijection.element})
In [33]:
prob_eq_sum2 = prob_eq_sum1.inner_expr().rhs.operands[0].compute(_Omega, replacements=[outcome_prob_neg])
prob_eq_sum2:  ⊢  
In [34]:
prob_eq_sum3 = prob_eq_sum2.inner_expr().rhs.operands[1].compute(_Omega, replacements=[outcome_prob_pos])
prob_eq_sum3:  ⊢  

That logical equivalence of conditions is handled in a separate lemma, _fail_sum_prob_conds_equiv_lemma:

In [35]:
_fail_sum_prob_conds_equiv_lemma
In [36]:
# Here we explicitly preserve the -(e+1) expression; otherwise it becomes (-e-1) and
# later won't match up with the expression to be substituted for
conditions_equiv = (
    _fail_sum_prob_conds_equiv_lemma.instantiate(preserve_expr=Neg(Add(e, one)))
    .instantiate(preserve_expr=Neg(Add(e, one)), sideeffect_automation=False))
conditions_equiv:  ⊢  
In [37]:
prob_eq_sum4 = prob_eq_sum3.inner_expr().lhs.operand.body
prob_eq_sum4:
In [38]:
prob_eq_sum4 = prob_eq_sum3.inner_expr().lhs.operand.body.substitute_condition(
    conditions_equiv, preserve_all=True, sideeffect_automation=False)
prob_eq_sum4:  ⊢  
_fail_sum may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [39]:
%qed
proveit.physics.quantum.QPE._fail_sum has been proven.
Out[39]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation410, 2, 5  ⊢  
  : , : , :
2instantiation361, 3, 4, 5  ⊢  
  : , : , : , :
3instantiation335, 6, 7  ⊢  
  : , : , :
4instantiation335, 8, 9  ⊢  
  : , : , :
5instantiation376, 10  ⊢  
  : , : , :
6instantiation11, 426  ⊢  
  :
7instantiation12, 45, 13, 224, 222*, 14*  ⊢  
  : , : , : , : , : , : , : , :
8instantiation335, 15, 16  ⊢  
  : , : , :
9modus ponens17, 18  ⊢  
10instantiation376, 19  ⊢  
  : , : , :
11axiom  ⊢  
 proveit.physics.quantum.QPE._fail_def
12conjecture  ⊢  
 proveit.statistics.prob_of_all_events_transformation
13instantiation88, 20  ⊢  
  : , :
14instantiation21, 347, 444, 349, 22, 79, 23, 24*  ⊢  
  : , : , : , : , : , :
15instantiation335, 25, 26  ⊢  
  : , : , :
16instantiation44, 45, 27, 28*, 43*, 29*  ⊢  
  : , : , : , : , :
17instantiation53, 389  ⊢  
  : , : , : , : , : , :
18generalization30  ⊢  
19modus ponens31, 32  ⊢  
20instantiation118, 225  ⊢  
  : , : , :
21conjecture  ⊢  
 proveit.numbers.modular.redundant_mod_elimination_in_sum_in_modabs
22instantiation450, 437, 33  ⊢  
  : , : , :
23instantiation450, 34, 35  ⊢  
  : , : , :
24instantiation329, 36, 37  ⊢  
  : , : , :
25instantiation38, 45, 39, 40, 41, 71, 42*, 48*, 43*  ⊢  
  : , : , : , : , : , : , : , :
26instantiation44, 45, 46, 47*, 48*, 49*  ⊢  
  : , : , : , : , :
27instantiation69, 64, 71  ⊢  
  : , : , : , :
28instantiation72, 50,  ⊢  
  :
29instantiation74, 444, 347, 349  ⊢  
  : , : , : , : , :
30instantiation51, 52  ⊢  
  : , : , :
31instantiation53, 389  ⊢  
  : , : , : , : , : , :
32generalization54  ⊢  
33instantiation450, 445, 55  ⊢  
  : , : , :
34conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
35instantiation450, 56, 252  ⊢  
  : , : , :
36instantiation346, 347, 452, 444, 349, 57, 59, 60, 58  ⊢  
  : , : , : , : , : , :
37instantiation180, 59, 60, 61  ⊢  
  : , : , :
38conjecture  ⊢  
 proveit.statistics.prob_of_disjoint_events_is_prob_sum
39instantiation62, 428, 63, 70, 64  ⊢  
  : , : , :
40instantiation350  ⊢  
  :
41instantiation65, 338, 339, 355, 442, 66  ⊢  
  : , : , : , :
42instantiation67, 68,  ⊢  
  :
43instantiation74, 444, 347, 349  ⊢  
  : , : , : , : , :
44conjecture  ⊢  
 proveit.statistics.prob_of_all_as_sum
45conjecture  ⊢  
 proveit.physics.quantum.QPE._Omega_is_sample_space
46instantiation69, 70, 71  ⊢  
  : , : , : , :
47instantiation72, 73,  ⊢  
  :
48instantiation74, 444, 347, 349  ⊢  
  : , : , : , : , :
49instantiation74, 444, 347, 349  ⊢  
  : , : , : , : , :
50instantiation90, 300, 75,  ⊢  
  : , :
51axiom  ⊢  
 proveit.core_expr_types.conditionals.condition_replacement
52instantiation76, 426  ⊢  
  :
53axiom  ⊢  
 proveit.core_expr_types.lambda_maps.lambda_substitution
54instantiation77, 78  ⊢  
  : , : , :
55instantiation441, 300, 301  ⊢  
  : , :
56conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
57instantiation370  ⊢  
  : , :
58instantiation450, 430, 79  ⊢  
  : , : , :
59instantiation450, 430, 94  ⊢  
  : , : , :
60instantiation450, 430, 80  ⊢  
  : , : , :
61instantiation350  ⊢  
  :
62conjecture  ⊢  
 proveit.logic.sets.unification.union_inclusion
63instantiation370  ⊢  
  : , :
64instantiation86, 338, 355, 442, 81  ⊢  
  : , : , : , :
65conjecture  ⊢  
 proveit.numbers.number_sets.integers.disjoint_intervals
66instantiation113, 366, 82, 116, 83, 98  ⊢  
  : , :
67axiom  ⊢  
 proveit.logic.booleans.eq_true_intro
68instantiation410, 84, 85,  ⊢  
  : , : , :
69conjecture  ⊢  
 proveit.logic.sets.functions.injections.subset_injection
70instantiation86, 338, 339, 442, 87  ⊢  
  : , : , : , :
71instantiation88, 89  ⊢  
  : , :
72conjecture  ⊢  
 proveit.physics.quantum.QPE._outcome_prob
73instantiation90, 300, 304,  ⊢  
  : , :
74conjecture  ⊢  
 proveit.core_expr_types.conditionals.true_condition_elimination
75instantiation450, 91, 92,  ⊢  
  : , : , :
76conjecture  ⊢  
 proveit.physics.quantum.QPE._fail_sum_prob_conds_equiv_lemma
77conjecture  ⊢  
 proveit.core_expr_types.conditionals.condition_substitution
78instantiation376, 93  ⊢  
  : , : , :
79instantiation178, 94  ⊢  
  :
80instantiation450, 437, 95  ⊢  
  : , : , :
81instantiation113, 366, 96, 97, 98, 99  ⊢  
  : , :
82instantiation378  ⊢  
  : , : , :
83instantiation104, 327, 129, 100, 101, 102*, 103*  ⊢  
  : , : , :
84instantiation104, 105, 268, 106, 107, 108*, 109*,  ⊢  
  : , : , :
85instantiation110, 111, 112*,  ⊢  
  :
86conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_subset_eq
87instantiation113, 366, 114, 115, 116, 117  ⊢  
  : , :
88theorem  ⊢  
 proveit.logic.booleans.conjunction.left_from_and
89instantiation118, 119  ⊢  
  : , : , :
90conjecture  ⊢  
 proveit.physics.quantum.QPE._mod_add_closure
91instantiation434, 355, 442  ⊢  
  : , :
92assumption  ⊢  
93instantiation376, 239  ⊢  
  : , : , :
94instantiation450, 437, 120  ⊢  
  : , : , :
95instantiation450, 445, 301  ⊢  
  : , : , :
96instantiation378  ⊢  
  : , : , :
97instantiation121, 122, 123  ⊢  
  : , : , :
98instantiation156, 420, 342, 124, 125, 126*  ⊢  
  : , : , :
99instantiation147, 157, 127  ⊢  
  : , :
100instantiation162, 235, 431  ⊢  
  : , :
101instantiation128, 129, 235, 431, 130, 131  ⊢  
  : , : , :
102instantiation374, 132  ⊢  
  : , :
103instantiation361, 133, 134, 135  ⊢  
  : , : , : , :
104conjecture  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
105instantiation162, 342, 136,  ⊢  
  : , :
106instantiation162, 138, 420  ⊢  
  : , :
107instantiation137, 268, 138, 420, 270, 357,  ⊢  
  : , : , :
108instantiation329, 139, 140,  ⊢  
  : , : , :
109instantiation329, 141, 142,  ⊢  
  : , : , :
110conjecture  ⊢  
 proveit.physics.quantum.QPE._modabs_in_full_domain_simp
111instantiation143, 338, 442, 304, 144,  ⊢  
  : , : , :
112instantiation145, 146,  ⊢  
  :
113conjecture  ⊢  
 proveit.logic.booleans.conjunction.and_if_all
114instantiation378  ⊢  
  : , : , :
115instantiation147, 148, 149  ⊢  
  : , :
116instantiation156, 150, 342, 164, 165, 151*, 152*  ⊢  
  : , : , :
117instantiation214, 153  ⊢  
  : , :
118conjecture  ⊢  
 proveit.logic.sets.functions.bijections.membership_unfolding
119instantiation154, 155  ⊢  
  : , : , :
120instantiation450, 445, 300  ⊢  
  : , : , :
121conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
122instantiation156, 226, 420, 157, 158, 159*, 160*  ⊢  
  : , : , :
123instantiation214, 161  ⊢  
  : , :
124instantiation162, 164, 420  ⊢  
  : , :
125instantiation163, 342, 164, 420, 165, 166  ⊢  
  : , : , :
126instantiation361, 167, 334, 168  ⊢  
  : , : , : , :
127instantiation350  ⊢  
  :
128conjecture  ⊢  
 proveit.numbers.ordering.less_add_right
129instantiation260, 431, 170  ⊢  
  : , :
130instantiation169, 431, 170, 342, 341, 171  ⊢  
  : , : , :
131instantiation201, 452  ⊢  
  :
132instantiation361, 239, 172, 173  ⊢  
  : , : , : , :
133instantiation346, 347, 452, 444, 349, 174, 207, 423, 309  ⊢  
  : , : , : , : , : , :
134instantiation346, 452, 347, 174, 323, 349, 207, 423, 369, 385  ⊢  
  : , : , : , : , : , :
135instantiation361, 175, 176, 177  ⊢  
  : , : , : , :
136instantiation178, 268,  ⊢  
  :
137conjecture  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
138instantiation450, 437, 179  ⊢  
  : , : , :
139instantiation346, 444, 452, 347, 211, 349, 242, 325, 213,  ⊢  
  : , : , : , : , : , :
140instantiation180, 242, 325, 181,  ⊢  
  : , : , :
141instantiation376, 182  ⊢  
  : , : , :
142instantiation329, 183, 184,  ⊢  
  : , : , :
143conjecture  ⊢  
 proveit.numbers.number_sets.integers.in_interval
144instantiation223, 185, 186,  ⊢  
  : , :
145conjecture  ⊢  
 proveit.numbers.absolute_value.abs_neg_elim
146instantiation214, 244,  ⊢  
  : , :
147conjecture  ⊢  
 proveit.numbers.ordering.relax_equal_to_less_eq
148instantiation450, 437, 187  ⊢  
  : , : , :
149instantiation350  ⊢  
  :
150instantiation188, 366, 189, 226, 420, 381  ⊢  
  : , :
151instantiation361, 190, 191, 192  ⊢  
  : , : , : , :
152instantiation374, 193  ⊢  
  : , :
153instantiation243, 271, 245  ⊢  
  : , : , :
154conjecture  ⊢  
 proveit.logic.sets.functions.bijections.elim_domain_condition
155modus ponens194, 195  ⊢  
156conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
157instantiation403, 404, 447  ⊢  
  : , : , :
158instantiation196, 447  ⊢  
  :
159instantiation383, 409, 197  ⊢  
  : , :
160instantiation329, 198, 199  ⊢  
  : , : , :
161instantiation272, 306  ⊢  
  :
162conjecture  ⊢  
 proveit.numbers.addition.add_real_closure_bin
163conjecture  ⊢  
 proveit.numbers.ordering.less_eq_add_right
164instantiation450, 437, 200  ⊢  
  : , : , :
165instantiation290, 436, 435, 426  ⊢  
  : , : , :
166instantiation201, 444  ⊢  
  :
167instantiation329, 202, 203  ⊢  
  : , : , :
168instantiation374, 344  ⊢  
  : , :
169conjecture  ⊢  
 proveit.numbers.multiplication.strong_bound_via_right_factor_bound
170conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
171instantiation272, 428  ⊢  
  :
172instantiation350  ⊢  
  :
173instantiation374, 204  ⊢  
  : , :
174instantiation370  ⊢  
  : , :
175instantiation205, 444, 207, 423, 369, 385  ⊢  
  : , : , : , : , : , : , :
176instantiation314, 347, 452, 349, 206, 286, 207, 369, 423, 385, 208*  ⊢  
  : , : , : , : , : , :
177instantiation314, 444, 452, 347, 286, 349, 325, 423, 385, 287*  ⊢  
  : , : , : , : , : , :
178conjecture  ⊢  
 proveit.numbers.negation.real_closure
179instantiation450, 445, 339  ⊢  
  : , : , :
180conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
181instantiation350  ⊢  
  :
182instantiation329, 209, 210  ⊢  
  : , : , :
183instantiation346, 444, 452, 347, 211, 349, 369, 325, 213,  ⊢  
  : , : , : , : , : , :
184instantiation212, 325, 213, 326,  ⊢  
  : , : , :
185instantiation372, 338, 339, 320,  ⊢  
  : , : , :
186instantiation214, 215,  ⊢  
  : , :
187instantiation450, 445, 338  ⊢  
  : , : , :
188conjecture  ⊢  
 proveit.numbers.addition.add_real_closure
189instantiation378  ⊢  
  : , : , :
190instantiation329, 216, 217  ⊢  
  : , : , :
191instantiation350  ⊢  
  :
192instantiation374, 218  ⊢  
  : , :
193instantiation361, 239, 219, 220  ⊢  
  : , : , : , :
194instantiation221, 222*  ⊢  
  : , : , : , : , : , :
195instantiation223, 224, 225  ⊢  
  : , :
196conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
197instantiation450, 430, 226  ⊢  
  : , : , :
198instantiation329, 227, 228  ⊢  
  : , : , :
199instantiation229, 380, 334  ⊢  
  : , :
200instantiation450, 445, 435  ⊢  
  : , : , :
201conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
202instantiation376, 230  ⊢  
  : , : , :
203instantiation329, 231, 232  ⊢  
  : , : , :
204instantiation329, 233, 234  ⊢  
  : , : , :
205conjecture  ⊢  
 proveit.numbers.addition.leftward_commutation
206instantiation370  ⊢  
  : , :
207instantiation450, 430, 235  ⊢  
  : , : , :
208instantiation329, 236, 237, 238*  ⊢  
  : , : , :
209instantiation376, 239  ⊢  
  : , : , :
210instantiation329, 240, 241  ⊢  
  : , : , :
211instantiation370  ⊢  
  : , :
212conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_21
213instantiation379, 242,  ⊢  
  :
214conjecture  ⊢  
 proveit.numbers.ordering.relax_less
215instantiation243, 244, 245,  ⊢  
  : , : , :
216instantiation376, 311  ⊢  
  : , : , :
217instantiation329, 246, 247  ⊢  
  : , : , :
218instantiation376, 328  ⊢  
  : , : , :
219instantiation374, 248  ⊢  
  : , :
220instantiation374, 249  ⊢  
  : , :
221conjecture  ⊢  
 proveit.logic.sets.functions.bijections.bijection_transitivity
222instantiation376, 250  ⊢  
  : , : , :
223theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
224instantiation251, 252, 338, 442, 300  ⊢  
  : , : , : , : , :
225conjecture  ⊢  
 proveit.physics.quantum.QPE._sample_space_bijection
226instantiation450, 437, 253  ⊢  
  : , : , :
227instantiation376, 344  ⊢  
  : , : , :
228instantiation376, 328  ⊢  
  : , : , :
229conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_basic
230instantiation329, 254, 255  ⊢  
  : , : , :
231instantiation346, 347, 452, 444, 349, 256, 380, 385, 409  ⊢  
  : , : , : , : , : , :
232instantiation266, 409, 380, 267  ⊢  
  : , : , :
233instantiation376, 257  ⊢  
  : , : , :
234instantiation329, 258, 259  ⊢  
  : , : , :
235instantiation260, 431, 342  ⊢  
  : , :
236instantiation376, 261  ⊢  
  : , : , :
237instantiation374, 262  ⊢  
  : , :
238instantiation329, 263, 264  ⊢  
  : , : , :
239instantiation265, 325, 409  ⊢  
  : , :
240instantiation346, 347, 452, 444, 349, 323, 369, 385, 409  ⊢  
  : , : , : , : , : , :
241instantiation266, 409, 369, 267  ⊢  
  : , : , :
242instantiation450, 430, 268,  ⊢  
  : , : , :
243axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
244instantiation269, 270, 271,  ⊢  
  : , : , :
245instantiation272, 447  ⊢  
  :
246instantiation346, 444, 366, 347, 367, 349, 325, 368, 409, 369  ⊢  
  : , : , : , : , : , :
247instantiation332, 347, 452, 349, 273, 325, 368, 409, 326  ⊢  
  : , : , : , : , : , : , : , :
248instantiation303, 309, 325, 385, 274  ⊢  
  : , : , :
249instantiation329, 275, 276  ⊢  
  : , : , :
250instantiation374, 277  ⊢  
  : , :
251conjecture  ⊢  
 proveit.numbers.modular.interval_left_shift_bijection
252instantiation278, 452, 433  ⊢  
  : , :
253instantiation450, 445, 354  ⊢  
  : , : , :
254instantiation376, 310  ⊢  
  : , : , :
255instantiation329, 279, 280  ⊢  
  : , : , :
256instantiation370  ⊢  
  : , :
257instantiation281, 423  ⊢  
  :
258instantiation346, 444, 452, 347, 323, 349, 282, 369, 385  ⊢  
  : , : , : , : , : , :
259instantiation283, 347, 452, 349, 323, 369, 385  ⊢  
  : , : , : , :
260conjecture  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
261instantiation374, 284  ⊢  
  : , :
262instantiation285, 347, 452, 444, 349, 286, 423, 385, 325  ⊢  
  : , : , : , : , : , :
263instantiation376, 287  ⊢  
  : , : , :
264instantiation288, 325  ⊢  
  :
265conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
266conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
267instantiation350  ⊢  
  :
268instantiation450, 437, 289,  ⊢  
  : , : , :
269conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
270instantiation290, 338, 339, 320,  ⊢  
  : , : , :
271instantiation291, 292  ⊢  
  :
272conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
273instantiation370  ⊢  
  : , :
274instantiation335, 293, 294  ⊢  
  : , : , :
275instantiation329, 295, 296  ⊢  
  : , : , :
276instantiation329, 297, 298  ⊢  
  : , : , :
277instantiation299, 300, 301  ⊢  
  : , :
278conjecture  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
279instantiation346, 347, 452, 444, 349, 348, 380, 353, 409  ⊢  
  : , : , : , : , : , :
280instantiation314, 444, 452, 347, 315, 349, 380, 353, 409, 316*  ⊢  
  : , : , : , : , : , :
281conjecture  ⊢  
 proveit.numbers.multiplication.mult_zero_right
282conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
283conjecture  ⊢  
 proveit.numbers.addition.elim_zero_any
284instantiation302, 325  ⊢  
  :
285conjecture  ⊢  
 proveit.numbers.multiplication.distribute_through_sum
286instantiation370  ⊢  
  : , :
287instantiation303, 409, 423, 352  ⊢  
  : , : , :
288conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_left
289instantiation450, 445, 304,  ⊢  
  : , : , :
290conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
291conjecture  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
292instantiation305, 306  ⊢  
  :
293instantiation329, 307, 308  ⊢  
  : , : , :
294instantiation383, 325, 309  ⊢  
  : , :
295instantiation376, 310  ⊢  
  : , : , :
296instantiation376, 311  ⊢  
  : , : , :
297instantiation329, 312, 313  ⊢  
  : , : , :
298instantiation314, 347, 452, 444, 349, 315, 353, 409, 369, 316*  ⊢  
  : , : , : , : , : , :
299axiom  ⊢  
 proveit.physics.quantum.QPE._mod_add_def
300conjecture  ⊢  
 proveit.physics.quantum.QPE._best_floor_is_int
301instantiation450, 317, 318  ⊢  
  : , : , :
302conjecture  ⊢  
 proveit.numbers.negation.mult_neg_one_left
303conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
304instantiation450, 319, 320,  ⊢  
  : , : , :
305conjecture  ⊢  
 proveit.numbers.negation.int_neg_closure
306instantiation321, 322, 389  ⊢  
  : , :
307instantiation346, 444, 452, 347, 323, 349, 325, 369, 385  ⊢  
  : , : , : , : , : , :
308instantiation324, 325, 385, 326  ⊢  
  : , : , :
309instantiation450, 430, 327  ⊢  
  : , : , :
310instantiation376, 344  ⊢  
  : , : , :
311instantiation376, 328  ⊢  
  : , : , :
312instantiation329, 330, 331  ⊢  
  : , : , :
313instantiation332, 347, 444, 452, 349, 333, 380, 353, 409, 369, 334  ⊢  
  : , : , : , : , : , : , : , :
314conjecture  ⊢  
 proveit.numbers.addition.association
315instantiation370  ⊢  
  : , :
316instantiation335, 336, 337  ⊢  
  : , : , :
317instantiation434, 338, 442  ⊢  
  : , :
318assumption  ⊢  
319instantiation434, 338, 339  ⊢  
  : , :
320assumption  ⊢  
321conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
322instantiation340, 414, 341  ⊢  
  :
323instantiation370  ⊢  
  : , :
324conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_12
325instantiation450, 430, 342  ⊢  
  : , : , :
326instantiation350  ⊢  
  :
327instantiation450, 437, 343  ⊢  
  : , : , :
328instantiation376, 344  ⊢  
  : , : , :
329axiom  ⊢  
 proveit.logic.equality.equals_transitivity
330instantiation346, 347, 452, 444, 349, 348, 380, 353, 345  ⊢  
  : , : , : , : , : , :
331instantiation346, 452, 366, 347, 348, 367, 349, 380, 353, 368, 409, 369  ⊢  
  : , : , : , : , : , :
332conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general
333instantiation370  ⊢  
  : , :
334instantiation350  ⊢  
  :
335theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
336instantiation351, 409, 423, 352  ⊢  
  : , : , :
337instantiation383, 409, 353  ⊢  
  : , :
338instantiation441, 354, 436  ⊢  
  : , :
339instantiation448, 355  ⊢  
  :
340conjecture  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
341instantiation356, 357, 358  ⊢  
  : , : , :
342instantiation450, 437, 359  ⊢  
  : , : , :
343instantiation450, 445, 360  ⊢  
  : , : , :
344instantiation361, 362, 363, 364  ⊢  
  : , : , : , :
345instantiation365, 366, 367, 368, 409, 369  ⊢  
  : , :
346conjecture  ⊢  
 proveit.numbers.addition.disassociation
347axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
348instantiation370  ⊢  
  : , :
349conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
350axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
351conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
352conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
353instantiation450, 430, 371  ⊢  
  : , : , :
354instantiation448, 442  ⊢  
  :
355instantiation441, 414, 436  ⊢  
  : , :
356conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
357conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
358instantiation372, 436, 435, 426  ⊢  
  : , : , :
359instantiation450, 445, 414  ⊢  
  : , : , :
360instantiation441, 402, 417  ⊢  
  : , :
361conjecture  ⊢  
 proveit.logic.equality.four_chain_transitivity
362instantiation376, 373  ⊢  
  : , : , :
363instantiation374, 375  ⊢  
  : , :
364instantiation376, 377  ⊢  
  : , : , :
365conjecture  ⊢  
 proveit.numbers.addition.add_complex_closure
366conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat3
367instantiation378  ⊢  
  : , : , :
368instantiation379, 380  ⊢  
  :
369instantiation450, 430, 381  ⊢  
  : , : , :
370conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
371instantiation450, 437, 382  ⊢  
  : , : , :
372conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
373instantiation383, 384, 385  ⊢  
  : , :
374theorem  ⊢  
 proveit.logic.equality.equals_reversal
375instantiation386, 423, 395, 394, 411  ⊢  
  : , : , :
376axiom  ⊢  
 proveit.logic.equality.substitution
377instantiation387, 388, 389  ⊢  
  : , :
378conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
379conjecture  ⊢  
 proveit.numbers.negation.complex_closure
380instantiation390, 391, 392  ⊢  
  : , :
381instantiation450, 437, 393  ⊢  
  : , : , :
382instantiation450, 445, 443  ⊢  
  : , : , :
383conjecture  ⊢  
 proveit.numbers.addition.commutation
384instantiation450, 430, 394  ⊢  
  : , : , :
385instantiation450, 430, 395  ⊢  
  : , : , :
386conjecture  ⊢  
 proveit.numbers.exponentiation.product_of_real_powers
387conjecture  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
388instantiation450, 396, 397  ⊢  
  : , : , :
389conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat1
390conjecture  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
391instantiation398, 409, 399, 400  ⊢  
  : , :
392instantiation450, 430, 401  ⊢  
  : , : , :
393instantiation450, 445, 402  ⊢  
  : , : , :
394instantiation403, 404, 440  ⊢  
  : , : , :
395instantiation450, 437, 405  ⊢  
  : , : , :
396conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
397instantiation450, 406, 407  ⊢  
  : , : , :
398conjecture  ⊢  
 proveit.numbers.division.div_complex_closure
399instantiation408, 423, 409  ⊢  
  : , :
400instantiation410, 411, 412  ⊢  
  : , : , :
401instantiation450, 437, 413  ⊢  
  : , : , :
402instantiation448, 414  ⊢  
  :
403theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
404instantiation415, 416  ⊢  
  : , :
405instantiation450, 445, 417  ⊢  
  : , : , :
406conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
407instantiation450, 418, 419  ⊢  
  : , : , :
408conjecture  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
409instantiation450, 430, 420  ⊢  
  : , : , :
410theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
411instantiation421, 428  ⊢  
  :
412instantiation422, 423  ⊢  
  :
413instantiation450, 445, 424  ⊢  
  : , : , :
414instantiation450, 425, 426  ⊢  
  : , : , :
415theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
416conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
417instantiation448, 436  ⊢  
  :
418conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
419instantiation450, 427, 428  ⊢  
  : , : , :
420instantiation450, 437, 429  ⊢  
  : , : , :
421conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
422conjecture  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
423instantiation450, 430, 431  ⊢  
  : , : , :
424instantiation432, 449, 433  ⊢  
  : , :
425instantiation434, 436, 435  ⊢  
  : , :
426assumption  ⊢  
427conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
428conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat2
429instantiation450, 445, 436  ⊢  
  : , : , :
430conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
431instantiation450, 437, 438  ⊢  
  : , : , :
432conjecture  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
433instantiation450, 439, 440  ⊢  
  : , : , :
434conjecture  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
435instantiation441, 442, 443  ⊢  
  : , :
436instantiation450, 451, 444  ⊢  
  : , : , :
437conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
438instantiation450, 445, 449  ⊢  
  : , : , :
439conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
440axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
441conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
442instantiation450, 446, 447  ⊢  
  : , : , :
443instantiation448, 449  ⊢  
  :
444theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
445conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
446conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
447conjecture  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
448conjecture  ⊢  
 proveit.numbers.negation.int_closure
449instantiation450, 451, 452  ⊢  
  : , : , :
450theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
451conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
452theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements