--
-- By case analysis
--

open INV
-- arbitrary objects
  op s : -> System .
-- assumptions
  eq fifo1(s) = empty .
-- check if the predicate is true.
  red inv210(s,tag) .
close
--
open INV
-- arbitrary objects
  op s : -> System .
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq (tag2(s) = 1st(pair10)) = false .
-- check if the predicate is true.
  red inv210(s,tag) .
close
--
open INV
-- arbitrary objects
  op s : -> System .
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq tag2(s) = 1st(pair10) .
  eq (tag1(s) = 1st(pair10)) = false .
-- check if the predicate is true.
  red inv120(s) implies inv210(s,tag) .
close
--
open INV
-- arbitrary objects
  op s : -> System .
  op pair10 : -> Pair .
  op pfifo10 : -> PFifo .
-- assumptions
  eq fifo1(s) = pair10 | pfifo10 .
  eq tag2(s) = 1st(pair10) .
  eq tag1(s) = 1st(pair10) .
-- check if the predicate is true.
  red inv230(s,tag) implies inv210(s,tag) .
close