ГОСТ Р ИСО 18629-13-2011
(forall (?d1 ?d2 ?r)
(= (mult ?r (add ?d1 ?d2)) (add (mult ?r ?d1) (mult ?r ?d2))))
7.7.9 Аксиома 9
Операцияумножения временных интервалов на скаляры является
дистрибутивной:
(forall (?d ?r ?s)
(= (mult (add ?r ?s) ?d) (add (mult ?r ?d) (mult ?s ?d))))
7.7.10 Аксиома 10
Операцияумножения временных интервалов на скаляры является
ассоциативной:
(forall (?d ?r ?s)
(= (mult (mult ?r ?s) ?d) (mult ?r (mult ?s ?d))))
7.7.11 Аксиома 11
Символ константы one является мультипликативной единицей,
(forall (?d)
(= ?d (mult one ?d)))
7.7.12 Аксиома 12
Функцияaddнавременныхинтервалахсохраняетструктуру
упорядочения lesser.
(forall (?d1 ?d2 ?d3)
(and (timeduration ?dl)
(timeduration ?d2)
(timeduration ?d3))
(iff (lesser ?d1 ?d2)
(lesser (add ?d1 ?d3) (add ?d2 ?d3))))
7.7.13 Аксиома 13
Если два временных интервала равны, то результат их сложения также
будет тем же.
(forall (?d1 ?у ?z)
(and (timeduration ?d1)
(timeduration ?d2)
(timeduration ?d3))
(iff (= ?d1 ?d2)
(=(add ?d1 ?d3) (add ?d2 ?d3)))))
7.7.14 Аксиома 14
20