node cdrom(speed: int) returns (plus, minus, error: bool)
var ps, count: int;
let
  ps = 0 -> pre speed;

  assume h1 : speed - ps <= 4 and speed - ps >= -4;
  assume h2 : if (false -> pre plus) then (speed - ps > 0)
              else if (false -> pre minus) then (speed - ps < 0)
              else true;

  plus = (ps <= 9);
  minus = (ps >= 11);

  count = if speed < 8 or speed > 12
            then (0 -> pre count) + 1 else 0;

  error = (count >= 15);
  guarantee g: not error and (true -> not pre error);
tel