Show the Proof¶

In [1]:
import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

Out[1]:
step typerequirementsstatement
0instantiation1, 2, 3, 4, 5*, 6*
: , : , : , : , : , : , : , :
1theorem
proveit.statistics.prob_of_all_events_transformation
2theorem
proveit.physics.quantum.QPE._Omega_is_sample_space
3instantiation7, 8
: , :
4instantiation9, 29, 60, 65, 56
: , : , : , : , :
5instantiation10, 11
: , : , :
6instantiation12, 31, 67, 32, 13, 43, 14, 15*
: , : , : , : , : , :
7theorem
proveit.logic.booleans.conjunction.left_from_and
8instantiation16, 17
: , : , :
9theorem
proveit.numbers.modular.interval_left_shift_bijection
10axiom
proveit.logic.equality.substitution
11instantiation18, 19
: , :
12theorem
proveit.numbers.modular.redundant_mod_elimination_in_sum_in_modabs
13instantiation68, 52, 20
: , : , :
14instantiation68, 21, 22
: , : , :
15instantiation23, 24, 25
: , : , :
16theorem
proveit.logic.sets.functions.bijections.membership_unfolding
17theorem
proveit.physics.quantum.QPE._sample_space_bijection
18theorem
proveit.logic.equality.equals_reversal
19instantiation26, 56, 54
: , :
20instantiation68, 55, 27
: , : , :
21theorem
proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
22instantiation68, 28, 29
: , : , :
23axiom
proveit.logic.equality.equals_transitivity
24instantiation30, 31, 40, 67, 32, 33, 36, 37, 34
: , : , : , : , : , :
25instantiation35, 36, 37, 38
: , : , :
26axiom
27instantiation61, 56, 54
: , :
28theorem
proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
29instantiation39, 40, 41
: , :
30theorem
31axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
32theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
33instantiation42
: , :
34instantiation68, 44, 43
: , : , :
35theorem
36instantiation68, 44, 50
: , : , :
37instantiation68, 44, 45
: , : , :
38instantiation46
:
39theorem
proveit.numbers.exponentiation.exp_natpos_closure
40theorem
proveit.numbers.numerals.decimals.nat2
41instantiation68, 47, 48
: , : , :
42theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
43instantiation49, 50
:
44theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
45instantiation68, 52, 51
: , : , :
46axiom
proveit.logic.equality.equals_reflexivity
47theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
48axiom
proveit.physics.quantum.QPE._t_in_natural_pos
49theorem
proveit.numbers.negation.real_closure
50instantiation68, 52, 53
: , : , :
51instantiation68, 55, 54
: , : , :
52theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
53instantiation68, 55, 56
: , : , :
54instantiation68, 57, 58
: , : , :
55theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
56theorem
proveit.physics.quantum.QPE._best_floor_is_int
57instantiation59, 60, 65
: , :
58assumption
59theorem
proveit.numbers.number_sets.integers.int_interval_within_int
60instantiation61, 62, 63
: , :
61theorem
62instantiation64, 65
:
63instantiation68, 66, 67
: , : , :
64theorem
proveit.numbers.negation.int_closure
65instantiation68, 69, 70
: , : , :
66theorem
proveit.numbers.number_sets.integers.nat_within_int
67theorem
proveit.numbers.numerals.decimals.nat1
68theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
69theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
70theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
*equality replacement requirements