Go backward to The Fairness Requirement
Go up to Top
Go forward to Proof of Fairness
Proving Psi Implements Phi
- Prove Psi Phi
- Init
Init
- always [A]
always [A]
- Psi WF(A)
and WF(A)
- Proof of Step Simulation:
-
[A]
[A]
-
[A] alpha or ... or gamma
or ( = )
- beta A
- beta A
- (<, >' = <, >) for all
others.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine