ГОСТ Р ИСО 18629-14—2011
8.7.2 Аксиома 2
Сумма любых двух аддитивных элементов также является аддитивным элементом.
(foraII (?q1 ?q2)
(implies (and (additive ?q1)
(additive ?q2))
(additive <quantity_plus ?q1 ?q2))))
8.7.3 Аксиома 3
Функция quantity_pJus является ассоциативной.
(foraII (?q1 ?q2 ?q3)
(implies (and (additive ?q1)
(additive ?q2)
(additive ?q3))
(= (quantity_plus (?q1 ?q2) ?q3) (quantity_plus (quantity_plus (?q1 ?q2) ?q3)))
8.7.4 Аксиома 4
Zero_quantity является единичным элементом.
((oral! (?q>
(Implies (additive ?q)
(= ?q (quantity_plus ?q zero_quantity)))
8.7.5 Аксиома 5
Для любого аддитивного элемента существует его аддитивная инверсия.
(foraII (?q>
(implies (additive ?q)
(exists (?p)
(= zero_quantlty (quantity_plus ?q ?p)}»)
8.7.6 Аксиома 6
Функция quantity_plus является коммутативной.
(forall (?q1 ?q2)
(implies (and (additive ?q1)
(additive ?q2))
(» (quantity_plus ?q1 ?q2) (quantity_plus ?q2 ?q1)))
8.7.7 Аксиома 7
Если количество ?q1 превышает количество ?q2. то прибавление к ним любого количества будет
сохранять их упорядочение.
(forall (?q1 ?q2 ?q3)
(implies (and (additive ?q1)
(additive ?q2)
(additive ?q3))
(iff (greater ?q1 ?q2)
(greater (quantity_plus ?q1 ?q3) (quantity_plus ?q2 ?q3))))
8.7.8 Аксиома 8
Если количество ?q1 равно количеству ?q2. то прибавление к ним любого количества будет сохра
нять их равенство.
(forall (?q1 ?q2 ?q3)
(■лplies (and
(additive ?q1)
(additive ?q2)
(additive ?q3))
(Iff <= ?q1 ?q2)
(* (quantity_plus ?q1 ?q3) (quantlty_plus ?q2 ?q3)>))>
8.7.9 Аксиома 9
Отношение упорядочения, большее по аддитивным элементам, является транзитивным.
ю