For all set types S that are models concept Set (std::set , interval_set, separate_interval_set and split_interval_set) 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 (operator ==) which implies the law's validity for the weaker element equality is_element_equal. Throughout this chapter we will denote element equality as =e= instead of is_element_equal where a short notation is advantageous.

Laws on set union

For the operation set union available as operator +, +=, |, |= and the neutral element identity_element<S>::value() 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

Laws on set intersection

For the operation set intersection available as operator &, &= 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

Laws on set difference

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 +, & and - 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                 ==

Distributivity Laws

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 + and & are swapped. So we can have small operator signatures like +,& and &,+ 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 =v= below.

     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 RightDistributivity with operator signature +,- instantiated for split_interval_sets holds only for element equality (denoted as =e=):

RightDistributivity<S,+,-,=e= > : S a,b,c; (a + b) - c =e= (a - c) + (b - c)

The remaining five instantiations of RightDistributivity are valid for lexicographical equality (demoted as ==) as well.

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.

DeMorgan's Law

De Morgans Law is better known in an incarnation where the unary complement operation ~ is used. ~(a+b) == ~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.

Symmetric Difference

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.