Proof of proveit.logic.booleans.conjunction.falsified_and_if_not_left theorem

import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.conjunction import nand_if_not_left
theory = proveit.Theory() # the theorem's theory

%proving falsified_and_if_not_left

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

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

defaults.assumptions = falsified_and_if_not_left.all_conditions()

defaults.assumptions:

nand_if_not_left

 ⊢  

nand = nand_if_not_left.instantiate({A:A, B:B})

nand: ,  ⊢  

# To do this manually, we'd execute nand.equate_negated_to_false(assumptions=conditions) and then generalize.
# But it can figure this out via automation.
%qed

proveit.logic.booleans.conjunction.falsified_and_if_not_left has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	,  ⊢
	:
2	axiom		⊢
	proveit.logic.booleans.negation.negation_elim
3	instantiation	4, 5, 6, 8	,  ⊢
	: , :
4	conjecture		⊢
	proveit.logic.booleans.conjunction.nand_if_not_left
5	instantiation	7, 8	⊢
	:
6	instantiation	9, 10	⊢
	:
7	conjecture		⊢
	proveit.logic.booleans.in_bool_if_false
8	assumption		⊢
9	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
10	assumption		⊢