Go backward to Eventuality Properties
Go up to Top
Go forward to Other Properties

Example

Prove WF1
- $P$ <- $n$ in Nat and $x$ = n $Q$ <- $x$ = n+1
  A <-A, A <- A₁, $f$ <- < $x$ , $y$ >
Hypotheses:
- ( $n$ in Nat and $x$ = n) and [A]_{<x, y>}
  $=>$ (( $n$ in Nat and $x'$ = n) or ( $x'$ = n+1))
  ( $n$ in Nat and $x$ = n) and <A₁>_{<x, y>}
  $=>$ ( $x'$ = n+1))
  ( $n$ in Nat and $x$ = n) and <A₁>_{<x, y>}
  $=>$ Enabled <A₁>_{<x, y>}
- From definitions of A₁ and A.
Conclusion:
- always [A]_{<x, y>} and WF_{<x, y>}(A₁)
  $=>$ (( $n$ in Nat and $x$ = n) $|->$ ( $x$ = n+1))

Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine