Go backward to Machine Closure
Go up to Top
Go forward to Additional Temporal Operators
Closure and Hiding
- Special hypotheses:
- A() and ... and A()
A().
- For proof, first compute A().
- Can be done by Proposition 1 for formulas with no internal variables.
- For formulas with internal variables, use Proposition 2 to allow
application of Proposition .
- Proposition 2:
- Let be tuples of variables such that no variable
in occurs in or in any with notequal .
- If |= and A(M) exists :
A(),
then |= and A(exists : M)
A(exists : ).
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine