Tree Ordered Activity Axioms

Grammar Name: treeordered.bnf

Extension Name: treeordered.def

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

Process Descriptions

(treeordered ?a)

< treeordered_spec > ::=  (forall (< variable >)
				(if	  (occurrence < variable > < term >)
				  	  < ordered_sentence >)) |
			  (forall (< variable >)
				(if	  (occurrence < variable > < term >)
					  < ordered_formula >))

(nondet_treeordered ?a)

< nondet_treeordered_spec > ::=  (forall (< variable >) 
				  (if	    (occurrence < variable > < term >)
					    (or < ordered_sentence >*)))

(partial_treeordered ?a)

< partial_treeordered_spec > ::=  (forall (< variable >) 
				  	(if	  (occurrence < variable > < term >)
					    	  (or {< ordered_sentence >* |
						      < ordered_list >*})))

(scrambled ?a)

< scrambled_spec > ::=	(forall (< variable >)
                                (if	  (occurrence < variable > < term >)
                                          (or < ordered_list >*)))