Mixed Precondition Axioms

Grammar Name: mixed_precond.bnf

Extension Name: mixed_precond.def

Grammars required by Process Descriptions: None

Process Descriptions

< simple_mix_precond > ::=	(forall (?s) 
					(if	  (and	(occurrence ?s < term >)
							(legal ?s))
						  < simple_mix_axiom >))) |
                                (forall (?s)
                                        (if	  (and  (legal ?s)
                                                        < simple_mix_axiom >)
                                                  (legal (successor < term > ?s))))

< mix_precond > ::=		(forall (?s) 
					(if	  (and	(occurrence ?s < term >)
							(legal ?s))
						  < mix_formula >)))

Auxiliary Rules

< simple_mix_literal > ::=	(= (beginof ?s) < term >) (prior  ?s)

< simple_mix_formula > ::=	(and < simple_mix_literal >*) 

< simple_mix_axiom > ::=	({forall | exists} < variable >*) < simple_mix_formula >)

< ordered_mix_literal > ::=	< simple_mix_literal > |
				(before (beginof ?s) < term >) (prior < term > ?s) |
				(before < term > (beginof ?s)) (prior < term > ?s) 

< mix_formula > ::=		< ordered_mix_literal > |
				(not < mix_formula >) |
				({and | or} < mix_formula >*) | 
				({if | iff} < mix_formula >) 

< mix_axiom > ::=		({forall | exists} < variable >*) < mix_formula >)