ГОСТ Р ИСО 18629-13-2011
(forall (?а1 ?а2 ?s ?s1)
(implies (and (envelope ?al ?a2 ?s)
(live_branch ?s1 ?s ?a2))
(live_branch ?s1 ?s ?a1)))
9.6.6 Аксиома 6
Любая неактивная часть операции является активной «теневой» частью.
(forall (?а1 ?а2 ?s ?s1)
(implies (and (umbra ?al ?a2 ?s)
(dead_branch ?s1 ?s ?a2))
(live_branch ?s1 ?s ?al)))
9.6.7 Аксиома 7
Оболочка для операции ?а1 является неограниченной в активных
областях для операции ?а1.
(forall (?а1 ?а2 ?s ?о)
(implies (and (envelope ?а1 ?a2 ?s)
(occurrence ?o ?a1)
(root_occ ?s ?o))
(unconstrained ?o)))
9.6.8 Аксиома 8
«Теневая» область для операции ?а1 является неограниченной в
неактивных областях для операции ?а1.
(forall (?а1 ?а2 ?s ?о)
(implies (and (umbra ?а
1
?a2 ?s)
(occurrence ?o ?al)
(root_occ ?s ?o))
(unconstrained ?o)))
30