open INV
  op s : -> System .
  red inv200(s,pair1,pair2,pair3,empty,pfifo)
      implies inv180(s,pair1,pair2,pair3,pfifo) .
close