Proof of proveit.logic.booleans.disjunction.binary_closure theorem

import proveit
# we need to import false_or_false_negated to derive it's side-effects:
from proveit.logic.booleans.disjunction import \
    (true_or_true, false_or_true, true_or_false, false_or_false_negated)
theory = proveit.Theory() # the theorem's theory

%proving binary_closure

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
binary_closure:
(see dependencies)

binary_closure may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.logic.booleans.disjunction.binary_closure has been proven.

	step type	requirements	statement
0	modus ponens	1, 2	⊢
1	instantiation	3, 4	⊢
	: , : , : , : , : , : , :
2	instantiation	8, 5, 6	⊢
	: , :
3	conjecture		⊢
	proveit.logic.booleans.quantification.universality.bundle
4	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
5	generalization	7	⊢
6	instantiation	8, 9, 10	⊢
	: , :
7	instantiation	19, 11	⊢
	:
8	conjecture		⊢
	proveit.logic.booleans.forall_over_bool_by_cases
9	instantiation	19, 12	⊢
	:
10	instantiation	13, 14	⊢
	:
11	instantiation	15, 16, 17, 20	⊢
	: , :
12	theorem		⊢
	proveit.logic.booleans.disjunction.false_or_true
13	axiom		⊢
	proveit.logic.booleans.negation.operand_is_bool
14	instantiation	19, 18	⊢
	:
15	conjecture		⊢
	proveit.logic.booleans.disjunction.or_if_left
16	instantiation	19, 20	⊢
	:
17	assumption		⊢
18	theorem		⊢
	proveit.logic.booleans.disjunction.false_or_false_negated
19	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
20	axiom		⊢
	proveit.logic.booleans.true_axiom