Extension Name: subtree.def
Primitive Lexicon: None
Defined Lexicon:
Relations:
Definitional Extensions Required by this Extension: None
Grammar: subtree.bnf
(forall (?s1 ?s2 ?a) (iff (subtree_embed ?s1 ?s2 ?a) (forall (?s3) (if (min_precedes ?s1 ?s3 ?a) (exists (?s4) (and (min_precedes ?s2 ?s4 ?a) (iso_occ ?s4 ?s3 ?a)))))))Definition 2 An activity is multiple outcome iff any two activity trees can be embedded into one another.
(forall (?a) (iff (multiple_outcome ?a) (forall (?s1 ?s2) (if (and (root ?s1 ?a) (root ?s2 ?a)) (or (subtree_embed ?s1 ?s2 ?a) (subtree_embed ?s2 ?s1 ?a))))))Definition 3 An activity ?a is weak outcome iff there exists a minimal activity tree that can be embedded into all other minimal activity trees of ?a.
(forall (?a) (iff (weak_outcome ?a) (exists (?s1) (and (root ?s1 ?a) (forall (?s2) (if (root ?s2 ?a) (subtree_embed ?s2 ?s1 ?a)))))))Definition 4 An activity ?a has a nondeterministic outcome iff there exists a minimal activity tree that can be embedded into other minimal activity trees of ?a, and there also exists branches that cannot be embedded.
(forall (?a) (iff (nondet_outcome ?a) (exists (?s1 ?s2 ?s3) (and (root ?s1 ?a) (root ?s2 ?a) (subtree_embed ?s2 ?s1 ?a) (root ?s3 ?a) (forall (?s4) (if (root ?s4 ?a) (not (or (subtree_embed ?s3 ?s4 ?a) (subtree_embed ?s4 ?s3 ?a)))))))))Definition 5 An activity is imiscible iff no tree in the spectrum can be embedded into any other.
(forall (?a) (iff (imiscible ?a) (forall (?s1 ?s2) (if (and (root ?s1 ?a) (root ?s2 ?a)) (not (or (subtree_embed ?s1 ?s2 ?a) (subtree_embed ?s2 ?s1 ?a)))))))