--
-- Claim 14 (**PROVED**) (Used Claims: 12,13)
--
--   ((pc(s,i) = l2 /\ i \in queue(s) /\ where(queue(s),i) = s(n) /\ pc(s,top(queue(s))) = l2)
--    |-->
--    (pc(s,i) = l2 /\ i \in queue(s) /\ where(queue(s),i) = n))
--

--
-- Claim 15 (**PROVED**) (Used Claims: 12,14)
--
--   ((pc(s,i) = l2 /\ i \in queue(s) /\ where(queue(s),i) = s(n) /\ 
--     (pc(s,top(queue(s))) = l2 \/ pc(s,top(queue(s))) = cs))
--    |-->
--    (pc(s,i) = l2 /\ i \in queue(s) /\ where(queue(s),i) = n))
--

--
-- Claim 16 (**PROVED**) (Used Claims: 9,10,11,15)
--
--   ((pc(s,i) = l2 /\ i \in queue(s) /\ where(queue(s),i) = n)
--    |-->
--    ((pc(s,i) = l2 /\ i \in queue(s) /\ where(queue(s),i) < n) \/
--     (pc(s,i) = cs)))
--

-- 
-- Claim 17 (**PROVED**) (Used Claims: 16)
--
--   ((pc(s,i) = l2 /\ i \in queue(s)) |--> (pc(s,i) = cs))
--

-- *** lockout freedom
-- Claim 18 (**PROVED**) (Used Claims: 8,17)
--
--   ((pc(s,i) = l2) |--> (pc(s,i) = cs))
--

mod PROVED {
  pr(QLOCK)
  pr(OTSLOGIC)
-- declare proved properties
  op inv8 : Sys Pid -> Bool
  op inv9 : Sys Pid -> Bool
  op inv10 : Sys Pid Nat -> Bool
  op ens11 : Sys Pid -> Bool
  op ens12 : Sys Pid Nat -> Bool
  op ens13 : Sys Pid Nat -> Bool
-- CafeOBJ variables
  var S : Sys
  var I : Pid
  var N : Nat 
-- define proved properties
  eq inv8(S,I) = invariant (pc(S,I) = l2 => (pc(S,I) = l2 /\ I \in queue(S))) .
  eq inv9(S,I) = invariant (((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = 0)
                            =>
                            (pc(S,I) = l2 /\ top(queue(S)) = I))) .
  eq inv10(S,I,N) 
     = invariant ((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = s(N))
                  =>
                  (pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = s(N) /\
                   (pc(S,top(queue(S))) = l2 \/ pc(S,top(queue(S))) = cs))) .
  eq ens11(S,I) = ((pc(S,I) = l2 /\ top(queue(S)) = I) ensures pc(S,I) = cs) .
  eq ens12(S,I,N) 
     = ((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = s(N) /\ pc(S,top(queue(S))) = cs)
        ensures
        (pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = N)) .
  eq ens13(S,I,N) 
     = ((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = s(N) /\ pc(S,top(queue(S))) = l2)
        ensures
        (pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = s(N) /\ pc(S,top(queue(S))) = cs)) .
}

mod LTO {
  pr(PROVED)
-- arbitrary objects
  op s : -> Sys
  op i : -> Pid
  op n : -> Nat
-- declare leadsto candidates
  op lto14 : Sys Pid Nat -> Bool
  op lto15 : Sys Pid Nat -> Bool
  op lto16 : Sys Pid Nat -> Bool
  op lto17 : Sys Pid -> Bool
  op lto18 : Sys Pid -> Bool
-- CafeOBJ variables
  var S : Sys
  var I : Pid
  var N : Nat 
-- define leadsto candidates
  eq lto14(S,I,N) 
     = ((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = s(N) /\ pc(S,top(queue(S))) = l2)
        |-->
        (pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = N)) .
  eq lto15(S,I,N) 
     = ((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = s(N) /\ 
         (pc(S,top(queue(S))) = l2 \/ pc(S,top(queue(S))) = cs))
        |-->
        (pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = N)) .
  eq lto16(S,I,N) 
     = ((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) = N)
        |-->
        ((pc(S,I) = l2 /\ I \in queue(S) /\ where(queue(S),I) < N) \/
         (pc(S,I) = cs))) .
  eq lto17(S,I) = ((pc(S,I) = l2 /\ I \in queue(S)) |--> (pc(S,I) = cs)) .
  eq lto18(S,I) = ((pc(S,I) = l2) |--> (pc(S,I) = cs)) .
}