th FLAG is sort Flag .
  ops (up_)(dn_)(rev_) : Flag -> Flag . 
  op up?_ : Flag -> Bool . 
  var F : Flag .
  eq up? up F = true . 
  eq up? dn F = false . 
  eq up? rev F = not up? F . 
endth