, interval_set, separate_interval_set и split_interval_set большинство известных математических laws на сетках были успешно проверены через LaBatea. Следующие таблицы давать обзор проверенных законов, заказанных операциями. Если возможно, законы формулируются с более сильным лексикографическим равенством (operator ==) что подразумевает действительность закона для более слабого элемента равенства is_element_equal. На протяжении всей этой главы мы обозначим равенство элементов как =e= вместо этого is_element_equal где короткая нотация выгодна. .

Laws on set union

S() эти законы содержат:

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

Для операцииустановлено пересечение, доступное как<operator&, &=>эти законы были подтверждены:

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

Для заданных различий существуют только эти законы. Он не ассоциативный и не коммутативный. Его нейтралитет несимметричен.

RightNeutrality<S,-,== > : S a;   a-S() == a
Inversion<S,-,== >:        S a;   a - a == S()

В следующей таблице приведены законы, которые используют<+>,<&>и<->в качестве одной операции. Для всех валидированных законов левая и правая стороны уравнений лексикографически равны, как обозначается<==>в ячейках таблицы.

                 +    &   -
Associativity    ==   ==
Neutrality       ==       ==
Commutativity    ==   ==
Inversion                 ==

Distributivity Laws

Законы, такие как дистрибутивность, которые используют более одной операции, иногда могут быть инстанцированы для различных последовательностей операторов. В двух инстанциациях законов распределения заменяются операторы<+>и<&>. Таким образом, мы можем иметь небольшие подписи операторов, такие как<+,&>и<&,+>, чтобы описать такие инстанциации, которые будут использоваться ниже. Не все примеры законов распределения приводят к лексикографическому равенству. Поэтому они обозначаются с помощьюпеременнойравенства<=v=>ниже.

     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)

В следующей таблице показана взаимосвязь между экземплярами права,интервалом, сочетающим стильи используемым соотношением равенства.

                                  +,&    &,+
     Distributivity  joining      ==     ==
                     separating   ==     ==
                     splitting    =e=    =e=
                                  +,-    &,-
RightDistributivity  joining      ==     ==
                     separating   ==     ==
                     splitting    =e=    ==

В таблице представлен обзор 12 инстанциаций четырех законов дистрибутивности и показаны уравнения, для которых эти инстанциации предназначены. Например,<RightDistributivity>с подписью оператора<+,->, созданной для<split_interval_sets>, имеет только равенство элементов (обозначается как<=e=>):

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

Остальные пять инстанциаций<RightDistributivity>действительны и для лексикографического равенства (понижаются до<==>).

Интервалы, сочетающие стили, соответствуют контейнерам в соответствии с

style       set
joining     interval_set
separating  separate_interval_set
splitting   split_interval_set

Наконец, есть два закона, которые объединяют все три основные операции: Закон де Моганса и симметричные различия.

DeMorgan's Law

Закон Де Моргана более известен в инкарнации, где используется операция унарного комплемента<~>.<~(a+b)== ~a*~b>. Приведенная ниже версия является адаптацией для разности бинарных множеств<->, которая также называетсяотносительным дополнением.

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=

Опять же, не все законы справедливы для лексикографического равенства. Вторая инстанциация относится только к равенству элементов, если интервальные множества не соединяются.

Symmetric Difference

SymmetricDifference<S,== > : S a,b,c; (a + b) - (a & b) == (a - b) + (b - a)

Наконец, симметричное различие относится ко всем типам наборов icl и лексикографическому равенству.