Proof of proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin theorem¶

In [1]:
import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import in_bool
from proveit.logic.booleans.disjunction import demorgans_law_and_to_or_bin_explicit
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving demorgans_law_and_to_or_bin

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
demorgans_law_and_to_or_bin:
(see dependencies)
In [3]:
defaults.assumptions = demorgans_law_and_to_or_bin.all_conditions()

defaults.assumptions:
In [4]:
in_bool(defaults.assumptions[0].operands[0].operands[0].operand).prove()

In [5]:
in_bool(defaults.assumptions[0].operands[0].operands[1].operand).prove()

In [6]:
demorgans_law_and_to_or_bin_explicit

In [7]:
demorgans_law_and_to_or_bin_explicit.instantiate(
{A:A, B:B}, assumptions = demorgans_law_and_to_or_bin.all_conditions())

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

In [8]:
%qed

proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin has been proven.

Out[8]:
step typerequirementsstatement
0generalization1
1instantiation2, 3, 4, 13
: , :
2conjecture
proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin_explicit
3instantiation10, 5
:
4instantiation10, 6
:
5instantiation7, 9
: , :
6instantiation8, 9
: , :
7axiom
proveit.logic.booleans.conjunction.left_in_bool
8axiom
proveit.logic.booleans.conjunction.right_in_bool
9instantiation10, 11
:
10axiom
proveit.logic.booleans.negation.operand_is_bool
11instantiation12, 13
:
12conjecture
proveit.logic.booleans.in_bool_if_true
13assumption