--
-- Claim 11 (**PROVED**) (Used Claims: 2,3)
--
--   pc(s,i) = l2 and top(queue(s)) = i ensures pc(s1,i) = cs
--

--
-- Claim 12 (**PROVED**) (Used Claims: Nonce)
--
--   pc(s,i) = l2 and i \in queue(s) and where(queue(s),i) = s(n) and pc(s,top(queue(s))) = cs
--   ensures
--   pc(s,i) = l2 and i \in queue(s) and where(queue(s),i) = n
--

--
-- Claim 13 (**PROVED**) (Used Claims: 2)
--
--   pc(s,i) = l2 and i \in queue(s) and where(queue(s),i) = s(n) and pc(s,top(queue(s))) = l2
--   ensures
--   pc(s,i) = l2 and i \in queue(s) and where(queue(s),i) = s(n) and pc(s,top(queue(s))) = cs
--

mod ENS {
  pr(QLOCK)
  pr(INV)
-- arbitrary objects
  op i : -> Pid
  op n : -> Nat
-- declare claims to prove
  op ens11-1 : Sys Pid -> Bool
  op ens11-2 : Sys Pid -> Bool
  op ens12-1 : Sys Pid Nat -> Bool
  op ens12-2 : Sys Pid Nat -> Bool
  op ens13-1 : Sys Pid Nat -> Bool
  op ens13-2 : Sys Pid Nat -> Bool
-- CafeOBJ variables
  var S :  Sys
  var I : Pid
  var N : Nat
-- define claims to prove
  eq ens11-1(S,I) = (pc(S,I) = l2 and top(queue(S)) = I) .
  eq ens11-2(S,I) = (pc(S,I) = cs) .
  eq ens12-1(S,I,N) 
     = (pc(S,I) = l2 and I \in queue(S) and where(queue(S),I) = s(N) and pc(S,top(queue(S))) = cs) .
  eq ens12-2(S,I,N) = (pc(S,I) = l2 and I \in queue(S) and where(queue(S),I) = N) .
  eq ens13-1(S,I,N) 
     = (pc(S,I) = l2 and I \in queue(S) and where(queue(S),I) = s(N) and pc(S,top(queue(S))) = l2) .
  eq ens13-2(S,I,N) 
     = (pc(S,I) = l2 and I \in queue(S) and where(queue(S),I) = s(N) and pc(S,top(queue(S))) = cs) .
}

mod ESTEP {
  pr(ENS)
-- arbitrary objects
  ops s s' : -> Sys
-- declare predicates to prove in each eventually case
  op estep11 : Pid -> Bool
  op estep12 : Pid Nat -> Bool
  op estep13 : Pid Nat -> Bool
 -- CafeOBJ variables
  var I : Pid
  var N : Nat
-- define predicates to prove in each eventually case
  eq estep11(I) = ens11-1(s,I) and not ens11-2(s,I) and ens11-2(s',I) .
  eq estep12(I,N) = ens12-1(s,I,N) and not ens12-2(s,I,N) and ens12-2(s',I,N) .
  eq estep13(I,N) = ens13-1(s,I,N) and not ens13-2(s,I,N) and ens13-2(s',I,N) .
}

mod USTEP {
  pr(ENS)
-- arbitrary objects
  ops s s' : -> Sys
-- declare predicates to prove in each unlesss case
  op ustep11 : Pid -> Bool
  op ustep12 : Pid Nat -> Bool
  op ustep13 : Pid Nat -> Bool
-- CafeOBJ variables
  var I : Pid
  var N : Nat
-- define predicates to prove in each unless case
  eq ustep11(I) = (ens11-1(s,I) and not ens11-2(s,I)) implies (ens11-1(s',I) or ens11-2(s',I)) .
  eq ustep12(I,N) 
     = (ens12-1(s,I,N) and not ens12-2(s,I,N)) implies (ens12-1(s',I,N) or ens12-2(s',I,N)) .
  eq ustep13(I,N) 
     = (ens13-1(s,I,N) and not ens13-2(s,I,N)) implies (ens13-1(s',I,N) or ens13-2(s',I,N)) .
}