Go backward to Proof
Go up to Top
Go forward to More About Invariance Proofs
General Invariance Proofs
- Special case Phi always
- was invariant of [A]
- could be used as in INV1.
- Generally Phi always
- need not be invariant.
- Find invariant
- Creativity is in finding
- Invariance proof itself mechanical.
INV1 reduces temporal reasoning to ordinary (non-temporal) reasoning!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine