Repetitive Activity Axioms

Grammar Name: repetitive.bnf

Extension Name: repetitive.def

Grammars required by Process Descriptions: None

Process Descriptions

(repetitive ?occ)

< repetitive_spec > ::=	(forall (< term > ?s1 ?s2)
				(iff	(do < term > ?s1 ?s2)
					< rep_formula >))

(nondet_repetitive ?occ)

< nondet_rep_spec > ::=	(forall (< term > ?s1 ?s2)
				(iff	(do < term > ?s1 ?s2)
					(or	< rep_formula >*)))

(partial_repetitive ?occ)

< partial_rep_spec > ::= (forall (< term > ?s1 ?s2)
                                (iff    (do < term > ?s1 ?s2)
					< partial_rep_formula >

Auxiliary Rules

< rep_formula > ::=  (exists (< term >)
			(and	(subactivity < term > < term >)
				(forall (?s3)
				   (if	 (do < term > ?s1 ?s3)
					    (or  (= ?s2 ?s3)
						 (do < term > ?s3 ?s2))))))

< partial_rep_formula > ::=  (exists (< term > ?s3)
				(and	(subactivity < term > < term >)
				   	(do < term > ?s1 ?s3)
					(or	(= ?s2 ?s3)
					 	(do < term > ?s3 ?s2))))