Updating QPE presumptions.txt files

sandialabs · Jan 5, 2023 · 75848ce · 75848ce
1 parent 92fa4eb
commit 75848ce
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 7 deletions.
diff --git a/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/_psi_t_var_formula/presumptions.txt b/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/_psi_t_var_formula/presumptions.txt
@@ -58,7 +58,6 @@ proveit.logic.booleans.conjunction.quantification_from_conjunction
 proveit.logic.booleans.conjunction.redundant_conjunction
 proveit.logic.booleans.conjunction.redundant_conjunction_general
 proveit.logic.booleans.conjunction.right_from_and
-proveit.logic.booleans.false_is_bool
 proveit.logic.booleans.fold_is_bool
 proveit.logic.booleans.from_not_false
 proveit.logic.booleans.implication.false_antecedent_implication
@@ -69,7 +68,6 @@ proveit.logic.booleans.implication.untrue_antecedent_implication
 proveit.logic.booleans.in_bool_if_true
 proveit.logic.booleans.negation.double_negation_elim
 proveit.logic.booleans.negation.negation_intro
-proveit.logic.booleans.true_is_bool
 proveit.logic.booleans.unfold_is_bool
 proveit.logic.booleans.unfold_is_bool_explicit
 proveit.logic.equality.equals_reversal

diff --git a/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_best_guarantee/presumptions.txt b/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_best_guarantee/presumptions.txt
@@ -188,7 +188,6 @@ proveit.numbers.exponentiation.exp_complex_closure
 proveit.numbers.exponentiation.exp_eq
 proveit.numbers.exponentiation.exp_eq_real
 proveit.numbers.exponentiation.exp_int_closure
-proveit.numbers.exponentiation.exp_monotonicity_large_base_less
 proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
 proveit.numbers.exponentiation.exp_nat_pos_expansion
 proveit.numbers.exponentiation.exp_nat_pos_rev

diff --git a/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_exact/presumptions.txt b/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_exact/presumptions.txt
@@ -185,7 +185,6 @@ proveit.numbers.division.weak_div_from_numer_bound__pos_denom
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
 proveit.numbers.exponentiation.exp_complex_closure
 proveit.numbers.exponentiation.exp_int_closure
-proveit.numbers.exponentiation.exp_monotonicity_large_base_less
 proveit.numbers.exponentiation.exp_nat_pos_expansion
 proveit.numbers.exponentiation.exp_nat_pos_rev
 proveit.numbers.exponentiation.exp_natpos_closure

diff --git a/.../proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_precision_guarantee/presumptions.txt b/.../proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_precision_guarantee/presumptions.txt
@@ -235,7 +235,6 @@ proveit.numbers.exponentiation.exp_eq
 proveit.numbers.exponentiation.exp_even_neg_base_lesseq
 proveit.numbers.exponentiation.exp_factored_real
 proveit.numbers.exponentiation.exp_int_closure
-proveit.numbers.exponentiation.exp_monotonicity_large_base_less
 proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
 proveit.numbers.exponentiation.exp_nat_pos_expansion
 proveit.numbers.exponentiation.exp_nat_pos_rev
@@ -250,7 +249,6 @@ proveit.numbers.exponentiation.exp_real_pos_closure
 proveit.numbers.exponentiation.exp_zero_eq_one
 proveit.numbers.exponentiation.exponent_log_with_same_base
 proveit.numbers.exponentiation.exponentiated_one
-proveit.numbers.exponentiation.exponentiated_zero
 proveit.numbers.exponentiation.int_exp_of_exp
 proveit.numbers.exponentiation.int_exp_of_neg_exp
 proveit.numbers.exponentiation.neg_power_as_div
@@ -305,7 +303,6 @@ proveit.numbers.multiplication.mult_real_closure_bin
 proveit.numbers.multiplication.mult_real_pos_closure
 proveit.numbers.multiplication.mult_real_pos_closure_bin
 proveit.numbers.multiplication.mult_zero_any
-proveit.numbers.multiplication.mult_zero_left
 proveit.numbers.multiplication.mult_zero_right
 proveit.numbers.multiplication.reversed_strong_bound_via_right_factor_bound
 proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound