\begin{zed}
  ADDR   == \nat \\
  MemMan \defs [f,u:\power ADDR | f \cap u = \emptyset ] \\
  MMInit \defs [MemMan | f = 0 \upto 100 \land u = \emptyset] \\
  MMOp   \defs [\Delta MemMan | f' \cup u' = f \cup u] \\
  Alloc  \defs [MMOp; a!:ADDR | a! \in f \land u' = u \cup \{a!\}] \\
  Free   \defs [MMOp; a?:ADDR | a? \in u \land f' = f \cup \{a?\}] \also
\end{zed}

\begin{zed}
  Test1  \defs MMInit' \semi Alloc \\
\end{zed}

\begin{zed}
  Test2 \defs Test1[a! := 42, f' := (0 \upto 41) \cup (43 \upto 100)] \\
\end{zed}

\begin{zed}
  Test4  \defs Test1[a! := 0, u' := \{0\}, f' := 1 \upto 100]
\end{zed}