# Demonstrations for the theory of proveit.logic.booleans.conjunction¶

In [1]:
from proveit import ExprTuple
from proveit import a, b, c, d, e, f, A,B,C,D,E,F,G,H, i, j, k, l, m,n
from proveit.core_expr_types import A_1_to_m, B_1_to_n,C_1_to_n
from proveit.logic import And, Or, Not, TRUE, FALSE, Equals, in_bool, Boolean
from proveit.numbers import zero, one, two, three,five,Add, Exp, subtract
%begin demonstrations

In [2]:
#And(A,B,C,D,E,F).derive_some_from_and(3, assumptions=[And(A,B,C,var_iter(D, one, one),E,F)])

In [3]:
#And(var_iter(A, one, five), var_iter(B, one, two), var_iter(C, one, three)).derive_some_from_and(1)

In [4]:
#And(A_1_to_m, B_1_to_n, C_1_to_n).derive_some_from_and(1)

In [5]:
Equals(Add(zero, Add(subtract(m, one), one)), Add(subtract(m, one), one))

Out[5]:
In [6]:
#Equals(Add(zero, Add(subtract(m, one), one)), Add(subtract(m, one), one)).prove()

In [7]:
expr = And(a, b, c, d, e, f)

Out[7]:
expr:
In [8]:
expr.copy().with_wrapping_at(3)

Out[8]:
In [9]:
new_expr = expr.copy().with_wrapping_at(3)

Out[9]:
new_expr:
In [10]:
expr

Out[10]:
In [11]:
new_expr

Out[11]:
In [12]:
expr = And(Or(a, b, c), Or(b, c, d), Or(d, e, f))

Out[12]:
expr:
In [13]:
new_expr = expr.copy()

Out[13]:
new_expr:
In [14]:
new_expr.inner_expr().operands[1].with_wrapping_at(3)

Out[14]:
In [15]:
expr

Out[15]:
In [16]:
print(expr==new_expr)

True

In [17]:
And(TRUE, TRUE).evaluation()

Out[17]:
In [18]:
And(TRUE, TRUE, TRUE).evaluation()

Out[18]:
In [19]:
Not(FALSE).prove()

Out[19]:
In [20]:
And(TRUE, Not(FALSE), TRUE).evaluation()

Out[20]:
In [21]:
And(TRUE, Not(FALSE), TRUE).prove()

Out[21]:
In [22]:
And(TRUE, Not(FALSE), TRUE).evaluation()

Out[22]:
In [23]:
And(TRUE, Or(TRUE, FALSE)).evaluation()

Out[23]:
In [24]:
And(TRUE, Or(TRUE, FALSE), FALSE).evaluation()

Out[24]:
In [ ]:


In [ ]:


In [25]:
And(TRUE, TRUE).prove()

Out[25]:
In [26]:
Not(And(TRUE, FALSE)).prove()

Out[26]:
In [27]:
Not(And(FALSE,TRUE)).prove()

Out[27]:
In [28]:
Not(And(FALSE,FALSE)).prove()

Out[28]:
In [29]:
And(A,B).prove([A,B])

Out[29]:
In [30]:
Not(And(A,B)).prove([in_bool(A), in_bool(B), Not(B)])

Out[30]:
, ,  ⊢
In [31]:
Not(And(A,B)).prove([in_bool(A), in_bool(B), Not(A)])

Out[31]:
, ,  ⊢
In [32]:
Not(And(A,B,C)).prove([Not(B)])

Out[32]:
In [33]:
And(A,B).derive_any(0,[And(A,B), *in_bool(A,B)])

Out[33]:
In [34]:
And(A,B).derive_any(1,[And(A,B), *in_bool(A,B)])

Out[34]:
In [35]:
And(A,B).commutation(assumptions=in_bool(A, B))

Out[35]:
In [36]:
And(A,B).commute(assumptions=[And(A, B)])

Out[36]:
In [37]:
in_bool(D).prove([in_bool(And(A,B,C,D))])

Out[37]:
In [38]:
from  proveit.logic.booleans.conjunction import each_is_bool
expr = each_is_bool.instance_expr.explicit_conditions()[0].element

Out[38]:
expr:
In [39]:
from proveit.logic import InSet
from proveit.numbers import Natural
expr.derive_any(1, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])

Out[39]:
, ,  ⊢
In [40]:
expr.derive_some(0, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])

Out[40]:
, ,  ⊢
In [41]:
expr.derive_some(2, assumptions=[InSet(m, Natural), InSet(n, Natural), expr])

Out[41]:
, ,  ⊢
In [42]:
from  proveit.logic.booleans.conjunction import any_from_and
any_from_and

Out[42]:
In [ ]:


In [43]:
And(A,B,C).prove([A,C,B])

Out[43]:
, ,  ⊢
In [44]:
And(A,B,C,D,E,F,G).associate(2,length=2,assumptions=[And(A,B,And(C,D),E,F,G),And(A,B,C,D,E,F,G),in_bool(A), in_bool(B),in_bool(C),in_bool(D),in_bool(E),in_bool(F),in_bool(G)])

Out[44]:
In [45]:
And(A,B,C,D,E).commute(1,3,[And(A,B,C,D,E), *in_bool(A,B,C,D,E)])

Out[45]:
In [46]:
And(A,B,C,D,E).group_commute(0,1,length=3, assumptions=[And(A,B,C,D,E), *in_bool(A,B,C,D,E)])

Out[46]:
In [47]:
expr = Or(A, B, And(C, D, E))

Out[47]:
expr:
In [48]:
expr.inner_expr().operands[-1].commutation(0, -1, assumptions=in_bool(C, D, E))

Out[48]:
, ,  ⊢
In [49]:
kt = expr.inner_expr().operands[-1].associate(0, length=2, assumptions=[expr])

Out[49]:
kt:
In [50]:
expr = kt.expr

Out[50]:
expr:
In [51]:
expr = expr.inner_expr().operands[-1].disassociate(0, assumptions=[expr])

Out[51]:
expr:
In [52]:
in_bool(And(A,B)).prove([in_bool(A), in_bool(B)])

Out[52]:
In [53]:
in_bool(And(A,B,C,D)).prove([in_bool(A), in_bool(B), in_bool(C), in_bool(D)])

Out[53]:
, , ,  ⊢
In [54]:
And(A,B).prove([Not(Or(Not(A), Not(B)))])

Out[54]:
In [55]:
And(A,B,C).prove([Not(Or(Not(A), Not(B), Not(C)))])

Out[55]:

## Axioms¶

In [56]:
Equals(And(TRUE, TRUE), TRUE).prove()

Out[56]:
In [57]:
Equals(And(TRUE, FALSE), FALSE).prove()

Out[57]:
In [58]:
Equals(And(FALSE, TRUE), FALSE).prove()

Out[58]:
In [59]:
Equals(And(FALSE, FALSE), FALSE).prove()

Out[59]:
In [60]:
in_bool(A).prove([in_bool(And(A,B))])

Out[60]:
In [61]:
in_bool(B).prove([in_bool(And(A,B))])

Out[61]:
In [62]:
Equals(And(FALSE, TRUE), FALSE).prove()

Out[62]:
In [63]:
Equals(And(FALSE, FALSE), FALSE).prove()

Out[63]:
In [64]:
in_bool(A).prove([in_bool(And(A,B))])

Out[64]:
In [65]:
in_bool(B).prove([in_bool(And(A,B))])

Out[65]:
In [66]:
%end demonstrations