Extension Name: ordered.def
Primitive Lexicon: None
Defined Lexicon:
Relations:
Definitional Extensions Required by this Extension: None
Grammar: ordered.bnf
(forall (?s1 ?s2 ?a) (iff (mono_tree ?s1 ?s2 ?a) (forall (?s3 ?s4 ?s5) (if (and (min_precedes ?s1 ?s3 ?a) (min_precedes ?s2 ?s4 ?a) (mono ?s3 ?s4 ?a) (min_precedes ?s3 ?s5 ?a)) (exists (?s6) (and (mono ?s5 ?s6 ?a) (min_precedes ?s4 ?s6 ?a)))))))Definition 2 This relation holds iff there exists an order automorphism that maps the subtree rooted in ?s1 to the subtree rooted in ?s2.
(forall (?s1 ?s2 ?a) (iff (order_tree ?s1 ?s2 ?a) (and (mono_tree ?s1 ?s2 ?a) (forall (?s3 ?s4 ?s5 ?s6) (if (and (min_precedes ?s1 ?s3 ?a) (min_precedes ?s2 ?s4 ?a) (cousin ?s3 ?s4 ?a) (min_precedes ?s3 ?s5 ?a) (cousin ?s5 ?s6 ?a)) (iff (iso_occ ?s3 ?s5 ?a) (iso_occ ?s4 ?s6 ?a)))))))Definition 3 Two activity occurrences are root automorphic iff there exist atomic subactivity occurrences of each activity occurrence that are the roots of isomorphic subtrees.
(forall (?occ1 ?occ2) (iff (root_automorphic ?occ1 ?occ2) (exists (?a ?s1 ?s2) (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (subactivity_occurrence ?s1 ?occ1) (subactivity_occurrence ?s2 ?occ2) (order_tree ?s1 ?s2 ?a) (order_tree ?s2 ?s1 ?a)))))Definition 4 An activity occurrence is ordered iff it is root automorphic with every other activity occurrence in the same tree.
(forall (?occ1) (iff (ordered ?occ1) (forall (?occ2) (if (same_grove ?occ1 ?occ2) (root_automorphic ?occ1 ?occ2)))))Definition 5 An activity occurrence is nondeterministically ordered iff each activity occurrence in the same tree is root automorphic to some other activity occurrence in the same tree.
(forall (?occ1) (iff (nondet_ordered ?occ1) (forall (?occ2) (if (same_grove ?occ1 ?occ2) (exists (?occ3) (and (same_grove ?occ1 ?occ3) (not (= ?occ3 ?occ2)) (root_automorphic ?occ2 ?occ3)))))))Definition 6 An activity is broken ordered iff there exist activity occurrences in the same tree that are root automorphic to some other activity occurrences in the same tree, and there also exist activity occurrences in same tree that are not root automorphic to any other activity occurrence.
(forall (?occ1) (iff (broken_ordered ?occ1) (exists (?occ2) (and (same_grove ?occ1 ?occ2) (not (= ?occ1 ?occ2)) (root_automorphic ?occ1 ?occ2) (forall (?occ3) (if (and (same_grove ?occ3 ?occ1) (not (= ?occ3 ?occ2))) (not (root_automorphic ?occ3 ?occ2))))))))Definition 7 An activity occurrence is unordered iff none of the activity occurrences in the same tree are root automorphic.
(forall (?occ1) (iff (unordered ?occ1) (forall (?occ2) (if (and (same_grove ?occ1 ?occ2) (not (= ?occ1 ?occ2))) (not (root_automorphic ?occ1 ?occ2))))))