Go backward to Proving Psi Implements Phi Go up to Top Go forward to Hiding Variables

Proof of Fairness

• Psi => WF_<x,y>(A₁)
  • x is incremented infinitely often.
  • Application of SF₂.
  • Use beta₁ for A.
  • Strengthen A by invariant I through application of INV2.
  • I <=> x in Nat
    and (((sem=1) and (pc₁ = pc₂ = "a"))
       or ((sem=0)
          and (((pc₁ = "a") and (pc₂ in {"b", "g"}))
             or ((pc₂ = "a")
                and (pc₁ in {"b", "g"})))))

For details, see the paper.