ГОСТ Р ИСО 18629-13-2011
тогда и только тогда, когдаэлемент ?s1 предшествует элементу ?s2 при
упорядочении, а между этими элементами при упорядочении отсутствует какой-
либо элемент субоперации.
(forall (?sl ?s2 ?а) (iff (next_soo ?sl ?s2 ?a)
(and (soo_precedes ?s1 ?s2 ?a)
(not (exists (?s3)
(and (soo_precedes ?sl ?s3 ?a)
(soo_precedes ?s3?s2?a)))))))
6.6 Аксиомы теории упорядочения элементов субопераций
6.6.1 Аксиома 1
Примитивный символ отношения soo„precedes упорядочивает элементы
субопераций.
(forall (?s1 ?s2 ?а)
(implies (soo_precedes ?sl ?s2 ?a)
(and (soo ?s1 ?a)
(soo ?s2 ?a))))
6.6.2 Аксиома 2
Элементы упорядочения элементов субоперации являются элементами
дерева операций.
(forall (?а ?s)
(implies (soo ?s ?a)
(or (root ?s?a)
(exists (?s1)
(min_precedes ?sl ?s ?a)))))
6.6.3 Аксиома 3
Примитивная функция отношения soomap отображает дерево операций
на упорядоченную структуру элементов субопераций.
(forall (?s ?а)
(soo (soomap ?s) ?a))
6.6.4 Аксиома 4
Элементыупорядоченнойструктурыэлементовсубопераций
фиксируются с помощью примитивной функции отношения soomap.
(forall (?s ?а)
(implies (soo ?s ?a)
(=?s (soomap ?s))))
6.6.5 Аксиома 5
13