Classes of Iterated Occurrences

Classes of Iterated Occurrences

Extension Name: iterate.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

Theories Required by this Extension: ioo.th,act_occ.th, complex.th, atomic.th, subactivity.th, occtree.th, psl_core.th

Definitional Extensions Required by this Extension: repetitive.def

Definitions

Definition 1 An activity occurrence is a leaf of an iterated occurrence ordering for an activity ?a if and only if it is an element of the ordering and there does not exist an activity occurrence that follows it in the ordering. 
(forall (?occ ?a) (iff (leaf_rep ?occ ?a) 
(and	(exists (?occ1)
		(rep_precedes ?occ1 ?occ ?a))
	(not (exists (?occ2)
		(rep_precedes ?occ ?occ2 ?a))))))
Definition 2 Two activity occurrences in the same activity tree are rep_equiv iff they agree that their leaf occurrences are also leaf occurrences of an iterated occurrence ordering. 
(forall (?occ1 ?occ2) (iff (rep_equiv ?occ1 ?occ2) 
(forall (?s1 ?s2 ?a)
	(if	  (and	(leaf_occ ?s1 ?occ1)
			(leaf_occ ?s2 ?occ2)
			(same_grove ?occ1 ?occ2)
			(occurrence_of ?occ1 ?a))
		  (iff	(leaf_rep ?s1 ?a)
			(leaf_rep ?s2 ?a))))))
Definition 3 An activity occurrence is iterated iff the leaf occurrences of all other activity occurrences in the same activity tree are also leaf occurrences of an iterated occurrence ordering. 
(forall (?occ) (iff (iterated ?occ) 
(forall (?occ1)
	(if	  (same_grove ?occ ?occ1)
		  (rep_equiv ?occ ?occ1)))))
Definition 4 An activity occurrence is partial iterated iff activity occurrences in the same tree are rep_equiv iff their leaf occurrences are occurrence-isomorphic. 
(forall (?occ) (iff (partial_iterated ?occ) 
(forall (?occ1 ?occ2)
	(if	  (and	(same_grove ?occ ?occ1)
			(same_grove ?occ ?occ2))
		  (iff	(rep_equiv ?occ ?occ1)
			(exists (?s1 ?s2)
				(and	(leaf_occ ?s1 ?occ1)
					(leaf_occ ?s2 ?occ2)
					(iso_occ ?s1 ?s2))))))))
Definition 5 An activity occurrence is nondet iterated iff for activity occurrence in the same tree there exists another activity occurrence that has an occurrence-isomorphic leaf but which disagrees on whether or not that leaf is the leaf occurrence of an iterated occurrence ordering. 
(forall (?occ) (iff (nondet_iterated ?occ) 
(forall (?occ1 ?s1)
	(if	  (and	(same_grove ?occ ?occ1)
			(leaf_occ ?s1 ?occ1))
		  (exists (?occ2 ?s2)
			(and	(leaf_occ ?s2 ?occ2)
				(same_grove ?occ1 ?occ2)
				(iso_occ ?s1 ?s2)
				(not (rep_equiv ?occ ?occ1))))))))