Extension Name: atomic.th
Primitive Lexicon:
Relations:
Theories Required by this Extension: occtree.th,subactivity.th, psl_core.th
Definitional Extensions Required by this Extension: None
(forall (?a) (if (primitive ?a) (atomic ?a)))Axiom 2 The function conc is idempotent.
(forall (?a) (= ?a (conc ?a ?a)))Axiom 3 The function conc is commutative.
(forall (?a1 ?a2) (= (conc ?a1 ?a2) (conc ?a2 ?a1)))Axiom 4 The function conc is associative.
(forall (?a1 ?a2 ?a3) (= (conc ?a1 (conc ?a2 ?a3)) (conc (conc ?a1 ?a2) ?a3)))Axiom 5 The concurrent aggregation of atomic action is an atomic action.
(forall (?a1 ?a2) (iff (atomic (conc ?a1 ?a2)) (and (atomic ?a1) (atomic ?a2))))Axiom 6 An atomic activity ?a1 is a subactivity of an atomic activity ?a2 if and only if ?a2 is an idempotent for ?a1.
(forall (?a1 ?a2) (if (and (atomic ?a1) (atomic ?a2)) (iff (subactivity ?a1 ?a2) (= ?a2 (conc ?a1 ?a2)))))Axiom 7 An atomic action has a proper subactivity if and only if there exists another atomic activity which can be concurrently aggregated.
(forall (?a1 ?a2) (if (and (atomic ?a2) (subactivity ?a1 ?a2) (not (= ?a1 ?a2))) (exists (?a3) (and (atomic ?a3) (= ?a2 (conc ?a1 ?a3)) (not (exists (?a4) (and (atomic ?a4) (subactivity ?a4 ?a1) (subactivity ?a4 ?a3))))))))Axiom 8 The semilattice of atomic activities is distributive.
(forall (?a ?b0 ?b1) (if (and (atomic ?a) (atomic ?b0) (atomic ?b1) (subactivity ?a (conc ?b0 ?b1)) (not (primitive ?a))) (exists (?a0 ?a1) (and (subactivity ?a0 ?a) (subactivity ?a1 ?a) (= ?a (conc ?a0 ?a1))))))Axiom 9 Only atomic activities can be generator activities. Equivalently, only occurrences of atomic activities can be elements of an occurrence tree.
(forall (?a) (if (generator ?a) (atomic ?a)))Axiom 10 Atomic activities are activities.
(forall (?a) (if (atomic ?a) (activity ?a)))