# Theorems (or conjectures) for the theory of proveit.logic.booleans.conjunction¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprRange, IndexedVar
from proveit import A, B, C, D, E, i, j, k, l, m, n
from proveit.logic import And, Or, Not, TRUE, FALSE, Forall, in_bool, Boolean, Equals
from proveit.core_expr_types import A_1_to_l, A_1_to_m, B_1_to_m, C_1_to_m, C_1_to_n, D_1_to_n
from proveit.numbers import Natural, one
%begin theorems

Defining theorems for theory 'proveit.logic.booleans.conjunction'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

In [2]:
true_and_true = And(TRUE, TRUE)

Out[2]:
true_and_true (established theorem):

In [3]:
true_and_false_negated = Not(And(TRUE, FALSE))

Out[3]:
true_and_false_negated (established theorem):

In [4]:
false_and_true_negated = Not(And(FALSE, TRUE))

Out[4]:
false_and_true_negated (established theorem):

In [5]:
false_and_false_negated = Not(And(FALSE, FALSE))

Out[5]:
false_and_false_negated (established theorem):

In [6]:
empty_conjunction_eval = Equals(And(), TRUE)

Out[6]:
empty_conjunction_eval (established theorem):

In [7]:
left_from_and = Forall((A, B), A, conditions=[A, B])

Out[7]:
left_from_and (established theorem):

In [8]:
right_from_and = Forall((A, B), B, conditions=[A, B])

Out[8]:
right_from_and (established theorem):

In [9]:
and_if_both = Forall((A, B), And(A, B), conditions=[A, B])

Out[9]:
and_if_both (established theorem):

In [10]:
nand_if_left_but_not_right = Forall((A, B), Not(And(A, B)), conditions=[A, Not(B)])

Out[10]:
nand_if_left_but_not_right (established theorem):

In [11]:
nand_if_right_but_not_left = Forall((A, B), Not(And(A, B)), conditions=[Not(A), B])

Out[11]:
nand_if_right_but_not_left (established theorem):

In [12]:
nand_if_neither = Forall((A, B), Not(And(A, B)), conditions=[Not(A), Not(B)])

Out[12]:
nand_if_neither (established theorem):

In [13]:
nand_if_not_right = Forall((A,B), Not(And(A,B)), condition=Not(B), domain = Boolean)

Out[13]:
nand_if_not_right (conjecture with conjecture-based proof):

In [14]:
nand_if_not_left = Forall((A,B), Not(And(A,B)), condition=Not(A), domain = Boolean)

Out[14]:
nand_if_not_left (conjecture with conjecture-based proof):

In [15]:
nand_if_not_one = \
Forall((m, n),
Forall((A_1_to_m, B, C_1_to_n),
Not(And(A_1_to_m,B,C_1_to_n)), condition=Not(B)),
domain=Natural)

Out[15]:
nand_if_not_one (conjecture without proof):

In [16]:
falsified_and_if_not_right = Forall((A, B), Equals(And(A, B), FALSE), conditions=[A, Not(B)])

Out[16]:
falsified_and_if_not_right (conjecture with conjecture-based proof):

In [17]:
falsified_and_if_not_left = Forall((A, B), Equals(And(A, B), FALSE), conditions=[Not(A), B])

Out[17]:
falsified_and_if_not_left (conjecture with conjecture-based proof):

In [18]:
falsified_and_if_neither = Forall((A, B), Equals(And(A, B), FALSE), conditions=[Not(A), Not(B)])

Out[18]:
falsified_and_if_neither (established theorem):

In [19]:
unary_and_reduction_lemma = Forall(A, Equals(And(A), And(TRUE, A)), domain=Boolean)

Out[19]:
unary_and_reduction_lemma (conjecture with conjecture-based proof):

In [20]:
unary_and_reduction = Forall(A, Equals(And(A), A), domain=Boolean)

Out[20]:
unary_and_reduction (conjecture with conjecture-based proof):

Unproven

In [21]:
from_unary_and = Forall(A, A, conditions=[And(A)])

Out[21]:
from_unary_and (conjecture without proof):

In [22]:
unary_and_is_true_reduction = Forall(A, Equals(Equals(And(A), TRUE),
Equals(A, TRUE)))

Out[22]:
unary_and_is_true_reduction (conjecture without proof):

In [23]:
each_is_bool = \
Forall((m, n),
Forall((A_1_to_m, B, C_1_to_n), in_bool(B),
conditions=in_bool(And(A_1_to_m, B, C_1_to_n))),
domain=Natural)

Out[23]:
each_is_bool (conjecture without proof):

In [24]:
any_from_and = \
Forall((m, n),
Forall((A_1_to_m, B, C_1_to_n), B,
conditions=[A_1_to_m, B, C_1_to_n]),
domain=Natural)

Out[24]:
any_from_and (conjecture without proof):

In [25]:
some_from_and = \
Forall((l,m, n),
Forall((A_1_to_l,B_1_to_m,C_1_to_n),
And(B_1_to_m),
conditions=[A_1_to_l, B_1_to_m, C_1_to_n]),
domain = Natural)

Out[25]:
some_from_and (conjecture without proof):

In [26]:
and_if_all = Forall(m, Forall(A_1_to_m,
And(A_1_to_m),
conditions=A_1_to_m),
domain=Natural)

