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