Go backward to More About Invariance ProofsGo up to TopGo forward to Example |

- Something
*eventually*happens. - Termination
`eventually``terminated`.

- Service
- If process has requested service, it is eventually served.
`requested`*|->*`served`.

- Message delivery
- If a message is sent often enough, it is eventually delivered.
- (
`always``eventually``sent`)*=>*`eventually``delivered`.

*P**|->**Q*.`Phi`*and*(*n*in**Nat**)*=>*`eventually`(*x>n*)`Phi`*=>*((*n*in**Nat***and**x=n*)*|->*`eventually`(*x=n+1*))

*Must be derived from fairness condition!*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998