Branchwise Permuted Activity Axioms

Grammar Name: branchwise.bnf

Extension Name: branchwise.def

Grammars required by Process Descriptions: permute.bnf

Process Descriptions

(reordered ?a)

< reordered_spec > ::=	(forall (< variable >)
				(if	  (occurrence < variable > < term >)
					  < occurrence_sentence >))

(nondet_reordered ?a)

< nondet_reordered_spec > ::=  (forall (< variable >*) 
				  (if	  (occurrence < variable > < term >)
					    (or < occurrence_sentence >*)))

(partial_reordered ?a)

< partial_reordered_spec > ::=	(or  < nondet_reordered_spec >
				     < nonorderable_spec >)

(nonorderable ?a)

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