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
step type | requirements | statement | ||
---|---|---|---|---|
0 | instantiation | 1, 2, 3, 4, 5, 6 | , ⊢ | |
: , : , : | ||||
1 | reference | 12 | ⊢ | |
2 | instantiation | 20, 7 | , ⊢ | |
: , : | ||||
3 | instantiation | 21, 7 | , ⊢ | |
: , : | ||||
4 | reference | 10 | , ⊢ | |
5 | deduction | 8 | , ⊢ | |
6 | deduction | 9 | , ⊢ | |
7 | instantiation | 27, 10 | , ⊢ | |
: | ||||
8 | instantiation | 54, 11, 52 | , , ⊢ | |
: , : , : | ||||
9 | instantiation | 12, 13, 14, 28, 15, 16 | , , ⊢ | |
: , : , : | ||||
10 | instantiation | 17, 96, 97 | , ⊢ | |
: , : | ||||
11 | instantiation | 54, 18, 19 | , , ⊢ | |
: , : , : | ||||
12 | theorem | ⊢ | ||
proveit.logic.booleans.disjunction.singular_constructive_dilemma | ||||
13 | instantiation | 20, 22 | ⊢ | |
: , : | ||||
14 | instantiation | 21, 22 | ⊢ | |
: , : | ||||
15 | deduction | 23 | , , ⊢ | |
16 | deduction | 24 | , , ⊢ | |
17 | theorem | ⊢ | ||
proveit.numbers.ordering.less_or_greater_eq | ||||
18 | instantiation | 51, 39, 25 | , , ⊢ | |
: , : , : | ||||
19 | instantiation | 71, 26, 57 | , , ⊢ | |
: , : , : | ||||
20 | axiom | ⊢ | ||
proveit.logic.booleans.disjunction.left_in_bool | ||||
21 | axiom | ⊢ | ||
proveit.logic.booleans.disjunction.right_in_bool | ||||
22 | instantiation | 27, 28 | ⊢ | |
: | ||||
23 | instantiation | 54, 29, 39 | , , , ⊢ | |
: , : , : | ||||
24 | instantiation | 54, 30, 52 | , , , ⊢ | |
: , : , : | ||||
25 | instantiation | 71, 31, 32 | , , ⊢ | |
: , : , : | ||||
26 | instantiation | 71, 33, 34 | , , ⊢ | |
: , : , : | ||||
27 | theorem | ⊢ | ||
proveit.logic.booleans.in_bool_if_true | ||||
28 | instantiation | 35, 94, 36 | ⊢ | |
: , : | ||||
29 | instantiation | 54, 37, 55 | , , , ⊢ | |
: , : , : | ||||
30 | instantiation | 54, 38, 39 | , , , ⊢ | |
: , : , : | ||||
31 | instantiation | 71, 40, 41 | , , ⊢ | |
: , : , : | ||||
32 | instantiation | 74, 76, 75, 77 | ⊢ | |
: , : , : , : , : | ||||
33 | instantiation | 83, 42 | ⊢ | |
: , : , : | ||||
34 | instantiation | 83, 43 | , , ⊢ | |
: , : , : | ||||
35 | theorem | ⊢ | ||
proveit.logic.equality.rhs_via_equality | ||||
36 | instantiation | 44 | ⊢ | |
: , : | ||||
37 | instantiation | 99, 45 | , , ⊢ | |
: , : | ||||
38 | instantiation | 54, 46, 47 | , , , ⊢ | |
: , : , : | ||||
39 | instantiation | 60, 96, 97 | , ⊢ | |
: , : | ||||
40 | instantiation | 83, 48 | , , ⊢ | |
: , : , : | ||||
41 | instantiation | 83, 49 | ⊢ | |
: , : , : | ||||
42 | instantiation | 87, 59 | ⊢ | |
: , : | ||||
43 | instantiation | 88, 50 | , , ⊢ | |
: , : | ||||
44 | axiom | ⊢ | ||
proveit.numbers.ordering.less_eq_def | ||||
45 | instantiation | 51, 52, 53 | , , ⊢ | |
: , : , : | ||||
46 | instantiation | 54, 98, 55 | , , , ⊢ | |
: , : , : | ||||
47 | instantiation | 71, 56, 57 | , , ⊢ | |
: , : , : | ||||
48 | instantiation | 88, 58 | , , ⊢ | |
: , : | ||||
49 | instantiation | 87, 68 | ⊢ | |
: , : | ||||
50 | instantiation | 93, 96, 97, 59 | , , ⊢ | |
: , : | ||||
51 | theorem | ⊢ | ||
proveit.logic.equality.sub_right_side_into | ||||
52 | instantiation | 60, 97, 96 | , ⊢ | |
: , : | ||||
53 | instantiation | 71, 61, 62 | , , ⊢ | |
: , : , : | ||||
54 | theorem | ⊢ | ||
proveit.logic.equality.sub_left_side_into | ||||
55 | instantiation | 71, 63, 64 | , , ⊢ | |
: , : , : | ||||
56 | instantiation | 71, 65, 66 | , , ⊢ | |
: , : , : | ||||
57 | instantiation | 74, 75, 76, 77 | ⊢ | |
: , : , : , : , : | ||||
58 | instantiation | 91, 96, 97, 68 | , , ⊢ | |
: , : | ||||
59 | instantiation | 67, 68 | ⊢ | |
: , : | ||||
60 | axiom | ⊢ | ||
proveit.numbers.ordering.max_def_bin | ||||
61 | instantiation | 71, 69, 70 | , , ⊢ | |
: , : , : | ||||
62 | instantiation | 74, 76, 75, 77 | ⊢ | |
: , : , : , : , : | ||||
63 | instantiation | 71, 72, 73 | , , ⊢ | |
: , : , : | ||||
64 | instantiation | 74, 75, 76, 77 | ⊢ | |
: , : , : , : , : | ||||
65 | instantiation | 83, 78 | , , ⊢ | |
: , : , : | ||||
66 | instantiation | 83, 79 | , , ⊢ | |
: , : , : | ||||
67 | theorem | ⊢ | ||
proveit.numbers.ordering.relax_less | ||||
68 | assumption | ⊢ | ||
69 | instantiation | 83, 80 | , , ⊢ | |
: , : , : | ||||
70 | instantiation | 83, 81 | ⊢ | |
: , : , : | ||||
71 | axiom | ⊢ | ||
proveit.logic.equality.equals_transitivity | ||||
72 | instantiation | 83, 82 | ⊢ | |
: , : , : | ||||
73 | instantiation | 83, 84 | , , ⊢ | |
: , : , : | ||||
74 | axiom | ⊢ | ||
proveit.core_expr_types.conditionals.true_case_reduction | ||||
75 | axiom | ⊢ | ||
proveit.numbers.number_sets.natural_numbers.zero_in_nats | ||||
76 | theorem | ⊢ | ||
proveit.numbers.numerals.decimals.nat1 | ||||
77 | theorem | ⊢ | ||
proveit.core_expr_types.tuples.tuple_len_0_typical_eq | ||||
78 | instantiation | 87, 90 | , , ⊢ | |
: , : | ||||
79 | instantiation | 88, 85 | , , ⊢ | |
: , : | ||||
80 | instantiation | 88, 86 | , , ⊢ | |
: , : | ||||
81 | instantiation | 87, 92 | ⊢ | |
: , : | ||||
82 | instantiation | 87, 94 | ⊢ | |
: , : | ||||
83 | axiom | ⊢ | ||
proveit.logic.equality.substitution | ||||
84 | instantiation | 88, 89 | , , ⊢ | |
: , : | ||||
85 | instantiation | 93, 96, 97, 90 | , , ⊢ | |
: , : | ||||
86 | instantiation | 91, 97, 96, 92 | , , ⊢ | |
: , : | ||||
87 | theorem | ⊢ | ||
proveit.core_expr_types.conditionals.satisfied_condition_reduction | ||||
88 | theorem | ⊢ | ||
proveit.core_expr_types.conditionals.dissatisfied_condition_reduction | ||||
89 | instantiation | 93, 97, 96, 94 | , , ⊢ | |
: , : | ||||
90 | instantiation | 95, 96, 97, 98 | , , ⊢ | |
: , : | ||||
91 | theorem | ⊢ | ||
proveit.numbers.ordering.not_less_eq_from_less | ||||
92 | assumption | ⊢ | ||
93 | theorem | ⊢ | ||
proveit.numbers.ordering.not_less_from_less_eq | ||||
94 | assumption | ⊢ | ||
95 | theorem | ⊢ | ||
proveit.numbers.ordering.relax_equal_to_less_eq | ||||
96 | assumption | ⊢ | ||
97 | assumption | ⊢ | ||
98 | instantiation | 99, 100 | ⊢ | |
: , : | ||||
99 | theorem | ⊢ | ||
proveit.logic.equality.equals_reversal | ||||
100 | assumption | ⊢ |