Proof of proveit.logic.booleans.conjunction.nand_if_not_left theorem¶
In [1]:
import proveit
from proveit import defaults, B
from proveit.logic import TRUE, FALSE
from proveit.logic.booleans.conjunction import (
nand_if_right_but_not_left, nand_if_neither)
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving nand_if_not_left
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
nand_if_not_left:
(see dependencies)
nand_if_not_left:
(see dependencies)
In [3]:
defaults.assumptions = nand_if_not_left.all_conditions()
defaults.assumptions: 
In [4]:
nand_if_right_but_not_left
In [5]:
nand_if_neither
In [6]:
nand_if_right_but_not_left.instantiate({B:TRUE})
In [7]:
nand_if_neither.instantiate({B:FALSE})
In [8]:
%qed
Out[8]:
