ГОСТ Р ИСО 18629-13-2011
7.7.19 Аксиома 19
Значение функции продолжительности операции между временными
точками ?П и ?t2 является аддитивной инверсией этой функции между
временными точками ?t2 и ?П.
(forall (?П ?t2)
(implies (and (timepoint ?t1)
(timepoint ?t2))
(=zero (add (duration ?t1 ?t2) (duration ?t2 ?t1)))))
7.7.20 Аксиома 20
Для заданной временной точки ?t1, отличной от inf- или inf+,
продолжительность операции между временной точкой ?П и любой другой
временной точкой является однозначно определяемой.
(forall (?t1 ?t2 ?t3)
(implies (and (timepoint ?t1)
(timepoint ?t2)
(timepoint ?t3)
(not (= ?t1 inf-))
(not (= ?t2 inf+))
(=(duration ?t1 ?t2) (duration ?t1 ?t3)))
(=?t3 ?t2)))
7.7.21 Аксиома 21
Продолжительность операции от любой точки, отличной от inf- до inf-,
является константой max-, а продолжительность операции от любой точки,
отличной от inf-*-, до inf+ является константой тах+.
(forall (?t)
(and (implies (and(timepoint ?t)
(not (= ?t inf-)))
(=max+ (duration inf- ?t)))
(implies (and (timepoint ?t)
(not (= ?t inf-*-)))
(= max- (duration inf-*- ?t)))
7.7.22 Аксиома 22
Продолжительность операции от inf- до любой точки, отличной от inf-,
является константой тах+ , а продолжительность операции от inf-*- до любой
точки, отличной от inf+, является константой max-.
(forall (?t)
(and (implies (and(timepoint ?t)
(not (= ?t inf-)))
(= max- (duration ?t inf-)))
(implies (and (timepoint ?t)
(not (= ?t inf+)))
22