open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq (pc(s,i) = l2) = false .
-- check if the predicate is true 
  red inv10(s,i,n) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq i \in queue(s) = false .
-- check if the predicate is true 
  red inv10(s,i,n) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq (where(queue(s),i) = s(n)) = false .
-- check if the predicate is true 
  red inv10(s,i,n) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq pc(s,i) = l2 .
  eq i \in queue(s) = true .
  eq where(queue(s),i) = s(n) .
  eq empty?(queue(s)) = true .
-- check if the predicate is true 
  red inv3(s,i) implies inv10(s,i,n) .
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq pc(s,i) = l2 .
  eq i \in queue(s) = true .
  eq where(queue(s),i) = s(n) .
  eq empty?(queue(s)) = false .
-- check if the predicate is true 
  red inv5(s,top(queue(s))) implies inv10(s,i,n) .
close