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, , , ,  ⊢  
  : , : , :
3instantiation16, 11, 10, 7, 12, 18, 8, 9, ,  ⊢  
  : , : , : , : , : , :
4axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
5instantiation16, 10, 11, 12, 13, 14, 19, 15, ,  ⊢  
  : , : , : , : , : , :
6instantiation16, 17, 18, 19, 20, ,  ⊢  
  : , : , : , : , : , :
7instantiation21  ⊢  
  : , :
8assumption  ⊢  
9assumption  ⊢  
10axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
11theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
12theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
13instantiation21  ⊢  
  : , :
14assumption  ⊢  
15assumption  ⊢  
16theorem  ⊢  
 proveit.numbers.multiplication.strong_bound_via_factor_bound
17theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
18assumption  ⊢  
19assumption  ⊢  
20assumption  ⊢  
21theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq