Go backward to ProofGo up to TopGo forward to More About Invariance Proofs |

- Special case
`Phi`*=>*`always`*T**T*was invariant of [`A`]_{<x, y>}*T*could be used as*I*in INV1.

- Generally
`Phi`*=>*`always`*P**P*need*not*be invariant.- Find invariant
*I**=>**P*

- Creativity is in finding
*I*- Invariance proof itself mechanical.

*INV1 reduces temporal reasoning to ordinary (non-temporal) reasoning!*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998