\[ [T] \]

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

\begin{schema}{C}
  l : \iseq T
\ST
 \size l \leq max
\end{schema} 
    
\begin{schema}{CInit}
C'
\ST
      l' = \emptyseq 
\end{schema}

\begin{schema}{CEnter}
      \Delta C \\
      p? : T 
\ST
	 \size l < max \\
 p? \nmem \ran l \\
 l' = l \cat \lseq p? \rseq
\end{schema}

\begin{schema}{CLeave}
      \Delta C \\
      p? : T 
\ST
 p? \mem \ran l \\
 l' = l \filter (T \setminus \{ p? \})
\end{schema}