logo

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