Go backward to Special Cases of Unless
Go up to Top
Go forward to Ensures

Special Cases of Unless

$p$ unless $q$ not $q$ is invariant

$p$ is stable
- not $q$ $<=>$ true (not $q$ is invariant).
- $p$ unless $q$ (premise),
- $p$ unless false (substitution axiom on above two),
- $p$ is stable (definition).
Always-Section
- Defines an invariant.
- Construction like that of initial condition by initially-section.

Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine

$p$ `unless` $q$	not $q$ is invariant
$p$ is stable