(forall (?a)
	(iff	(AtomicProcess ?a)
		(and	(atomic ?a)
			(markov_precond ?a)
			(markov_effects ?a))))

(forall (?a)
	(iff	(CompositeProcess ?a)
		(and	(activity ?a)
			(not (atomic ?a)))))

(forall (?a)
	(iff	(Sequence ?a)
		(and	(uniform ?a)
			(forall (?occ)
				(implies  (occurrence_of ?occ ?a)
					  (and	(simple ?occ)
						(ordered ?occ)
						(strong_poset ?occ)))))))

(forall (?a)
	(iff	(Split ?a)
		(and	(uniform ?a)
			(forall (?occ)
				(implies  (occurrence_of ?occ ?a)
					  (and	(not (simple ?occ))
						(ordered ?occ)
						(strong_poset ?occ)))))))

(forall (?a)
	(iff	(Unordered ?a)
		(and	(uniform ?a)
			(forall (?occ)
				(implies  (occurrence_of ?occ ?a)
					  (and 	(ordered ?occ)
						(permuted ?occ)
					  	(bag ?occ)))))))

(forall (?a)
	(iff	(Choice ?a)
		(and	(uniform ?a)
			(forall (?occ)
				(implies  (occurrence_of ?occ ?a)
					  (and	(simple ?occ)
						(unordered ?occ)
					  	(choice_poset ?occ)))))))

(forall (?a)
	(iff	(IfThenElse ?a)
		(conditional ?a)))

(forall (?a)
	(iff	(RepeatUntil ?a)
		(and	(conditional ?a)
			(forall (?occ)
				(implies  (occurrence_of ?occ ?a)
					  (repetitive ?occ))))))