Ordered Activity Axioms

Grammar Name: ordered.bnf

Extension Name: ordered.def

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

Process Descriptions

(ordered ?occ)

< ordered_spec > ::=	(forall (< variable >)
				(if	  (same_tree < variable > ?occ)
				  	  < ordered_sentence >)) |
			(forall (< variable >)
				(if	  (same_tree < variable > ?occ)
					  < ordered_formula >))

(nondet_ordered ?occ)

< nondet_ordered_spec > ::=  (forall (< variable >) 
				  (if	    (same_tree < variable > ?occ)
					    (or < ordered_sentence >*)))

(broken_ordered ?occ)

< broken_ordered_spec > ::=  (forall (< variable >) 
				  (if	    (same_tree < variable > ?occ)
					    (or {< ordered_sentence >* |
						< ordered_list >*})))

(unordered ?occ)

< unordered_spec > ::=	(forall (< variable >)
                                (if	  (same_tree < variable > ?occ)
                                          (or < ordered_list >*)))

Auxiliary Rules

< ordered_literal > ::=	  (min_precedes < variable > < variable > < term >) |
			  (next_subocc < variable > < variable > < term >) 

< ordered_list > ::=	  < ordered_literal > |
			  (and < ordered_literal >*)

< conditional_occurrence > ::=	(if	  < occurrence_formula >
					  < ordered_list >)

< ordered_sentence > ::= 	(exists (< variable >)
					(and	(root_occ < variable > ?occ)
				  		< occurrence_disjunct >
						< conditional_occurrence >))))

< ordered_conjunct > ::=	< ordered_literal > |
                                (and < ordered_formula >*)

< ordered_formula > ::=		(exists (< variable >)
                                        (and    (root_occ < variable > ?occ)
                                                < occurrence_disjunct >
						< ordered_conjunct >)) |
				(or < ordered_formula >*)