ГОСТ Р ИСО 18629-13-2011
(and (occurrence_of ?s2 ?а)
(legal ?s2)
(endjso ?s1 ?s2 ?s3 ?s4))))))))
8.5.3 Определение 3
Допустимый автоморфизм дерева элементов сохраняет допустимые
элементы ?а1 и отображает элемент ?s1 в ?s2, а также сохраняет дерево
операций для ?а2.
(forall (?а1 ?а2 ?s1 ?s2) (iff (tree_map ?s1 ?s2 ?a1 ?a2)
(and (legal_map ?s1 ?s2 ?a1)
(forall (?s3 ?s4)
(implies (min_precedes ?s3 ?s4 ?a)
(exists (?s5 ?s6)
(and (min_precedes ?s5 ?s6 ?a2)
(endjso ?s3 ?s5 ?sl ?s2)
(endjso ?s4?s6 ?s1 ?s2))))))))
8.6 Аксиомы теории автоморфизма дерева элементов
Ниже приведен полный набор аксиом для теории автоморфизма дерева
элементов.
8.6.1 Аксиома 1
Если ?а2 является убиквитарной операцией для операции ?а1, то
элементы субоперации на дереве операций для операции ?а2 сохраняются с
помощью автоморфизмов дерева элементов, которое сохраняет допустимые
элементы операции ?а1.
(forall (?а1 ?а2 ?s1 ?s2)
(implies (and (ubiquitous ?a1 ?a2)
(min_precedes ?s1 ?s2?a2))
(exists (?s3 ?s4 ?s5 ?s6)
(and (tree_equiv ?s1 ?s2)
(tree_equiv ?s3 ?s4)
(occurrence ?s5 ?a1)
(occurrence ?s6 ?a1)
(legal_equiv ?s5 ?s6)
(endjso ?s3 ?s4 ?s5 ?s6)))))
8.6.2 Аксиома 2
Если ?a2 является убиквитарной операцией для операции ?а1, то любые
автоморфизмы дерева элементов, которые сохраняют элементы субоперации
на дереве операций для операции ?а2, также сохраняют допустимые элементы
операции ?а1.
26