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 type	requirements	statement
0	instantiation	1, 2, 3	⊢
	: , : , :
1	reference	19	⊢
2	instantiation	4, 49, 5, 6^, 7^, 8^*	⊢
	: , : , :
3	instantiation	19, 9, 10	⊢
	: , : , :
4	theorem		⊢
	proveit.logic.sets.enumeration.nonmembership_equiv
5	instantiation	33	⊢
	: , : , : , :
6	instantiation	13, 11^*	⊢
	: , :
7	instantiation	13, 12^*	⊢
	: , :
8	instantiation	13, 14^*	⊢
	: , :
9	instantiation	29, 15	⊢
	: , : , :
10	instantiation	22, 16	⊢
	:
11	instantiation	19, 17, 21	⊢
	: , : , :
12	instantiation	19, 18, 21	⊢
	: , : , :
13	axiom		⊢
	proveit.logic.equality.not_equals_def
14	instantiation	19, 20, 21	⊢
	: , : , :
15	instantiation	22, 23	⊢
	:
16	instantiation	24, 49, 25, 26	⊢
	: , :
17	instantiation	29, 27	⊢
	: , : , :
18	instantiation	29, 28	⊢
	: , : , :
19	axiom		⊢
	proveit.logic.equality.equals_transitivity
20	instantiation	29, 30	⊢
	: , : , :
21	axiom		⊢
	proveit.logic.booleans.negation.not_f
22	axiom		⊢
	proveit.logic.booleans.eq_true_intro
23	instantiation	53, 79, 31, 32	⊢
	: , :
24	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_all
25	instantiation	33	⊢
	: , : , : , :
26	axiom		⊢
	proveit.logic.booleans.true_axiom
27	instantiation	36, 34	⊢
	:
28	instantiation	36, 35	⊢
	:
29	axiom		⊢
	proveit.logic.equality.substitution
30	instantiation	36, 37	⊢
	:
31	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
32	instantiation	56, 72, 57, 38, 39, 59^, 40^	⊢
	: , : , :
33	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
34	instantiation	43, 41	⊢
	: , :
35	instantiation	43, 42	⊢
	: , :
36	axiom		⊢
	proveit.logic.booleans.negation.negation_elim
37	instantiation	43, 44	⊢
	: , :
38	instantiation	77, 73, 45	⊢
	: , : , :
39	instantiation	62, 46	⊢
	:
40	theorem		⊢
	proveit.numbers.numerals.decimals.add_3_2
41	instantiation	47, 48	⊢
	: , :
42	instantiation	53, 79, 49, 50	⊢
	: , :
43	theorem		⊢
	proveit.logic.equality.unfold_not_equals
44	instantiation	53, 79, 61, 51	⊢
	: , :
45	instantiation	77, 75, 52	⊢
	: , : , :
46	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
47	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
48	instantiation	53, 54, 79, 55	⊢
	: , :
49	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
50	instantiation	56, 72, 57, 58, 59^, 60^	⊢
	: , : , :
51	theorem		⊢
	proveit.numbers.numerals.decimals.less_2_3
52	instantiation	77, 78, 61	⊢
	: , : , :
53	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_nat
54	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
55	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
56	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
57	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
58	instantiation	62, 63	⊢
	:
59	instantiation	64, 65, 66	⊢
	: , : , :
60	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
61	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
62	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
63	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
64	theorem		⊢
	proveit.logic.equality.sub_right_side_into
65	instantiation	67, 69	⊢
	:
66	instantiation	68, 69, 70	⊢
	: , :
67	theorem		⊢
	proveit.numbers.addition.elim_zero_right
68	theorem		⊢
	proveit.numbers.addition.commutation
69	instantiation	77, 71, 72	⊢
	: , : , :
70	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
71	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
72	instantiation	77, 73, 74	⊢
	: , : , :
73	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
74	instantiation	77, 75, 76	⊢
	: , : , :
75	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
76	instantiation	77, 78, 79	⊢
	: , : , :
77	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
78	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
79	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
^*equality replacement requirements