Go backward to Conjoining Specifications
Go up to Top
Go forward to Two Queues in Series
Proposition
- Proposition
- If
exists : Init and always [A]
and
and A (' = )
- then
|= (and ) = exists : and
Init
and and always [or A and (^' =
^)]
and and
- where
<, ..., >
and all free variables of
and ^ <, ..., , , ...,
>
- GCD:
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine