From 75848ce926551d0c922194bdeb3f5174142f77cd Mon Sep 17 00:00:00 2001 From: Wayne Witzel Date: Thu, 5 Jan 2023 13:27:14 -0700 Subject: [PATCH] Updating QPE presumptions.txt files --- .../_theory_nbs_/proofs/_psi_t_var_formula/presumptions.txt | 2 -- .../_theory_nbs_/proofs/qpe_best_guarantee/presumptions.txt | 1 - .../quantum/QPE/_theory_nbs_/proofs/qpe_exact/presumptions.txt | 1 - .../proofs/qpe_precision_guarantee/presumptions.txt | 3 --- 4 files changed, 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 index 61b6c360e31c..0037a200da3e 100644 --- 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 index 0fb53146e989..b647fd15b38b 100644 --- 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 index 8854e16280b9..b24f4b4ef924 100644 --- 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/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_precision_guarantee/presumptions.txt b/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_precision_guarantee/presumptions.txt index 7bc6acb96a28..3aa3e3a73472 100644 --- a/packages/proveit/physics/quantum/QPE/_theory_nbs_/proofs/qpe_precision_guarantee/presumptions.txt +++ b/packages/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