Folded Activity Axioms

Grammar Name: folded.bnf

Extension Name: folded.def

Grammars required by Process Descriptions: permute.bnf

Process Descriptions

(folded ?occ)

< folded_spec > ::=	(exists (< variable >)
				(and	(same_tree < variable > ?occ)
				  	< occurrence_axiom >))

(nondet_folded ?occ)

< nondet_folded_spec > ::=  (exists (< variable >) 
				  (and	(same_tree < variable > ?occ)
				 	(or < occurrence_axiom >*)))

(partial_folded ?occ)

< partial_folded_spec > ::=	(or  < nondet_folded_spec >
				     < rigid_spec >)

(rigid ?occ)

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

Auxiliary Rules

< occurrence_disjunct > ::=	< occurrence_literal > |
				(or < occurrence_literal >*)

< occurrence_axiom > ::= 	(exists (< variable >*) 
				  	< occurrence_disjunct >)