in invariants-1.mod

mod INV2 {
  inc(ISTEP1)
-- declare another invariant candidate 
  op inv2 : Sys Pid -> Bool
-- CafeOBJ variables
  var S :  Sys
  vars I : Pid
-- defining the invariant candidate
  eq inv2(S,I) = (pc(S,I) = cs implies top(queue(S)) = I) .
}

mod ISTEP2 {
  inc(INV2)
-- s stands for current state and 
-- s' stans for next state
   ops s s' : -> Sys .
-- declare predicates to prove in inductive step
  op istep2 : Pid -> Bool .
-- CafeOBJ variables
  vars I : Pid
-- for defining predicates to prove in inductive step
  eq istep2(I) = inv2(s,I) implies inv2(s',I) .
}