ГОСТР ИСО 18629-43—2011
3
(forall (?s1 ?s2 ?а) (iff(snapshot ?s1 ?s2 ?a)
(and (iso
_
occ ?s1 ?s2)
(soo ?s2 ?a)
(implies (root
_
soo ?s2 ?a)
(root ?s1 ?a))
(forall (?s3)
(implies (soo
_
precedes ?s3 ?s2 ?a)
(exists (?s4)
(and (mm
_
precedes ?s4 ?s1 ?a)
(or(mono ?s3 ?s4 ?a)
(=?s ?s
4
)))))))))
6.5.3 rotate
На дереве дойствий для ?a. содержащем ?s, множество последующих событий является копией
множества вершин дерева для ?s. имеющихобщего родителя.
(forall (?s ?а) (iff(rotate ?s?a)
(and (forall (?s1)
(implies (next
_
subocc ?s ?s1 ?a)
(exists (?s2)
(and (sibling ?s ?s2 ?a)
(iso
_
occ ?s1 ?s2)))))
(forall (?s3)
(implies (sibling ?s ?s3 ?a)
(same
_
bag ?s?s3 ?a))))))
6.5.4 reflect
На дереве действий для ?a. содержащем ?s. множество последующих событий является копией
множества последующихэлементов ?sупорядочивания событий.
(forall (?s ?а) (iff(reflect ?s ?a)
(forall (?s1)
(iff (next
_
subocc ?s ?s1 ?a)
(exists (?s2 ?s3)
(and (next
_
soo ?s2 ?s3?a)
(snapshot ?s ?s2 ?a)
(iso
_
occ ?s1 ?s3)))))))
6.5.5 flip
На дереве действий для ?a. содержащем ?s. множество последующих событий является копией
множества последующихэлементов ?s упорядочивания событий вместе с копией вершин дерева для ?s
(имеющихобщего родителя).
(forall (?s ?а) (iff(flip ?s ?a)
(forall (?s1)
(iff(next
_
subocc ?s ?s1 ?a)
(or (exists (?s2 ?s3)
(and (snapshot ?s ?s2 ?a)
(next
_
soo ?s2 ?s3 ?a)
(iso
_
occ?s1 ?s3)))
(exists (?s2)
(and (sibling ?s?s2 ?a)
(iso
_
occ?s1 ?s2))))))))
6.5.6 turn
На дереве действий для ?a, содержащем ?s, множество последующих событий является копией
множества последующих элементов ?s упорядочивания событий вместе с копией вершин дерева для ?s
(имеющихобщего родителя), удовлетворяющих условию «same
_
bag».
(forall (?s ?а) (iff(turn ?s ?a)
(and (exists (?s5)
(and (sibling ?s5 ?a)
(same
_
bag ?s ?s5 ?a)))
6