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

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

%proving falsified_and_if_not_right

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

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

defaults.assumptions = falsified_and_if_not_right.all_conditions()

defaults.assumptions:

nand_if_not_right

 ⊢  

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

nand: ,  ⊢  

# To do this manually, 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_right 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, 11	,  ⊢
	: , :
4	conjecture		⊢
	proveit.logic.booleans.conjunction.nand_if_not_right
5	instantiation	10, 7	⊢
	:
6	instantiation	8, 9	⊢
	:
7	assumption		⊢
8	axiom		⊢
	proveit.logic.booleans.negation.operand_is_bool
9	instantiation	10, 11	⊢
	:
10	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
11	assumption		⊢