Extension Name: permute.def
Primitive Lexicon: None
Defined Lexicon:
Relations:
Definitional Extensions Required by this Extension: None
Grammar: permute.bnf
(forall (?occ1 ?occ2) (iff (branch_monomorphic ?occ1 ?occ2) (forall (?s1 ?a) (if (and (occurrence_of ?occ1 ?a) (subactivity_occurrence ?s1 ?occ1)) (exists (?s2) (and (subactivity_occurrence ?s2 ?occ2) (mono ?s1 ?s2 ?a)))))))Definition 2 Two branches of a minimal activity tree are branch-automorphic iff the set of atomic activity occurrences on one branch is a permutation of the the set of atomic activity occurrences on the other branch.
(forall (?occ1 ?occ2) (iff (branch_automorphic ?occ1 ?occ2) (and (branch_monomorphic ?occ1 ?occ2) (branch_monomorphic ?occ2 ?occ1))))Definition 3 An activity occurrences is permuted iff the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on every other branch.
(forall (?occ) (iff (permuted ?occ) (forall (?occ1 ?occ2) (if (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ)) (branch_automorphic ?occ1 ?occ)))))Definition 4 An activity occurrence is nondeterministically permuted iff the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on some other branch.
(forall (?occ) (iff (nondet_permuted ?occ) (forall (?occ1) (if (same_grove ?occ1 ?occ) (exists (?occ2) (and (same_grove ?occ1 ?occ2) (not (= ?occ1 ?occ2)) (branch_automorphic ?occ1 ?occ2)))))))Definition 5 An activity occurrence is partially permuted iff there exists a branch such that the set of atomic subactivity occurrences is a permutation of the atomic subactivity occurrences on some other branch, and there exists a branch that is not a permutation of any other branch.
(forall (?occ) (iff (partial_permuted ?occ) (exists (?occ1 ?occ2 ?occ3) (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ) (not (= ?occ1 ?occ2)) (branch_automorphic ?occ1 ?occ2) (same_grove ?occ3 ?occ) (forall (?occ4) (if (and (same_grove ?occ3 ?occ4) (branch_automorphic ?occ3 ?occ4)) (= ?occ3 ?occ4)))))))Definition 6 An activity occurrence is simple iff none of the branches in an activity tree are branch automorphic.
(forall (?occ) (iff (simple ?occ) (forall (?occ1 ?occ2) (if (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ) (branch_automorphic ?occ1 ?occ2)) (= ?occ1 ?occ2)))))