In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit import e
from proveit.physics.quantum.QPE import (
_success_def, _fail_def, _Omega, _outcome_prob, _Omega_is_sample_space, _sample_space_bijection,
_two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos, _best_floor_is_int)
In [2]:
%proving _success_complements_failure
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_success_complements_failure:
(see dependencies)
_success_complements_failure:
(see dependencies)
In [3]:
defaults.assumptions = _success_complements_failure.conditions
defaults.assumptions: 
In [4]:
success_def_inst = _success_def.instantiate()
success_def_inst: 
⊢ 
⊢ 
In [5]:
fail_def_inst = _fail_def.instantiate()
fail_def_inst: ⊢ 
⊢ 
In [6]:
success_def_inst.inner_expr().rhs.compute_via_complement(
fail_def_inst.rhs, _Omega, replacements=[fail_def_inst.derive_reversed()])
In [7]:
%qed
Out[7]:
