Permuted Activity Axioms

Grammar Name: permute.bnf

Extension Name: permute.def

Grammars required by Process Descriptions: None

Process Descriptions

(permuted ?occ)

< permuted_spec > ::=	(forall (< variable >)
				(if	  (same_tree < variable > ?occ)
					  < occurrence_sentence >))

(nondet_permuted ?occ)

< nondet_permuted_spec > ::=  (forall (< variable >*) 
				  (if	  (same_tree < variable > ?occ)
					    (or < occurrence_sentence >*)))

(partial_permuted ?occ)

< partial_permuted_spec > ::=	(or  < nondet_permuted_spec >
				     < simple_spec >)

(simple ?occ)

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

Auxiliary Rules

< occurrence_literal > ::=	(occurrence < variable > < term >)
				(subactivity_occurrence < variable > < variable >)

< occurrence_formula > ::=	< occurrence_literal > |
				(and < occurrence_literal >*)

< occurrence_sentence > ::= 	(exists (< variable >*) 
				  	< occurrence_formula >)

< branch_spec > ::=	(and	(same_tree < variable > ?occ)+
				(not (= < variable > ?occ))+)