--
-- By case analysis
--

open INV
-- arbitrary objects
  op s : -> System .
-- assumptions
  eq fifo2(s) = empty .
-- check if the predicate is true.
  red inv220(s,pair) .
close
--
open INV
-- arbitrary objects
  op s : -> System .
  op tag10 : -> Tagvalue .
  op bfifo10 : -> BFifo .
-- assumptions
  eq fifo2(s) = tag10 | bfifo10 .
  eq tag1(s) = tag10 .
-- check if the predicate is true.
  red inv220(s,pair) .
close
--
open INV
-- arbitrary objects
  op s : -> System .
  op tag10 : -> Tagvalue .
  op bfifo10 : -> BFifo .
-- assumptions
  eq fifo2(s) = tag10 | bfifo10 .
  eq tag1(s) = tag10 .
  eq tag2(s) = tag10 .
-- check if the predicate is true.
  red inv110(s) implies inv220(s,pair) .
close
--
open INV
-- arbitrary objects
  op s : -> System .
  op tag10 : -> Tagvalue .
  op bfifo10 : -> BFifo .
-- assumptions
  eq fifo2(s) = tag10 | bfifo10 .
  eq tag1(s) = tag10 .
  eq (tag2(s) = tag10) = false .
-- check if the predicate is true.
  red inv240(s,pair) implies inv220(s,pair) .
close