logo

Theorems (or conjectures) for the theory of proveit.logic.sets.subtraction

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.logic import Forall, Iff, InSet, NotInSet, Set, Difference, And, Or, Equals, NotEquals
from proveit import x, y, S, A, B
%begin theorems

Defining theorems for theory 'proveit.logic.sets.subtraction'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [2]:
membership_unfolding = Forall((x, A, B), And(InSet(x, A), NotInSet(x, B)), 
                             conditions=[InSet(x, Difference(A, B))])
membership_unfolding (conjecture without proof):
In [3]:
membership_folding = Forall((x, A, B), InSet(x, Difference(A, B)), 
                           conditions=[InSet(x, A), NotInSet(x, B)])
membership_folding (conjecture without proof):
In [4]:
nonmembership_equiv = Forall((x, A, B), Equals(NotInSet(x, Difference(A, B)), 
                                              Or(NotInSet(x, A), InSet(x, B))))
nonmembership_equiv (conjecture without proof):
In [5]:
nonmembership_folding = Forall((x, A, B), NotInSet(x, Difference(A, B)), 
                              conditions=[Or(NotInSet(x, A), InSet(x, B))])
nonmembership_folding (conjecture without proof):
In [6]:
nonmembership_unfolding = Forall((x, A, B), Or(NotInSet(x, A), InSet(x, B)),
                                 condition=NotInSet(x, Difference(A, B)))
nonmembership_unfolding (conjecture without proof):
In [7]:
all_but_one_membership_unfolding = Forall((S, y), Forall(x, And(InSet(x, S), NotEquals(x, y)), 
                                                         domain=Difference(S, Set(y))))
all_but_one_membership_unfolding (conjecture without proof):
In [8]:
all_but_one_membership_folding = Forall((S, y), Forall(x, InSet(x, Difference(S, Set(y))),
                                                       domain=S, condition=NotEquals(x, y)))
all_but_one_membership_folding (conjecture without proof):
In [9]:
all_but_one_nonmembership_unfolding = Forall((S, y), Forall(x, Or(NotInSet(x, S), Equals(x, y)), 
                                                            condition=NotInSet(x, Difference(S, Set(y)))))
all_but_one_nonmembership_unfolding (conjecture without proof):
In [10]:
all_but_one_nonmembership_folding = Forall((S, y), Forall(x, NotInSet(x, Difference(S, Set(y))),
                                                          conditions=Or(NotInSet(x, S), Equals(x, y))))
all_but_one_nonmembership_folding (conjecture without proof):
In [11]:
%end theorems

These theorems may now be imported from the theory package: proveit.logic.sets.subtraction