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))