vocabulary CinemaBookings;
each CinemaID is written as Auto Counter;
each Cinema is identified by its ID;
each FilmID is written as Auto Counter;
each Film is identified by its ID;
each Name is written as String;
Film has at most one Name;
each PersonID is written as Auto Counter;
each Person is identified by its ID;
Person has one login-Name,
Name is of at most one Person;
each Row Number is written as Char(2);
each Number is written as Unsigned Integer(16) restricted to {1..};
each Row is identified by its Number;
each Seat is identified by a Cinema, a Row and a Number where
that Cinema has that Seat,
that Seat is in at most one Cinema,
that Seat is in one Row,
that Row contains that Seat,
that Seat has one Number,
that Number is of that Seat;
each SectionName is written as String;
each Section is identified by its Name;
Seat is in at most one Section,
that Section contains at least one Seat;
each Showing is where
some Cinema shows some Film on some DateTime,
that Film is showing on that DateTime at that Cinema;
each Booking is where
some Person booked some Number of seats for some Showing,
that Person booked that Showing for one Number of seats;
Booking is confirmed;
each Seat Allocation is where
some Booking has some allocated-Seat;
some Booking
(in which some Person booked some Number of seats for some Showing
(in which some Film is showing on some DateTime at some Cinema))
has some allocated Seat
only if that Seat is in that Cinema;