logo
In [1]:
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
In [2]:
%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".
In [3]:
defaults.assumptions = falsified_and_if_not_right.all_conditions()
defaults.assumptions:
In [4]:
nand_if_not_right
In [5]:
nand = nand_if_not_right.instantiate({A:A, B:B})
nand: ,  ⊢  
In [6]:
# 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.
Out[6]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation2, 3,  ⊢  
  :
2axiom  ⊢  
 proveit.logic.booleans.negation.negation_elim
3instantiation4, 5, 6, 11,  ⊢  
  : , :
4conjecture  ⊢  
 proveit.logic.booleans.conjunction.nand_if_not_right
5instantiation10, 7  ⊢  
  :
6instantiation8, 9  ⊢  
  :
7assumption  ⊢  
8axiom  ⊢  
 proveit.logic.booleans.negation.operand_is_bool
9instantiation10, 11  ⊢  
  :
10conjecture  ⊢  
 proveit.logic.booleans.in_bool_if_true
11assumption  ⊢