\begin{schema}{R}
  Marlowe\\
  Kurbel
\ST
  bkd = no  \implies tkt = null \land kpool = mpool\\
  bkd = yes \implies tkt \neq null \land 
      kpool = (mpool \union \{ ticket^{-1}(tkt) \})
\end{schema}