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

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, P, i, j, k, l, m, n, Pk
from proveit.logic import And, Implies, 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 one, Add, Integer, Interval, LessEq, Natural

%begin theorems

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

true_and_true = And(TRUE, TRUE)

true_and_true (established theorem):

true_and_false_negated = Not(And(TRUE, FALSE))

true_and_false_negated (established theorem):

false_and_true_negated = Not(And(FALSE, TRUE))

false_and_true_negated (established theorem):

false_and_false_negated = Not(And(FALSE, FALSE))

false_and_false_negated (established theorem):

empty_conjunction_eval = Equals(And(), TRUE)

empty_conjunction_eval (established theorem):

left_from_and = Forall((A, B), A, conditions=[A, B])

left_from_and (established theorem):

right_from_and = Forall((A, B), B, conditions=[A, B])

right_from_and (established theorem):

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

and_if_both (established theorem):

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

nand_if_left_but_not_right (established theorem):

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

nand_if_right_but_not_left (established theorem):

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

nand_if_neither (established theorem):

nand_if_not_right = Forall((A,B), Not(And(A,B)), condition=Not(B), domain = Boolean)

nand_if_not_right (conjecture with conjecture-based proof):

nand_if_not_left = Forall((A,B), Not(And(A,B)), condition=Not(A), domain = Boolean)

nand_if_not_left (conjecture with conjecture-based proof):

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)

nand_if_not_one (conjecture without proof):

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

falsified_and_if_not_right (conjecture with conjecture-based proof):

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

falsified_and_if_not_left (conjecture with conjecture-based proof):

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

falsified_and_if_neither (established theorem):

unary_and_reduction_lemma = Forall(A, Equals(And(A), And(TRUE, A)), domain=Boolean)

unary_and_reduction_lemma (conjecture with conjecture-based proof):

unary_and_reduction = Forall(A, Equals(And(A), A), domain=Boolean)

unary_and_reduction (conjecture with conjecture-based proof):

Unproven

from_unary_and = Forall(A, A, conditions=[And(A)])

from_unary_and (conjecture without proof):

unary_and_is_true_reduction = Forall(A, Equals(Equals(And(A), TRUE), 
                                               Equals(A, TRUE)))

unary_and_is_true_reduction (conjecture without proof):

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)

each_is_bool (conjecture without proof):

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)

any_from_and (conjecture without proof):

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)

some_from_and (conjecture without proof):

and_if_all = Forall(m, Forall(A_1_to_m, 
                            And(A_1_to_m), 
                            conditions=A_1_to_m), 
                  domain=Natural)

and_if_all (conjecture without proof):

true_eval = Forall(m, Forall(A_1_to_m, 
                            Equals(And(A_1_to_m), TRUE), 
                            conditions=A_1_to_m),
                  domain=Natural)

true_eval (conjecture without proof):

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)

false_eval (conjecture without proof):

binary_closure = Forall((A, B), in_bool(And(A, B)), domain=Boolean)

binary_closure (conjecture with conjecture-based proof):

closure = Forall(m, Forall(A_1_to_m, 
                           in_bool(And(A_1_to_m)), 
                           domain=Boolean),
                 domain=Natural)

closure (conjecture without proof):

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

demorgans_law_or_to_and_bin (conjecture without proof):

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)

demorgans_law_or_to_and (conjecture without proof):

commutation = Forall((A, B), Equals(And(A, B), And(B, A)), domain=Boolean)

commutation (conjecture with conjecture-based proof):

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

commute (conjecture without proof):

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)

rightward_commutation (conjecture without proof):

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)

leftward_commutation (conjecture without proof):

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)

rightward_commute (conjecture without proof):

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)

leftward_commute (conjecture without proof):

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)

association (conjecture without proof):

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)

disassociation (conjecture without proof):

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)

associate (conjecture without proof):

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)

disassociate (conjecture without proof):

redundant_conjunction = Forall(n, Forall(A, And(ExprRange(k, A, one, n)),
                                condition=A), domain=Natural)

redundant_conjunction (conjecture without proof):

redundant_conjunction_general = Forall((i, j), Forall(A, And(ExprRange(k, A, i, j)),
                                conditions=[A, LessEq(i, Add(j, one))]),
                               domain=Integer)

redundant_conjunction_general (conjecture without proof):

conjunction_eq_quantification = Forall(
    (i, j), Forall(P, Equals(And(ExprRange(k, Pk, i, j)),
                             Forall(k, Pk, domain=Interval(i,j))),
                   conditions=[LessEq(i, Add(j, one))]),
    domain=Integer)

conjunction_eq_quantification (conjecture without proof):

conjunction_from_quantification = Forall(
    (i, j), Forall(P, Implies(Forall(k, Pk, domain=Interval(i,j)), 
                              And(ExprRange(k, Pk, i, j))),
                   conditions=[LessEq(i, Add(j, one))]),
    domain=Integer)

conjunction_from_quantification (conjecture without proof):

quantification_from_conjunction = Forall(
    (i, j), Forall(P, Implies(And(ExprRange(k, Pk, i, j)),
                              Forall(k, Pk, domain=Interval(i,j)))),
    domain=Integer)

quantification_from_conjunction (conjecture without proof):

%end theorems

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