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,  ⊢  
  : , : , :
1theorem  ⊢  
 proveit.logic.sets.inclusion.fold_subset_eq
2instantiation3, 32, 4, 5, 6,  ⊢  
  : , : , : , :
3theorem  ⊢  
 proveit.logic.sets.enumeration.true_for_each_then_true_for_all
4instantiation35  ⊢  
  : , :
5instantiation8, 32, 9, 7  ⊢  
  : , : , :
6instantiation8, 32, 9, 10  ⊢  
  : , : , :
7instantiation11, 12, 13, 14  ⊢  
  : , :
8theorem  ⊢  
 proveit.logic.sets.enumeration.fold
9instantiation35  ⊢  
  : , :
10instantiation15, 16, 17, 18  ⊢  
  : , :
11theorem  ⊢  
 proveit.logic.booleans.disjunction.or_if_right
12instantiation19, 20, 21  ⊢  
  : , : , : , : , :
13instantiation22  ⊢  
  : , :
14assumption  ⊢  
15theorem  ⊢  
 proveit.logic.booleans.disjunction.or_if_left
16instantiation22  ⊢  
  : , :
17instantiation22  ⊢  
  : , :
18assumption  ⊢  
19theorem  ⊢  
 proveit.logic.booleans.disjunction.each_is_bool
20theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
21instantiation23, 24  ⊢  
  :
22axiom  ⊢  
 proveit.logic.equality.equality_in_bool
23theorem  ⊢  
 proveit.logic.booleans.in_bool_if_true
24instantiation25, 26, 27, 28  ⊢  
  : , : , :
25theorem  ⊢  
 proveit.logic.sets.enumeration.unfold
26theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
27instantiation29  ⊢  
  : , : , :
28instantiation30, 31, 32, 33, 34  ⊢  
  : , : , : , : , :
29theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
30theorem  ⊢  
 proveit.logic.sets.enumeration.in_enumerated_set
31axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
32theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
33theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
34instantiation35  ⊢  
  : , :
35theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq