logo

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, ,  ⊢  
  : , : , :
1reference57  ⊢  
2instantiation4, 67, 73, 5, 71, 87, 79, 80, 81, 82, 83, ,  ⊢  
  : , : , : , :
3instantiation57, 6, 7, ,  ⊢  
  : , : , :
4theorem  ⊢  
 proveit.numbers.addition.elim_zero_any
5instantiation84  ⊢  
  : , : , : , : , : , :
6instantiation57, 8, 9, ,  ⊢  
  : , : , :
7instantiation42, 106, 103, 75, 10, 61, 78, 24, 17, 11, 82, 12*, ,  ⊢  
  : , : , : , : , : , :
8instantiation57, 13, 14, ,  ⊢  
  : , : , :
9instantiation42, 103, 106, 15, 16, 61, 24, 17, 81, 82, 18*, ,  ⊢  
  : , : , : , : , : , :
10instantiation54  ⊢  
  : , : , :
11instantiation36, 83, 81  ⊢  
  : , :
12instantiation49, 19, 69*  ⊢  
  : , :
13instantiation57, 20, 21, ,  ⊢  
  : , : , :
14instantiation42, 102, 106, 74, 22, 23, 24, 79, 80, 83, 81, 82, 25*, ,  ⊢  
  : , : , : , : , : , :
15instantiation85  ⊢  
  : , :
16instantiation54  ⊢  
  : , : , :
17instantiation104, 92, 26  ⊢  
  : , : , :
18instantiation49, 27, 28*  ⊢  
  : , :
19instantiation63, 75, 103, 102, 78, 64, 79, 82, 29*  ⊢  
  : , : , : , : , : , :
20instantiation57, 30, 31, ,  ⊢  
  : , : , :
21instantiation42, 75, 103, 32, 78, 33, 34, 87, 79, 80, 83, 81, 82, 35*, ,  ⊢  
  : , : , : , : , : , :
22instantiation54  ⊢  
  : , : , :
23instantiation89  ⊢  
  : , : , : , : , :
24instantiation36, 80, 87  ⊢  
  : , :
25instantiation42, 75, 103, 102, 78, 37, 79, 80, 83, 38*  ⊢  
  : , : , : , : , : , :
26instantiation104, 96, 39  ⊢  
  : , : , :
27instantiation63, 75, 106, 102, 78, 40, 79, 81, 41*  ⊢  
  : , : , : , : , : , :
28instantiation42, 75, 103, 102, 78, 64, 79, 43*  ⊢  
  : , : , : , : , : , :
29instantiation86, 82  ⊢  
  :
30instantiation57, 44, 45, ,  ⊢  
  : , : , :
31instantiation72, 46, 103, 75, 47, 61, 78, 87, 79, 80, 83, 81, 82, ,  ⊢  
  : , : , : , : , : , : , :
32theorem  ⊢  
 proveit.numbers.numerals.decimals.nat8
33instantiation85  ⊢  
  : , :
34instantiation48  ⊢  
  : , : , : , : , : , : , : , :
35instantiation49, 50, 69*  ⊢  
  : , :
36theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
37instantiation85  ⊢  
  : , :
38instantiation57, 51, 52  ⊢  
  : , : , :
39instantiation104, 100, 53  ⊢  
  : , : , :
40instantiation54  ⊢  
  : , : , :
41instantiation86, 81  ⊢  
  :
42theorem  ⊢  
 proveit.numbers.addition.association
43instantiation57, 55, 56  ⊢  
  : , : , :
44instantiation57, 58, 59, ,  ⊢  
  : , : , :
45instantiation72, 67, 103, 102, 60, 61, 87, 79, 80, 83, 81, 82, ,  ⊢  
  : , : , : , : , : , : , :
46theorem  ⊢  
 proveit.numbers.numerals.decimals.nat7
47instantiation62  ⊢  
  : , : , : , : , : , : , :
48theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_8_typical_eq
49theorem  ⊢  
 proveit.logic.equality.equals_reversal
50instantiation63, 75, 103, 102, 78, 64, 79, 87, 65*  ⊢  
  : , : , : , : , : , :
51instantiation68, 66  ⊢  
  : , : , :
52theorem  ⊢  
 proveit.numbers.numerals.decimals.add_3_3
53instantiation104, 105, 67  ⊢  
  : , : , :
54theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
55instantiation68, 69  ⊢  
  : , : , :
56theorem  ⊢  
 proveit.numbers.numerals.decimals.add_2_1
57axiom  ⊢  
 proveit.logic.equality.equals_transitivity
58instantiation72, 102, 73, 70, 71, 87, 79, 80, 81, 82, 83, ,  ⊢  
  : , : , : , : , : , : , :
59instantiation72, 73, 74, 75, 76, 77, 78, 87, 79, 80, 81, 82, 83, ,  ⊢  
  : , : , : , : , : , : , :
60instantiation84  ⊢  
  : , : , : , : , : , :
61instantiation85  ⊢  
  : , :
62theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_7_typical_eq
63theorem  ⊢  
 proveit.numbers.multiplication.distribute_through_sum
64instantiation85  ⊢  
  : , :
65instantiation86, 87  ⊢  
  :
66theorem  ⊢  
 proveit.numbers.numerals.decimals.add_1_2
67theorem  ⊢  
 proveit.numbers.numerals.decimals.nat6
68axiom  ⊢  
 proveit.logic.equality.substitution
69theorem  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
70instantiation88  ⊢  
  : , : , : , :
71instantiation88  ⊢  
  : , : , : , :
72theorem  ⊢  
 proveit.numbers.addition.leftward_commutation
73theorem  ⊢  
 proveit.numbers.numerals.decimals.nat4
74theorem  ⊢  
 proveit.numbers.numerals.decimals.nat5
75axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
76instantiation88  ⊢  
  : , : , : , :
77instantiation89  ⊢  
  : , : , : , : , :
78theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
79instantiation104, 92, 90  ⊢  
  : , : , :
80instantiation104, 92, 91  ⊢  
  : , : , :
81assumption  ⊢  
82assumption  ⊢  
83instantiation104, 92, 93  ⊢  
  : , : , :
84theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_6_typical_eq
85theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
86theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
87assumption  ⊢  
88theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
89theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
90instantiation104, 96, 94  ⊢  
  : , : , :
91instantiation104, 96, 95  ⊢  
  : , : , :
92theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
93instantiation104, 96, 97  ⊢  
  : , : , :
94instantiation104, 100, 98  ⊢  
  : , : , :
95instantiation104, 100, 99  ⊢  
  : , : , :
96theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
97instantiation104, 100, 101  ⊢  
  : , : , :
98instantiation104, 105, 102  ⊢  
  : , : , :
99instantiation104, 105, 103  ⊢  
  : , : , :
100theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
101instantiation104, 105, 106  ⊢  
  : , : , :
102theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
103theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
104theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
105theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
106theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
*equality replacement requirements