ГОСТ Р ИСО 18629-13-2011
(forall (?d
1
?d2)
(implies (and (timeduration ?d1)
(timeduration ?d2))
(timeduration (add ?d1 ?d2))))
7.7.3 Аксиома 3
Функция add является ассоциативной.
(forall (?d1 ?d2 ?d3)
(implies (and (timeduration ?d1)
(timeduration ?d2)
(timeduration ?d3))
(= (add (add ?dl ?d2) ?d3) (add ?dl (add ?d2 ?d3))))
7.7.4 Аксиома 4
Символ константы zero является аддитивной единицей.
(forall (?d)
(implies (timeduration ?d)
(= (add ?dzero) ?d))}
7.7.5 Аксиома 5
Временной интервал, взятый с противоположным знаком, также является
временным интервалом.
(forall (?d1)
(implies (timeduration ?d1)
(exists (?d2)
(and (timeduration ?d2)
(= (add ?d1 ?d2) zero))))
7.7.6 Аксиома 6
Функция add является коммутативной.
(forall (?d1 ?d2)
(implies (and (timeduration ?d1)
(timeduration ?d2))
(= (add ?d1 ?d2) (add ?d2 ?dl))))
7.7.7 Аксиома 7
Результат умножения временного интервала на скалярную величину
также является временным интервалом.
(forall (?d ?r)
(implies (timeduration ?d)
(timeduration (mult ?r ?d))))
7.7.8 Аксиома 8
Временные интервалы могут умножаться на скаляры:
19