open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq i \in queue(s) = false .
-- check if the predicate is true
  red inv9(s,i) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq (where(queue(s),i) = 0) = false .
-- check if the predicate is true
  red inv9(s,i) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq i \in queue(s) = true .
  eq where(queue(s),i) = 0 .
-- check if the predicate is true
  red inv9(s,i) .
close