Extension Name: variation.def
Primitive Lexicon: None
Defined Lexicon:
Relations:
Definitional Extensions Required by this Extension: subtree.def
Grammar: variation.bnf
(forall (?occ1 ?occ2 ?a) (iff (min_equiv ?occ1 ?occ2 ?a) (and (subtree_embed ?occ1 ?occ2 ?a) (subtree_embed ?occ2 ?occ1 ?a))))Definition 2 An activity is uniform iff all of its minimal activity trees are isomorphic.
(forall (?a) (iff (uniform ?a) (forall (?occ1 ?occ2) (if (and (root ?occ1 ?a) (root ?occ2 ?a)) (min_equiv ?occ1 ?occ2 ?a)))))Definition 3 An activity ?a is variegated iff all of its minimal activity trees whose root occurrences are occurrence-equivalent are also isomorphic.
(forall (?a) (iff (variegated ?a) (and (exists (?a1) (forall (?occ1 ?occ2) (if (and (occurrence_of ?occ1 ?a1) (occurrence_of ?occ2 ?a1) (root ?occ1 ?a) (root ?occ2 ?a)) (min_equiv ?occ1 ?occ2 ?a)))) (exists (?a2 ?occ3 ?occ4) (and (occurrence_of ?occ3 ?a2) (occurrence_of ?occ4 ?a2) (root ?occ3 ?a) (root ?occ4 ?a) (not (min_equiv ?occ3 ?occ4 ?a)))))))Definition 4 An activity is multiform iff there exist nonisomorphic activity trees whose root occurrences are occurrence equivalent.
(forall (?a) (iff (multiform ?a) (forall (?a1 ?occ1) (if (and (root ?occ1 ?a) (occurrence_of ?occ1 ?a1)) (exists (?occ2 ?occ3) (and (occurrence_of ?occ2 ?a1) (occurrence_of ?occ3 ?a1) (root ?occ2 ?a) (root ?occ3 ?a) (not (min_equiv ?occ2 ?occ3 ?a))))))))