Go backward to Proof Go up to Top Go forward to More About Invariance Proofs

General 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!