# 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