Go backward to Proof of Union Theorem
Go up to Top
Go forward to Specifications that Compose

Collaries

$p$ is stable in $F$ [] $G$ $<=>$
( $p$ is stable in $F$ and $p$ is stable in $G$ )
$p$ unless $q$ in $F$ $p$ is stable in $G$

$p$ unless $q$ in $F$ [] $G$
$p$ is invariant $q$ in $F$ $p$ is stable in $G$

$p$ is invariant $q$ in $F$ [] $G$
$p$ ensures $q$ in $F$ $p$ is stable in $G$

$p$ ensures $q$ in $F$ [] $G$
Locality:
- $p$ is a local predicate of $F$ , if it only mentions variables that can be modified by $F$ alone.
- If $p$ is a local predicate of $F$ , then the following properties hold in $F$ [] $G$ , for any $G$ : $p$ unless $q$ , $p$ ensures $q$ , $p$ is invariant.

Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine

$p$ `unless` $q$ in $F$	$p$ is stable in $G$
$p$ `unless` $q$ in $F$ [] $G$

$p$ is invariant $q$ in $F$	$p$ is stable in $G$
$p$ is invariant $q$ in $F$ [] $G$

$p$ `ensures` $q$ in $F$	$p$ is stable in $G$
$p$ `ensures` $q$ in $F$ [] $G$