ГОСТ Р ИСО 18629-12—2010
7.5.3 Аксиома 3
Отношение earlier является транзитивным для множества случаев:
(forall (?осс1 ?осс2 ?оссЗ)
(implies (and (earlier ?осс 1?осс2)
(earlier ?осс2 ?оссЗ))
(earlier ?осс1 ?оссЗ)))
7.5.4Аксиома 4
Ветвь дерева случаев представляет собой полностью упорядоченное множество случаевдеятель
ности:
(forall (?осс1 ?осс2 ?оссЗ)
(implies (and (earlier ?осс 1?осс2)
(earlier ?оссЗ ?осс2)
(or (earlier ?осс1 ?оссЗ)
(earlier ?оссЗ ?осс1)
(= ?оссЗ ?осс1))))
7.5.5Аксиома 5
Ни один случай не может произойти раньше начального случая:
(forall (?осс1 ?осс2)
(implies (initial ?ocd)
(not (exists (?осс2)
(earlier ?осс2 ?осс1)))))
7.5.6Аксиома 6
Каждая ветвь дерева случаев имеет начальный случай:
(forall (?осс1 ?осс2)
(implies(earlier ?осс1 ?осс2)
(exists (?осср)
(and (initial ?осср)
(or (earlier ?осср ?ocd)
(=?осср?осс1))))))
7.5.7 Аксиома 7
Каждаядеятельность имеет начальный случай:
(forall (?а)
(implies (activity ?а)
(exists (?s)
(and (occurrence_of ?s ?a)
(initial ?s)))))
7.5.8 Аксиома 8
Два начальныхслучая деятельности дерева случаев неявляются случаями одной итой же деятель
ности:
(forall (?осс1 ?осс2 ?а)
(implies (and (initial ?осс1)
(initial ?осс2)
(occurrence_of ?осс1 ?а)
(occunrence_of ?осс2 ?а))
(= ?осс1 ?осс2)))
7.5.9 Аксиома 9
Элемент случаядеятельности, представляющий случай деятельности:
(forall (?а ?осс)
(implies (and (activity_occurrence ?осс)
(activity ?а))
(occurrence_of (successor ?a ?occ) ?a))))
7.5.10 Аксиома 10
Каждый случай, не являющийся начальным, представляет собой следующий элемент другого
случая:
Ю