open INV
  op s : -> System .
  red inv190(s,tag1,tag2,tag3,empty,bfifo) 
      implies inv170(s,tag1,tag2,tag3,bfifo) .
close