--
-- Claim 1 (**Proved**) (Used Lemmas: 2)
--
--   invariants (pc(s,i) = cs and pc(s,j) = cs implies i = j)
--

--
-- Claim 2 (**Proved**) (Used Lemmas: 1,3)
--
--   invariants (pc(s,i) = cs implies top(queue(s)) = i)
--

--
-- Claim 3 (**Proved**) (Used Lemmas: 1,2,4)
--
--   invariants (pc(s,i) = l2 or pc(s,i) = cs implies not empty?(queue(s)))
--

--
-- Claim 4 (**Proved**) (Used Lemmas: 2)
--
--   invariants (pc(s,i) = l2 implies i \in queue(s))
--

mod INV {
  pr(QLOCK)
-- arbitrary objects
  ops i j : -> Pid
-- declare invariant candidates
  op inv1 : Sys Pid Pid -> Bool
  op inv2 : Sys Pid -> Bool
  op inv3 : Sys Pid -> Bool
  op inv4 : Sys Pid -> Bool
-- CafeOBJ variables
  var S :  Sys
  vars I J : Pid
-- define invariant candidates
  eq inv1(S,I,J) = (pc(S,I) = cs and pc(S,J) = cs implies I = J) .
  eq inv2(S,I) = (pc(S,I) = cs implies top(queue(S)) = I) .
  eq inv3(S,I) = (pc(S,I) = l2 or pc(S,I) = cs implies not empty?(queue(S))) .
  eq inv4(S,I) = (pc(S,I) = l2 implies I \in queue(S)) .
}

mod ISTEP {
  pr(INV)
-- arbitrary objects
  ops s s' : -> Sys
-- declare predicates to prove in inductive step
  op istep1 : Pid Pid -> Bool
  op istep2 : Pid -> Bool
  op istep3 : Pid -> Bool
  op istep4 : Pid -> Bool
-- CafeOBJ variables
  vars I J : Pid
-- define predicates to prove in inductive step
  eq istep1(I,J) = inv1(s,I,J) implies inv1(s',I,J) .
  eq istep2(I) = inv2(s,I) implies inv2(s',I) .
  eq istep3(I) = inv3(s,I) implies inv3(s',I) .
  eq istep4(I) = inv4(s,I) implies inv4(s',I) .
}