open INV
-- arbitrary objects
  op s : -> Sys .
-- check if the predicate is true .
  red inv4(s,i) implies inv8(s,i) .
close