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, 4,  ⊢  
  : , :
1theorem  ⊢  
 proveit.numbers.ordering.not_less_from_less_eq
2reference44  ⊢  
3reference40  ⊢  
4instantiation5, 39, 21, 6, 7, 8*, 9*,  ⊢  
  : , : , :
5theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
6instantiation10, 40, 46  ⊢  
  : , :
7instantiation11, 21, 40, 46, 12, 13,  ⊢  
  : , : , :
8instantiation14, 37, 36, 15, 16  ⊢  
  : , : , :
9instantiation17, 18, 19  ⊢  
  : , : , :
10theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
11theorem  ⊢  
 proveit.numbers.ordering.less_add_right_weak
12assumption  ⊢  
13instantiation20, 57  ⊢  
  :
14theorem  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
15instantiation55, 43, 21  ⊢  
  : , : , :
16instantiation22, 23, 24  ⊢  
  : , : , :
17axiom  ⊢  
 proveit.logic.equality.equals_transitivity
18instantiation25, 26, 27, 54, 28, 29, 32, 36, 30  ⊢  
  : , : , : , : , : , :
19instantiation31, 36, 32, 33  ⊢  
  : , : , :
20theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_lower_bound
21instantiation55, 49, 34  ⊢  
  : , : , :
22theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
23theorem  ⊢  
 proveit.numbers.numerals.decimals.add_5_1
24instantiation35, 36, 37  ⊢  
  : , :
25theorem  ⊢  
 proveit.numbers.addition.disassociation
26axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
27theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
28theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
29instantiation38  ⊢  
  : , :
30instantiation55, 43, 39  ⊢  
  : , : , :
31theorem  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
32instantiation55, 43, 40  ⊢  
  : , : , :
33instantiation41  ⊢  
  :
34instantiation55, 52, 42  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.numbers.addition.commutation
36instantiation55, 43, 46  ⊢  
  : , : , :
37instantiation55, 43, 44  ⊢  
  : , : , :
38theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
39instantiation45, 46  ⊢  
  :
40assumption  ⊢  
41axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
42instantiation55, 56, 47  ⊢  
  : , : , :
43theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
44instantiation55, 49, 48  ⊢  
  : , : , :
45theorem  ⊢  
 proveit.numbers.negation.real_closure
46instantiation55, 49, 50  ⊢  
  : , : , :
47theorem  ⊢  
 proveit.numbers.numerals.decimals.nat6
48instantiation55, 52, 51  ⊢  
  : , : , :
49theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
50instantiation55, 52, 53  ⊢  
  : , : , :
51instantiation55, 56, 54  ⊢  
  : , : , :
52theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
53instantiation55, 56, 57  ⊢  
  : , : , :
54theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
55theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
56theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
57theorem  ⊢  
 proveit.numbers.numerals.decimals.nat5
*equality replacement requirements