-- *** Mutual Exclusion
-- 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))
--

-- The following are needed for the proof of lockout freedom.

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

--
-- Claim 6 (**Proved**) (Used Lemmas: 2,5,7)
--
--   invariants (top(queue(s)) = i implies not(i \in get(queue(s))))
--

--
-- Claim 7 (**Proved**) (Used Lemmas: 2,5)
--
--   invariants (howmany(queue(s),i) = 0 or howmany(queue(s),i) = s(0))
--

--
-- The following claims can be derived from the above ones.
--

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

--
-- Claim 9 (**Proved**) (Used Lemmas: None)
--
--   invariants (pc(s,i) = l2 and i \in queue(s) and where(queue(s),i) = 0
--               implies
--               pc(s,i) = l2 and top(queue(s)) = i)
--

--
-- Claim 10 (**Proved**) (Used Lemmas: 3,5)
--
--   invariants (pc(s,i) = l2 and i \in queue(s) and where(queue(s),i) = s(n)
--               implies
--               pc(s,i) = l2 and i \in queue(s) and where(queue(s),i) = s(n) and
--               (pc(s,top(queue(s))) = l2 or pc(s,top(queue(s))) = cs))
--

mod INV {
  pr(QLOCK)
-- arbitrary objects
  ops i j : -> Pid
  op n : -> Nat
-- declare invariant candidates
  op inv1 : Sys Pid Pid -> Bool
  op inv2 : Sys Pid -> Bool
  op inv3 : Sys Pid -> Bool
  op inv4 : Sys Pid -> Bool
  op inv5 : Sys Pid -> Bool
  op inv6 : Sys Pid -> Bool
  op inv7 : Sys Pid -> Bool
  op inv8 : Sys Pid -> Bool
  op inv9 : Sys Pid -> Bool
  op inv10 : Sys Pid Nat -> Bool
-- CafeOBJ variables
  var S :  Sys
  vars I J : Pid
  var N : Nat
-- 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)) .
  eq inv5(S,I) = (I \in queue(S) implies (pc(S,I) = l2 or pc(S,I) = cs)) .
  eq inv6(S,I) = (top(queue(S)) = I implies not(I \in get(queue(S)))) .
  eq inv7(S,I) = (howmany(queue(S),I) = 0 or howmany(queue(S),I) = s(0)) .
  eq inv8(S,I) = (pc(S,I) = l2 implies pc(S,I) = l2 and I \in queue(S)) .
  eq inv9(S,I) = (pc(S,I) = l2 and I \in queue(S) and where(queue(S),I) = 0
                  implies
                  pc(S,I) = l2 and top(queue(S)) = I) .
  eq inv10(S,I,N) = (pc(S,I) = l2 and I \in queue(S) and where(queue(S),I) = s(N)
                     implies
                     pc(S,I) = l2 and I \in queue(S) and where(queue(S),I) = s(N) and
                     (pc(S,top(queue(S))) = l2 or pc(S,top(queue(S))) = cs)) .
}

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
  op istep5 : Pid -> Bool
  op istep6 : Pid -> Bool
  op istep7 : 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) .
  eq istep5(I) = inv5(s,I) implies inv5(s',I) .
  eq istep6(I) = inv6(s,I) implies inv6(s',I) .
  eq istep7(I) = inv7(s,I) implies inv7(s',I) .
  --
}