+\paragraph{Utilities}
+\begin{itemize}
+ \item \ZEROPOS: map $g -> 0, \OPEN~g$
+ \item \INITPOS: map $g -> i, \OPEN~g$
+ \item \ISFRESH: $\OPEN~g, 0 -> true | \_ -> false$
+ \item \FILTEROPEN: $G -> \FILTER(\ISOPEN,G)$
+ \item \DEEPCLOSE: prende uno stack ed un insieme di goal da chiudere, traversa
+ lo stack rimuovendo le occorrenze dei goal da $\tau$ e $\kappa$ e marcandole
+ chiuse in $\Gamma$
+\end{itemize}
+
+\paragraph{Invariants}
+\begin{itemize}
+ \item $\forall \ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s \in\tau\cup\kappa,
+ \exists g, s = \OPEN~g$ (i goal in $\tau$ e $\kappa$ sono aperti)
+ \item la lista dei goal nel metasenv contiene tutti e soli i goal presenti
+ sullo stack
+ \item lo stack puo' contenere goal duplicati nel caso di uso della select
+\end{itemize}
+