Out[26]:
and_if_all (conjecture without proof):

In [27]:
true_eval = Forall(m, Forall(A_1_to_m,
Equals(And(A_1_to_m), TRUE),
conditions=A_1_to_m),
domain=Natural)

Out[27]:
true_eval (conjecture without proof):

In [28]:
false_eval = Forall((m, n),
Forall((A_1_to_m, C_1_to_n),
Equals(And(A_1_to_m, FALSE, C_1_to_n), FALSE),
domain=Boolean),
domain=Natural)

Out[28]:
false_eval (conjecture without proof):

In [29]:
binary_closure = Forall((A, B), in_bool(And(A, B)), domain=Boolean)

Out[29]:
binary_closure (conjecture with conjecture-based proof):

In [30]:
closure = Forall(m, Forall(A_1_to_m,
in_bool(And(A_1_to_m)),
domain=Boolean),
domain=Natural)

Out[30]:
closure (conjecture without proof):

In [31]:
demorgans_law_or_to_and_bin = Forall((A,B), And(A,B), conditions=[Not(Or(Not(A), Not(B)))])

Out[31]:
demorgans_law_or_to_and_bin (conjecture without proof):

In [32]:
demorgans_law_or_to_and = \
Forall(m,
Forall(A_1_to_m,
And(A_1_to_m),
conditions=[Not(Or(ExprRange(i, Not(IndexedVar(A,i)),
one, m)))]),
domain = Natural)

Out[32]:
demorgans_law_or_to_and (conjecture without proof):

In [33]:
commutation = Forall((A, B), Equals(And(A, B), And(B, A)), domain=Boolean)

Out[33]:
commutation (conjecture with conjecture-based proof):

In [34]:
commute = Forall((A, B), And(B, A), conditions=[A, B])

Out[34]:
commute (conjecture without proof):

In [35]:
rightward_commutation = \
Forall((l, m, n),
Forall((A_1_to_l,B,C_1_to_m,D_1_to_n),
Equals(And(A_1_to_l, B, C_1_to_m, D_1_to_n),
And(A_1_to_l, C_1_to_m, B, D_1_to_n)) \
.with_wrapping_at(2),
domain = Boolean),
domain = Natural)

Out[35]:
rightward_commutation (conjecture without proof):

In [36]:
leftward_commutation = \
Forall((l, m, n),
Forall((A_1_to_l,B_1_to_m,C,D_1_to_n),
Equals(And(A_1_to_l, B_1_to_m, C, D_1_to_n),
And(A_1_to_l, C, B_1_to_m, D_1_to_n)) \
.with_wrapping_at(2),
domain=Boolean),
domain = Natural)

Out[36]:
leftward_commutation (conjecture without proof):

In [37]:
rightward_commute = \
Forall((l, m, n),
Forall((A_1_to_l,B,C_1_to_m,D_1_to_n),
And(A_1_to_l, C_1_to_m, B, D_1_to_n),
conditions=[And(A_1_to_l, B, C_1_to_m, D_1_to_n)]),
domain = Natural)

Out[37]:
rightward_commute (conjecture without proof):

In [38]:
leftward_commute = \
Forall((l, m, n),
Forall((A_1_to_l,B_1_to_m,C,D_1_to_n),
And(A_1_to_l, C, B_1_to_m,D_1_to_n),
conditions=[And(A_1_to_l, B_1_to_m, C, D_1_to_n)]),
domain = Natural)

Out[38]:
leftward_commute (conjecture without proof):

In [39]:
association = \
Forall((l,m,n),
Forall((A_1_to_l,B_1_to_m,C_1_to_n),
Equals(And(A_1_to_l, B_1_to_m, C_1_to_n),
And(A_1_to_l, And(B_1_to_m), C_1_to_n)) \
.with_wrapping_at(2),
domain=Boolean),
domain=Natural)

Out[39]:
association (conjecture without proof):

In [40]:
disassociation = \
Forall((l,m,n),
Forall((A_1_to_l,B_1_to_m,C_1_to_n),
Equals(And(A_1_to_l, And(B_1_to_m), C_1_to_n),
And(A_1_to_l, B_1_to_m, C_1_to_n)) \
.with_wrapping_at(2),
domain=Boolean),
domain=Natural)

Out[40]:
disassociation (conjecture without proof):

In [41]:
associate = \
Forall((l,m,n),
Forall((A_1_to_l,B_1_to_m,C_1_to_n),
And(A_1_to_l, And(B_1_to_m), C_1_to_n),
conditions=[And(A_1_to_l, B_1_to_m, C_1_to_n)]),
domain=Natural)

Out[41]:
associate (conjecture without proof):

In [42]:
disassociate = \
Forall((l,m,n),
Forall((A_1_to_l,B_1_to_m,C_1_to_n),
And(A_1_to_l, B_1_to_m, C_1_to_n),
conditions=[And(A_1_to_l, And(B_1_to_m), C_1_to_n)]),
domain=Natural)

Out[42]:
disassociate (conjecture without proof):

In [43]:
redundant_conjunction = Forall(n, Forall(A, And(ExprRange(k, A, one, n)), conditions=[A]),
domain=Natural)

Out[43]:
redundant_conjunction (conjecture without proof):

In [44]:
%end theorems

These theorems may now be imported from the theory package: proveit.logic.booleans.conjunction