open LTO
-- assumtptions
  eq n = 0 .
-- check if the property holds
  red (inv9(s,i) /\ ens11(s,i)) => lto16(s,i,n) .
close
--
open LTO
-- arbitrary objects
  op n1 : -> Nat .
-- assumtptions
  eq n = s(n1) .
-- facts
  vars P Q : Bool .
  eq ((P /\ where(queue(s),i) = n1) => ((P /\ where(queue(s),i) < s(n1)) \/ Q)) = true .
-- check if the property holds
  red (inv10(s,i,n1) /\ lto15(s,i,n1)) => lto16(s,i,n) .
close
--