\[ [PERSON,TITLE] \]
\begin{sidebyside}

\begin{axdef}
	black, brown, grey: PERSON \\
	filmA, filmB, filmC, filmD : TITLE
\end{axdef}

\begin{schema}{State}
	members : \pset PERSON \\
	rented : PERSON \rel TITLE \\
	stockLevel : TITLE \pfun \nat
\ST
	\dom rented \subseteq members \\
	\ran rented \subseteq \dom stockLevel \\
\end{schema}
 
\nextside

\begin{schema}{Init}
  State'
\ST
 members' = \emptyset \\
 stockLevel' = \emptyset
\end{schema}

\end{sidebyside}

\begin{sidebyside}

\begin{schema}{RentVideo}
 \Delta State \\
  p? : PERSON \\
  t? : TITLE
\ST
 p? \in members \\
t? \in \dom stockLevel \\
stockLevel (t?) > \# (rented \rres  \{ t? \} ) \\
(p?, t?) \nmem rented \\
rented' = rented \cup \{ (p?, t?) \} \\
stockLevel' = stockLevel \\
members' = members
\end{schema}
\nextside
\begin{schema}{AddTitle}
 \Delta State \\
  t? : TITLE \\
  level? : \nat
\ST
stockLevel' =  stockLevel \fovr \{(t?, level?) \} \\
  rented' = rented \\
  members' = members
\end{schema}
\end{sidebyside}

\begin{sidebyside}
\begin{schema}{DeleteTitle}
 \Delta State \\
  t? : TITLE
\ST
 t? \nmem \ran rented \\
t? \in \dom stockLevel \\
stockLevel' =  \{ t? \} \dsub stockLevel \\
  rented' = rented \\
  members' = members
\end{schema}
\nextside
\begin{schema}{AddMember}
 \Delta State \\
  p? : PERSON 
\ST
 p? \nmem members \\  
 stockLevel' =  stockLevel \\
  rented' = rented \\
  members' = members \cup \{ p? \}
\end{schema}
\end{sidebyside}
\begin{schema}{CopiesOut}
 \Xi State \\
  t? : TITLE \\
  copies! : \nat
\ST
t? \in \dom stockLevel \\
copies! =  \# (rented \rres  \{ t? \} ) \\
\end{schema}