For all set types
are models concept
most of the well known mathematical laws
on sets were successfully checked via LaBatea. The next tables are
giving an overview over the checked laws ordered by operations. If possible,
the laws are formulated with the stronger lexicographical equality (
which implies the law's validity for the weaker element equality
is_element_equal. Throughout this chapter
we will denote element equality as
a short notation is advantageous.
For the operation set union
+=, |, |= and the neutral element
which is the empty set
S() these laws hold:
Associativity<S,+,== >: S a,b,c; a+(b+c) == (a+b)+c Neutrality<S,+,== > : S a; a+S() == a Commutativity<S,+,== >: S a,b; a+b == b+a
For the operation set intersection
&= these laws were validated:
Associativity<S,&,== >: S a,b,c; a&(b&c) == (a&b)&c Commutativity<S,&,== >: S a,b; a&b == b&a
For set difference there are only these laws. It is not associative and not commutative. It's neutrality is non symmetrical.
RightNeutrality<S,-,== > : S a; a-S() == a Inversion<S,-,== >: S a; a - a == S()
Summarized in the next table are laws that use
as a single operation. For all validated laws, the left and right hand sides
of the equations are lexicographically equal, as denoted by
== in the cells of the table.
+ & - Associativity == == Neutrality == == Commutativity == == Inversion ==
Laws, like distributivity, that use more than one operation can sometimes
be instantiated for different sequences of operators as can be seen below.
In the two instantiations of the distributivity laws operators
are swapped. So we can have small operator signatures like
to describe such instantiations, which will be used below. Not all instances
of distributivity laws hold for lexicographical equality. Therefore they
are denoted using a variable equality
Distributivity<S,+,&,=v= > : S a,b,c; a + (b & c) =v= (a + b) & (a + c) Distributivity<S,&,+,=v= > : S a,b,c; a & (b + c) =v= (a & b) + (a & c) RightDistributivity<S,+,-,=v= > : S a,b,c; (a + b) - c =v= (a - c) + (b - c) RightDistributivity<S,&,-,=v= > : S a,b,c; (a & b) - c =v= (a - c) & (b - c)
The next table shows the relationship between law instances, interval combining style and the used equality relation.
+,& &,+ Distributivity joining == == separating == == splitting =e= =e= +,- &,- RightDistributivity joining == == separating == == splitting =e= ==
The table gives an overview over 12 instantiations of the four distributivity
laws and shows the equalities which the instantiations holds for. For instance
holds only for element equality (denoted as
RightDistributivity<S,+,-,=e= > : S a,b,c; (a + b) - c =e= (a - c) + (b - c)
The remaining five instantiations of
are valid for lexicographical equality (demoted as
Interval combining styles correspond to containers according to
style set joining interval_set separating separate_interval_set splitting split_interval_set
Finally there are two laws that combine all three major set operations: De Mogans Law and Symmetric Difference.
De Morgans Law is better known in an incarnation where the unary complement
~ is used.
~a * ~b.
The version below is an adaption for the binary set difference
-, which is also called relative complement.
DeMorgan<S,+,&,=v= > : S a,b,c; a - (b + c) =v= (a - b) & (a - c) DeMorgan<S,&,+,=v= > : S a,b,c; a - (b & c) =v= (a - b) + (a - c)
+,& &,+ DeMorgan joining == == separating == =e= splitting == =e=
Again not all law instances are valid for lexicographical equality. The second instantiations only holds for element equality, if the interval sets are non joining.
SymmetricDifference<S,== > : S a,b,c; (a + b) - (a & b) == (a - b) + (b - a)
Finally Symmetric Difference holds for all of icl set types and lexicographical equality.