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  ⊢  
  : , : , :
1reference4  ⊢  
2instantiation4, 5, 6  ⊢  
  : , : , :
3instantiation10, 7, 8  ⊢  
  : , : , :
4theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
5deduction9  ⊢  
6instantiation10, 26, 11  ⊢  
  : , : , :
7theorem  ⊢  
 proveit.numbers.numerals.decimals.nat5
8instantiation12  ⊢  
  : , : , : , : , :
9instantiation15, 13, 14  ⊢  
  : , : , :
10axiom  ⊢  
 proveit.logic.sets.enumeration.enum_set_def
11instantiation36  ⊢  
  : , : , :
12theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
13instantiation15, 16, 17  ⊢  
  : , : , :
14instantiation21, 26, 30, 33, 18, 35, 22, 44, 23, 24, 45  ⊢  
  : , : , : , : , : , : , :
15theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
16instantiation25, 26, 32, 33, 27, 19, 35, 20  ⊢  
  : , : , : , : , : , :
17instantiation21, 30, 32, 29, 22, 23, 24, 44, 45  ⊢  
  : , : , : , : , : , : , :
18instantiation36  ⊢  
  : , : , :
19instantiation40  ⊢  
  : , :
20instantiation25, 33, 26, 30, 35, 27, 28  ⊢  
  : , : , : , : , : , :
21theorem  ⊢  
 proveit.logic.booleans.disjunction.leftward_commutation
22instantiation31, 33, 32, 35, 29, 38  ⊢  
  : , : , : , : , :
23instantiation31, 30, 38  ⊢  
  : , : , : , : , :
24instantiation31, 32, 33, 34, 35, 38  ⊢  
  : , : , : , : , :
25theorem  ⊢  
 proveit.logic.booleans.disjunction.disassociate
26theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
27instantiation36  ⊢  
  : , : , :
28instantiation37, 38, 39, 42  ⊢  
  : , :
29instantiation40  ⊢  
  : , :
30theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
31theorem  ⊢  
 proveit.logic.booleans.disjunction.each_is_bool
32theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
33axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
34instantiation40  ⊢  
  : , :
35theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
36theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
37theorem  ⊢  
 proveit.logic.booleans.disjunction.or_if_left
38instantiation41, 42  ⊢  
  :
39instantiation43, 44, 45  ⊢  
  : , :
40theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
41theorem  ⊢  
 proveit.logic.booleans.in_bool_if_true
42assumption  ⊢  
43theorem  ⊢  
 proveit.logic.booleans.disjunction.binary_closure
44instantiation46  ⊢  
  : , :
45instantiation46  ⊢  
  : , :
46axiom  ⊢  
 proveit.logic.equality.equality_in_bool