reservation: THEORY
 BEGIN

  room: TYPE

  date: TYPE

  name: TYPE

  free: name

  reservations: TYPE = [room, date -> name]

  r: VAR room

  d, e: VAR date

  n: VAR name

  register: VAR reservations

  reserve(r: room, d: date, n: name, register: reservations):
  reservations = register WITH [(r, d) := n]

  cancel(r, d, register): reservations = register WITH [(r, d) := free]

  reserved(r, d, register): bool = register(r, d) /= free

  canceled_not_reserved: LEMMA
    FORALL r, d, register: NOT reserved(r, d, cancel(r, d, register))

  is_reserved: LEMMA
    FORALL r, d, n, register: reserved(r, d, reserve(r, d, n, register))
 END reservation