Compacted Activity Axioms

Grammar Name: compacted.bnf

Extension Name: compacted.def

Grammars required by Process Descriptions: folded.bnf, permute.bnf

Process Descriptions

(compacted ?a)

< compacted_spec > ::=	
(forall (< variable >)
	(if	  (occurrence < variable > < term >)
		  (exists (< variable >)
			(and	(occurrence < variable > < term >)
			  	< occurrence_axiom >)))))

(nondet_compacted ?a)

< nondet_compacted_spec > ::=  
(forall (< variable >)
	(if	  (occurrence < variable > < term >)
		  (exists (< variable >)
			(and	(occurrence < variable > < term >)
			  	(or < occurrence_axiom >*))))))

(partial_compacted ?a)

< partial_compacted_spec > ::=	(or  < nondet_compacted_spec >
				     < stiff_spec >)

(stiff ?a)

< stiff_spec > ::=	(exists (< variable >*) 
				(and	< occurrence_formula > 
					< branch_spec >))