\[ [T] \]

\begin{axdef}
max : \nat
\end{axdef}

\begin{schema}{A}
  s : \pset T
\ST
 \size s \leq max
\end{schema} 
    
\begin{schema}{AInit}
A'
\ST
      s' = \emptyset 
\end{schema}

\begin{schema}{AEnter}
      \Delta A \\
      p? : T 
\ST
	 \size s < max \\
 p? \nmem s \\
 s' = s \cup \{ p? \}
\end{schema}

\begin{schema}{ALeave}
      \Delta A \\
      p? : T 
\ST
 p? \mem s \\
 s' = s \setminus \{ p? \}
\end{schema}